Lesson 6.8 — Places, mutability and references: l-values, exclusivity, borrow checking¶

Techniques: l-values and places — a judgment that classifies every expression as a value, a place or a mutable place, so that assignment and &/&mut can demand storage (C's lvalues, C++'s value categories [CLANG-ExprClass], Rust's places, Pebble's §9.1); exclusivity — no two overlapping accesses to the same storage unless both are reads (Swift's Law of Exclusivity [SE0176]; Pebble's per-call rule E0414; Rust's &mut uniqueness); borrow checking with non-lexical lifetimes — lifetimes as sets of control-flow points computed from liveness and outlives constraints, then loans in scope as a forward dataflow (Rust RFC 2094 [RFC2094], [RUSTC-Borrowck]), and its Datalog restatement Polonius [POLONIUS] · Pebble implements: places and categories (the value/place/mut-place column of the typed dump), reference arguments (E0411–E0413) and the exclusivity rule E0414 — exercise E5; no borrow checker, because Pebble references cannot be stored or returned · Drills: none (quiz items loans-in-scope, nll-region are computational) · Prerequisites: Lesson 6.3; Lesson 5.7 (dataflow on the AST) · Time: 3.5 hours

A type says what a value is; it does not say whether an expression denotes storage. x + 1 = 2 is well typed in every sense except that x + 1 is not somewhere you can store. And storage is where the hardest bugs live: two names for the same memory, one of them writing while the other assumes the contents are stable. This lesson takes the three steps compilers take, each stronger than the last: classify expressions as places (C's lvalues); forbid overlapping accesses to the same place during a call (Swift and Pebble); and track how long a reference lives so that no conflicting access happens while it may still be used (Rust's borrow checker). Pebble stops at the second step, deliberately: with references only as parameters, the second step already guarantees that a &mut parameter never aliases another.

1. Problem and motivation¶

L-values and places¶

The problem. Assignment, &, &mut, ++ and C++ reference binding need an expression that names storage; reading needs only a value. C calls the former lvalues ("left of =") and adds modifiable lvalues (not const, not an array); C++11 refined the split into lvalues, xvalues and prvalues so that move semantics could tell "storage about to die" from "storage in use" [CLANG-ExprClass]. Rust calls them place expressions and separates the question "is it a place?" from "may I mutate it?" — let k is a place but not a mutable one, and &mut k is E0596. Every checker needs this second judgment, next to the type, and a mistake in it is a soundness hole: storing through a temporary silently loses the write, and binding a mutable reference to a constant breaks immutability.

Exclusivity¶

The problem. If a function takes two &mut int (or inout) parameters and the caller passes the same variable twice, the callee's reasoning — "writing a does not change b" — is false. The optimizer's reasoning is false too: without aliasing guarantees it must reload b after every store to a. Swift made this a language rule in Swift 4, the Law of Exclusivity: "two accesses to the same variable are not allowed to overlap unless both accesses are reads" [SE0176], enforced statically for local variables and inout arguments and dynamically for class properties and globals. Pebble adopts the static half for calls: a root variable passed as &mut must not appear in any other argument (E0414). Rust's &mut has the same meaning, "the only way to reach this memory right now".

Borrow checking with non-lexical lifetimes¶

The problem. When references can be stored in variables, returned and kept in data structures, "during the call" is no longer the answer to how long an access lasts. Rust's original borrow checker made a reference's lifetime its lexical scope, which rejected obviously fine code: let first = &v[0]; println!("{}", first); v.push(4); — first is never used after the print, yet its scope covers the push. RFC 2094 redefined a lifetime as the set of control-flow points where a reference may still be used, computed from liveness, and then checks each access against the loans that are in scope there [RFC2094]; it shipped with Rust 2018. Polonius reformulates the same check in Datalog with loans flowing through origins instead of points flowing into regions, which accepts some programs NLL rejects [POLONIUS].

2. Definitions and algorithms¶

L-values and places¶

Definition 6.8.1 (Places and categories)

Each expression has a category \(\kappa \in \{\mathsf{value}, \mathsf{place}, \mathsf{mutplace}\}\) as well as a type; the judgment is \(\Gamma \vdash e : \tau \mathrel{@} \kappa\). In Pebble (pebble-spec §9.1), with \(\mathrm{mut}(x)\) true for var bindings and &mut parameters (§6.4):

\[ \dfrac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau \mathrel{@} (\mathrm{mut}(x) \mathbin{?} \mathsf{mutplace} : \mathsf{place})}\ (\textsf{P-Var}) \qquad \dfrac{\Gamma \vdash e : \{\ldots, f : \tau, \ldots\} \mathrel{@} \kappa \qquad \kappa \ne \mathsf{value}}{\Gamma \vdash e.f : \tau \mathrel{@} \kappa}\ (\textsf{P-Field}) \]

