diff --git a/proposals/p6118.md b/proposals/p6118.md new file mode 100644 index 0000000000000..539eca7b0ab1f --- /dev/null +++ b/proposals/p6118.md @@ -0,0 +1,143 @@ +# Flow checking + + + +[Pull request](https://github.com/carbon-language/carbon-lang/pull/6118) + + + +## Table of contents + +- [Abstract](#abstract) +- [Problem](#problem) +- [Background](#background) +- [Proposal](#proposal) +- [Details](#details) +- [Rationale](#rationale) +- [Alternatives considered](#alternatives-considered) + + + +TODOs indicate where content should be updated for a proposal. See +[Carbon Governance and Evolution](/docs/project/evolution.md) for more details. + +## Abstract + +Carbon's language goals include support for +[practical safety mechanisms](../docs/project/goals.md#practical-safety-and-testing-mechanisms). +The [updated](p5914.md) Carbon safety strategy clarifies this by including +the requirement of using Carbon as a "rigorously memory safe programming language". + +This proposal introduces a principle "flow checking" to clarify, at a high level, +a technical approach to memory safety through static checking. + +## Problem + +A programming language design can support static checking in many different ways. +Ensuring safety as a language property is inseparably tied to design choices. +By clarifying the high-level approach taken and its commonality and difference +with models like Rust, we clarify the design options, identify open +questions and enable more concrete discussion. + +## Background + +A language design that supports both temporal memory safety and fine-grained control +over memory for performance-sensitive is a very hard problem. + +TODO: Is there any background that readers should consider to fully understand +this problem and your approach to solving it? + +## Proposal + +Flow checking is a specific form of static checking that is defined by the following characteristics: + +* flow- and path-sensitivity: flow checking ensures properties that hold at every program point, + taking into account information available from instructions and certain branch conditions leading up +* hybrid: flow checking is layered over a core, flow-insensitive type system as a "conservative extension". + Code must be accepted by the type system to be considered for flow checking, and information obtained through + flow checking does not influence type system. +* can optionally rely on annotations to specify effects of operations. This information can be used to identiy + operations as erroneous, even if they look acceptable from a type checking point of view. + +This definition is intentionally abstract and leaves out constraints on the type systems. A core type +system statically checks which operations are permitted on data. This gives possibility of enforcing +a programming discipline that maintains global invariants, which in turn can be useful for memory +safety and flow checking. + +Rust borrow checking is one form of flow checking system that relies heavily on type invariants +("aliasing-xor-mutability"). Rust does not need effect annotations because the type invariants are +very strong and generic library types that provide functionality provide sound operations where +the strength of the invariants hurt expressivity. + +Carbon's system of flow checking may choose less strong type invariants and/or different core +library operations to enable sound memory safe programming patterns. In particular, it +is possible to come up with more permissive regime for control of aliasing and non-interference. + +## Details + +TODO: Fully explain the details of the proposed solution. + +Temporal memory safety is mainly about ensuring reference and pointer validity in +the presence of operations that render them invalid. + +For a given memory location (place) $\pi$ and a program construct $p$ that refers to it, +the following core operations are a form of memory access that relies on `p` being a valid: + +* dereference `*p` +* member access `p.m` +* element access `p[i]` + +Carbon programs manipulate memory locations, which affects whether a given location $\pi$ +will satisfy the conditions safe access. We are often able to deduce from static properties +like well-typedness whether program access will be safe. In general, this problem +is undecidable, so static checking has to work with approximations. + +A standalone flow-insensitive type discipline that aims to provide safety has to +satisfy the following statement (type soundness): + +> If (program is well-typed) then (program execution is safe) + +We accept that type checking restricts programmers: there are safe programs which may not pass type checking. +Carbon's goal of incremental migration from C++ is fundamentally in conflict with such a notion +of type soundness: idiomatic C++ code may use programming patterns that are safe to execute but +fail to rigorous safety checks that enable compilers to verify. + +Thus, we pursue rigorous safety through a split into type and flow checking: + +> If (program is well-typed) then (if (program is flow-checked) then (program execution is safe)) + +Type safety in languages like C++ has come to mean preventing type errors due to mismatching +between data and supported operations. This is not enough for memory safety and sound execution. +Carbon's permissive mode (TODO: link) must apply the same type checking algorithm to a +programs that correspond to migrated C++ as well as Carbon programs that are rigorously memory safe. + +## Rationale + +TODO: How does this proposal effectively advance Carbon's goals? Rather than +re-stating the full motivation, this should connect that motivation back to +Carbon's stated goals and principles. This may evolve during review. Use links +to appropriate sections of [`/docs/project/goals.md`](/docs/project/goals.md), +and/or to documents in [`/docs/project/principles`](/docs/project/principles). +For example: + +- [Community and culture](/docs/project/goals.md#community-and-culture) +- [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem) +- [Performance-critical software](/docs/project/goals.md#performance-critical-software) +- [Software and language evolution](/docs/project/goals.md#software-and-language-evolution) +- [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write) +- [Practical safety and testing mechanisms](/docs/project/goals.md#practical-safety-and-testing-mechanisms) +- [Fast and scalable development](/docs/project/goals.md#fast-and-scalable-development) +- [Modern OS platforms, hardware architectures, and environments](/docs/project/goals.md#modern-os-platforms-hardware-architectures-and-environments) +- [Interoperability with and migration from existing C++ code](/docs/project/goals.md#interoperability-with-and-migration-from-existing-c-code) + +## Alternatives considered + +Rust borrow checking can be considered a flow checking system that is built on strong type invariants. +The strong type invariants make migration from C++ very difficult as they require a type discipline that +is incompatible with many established C++ patterns. + +TODO: What alternative solutions have you considered?