Borrow Checking as a Dataflow Analysis Over Places

A lifetime in a type is a name for a set of program points. &'a T does not mean “a pointer that lives for a” in any temporal sense; it means “a pointer that is valid at every point in the set a”. Borrow checking is therefore a question about sets of program points and the constraints between them, and the mechanism that answers it is a liveness analysis on a control-flow graph, not a scope walk. That framing explains both why the checker accepts programs that look unsound and why it rejects programs that are obviously fine.

The three constraint kinds

The checker works on a mid-level representation in which every local, temporary, and field access is a place, and every assignment, call, and borrow is an operation on places. It describes the constraints in terms of regions: a region is a set of program points, every reference type carries one, and a loan is a region paired with the place borrowed. Three kinds of constraint relate them, and the checker’s job is to find regions small enough to accept the program and large enough to keep it sound.

Outlives constraints relate regions: 'a: 'b means every point in 'a is also in 'b, so a region can be shrunk by adding points, never grown. These come from subtyping (a &'long T may be used where &'short T is expected) and from the requirement that a borrow’s region include the region of the place being borrowed.

Liveness constraints say that a region must include every point where a reference carrying it is live. Liveness here has the standard dataflow meaning: a variable is live at a point if some path from that point reads it before it is overwritten or goes out of scope. The set is computed by a backward pass over the control-flow graph, unioning successors’ live sets and adding the variables defined at the point.

Type constraints come from the program’s own operations. A borrow creates a loan: the place borrowed, the region of the borrow, and whether it is shared or mutable. A write to a place while a loan is live on it is an error, as is a move out of a borrowed place, as is a second mutable loan overlapping a live one.

The checker then solves for a minimal assignment of points to regions that satisfies all constraints. It does not search for a proof; it propagates liveness backwards and checks each loan against the loans and writes it overlaps. The whole analysis is polynomial, and the interesting engineering is in the representation rather than the asymptotics.

What lexical lifetimes got wrong

Before non-lexical lifetimes, a borrow’s region was the lexical scope of the reference’s declaration. That is sound (a borrow valid for the whole block is certainly valid where it is used), but it is unnecessarily strong, and it produced errors for programs that never use the reference after a certain point:

let mut v = vec![1, 2, 3];
let first = &v[0];
println!("{}", first);
v.push(4);            // rejected under lexical lifetimes: `first` still in scope

The borrow of v ends at the println!, because first is not live afterwards; nothing reads it. Under the lexical rule, the borrow lasts to the end of the block, so the mutable borrow for push conflicts with a shared borrow that no longer exists in any meaningful sense. The error message was technically correct and practically useless.

The fix was to replace the scope with liveness. A borrow’s region is the set of points where the reference is live, computed by the dataflow pass, plus the points needed to satisfy outlives constraints. The example above then compiles, and the rule it enforces is the one the programmer expects: the shared borrow ends at its last use.

The change also removed a class of problem with conditional control flow. Under lexical rules, a borrow inside one arm of an if lasted to the end of the enclosing block, so code that borrowed mutably in one branch and immutably in another conflicted even though the paths are disjoint. With liveness, the regions are per-path, and the borrow ends where the path ends.

Two refinements followed. Two-phase borrows split a mutable borrow into a reservation and an activation, so that v.push(v.len()) is accepted: the receiver is reserved before the argument is evaluated and activated at the call, which lets the shared read of v.len() overlap the reservation without overlapping the write. And the switch to a place-based representation allowed the checker to reason about disjoint fields: borrowing s.a mutably while s.b is borrowed shared is fine, because the loans are on different places.

Why the analysis is not a type system

The important structural point is that lifetimes are inferred, not declared, at the level the checker operates on. The annotations in signatures are contracts; inside a function body, the compiler assigns fresh region variables and solves for them. A function with no lifetime annotations still gets a full liveness-based analysis of its body.

This is why the checker needs no lifetime calculus of its own. It never has to prove that a region exists for all time; it only has to prove that every use of a reference falls inside its region and that no conflicting loan overlaps. Both are properties of a finite graph, and both are decided by propagation to a fixed point rather than by searching for a proof.

The cost is incompleteness in the other direction. The analysis is conservative about anything it cannot see into: a call to a function whose signature does not express the relationship between its arguments’ lifetimes will be assumed to borrow everything for the duration of the call. That is why signature annotations exist, and why an API that returns a reference derived from one of several arguments must name the lifetime explicitly; the compiler will not infer it from the body across a function boundary.

The limits that remain

Three classes of program are still rejected or accepted on grounds the analysis cannot express.

Conditional control flow that a path-insensitive analysis cannot distinguish. A loop that borrows a field on one iteration and reassigns the containing struct on another produces constraints that the propagation cannot satisfy, even when every execution is safe. This is the problem the Polonius formulation attacks: it replaces the “loan is live at a point” check with an origin-based analysis that tracks, for each point, which loans may still be used later along any path, and it handles the “borrow of a field of a struct that is later overwritten” case that the current checker rejects.

Self-referential structures. A struct that holds a reference to its own field cannot be expressed, because the reference’s region would have to include the struct’s own storage, and moving the struct invalidates the reference. The standard workarounds (pinning the value so it cannot move, or using an index instead of a reference) are design patterns rather than language features, and the pinning mechanism is itself a library-level contract.

Unsafe code. The checker’s guarantees stop at an unsafe block. Everything inside is checked for type correctness but not for aliasing, and the obligation to uphold the invariants passes to the programmer. This is why the boundary is drawn at a keyword rather than a lint: the compiler is asserting that it cannot verify the code, and the programmer is asserting that they have.

The error messages as a specification

A practical consequence of the design is that the checker’s diagnostics describe the constraint that failed rather than the rule that was violated. A conflict reports two loans with the points at which each is live and the operation that created the conflict, which is why the messages are long and why they are usually correct about what the problem is.

The message quality is a direct function of the analysis being explicit. Because regions are sets of points with named origins, the checker can say “this borrow is used here” rather than “this value does not live long enough”. Languages with weaker or implicit lifetime systems cannot produce that explanation, because they do not have the intermediate representation to produce it from.

For the programmer, the actionable part is that a rejection means the analysis found a point where two constraints overlap. Restructuring to shorten the region (moving a use earlier, cloning a small value, splitting a struct so fields are borrowed separately) resolves it. The checker is not guessing at intent; it is reporting a specific pair of program points, and the fix is to change the program so those points no longer overlap.

The relationship to the rest of this cluster is that the analysis is what makes the other mechanisms composable. Move semantics relies on it to know a destructor must not run, interior mutability is the sanctioned hole in it, and unsafe abstraction boundaries are where its guarantees are handed off to a human. The analysis itself is a liveness computation with a few constraint kinds, and its power comes from taking the results seriously rather than from sophistication.