Move Tracking: Catching Use-After-Handoff

The previous episode made the predicates sound: given a value, the type system can decide whether it is safe to move to another thread. That is the structural half of the guarantee. The other half is a question about time, not structure: once a value has been handed to another thread, using it afterward must be an error. A value moved into a child thread no longer belongs to the parent, and touching it from the parent is a use-after-move. Catching that is a flow analysis, and this episode is about how small it turned out to be, and the three ways the small version almost went wrong.

Why it barely has to do anything

The instinct, coming from Rust, is that this needs a borrow checker — the famously intricate machinery of loans and lifetimes. It doesn’t, and seeing why is the key to the whole design. Two narrowings collapse the problem.

First, almost nothing is actually consumed by a move. When a closure handed to a new thread captures a value, that value falls into one of three cases decided by the predicates from the last episode: a shareable (Sync) value is shared, not consumed; a non-sendable (!Send) value is rejected outright; only a value that is sendable but not shareable — an owned capability, the narrow class of things with a single owner — is genuinely moved and thus consumed. Trivial values are simply copied. So the flow analysis only ever has to track a small set of bindings: the owned capabilities.

Second, borrows are somebody else’s job. The whole apparatus of who-may-reference- what was already built in the memory and effect parts — regions, the Trivial constraint, the exclusivity rule on mutable borrows. Move tracking does not need to re-derive any of it; it needs only to follow moves. No loans, no lifetimes, just “this binding was handed off; has anyone used it since?” The result is a small pass, a couple hundred lines, rather than the large subsystem a full borrow checker would be — because, once again, the feature leans on machinery already built rather than rebuilding it.

Three ways the naive version breaks

The trial version tracked moves with a global set of variable names: move a value, add its name to the set, and flag any later reference to that name. This is correct for straight-line code with no shadowing, and wrong everywhere else. A careful review turned up exactly three ways it breaks, and each one shaped the real pass.

Shadowing. In let l = A in let l = B in ..., the name l refers to two different bindings, and a name-based set cannot tell them apart — move the second and the set thinks the first is gone too, or vice versa. Branches. If a value is moved in one arm of an if and not the other, is it usable afterward? A single flat set has no notion of “moved on one path.” Recursion. A value moved inside a function body that runs more than once is moved more than once — a double-move that straight-line tracking never anticipates.

The pass that fixes all three

The real analysis is a separate pass that runs after type inference, once unification has resolved every type — because deciding what is Send && !Sync requires the final types, and entangling that with inference would tangle flow analysis into unification. Run at that point, it sees resolved types and the full lexical structure at once. Three design choices answer the three breakages.

Against shadowing, every binding gets a fresh identity — an id minted at each let, each function parameter, each pattern binder — and the consumed set holds ids, not names. Two bindings both called l are simply two different ids; shadowing dissolves, because the checker never confused them in the first place. This is the same instinct that runs through the whole language — when one name carries two meanings, give them separate identities — now applied inside the move checker.

Against branches, the pass is flow-sensitive and conservative. It threads a consumed set through the program left to right; at an if or a match, it runs each branch from the same starting set and then merges by union — a binding moved in any branch is treated as moved afterward. That can reject a program that was actually fine, if the move only happened on a path not taken, but it never accepts an unsound one. Soundness over precision is the deliberate default: refuse the uncertain rather than allow the wrong.

Against recursion, the pass simply refuses to move a value captured from an outer scope inside a function that could run repeatedly, because a value moved on iteration one is gone by iteration two. It is the safe side of a line that could later be relaxed — a “runs at most once” notion would permit some of these — but for now the honest, conservative answer is no.

The seam left honest

One interaction is deliberately left half-done, and named rather than hidden. When a capability that a with block is responsible for cleaning up is moved into a spawned thread, the parent must not run its cleanup — responsibility has transferred to the child. Move tracking correctly forbids the parent from using the moved capability, but the actual transfer of the cleanup obligation to the child is code-generation work deferred to a later step. The sound stopgap is exactly the conservative move the rest of the pass makes: until cleanup-transfer is implemented, simply refuse to move a with-bound capability into a thread at all. Better to reject a valid program than to emit one that closes a resource twice.

Together with the last episode, the move guarantee is now whole: the predicates decide whether a value may cross a thread boundary, and this pass tracks whether it already has, so handing a capability to a thread and then touching it is a compile-time error rather than a runtime race. There is still one soundness gap the review found, and it is not about flow but about types that aren’t yet pinned down — a channel whose element type is still a variable, through which a non-sendable value could be smuggled. Closing it means teaching the type inference itself about Send. Next: polymorphic channels and the Send bound.