\[ \dfrac{\Gamma \vdash e_1 : [\tau; n] \mathrel{@} \kappa \qquad \kappa \ne \mathsf{value} \qquad \Gamma \vdash e_2 : \mathsf{int}}{\Gamma \vdash e_1[e_2] : \tau \mathrel{@} \kappa}\ (\textsf{P-Index}) \qquad \dfrac{\Gamma \vdash e : \tau \mathrel{@} \kappa}{\Gamma \vdash (e) : \tau \mathrel{@} \kappa}\ (\textsf{P-Paren}) \]

and every other expression (literals, operators, calls, fields or elements of a non-place) has category \(\mathsf{value}\). The root of a place is the variable of its P-Var leaf. Category is inherited from the root: "mutability belongs to the binding".

Algorithm 6.8.2 (Checking reference arguments)

Input: a call argument \(a\) and the parameter's mode \(m \in \{\text{by value}, \&, \&\mathsf{mut}\}\) and type \(\tau\).
Output: nothing, or one of E0411, E0412, E0413, E0401 (pebble-spec §13.3).
Precondition: names are resolved (Chapter 5); categories are computed by Definition 6.8.1.
Postcondition: accepted with \(m = \&\mathsf{mut}\) ⇒ \(a\) is &mut p with \(p\) a mutable place of type exactly \(\tau\) (Theorem 6.8.9).
Invariant: the place operand is typed in synthesis mode — a reference never converts (no literal rule, no expected type).

function CheckArgument(a, m, τ):
    if m = by value:
        if a is &p or &mut p:     report E0411 at a;  return
        check a against τ                                   # Lesson 6.4
        return
    if a is not (&p or &mut p) with the same mode m:   report E0411 at a;  return
    (σ, κ) ← Synth(p)                                       # type and category
    if κ = value:                  report E0412 at p;  return
    if m = &mut and κ ≠ mutplace:  report E0413 at root(p), note at root's declaration;  return
    if σ ≠ τ and σ, τ are not <error>:  report E0401 at p

Exclusivity¶

Definition 6.8.3 (Access; conflict; the Law of Exclusivity)

An access is a read or a write of a place over an interval of execution: instantaneous for x = e or reading x, and non-instantaneous for a &mut/inout argument (the whole call), a mutating method on a value (the whole method) or a live reference (its lifetime). Two accesses conflict if they overlap in time, touch overlapping storage, and at least one is a write. The Law of Exclusivity forbids conflicts [SE0176]. A checker is conservative if it rejects every program in which a conflict can happen; it may reject some that are conflict-free.

Algorithm 6.8.4 (Pebble's per-call exclusivity check, E0414)

Input: a call \(f(a_1, \ldots, a_n)\) whose arguments passed Algorithm 6.8.2.
Output: at most one E0414 per &mut root variable of the call, at the first other occurrence, with the note "'x' is passed as '&mut' here" (pebble-spec §9.3, §13.3).
Precondition: every name refers to a resolved binding; two different bindings never share storage in the caller's frame (they may if the caller's own reference parameters alias — excluded by induction, Theorem 6.8.10).
Postcondition: accepted ⇒ the root of each &mut argument occurs in no other argument (not as a place, not in an index, not by value).
Invariant: reported holds the roots already diagnosed in this call.

function CheckExclusivity(a1..an):
    reported ← ∅
    for i in 1..n where ai = &mut p:
        x ← root(p)
        if x ∈ reported: continue
        for j in 1..n, j ≠ i, in order; within aj in source order:
            if some name occurrence o in aj refers to x:
                report E0414 at o, note at the root name of ai;  reported ← reported ∪ {x};  break

The rule compares root variables, not places: swap(&mut a[0], &mut a[1]) is rejected although the elements are disjoint, as in Rust (§7), because the indices are not known statically in general.

Borrow checking with non-lexical lifetimes¶

Definition 6.8.5 (Points, loans, regions; liveness and outlives constraints [RFC2094])

A point is a location in the MIR control-flow graph (a statement of a basic block). A loan is created by each borrow r = &'a p or &'a mut p at point \(P\): the tuple \((\text{region } {'a}, \text{shared} \mid \text{mut}, p)\). A region (lifetime) is a set of points; 'a contains \(Q\) iff references of that lifetime may be used on entry to \(Q\). Regions are the least sets satisfying two kinds of constraints: liveness — if a variable whose type mentions 'r is live at \(Q\) (its current value may be used later), then \(Q \in {'r}\); and outlives at a point — \(({'a} : {'b}) \mathrel{@} P\), generated when a reference with lifetime 'a is copied into a location of lifetime 'b at \(P\) (including \(r = \&'a\,p\) assigning the loan's lifetime into \(r\)'s), requires 'a to include every point of 'b reachable from \(P\) without leaving 'b.

Algorithm 6.8.6 (Region inference by fixed point [RFC2094, Layer 1])

Input: the CFG; the liveness of every variable at every point; the outlives constraints.
Output: the least region for every region variable.
Precondition: liveness is computed (backward dataflow, Chapter 14).
Postcondition: the regions satisfy all constraints and are pointwise least.
Invariant: each region only grows, and every point it contains is forced by some constraint.

for each region r:  r ← { Q | some variable whose type mentions r is live at Q }
repeat
    changed ← false
    for each constraint (a : b) @ P:
        for each Q reachable from P by a depth-first search that stays inside b:
            if Q ∉ a:  a ← a ∪ {Q};  changed ← true
until not changed

Definition 6.8.7 (Loans in scope; relevant access)

A loan \(L\) is in scope at point \(Q\) if some path from its borrow reaches \(Q\) with every point on it in \(L\)'s region and no kill of \(L\) on it; an assignment lv = … kills the loans whose borrowed path has lv as a prefix (the old value is gone, so the borrow no longer protects anything). An access at \(Q\) is illegal if a loan in scope at \(Q\) is relevant to the accessed path (the same path, a prefix of it, or an extension of it, [RFC2094, Layer 5]) and the access and the loan are not both reads.

Algorithm 6.8.8 (Borrow check: loans in scope, then errors [RFC2094, Layer 5])

Input: the MIR CFG; the loans and their regions from Algorithm 6.8.6.
Output: the set of illegal accesses (E0499, E0502, E0506, …).
Precondition: regions are computed.
Postcondition: an access is reported iff a relevant, conflicting loan is in scope at its point (Definition 6.8.7).
Invariant: \(\mathit{IN}[Q]\) ⊇ the loans in scope on entry to \(Q\) along the paths already propagated; at the fixed point it is exact.

# phase 1: forward gen/kill dataflow over bit sets of loans
IN[entry] ← ∅;  IN[Q] ← ∅ for all other Q
repeat
    for each point Q in reverse post-order:
        IN[Q] ← ∪ OUT[pred] over predecessors
        S ← { L ∈ IN[Q] | Q ∈ region(L) }            # loans whose region ends are killed
        if Q is a borrow creating L:          S ← S ∪ {L}
        if Q assigns lv:                      S ← S \ { L | lv is a prefix of path(L) }
        OUT[Q] ← S
until no OUT changes

# phase 2: check each access against the loans in scope
for each point Q and each access (path p, read|write) at Q:
    for each L ∈ IN[Q] with Q ∈ region(L) and path(L) relevant to p:
        if not (access is read and L is shared):  report at Q, citing L's borrow and a later use

rustc's Borrows dataflow [RUSTC-Borrowck] is phase 1, with the kill "loans whose region does not include \(Q\)" precomputed as kill_loans_out_of_scope_at_location.

3. Worked examples¶

L-values and places¶

The type table of ch06-typecheck (pebble-spec §14.4) prints the category after every expression's type. For var xs = [1, 2]; let k = 1; it prints index : int mut-place for xs[k] (root xs is a var), name k : int place for k, and binary + : int value for xs[k] + 1. So bump(&mut xs[k]) is accepted, bump(&mut k) is E0413 at k (a place, not mutable), and bump(&mut (xs[0] + 1)) is E0412 (a value). C++ makes the same distinctions under other names — the clang++ box in §7 shows x + 1 = 2 ("expression is not assignable") and inc(x + 1) ("expects an lvalue").

Exclusivity¶

Algorithm 6.8.4 on swap(&mut xs[0], &mut xs[1]): \(a_1 = \&\mathsf{mut}\ xs[0]\) has root xs; scanning \(a_2\) finds xs at its first occurrence — E0414 there, note at the xs of \(a_1\); reported = {xs}, so \(a_2\)'s own &mut root is skipped and the call gets one error, not two. On add(&mut xs[0], &xs[1]), a shared reference to the same root is also rejected: the callee's src would change when it writes dst. For the program excl.pbl

fn swap(a: &mut int, b: &mut int) { let t = a; a = b; b = t; }
fn add(dst: &mut int, src: &int) { dst += src; }

fn main() -> int {
    var xs = [1, 2];
    let k = 3;
    swap(&mut xs[0], &mut xs[1]);   // one root, two &mut arguments
    add(&mut xs[0], &xs[1]);        // &mut and & of the same root
    add(&mut k, &xs[0]);            // k is immutable
    return xs[0];
}

the reference solution prints (output of pebblec --emit=typed-ast excl.pbl, standard error, complete):

excl.pbl:7:27: error[E0414]: 'xs' is passed as '&mut' and must not appear in another argument of the same call
    7 |     swap(&mut xs[0], &mut xs[1]);   // one root, two &mut arguments
      |                           ^~
excl.pbl:7:15: note: 'xs' is passed as '&mut' here
    7 |     swap(&mut xs[0], &mut xs[1]);   // one root, two &mut arguments
      |               ^~
excl.pbl:8:22: error[E0414]: 'xs' is passed as '&mut' and must not appear in another argument of the same call
    8 |     add(&mut xs[0], &xs[1]);        // &mut and & of the same root
      |                      ^~
excl.pbl:8:14: note: 'xs' is passed as '&mut' here
    8 |     add(&mut xs[0], &xs[1]);        // &mut and & of the same root
      |              ^~
excl.pbl:9:14: error[E0413]: cannot pass immutable 'k' as '&mut'
    9 |     add(&mut k, &xs[0]);            // k is immutable
      |              ^
excl.pbl:6:9: note: 'k' declared here
    6 |     let k = 3;
      |         ^

Borrow checking with non-lexical lifetimes¶

Number the statements of the §7 program nll.rs by their line: 3 first = &v[0] (loan \(L_1\), shared, path v), 4 println!(first), 5 v.push(4) (a mutable borrow of v: a deep write), 6 second = &v[1] (loan \(L_2\)), 7 v.push(5) (deep write), 8 println!(second).

Step	Result
Liveness of `first`	live at 4 only (its last use)
Liveness of `second`	live at 7, 8
Algorithm 6.8.6	`'first = {4}`; \(({'L_1} : {'first}) \mathrel{@} 3\) gives `'L1 = {4}`; `'second = {7, 8}`, `'L2 = {7, 8}`
Algorithm 6.8.8, phase 1	IN[4] = {L1}; at 5, \(5 \notin\) `'L1`: killed, IN[5] = ∅; IN[7] = {L2}, IN[8] = {L2}
Phase 2 at 5	deep write of `v`, no loan in scope — accepted
Phase 2 at 7	deep write of `v`; \(L_2\) is in scope, relevant (path `v`), shared vs write — error E0502 citing the borrow at 6 and the use at 8

A lexical checker would make 'L1 the whole scope of first (lines 3–9) and reject line 5 as well. rustc's message (§7) names exactly the three points of the table's last row.

4. Invariants and correctness¶

L-values and places¶

Theorem 6.8.9 (Accepted &mut arguments denote mutable storage of the parameter type)

If \(\Gamma \vdash p : \sigma \mathrel{@} \kappa\) by Definition 6.8.1 and Algorithm 6.8.2 accepts &mut p for a parameter &mut τ, then \(p\) denotes a storage location of type \(\tau\) that belongs to a var binding or to storage the caller received as &mut; so every write the callee makes through the parameter writes storage that the program is allowed to modify.

Proof

Algorithm 6.8.2 requires \(\kappa = \mathsf{mutplace}\) and \(\sigma = \tau\). By induction on the derivation of the category. P-Var: \(\kappa = \mathsf{mutplace}\) only if \(\mathrm{mut}(x)\), i.e. \(x\) is a var binding (its own storage) or a &mut parameter (by pebble-spec §9.3 an alias for a place the caller passed as &mut, which by the induction hypothesis applied to that call denotes modifiable storage). P-Field and P-Index: the premise \(\kappa \ne \mathsf{value}\) with the same \(\kappa\) means the base is a mutable place, so it denotes modifiable storage of an aggregate type, and a field or element of such storage is modifiable storage of the field's or element's type (value semantics, §9.2: the aggregate is stored inline, not shared). P-Paren: the same place. Every other expression is a value, which Algorithm 6.8.2 rejects (E0412). Since the category is computed with the type in one traversal, \(\sigma\) is the type of that storage.

Exclusivity¶

Theorem 6.8.10 (Pebble's rule makes &mut parameters unaliased)

In a Pebble program accepted by the checker, during every call, the storage denoted by a &mut parameter is disjoint from the storage denoted or read by every other parameter of the same call.

Proof

By induction on the depth of the call stack. Consider a call \(f(a_1, \ldots, a_n)\) in a function \(g\), with \(a_i = \&\mathsf{mut}\ p\), \(x = \mathrm{root}(p)\). By Algorithm 6.8.4, no other argument mentions \(x\). Pebble has no pointers and no heap references, and references exist only as parameters (E0420 forbids them elsewhere), so the storage an argument \(a_j\) denotes or reads is contained in the storage of the root variables it mentions. Distinct bindings of \(g\) have disjoint storage: locals are distinct slots of \(g\)'s frame; a by-value parameter is a copy; a reference parameter of \(g\) denotes a caller's place, and by the induction hypothesis (applied to the call of \(g\), one level shallower) a &mut parameter of \(g\) is disjoint from \(g\)'s other parameters, while two shared & parameters may overlap but are never written. The only case left is two shared parameters of \(g\) that overlap, one passed on as &mut — impossible, since &mut q needs a mutplace and a & parameter is not one (Theorem 6.8.9). Hence the storage of \(a_i\) is disjoint from that of every \(a_j\), \(j \ne i\). The base case is main, which has no parameters.

Borrow checking with non-lexical lifetimes¶

Theorem 6.8.11 (Loans stay in scope until the last use of the reference)

Let a loan \(L\) be created at \(P\) as \(R = \&p\) (or \(\&\mathsf{mut}\,p\)), and let the value of \(R\) — or a copy of it — be dereferenced at \(Q\). Then on every CFG path from \(P\) to \(Q\) along which that value is carried and on which no assignment kills \(L\), \(L\) is in scope at every point after \(P\) up to and including \(Q\). Consequently, if Algorithm 6.8.8 reports nothing, no conflicting access to \(p\) happens between the borrow and any use of the reference.

Proof

Fix such a path \(P = Q_0, Q_1, \ldots, Q_k = Q\) and follow the value: at each \(Q_i\) (\(i \ge 1\)) it is held by some variable \(V_i\), with \(V_1 = R\), changing only at copies \(V_{i+1} = V_i\). Every \(Q_i\) is in 'L. The variable holding the value at \(Q_i\) is live there (its value is used later, at \(Q\) at the latest), so by liveness \(Q_i \in \mathrm{region}(V_i)\). The borrow generates \(({'L} : \mathrm{region}(R)) \mathrel{@} P\), and each copy at \(Q_j\) generates \((\mathrm{region}(V_j) : \mathrm{region}(V_{j+1})) \mathrel{@} Q_j\). By induction along the path, \(Q_i \in {'L}\): the points \(Q_1 \ldots\) up to the first copy are reachable from \(P\) inside \(\mathrm{region}(R)\) (they are all in it by liveness), so Algorithm 6.8.6 adds them to 'L; after a copy at \(Q_j\), the points up to the next copy are reachable from \(Q_j\) inside \(\mathrm{region}(V_{j+1})\), so they are added to \(\mathrm{region}(V_j)\) and, by the induction hypothesis's constraint chain from 'L to \(\mathrm{region}(V_j)\), to 'L. \(L\) is in the IN set at every \(Q_i\). Phase 1 generates \(L\) at \(P\), keeps it where the point is in 'L (all \(Q_i\), just shown), and removes it only by a kill, which the path avoids; the dataflow's union at joins keeps it when other paths do not. Errors. An access to \(p\) at some \(Q_i\) that conflicts with \(L\) (a write, or any access if \(L\) is mutable) is relevant to \(L\) and is reported by phase 2. The kill case is sound for a different reason: an assignment to a prefix of the borrowed path replaces the value the loan pointed into, so later accesses touch new storage [RFC2094, Layer 5]. Soundness of the full Rust type system, including libraries that use unsafe, needs a semantic proof [JJKD18].

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Categories (Definition 6.8.1) with type checking	\(O(n)\)	linear	\(O(1)\) per node	\(n\) AST nodes
Exclusivity (Algorithm 6.8.4) per call	\(O(k \cdot s)\)	\(O(s)\): \(k\) is usually 0 or 1	\(O(k)\)	\(k\) `&mut` arguments, \(s\) total argument size
Region inference (Algorithm 6.8.6)	\(O(c \cdot \lvert\mathcal{P}\rvert)\) per round, at most \(r \cdot \lvert\mathcal{P}\rvert\) growing steps	a few rounds	\(O(r \cdot \lvert\mathcal{P}\rvert)\) bits	\(c\) constraints, \(r\) regions, \(\lvert\mathcal{P}\rvert\) points
Loans in scope (Algorithm 6.8.8)	\(O(\lvert\mathcal{P}\rvert \cdot \ell / w)\) per pass, \(d + 2\) passes	2–3 passes	\(O(\lvert\mathcal{P}\rvert \cdot \ell)\) bits	\(\ell\) loans, \(w\) word size, \(d\) loop nesting
Polonius (naive Datalog)	polynomial; the transitive `subset` per point is \(O(o^3 \cdot \lvert\mathcal{P}\rvert)\)	slower than NLL; optimized variants prune	\(O(o^2 \cdot \lvert\mathcal{P}\rvert)\)	\(o\) origins

Justification. Categories are one extra field computed in the same traversal. Exclusivity scans every other argument once per &mut argument. Region inference: every round either adds a point to a region (at most \(r \cdot \lvert\mathcal{P}\rvert\) times in total) or stops, and a round costs one bounded DFS per constraint. Loans in scope is a gen/kill bit-vector problem, which converges in (loop-connectedness + 2) passes in reverse post-order (Chapter 14). Polonius R2 closes subset transitively at each point: at most \(o^2\) facts per point, each derived from \(o\) pairs.

Pathological family. Region inference on a function with \(r\) references all copied into one another in a long chain across \(\lvert\mathcal{P}\rvert\) points grows every region to nearly all points: \(\Theta(r \cdot \lvert\mathcal{P}\rvert)\) bits and as many insertions — large generated functions (big match tables, macro expansions) are where rustc's borrow checker time concentrates. For exclusivity, a call with \(k\) &mut arguments to distinct roots and long index expressions costs \(k \cdot s\).

Scale. Pebble's checks are linear and invisible in the timing of Lesson 6.1 §5. rustc runs the borrow checker on MIR after type checking; it is one query per function body, so its cost parallels function size.

L-values and places¶

C++ value categories: lvalue / xvalue ("expiring", std::move(x)) / prvalue; const T& binds to prvalues by materializing a temporary — the "temporary: allowed" of Rust's &mut (v[0] + 1) in §7 is the same idea.
Modifiable places via types (C const, Rust let vs let mut): mutability on the binding (Rust, Pebble) or on the type (C, C++), where const int * restricts one path to the storage but not others.

Exclusivity¶

Place-sensitive exclusivity: disjoint fields (&mut s.a, &mut s.b) are accepted by Rust and by Swift for local structs, because field paths are static; array elements are not, because indices are not — the library function split_at_mut (§7) proves disjointness with unsafe inside.
Dynamic enforcement [SE0176]: class properties, globals and escaping closures in Swift record begin_access/end_access at run time and trap on a conflict; [SWIFT-Exclusivity] is the static half.

Borrow checking with non-lexical lifetimes¶

Two-phase borrows (v.push(v.len())): the &mut v of a method call is reserved first and activated at the call, so the argument may read v in between.

Polonius [POLONIUS]: origins contain loans rather than points; a loan is live where it is contained in a live origin. The naive rules R4–R8 (quoted from the Polonius book, rules/loans.md):

// R4: the issuing origins are the ones initially containing loans
origin_contains_loan_on_entry(Origin, Loan, Point) :-
  loan_issued_at(Origin, Loan, Point).

// R5: propagate loans within origins, at a given point, according to subsets
origin_contains_loan_on_entry(Origin2, Loan, Point) :-
  origin_contains_loan_on_entry(Origin1, Loan, Point),
  subset(Origin1, Origin2, Point).

// R6: propagate loans along the CFG, according to liveness
origin_contains_loan_on_entry(Origin, Loan, TargetPoint) :-
  origin_contains_loan_on_entry(Origin, Loan, SourcePoint),
  !loan_killed_at(Loan, SourcePoint),
  cfg_edge(SourcePoint, TargetPoint),
  (origin_live_on_entry(Origin, TargetPoint); placeholder(Origin, _)).

// R7: compute whether a loan is live at a given point, i.e. whether it is
// contained in a live origin at this point
loan_live_at(Loan, Point) :-
  origin_contains_loan_on_entry(Origin, Loan, Point),
  (origin_live_on_entry(Origin, Point); placeholder(Origin, _)).

// R8: compute illegal access errors, i.e. an invalidation of a live loan
errors(Loan, Point) :-
  loan_invalidated_at(Loan, Point),
  loan_live_at(Loan, Point).

R6 is phase 1 of Algorithm 6.8.8 with "region contains the point" replaced by "the origin holding the loan is live"; because subset is per point (R1–R3 in the book), a loan flows only along the paths where it was actually copied, which accepts the conditional-return case NLL rejects ("problem case #3" of [RFC2094]).

7. In real compilers¶

L-values and places¶

Clang computes categories in one function, ClassifyImpl, and Expr::isModifiableLvalue answers "may this be assigned" [CLANG-ExprClass]; rustc's MIR building distinguishes place and value expressions directly.

Not a place, not mutable: clang++ 23 and rustc 1.94

Reproduce (clang 23.1.2, rustc 1.94.1):

mkdir -p rs && cat > lvalue.cpp <<'EOF'
int f();
void inc(int &r) { ++r; }
int main() {
  int a[3] = {0, 0, 0};
  const int k = 1;
  int x = 0;
  a[1] = 5;        // a[1] is an lvalue: fine
  x + 1 = 2;       // x + 1 is a prvalue: not assignable
  f() = 3;         // a call returning int is a prvalue
  k = 4;           // an lvalue, but const
  inc(x + 1);      // a non-const reference cannot bind to a prvalue
  inc(x);          // fine
}
EOF
cat > rs/places.rs <<'EOF'
fn bump(n: &mut i32) { *n += 1; }
fn main() {
    let k = 1;
    let mut v = [1, 2, 3];
    bump(&mut k);          // an immutable binding cannot be borrowed as mutable
    bump(&mut (v[0] + 1)); // a temporary: allowed, but the change is lost
    v[0] += 1;
    println!("{:?}", v);
}
EOF
clang++-23 -fsyntax-only -fno-color-diagnostics lvalue.cpp
rustc --edition 2021 rs/places.rs -o /dev/null 2>&1 | grep -E '^(error|help)| *-->'

Output (complete):

lvalue.cpp:8:9: error: expression is not assignable
    8 |   x + 1 = 2;       // x + 1 is a prvalue: not assignable
      |   ~~~~~ ^
lvalue.cpp:9:7: error: expression is not assignable
    9 |   f() = 3;         // a call returning int is a prvalue
      |   ~~~ ^
lvalue.cpp:10:5: error: cannot assign to variable 'k' with const-qualified type 'const int'
   10 |   k = 4;           // an lvalue, but const
      |   ~ ^
lvalue.cpp:5:13: note: variable 'k' declared const here
    5 |   const int k = 1;
      |   ~~~~~~~~~~^~~~~
lvalue.cpp:11:3: error: no matching function for call to 'inc'
   11 |   inc(x + 1);      // a non-const reference cannot bind to a prvalue
      |   ^~~
lvalue.cpp:2:6: note: candidate function not viable: expects an lvalue for 1st argument
    2 | void inc(int &r) { ++r; }
      |      ^   ~~~~~~
4 errors generated.
error[E0596]: cannot borrow `k` as mutable, as it is not declared as mutable
 --> rs/places.rs:5:10
help: consider changing this to be mutable
error: aborting due to 1 previous error

What to notice: Clang separates "not a place" (lines 8, 9: prvalues) from "a place, not modifiable" (line 10: a const lvalue, with a note at the declaration — the same shape as Pebble's E0413 note). rustc's E0596 is Pebble's E0413; but &mut (v[0] + 1) is accepted by Rust, which materializes a temporary place, where Pebble reports E0412.

Exclusivity¶

Swift's DiagnoseStaticExclusivity.cpp runs a dataflow over begin_access/end_access markers in SIL [SWIFT-Exclusivity]; rustc reports the same conflicts through the borrow checker as E0499.

Two &mut borrows of one array in rustc 1.94

Reproduce (rustc 1.94.1):

mkdir -p rs && cat > rs/excl.rs <<'EOF'
fn swap(a: &mut i32, b: &mut i32) { std::mem::swap(a, b); }
fn main() {
    let mut v = [1, 2];
    swap(&mut v[0], &mut v[1]);               // two &mut borrows of v at once
    let (x, y) = v.split_at_mut(1);           // the library proves the halves disjoint
    swap(&mut x[0], &mut y[0]);
    println!("{:?}", v);
}
EOF
rustc --edition 2021 rs/excl.rs -o excl 2>&1

Output (complete):

error[E0499]: cannot borrow `v[_]` as mutable more than once at a time
 --> rs/excl.rs:4:21
  |
4 |     swap(&mut v[0], &mut v[1]);               // two &mut borrows of v at once
  |     ---- ---------  ^^^^^^^^^ second mutable borrow occurs here
  |     |    |
  |     |    first mutable borrow occurs here
  |     first borrow later used by call
  |
  = help: use `.split_at_mut(position)` to obtain two mutable non-overlapping sub-slices

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0499`.

What to notice: v[_] — rustc forgets the index, exactly like Algorithm 6.8.4 comparing roots: the two elements are disjoint, but the checker cannot know that for arbitrary indices. Its three labels are the three ingredients of Definition 6.8.3 (the first access, the overlapping one, and the use that makes the first last long enough). Line 5–6's split_at_mut is accepted: the disjointness proof lives in the library.

Borrow checking with non-lexical lifetimes¶

rustc builds MIR, infers regions (RegionInferenceContext::solve) and runs the Borrows dataflow of phase 1 [RUSTC-Borrowck]; the dev guide describes the pipeline [RUSTC-DevGuide-Typeck].

Non-lexical lifetimes in rustc 1.94, and the MIR they are computed on

Reproduce (rustc 1.94.1):

mkdir -p rs && cat > rs/nll.rs <<'EOF'
fn main() {
    let mut v = vec![1, 2, 3];
    let first = &v[0];        // shared borrow of v
    println!("{}", first);    // last use of `first`: the borrow ends here (NLL)
    v.push(4);                // accepted since Rust 2018: no live shared borrow
    let second = &v[1];
    v.push(5);                // rejected: `second` is used below
    println!("{}", second);
}
EOF
cat > rs/mir.rs <<'EOF'
pub fn first_then_push(v: &mut Vec<i32>) -> i32 {
    let r = &v[0];
    let x = *r;
    v.push(x);
    x
}
EOF
rustc --edition 2021 rs/nll.rs -o nll 2>&1 | head -10
rustc --edition 2021 --crate-type=lib --emit=mir -o - rs/mir.rs | sed -n '/^fn/,$p'

Output (complete):

error[E0502]: cannot borrow `v` as mutable because it is also borrowed as immutable
 --> rs/nll.rs:7:5
  |
6 |     let second = &v[1];
  |                   - immutable borrow occurs here
7 |     v.push(5);                // rejected: `second` is used below
  |     ^^^^^^^^^ mutable borrow occurs here
8 |     println!("{}", second);
  |                    ------ immutable borrow later used here

fn first_then_push(_1: &mut Vec<i32>) -> i32 {
    debug v => _1;
    let mut _0: i32;
    let _2: &i32;
    let mut _3: &std::vec::Vec<i32>;
    let _4: ();
    scope 1 {
        debug r => _2;
        scope 2 {
            debug x => _0;
        }
    }

    bb0: {
        _3 = &(*_1);
        _2 = <Vec<i32> as Index<usize>>::index(move _3, const 0_usize) -> [return: bb1, unwind continue];
    }

    bb1: {
        _0 = copy (*_2);
        _4 = Vec::<i32>::push(copy _1, copy _0) -> [return: bb2, unwind continue];
    }

    bb2: {
        return;
    }
}

What to notice: only line 7 is an error; line 5 is accepted because first's region ends at line 4 — the §3 table exactly, including the three points rustc cites (borrow at 6, conflicting access at 7, later use at 8). In the MIR, the loan is _3 = &(*_1) in bb0; _2 (the reference r) is last used by _0 = copy (*_2) in bb1, before push takes _1 mutably, so the loan's region ends before the conflicting access and the function is accepted. This --emit=mir output is the optimized MIR; the borrow checker runs on an earlier version of the same body (-Zdump-mir=nll on a nightly compiler shows it with the regions).

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
L-values and places	Decides where storage is needed and whether it may be modified; sound for `&mut` arguments (Theorem 6.8.9)	\(O(n)\) with the type checker	Separates "not a place" from "not mutable", with a note at the declaration	Low: one more attribute per expression	Every compiler: C/C++ value categories, Rust places, Pebble §9.1
Exclusivity	Conservative per-call rule on roots; no aliasing between a `&mut` parameter and others (Theorem 6.8.10); rejects disjoint elements	\(O(k \cdot s)\) per call	Points at the conflicting occurrence and the `&mut` it conflicts with	Low for calls on roots; medium for field-sensitive or dynamic enforcement	Swift (static + dynamic), Pebble E0414, Rust's `&mut`
Borrow checking with non-lexical lifetimes	References may be stored, returned and copied; accepts until the last use (Theorem 6.8.11); Polonius accepts more	Fixed point over regions + bit-vector dataflow; linear-ish in practice	Borrow, conflicting access and later use, each labelled	High: MIR, liveness, region inference, two-phase borrows	Rust (NLL since 2018, Polonius in development)

Choose places and per-call exclusivity (Pebble, Swift's inout) when references are only passed down to callees: two small checks give aliasing freedom. Choose a borrow checker when references are first-class values that live in variables and data structures and you want that without a garbage collector — and budget for region inference and for users learning to read its errors.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
L-values and places	`place-category`, `lvalue-cpp-bind`	—	`lvalues`	E5 (`E5_ReferencesNeedPlacesOfTheParameterType`, `E5_MutableReferencesNeedMutablePlaces`)
Exclusivity	`exclusivity-roots`, `e0414-once`	—	`exclusivity`	E5 (`E5_Exclusivity`)
Borrow checking with non-lexical lifetimes	`nll-region`, `loans-in-scope`	—	`borrowck`	—

References¶

See the chapter references.

Lesson 6.8 — Places, mutability and references: l-values, exclusivity, borrow checking¶

1. Problem and motivation¶

L-values and places¶

Exclusivity¶

Borrow checking with non-lexical lifetimes¶

2. Definitions and algorithms¶

L-values and places¶

Exclusivity¶

Borrow checking with non-lexical lifetimes¶

3. Worked examples¶

L-values and places¶

Exclusivity¶

Borrow checking with non-lexical lifetimes¶

4. Invariants and correctness¶

L-values and places¶

Exclusivity¶

Borrow checking with non-lexical lifetimes¶

5. Complexity¶

6. Variants and refinements¶

L-values and places¶

Exclusivity¶

Borrow checking with non-lexical lifetimes¶

7. In real compilers¶

L-values and places¶

Exclusivity¶

Borrow checking with non-lexical lifetimes¶

8. Comparison¶

9. Assessment¶

References¶