Compiler design / 13. Borrow validation and drops
Data-flow over HIR enforces shared and exclusive access, infers moves and publishes solver-independent facts beside unchanged HIR. The advisory drop candidates it also records are current scaffolding, not the final cleanup authority.
Two aliases may read the same value in peace. An overlapping mutation can poison every reader's assumptions while the bytes still sit in live memory. Borrow validation catches that conflict at compile time.
Borrow validation also computes last-use and optional transfer facts. It does not own lifetime topology or final backend cleanup. Those facts travel to lifetime and retained-edge analysis, then to a validated memory plan.
Moth's access rule in plain form:
Analysis reasons about places, storage roots and alias root sets. A local, a field path or a temporary can participate. Fresh rvalues passed to mutable call slots materialise into hidden locals first so the checker sees ordinary local access.
Moth is reference-semantic by default, copy-explicit and move-inferred. Reading or binding an existing value creates a shared read-only alias. It does not implicitly copy.
Alias activity is path-sensitive and control-flow-sensitive. Shared aliases, and exclusive aliases that have a reachable holder use, use non-lexical activity. Whether an issued but never-used exclusive capability may be elided remains an explicit experimental question; the reference baseline keeps that capability conservative until canonical semantics adopt the stronger rule.
Borrow validation reads validated HIR and publishes a solver-independent handoff of semantic facts. It records:
These are stable semantic outputs, not a required lattice, root table or solver storage format. Branches and loops remain path-sensitive, but a different solver may derive the same handoff differently. Borrow validation supplies facts without rewriting HIR or choosing lifetime topology or physical representation.
Today's alpha checker approximates these facts with an abstract-state lattice (uninitialized, slot, alias and slot + alias), a LocalId-centred root approximation, per-block may/must future-use precomputation and a forward fixed-point transfer implementation. These are current implementation details, not permanent architecture. Advisory drop candidates are scaffolding output only. They are not stable handoff facts, lifetime proof or accepted backend input.
A stronger production borrow solver and the Boracle reference solver may improve precision without changing this stable handoff or source semantics. Normal compilation does not depend on Boracle running.
Modules compile separately. The checker cannot always open a callee's HIR as local control flow when a call crosses a boundary.
Borrow-owned summaries cover:
Lifetime and retained-edge analysis adds complete result provenance, retained parameters, cardinality, detached stored-result effects, whole-domain kills, frontier-enabling effects, outcome-sensitive retention effects and outlives constraints. Cross-module call transfer consumes both summary layers through stable semantic metadata.
There is no move keyword. Future-use and last-use analysis asks whether a semantic place or value has a later source use on each relevant path.
A candidate is valid only when the proof also preserves any dependent temporary borrow and shows that no capable source alias survives the candidate cleanup frontier. A persistent edge or affine root must not disappear while a dependent temporary borrow remains usable. An inferred transfer moves existing affine cleanup responsibility and never duplicates it.
Optional inferred transfer follows one conservative path:
unproven transfer
-> borrow remains
-> statically proven region retains responsibilityFailure to prove transfer does not reject an otherwise valid source program. The source stays under its validated lifetime owner. This rule differs from channel send, which remains the accepted deferred mandatory-transfer boundary.
Borrow validation supplies these candidate and proof facts. Lifetime and retained-edge analysis consumes last-use and capable-source-death facts for retained-edge liveness and cleanup-frontier validation. The compiler-owned memory planner then uses the validated facts for affine transfer, obligation reclassification and REC selection. Borrow validation does not make any of those decisions.
The alpha details listed above are how today's checker approximates this contract. They are replaceable implementation choices, not a permanent handoff. Advisory drop candidates remain current Wasm scaffolding debt, not final lowering input.
Existing values stored in structs, choices, collections, maps or templates use shared alias semantics by default. Storing a value does not automatically duplicate its child.
copy place creates an independent value graph on purpose. A copied cyclic graph must enter one declared region as a whole.
~place requests exclusive mutation-capable access to an existing mutable place. It is not a move marker or a type constructor. Fresh rvalues satisfy ordinary mutable parameters without source ~. Mutable receiver methods still need an existing mutable place.
Assignment through a mutable alias writes through to the referent. It must not silently detach or rebind the alias.
Borrow validation reads validated HIR and supplies the next analysis with:
Lifetime and retained-edge analysis consumes the last-use classifications and capable-source-death proofs for retained-edge liveness and cleanup-frontier validation. It then owns:
The compiler-owned memory planner consumes these validated topology facts and the future-use, last-use and capable-source-death facts to decide affine transfer, obligation reclassification and REC selection. It owns concrete obligation transitions, cleanup and destruction plans. Borrow validation supplies facts. It does not choose target partition or physical representation.
The alpha checker realises these semantic outputs through the current implementation described above. Its advisory drop candidates remain current Wasm scaffolding debt and never become accepted backend input.
The alpha checker may expose advisory drop candidates to the current Wasm scaffolding path. They are implementation debt, not final cleanup decisions or accepted backend input. Final lowering consumes a validated memory plan instead.
The final lowering path consumes explicit validated artefacts. Borrow facts remain validated context:
borrow and last-use facts
-> validated lifetime topology
-> backend-neutral memory requirements
-> target partition and validation
-> target/profile memory planning
-> ValidatedMemoryPlan
-> backend loweringThe ValidatedMemoryPlan carries allocation-family layout, selected representations, planned affine-responsibility transitions, planned retained-edge obligation transitions, region and declared-region placement, hidden-destination plans, cleanup and destruction plans, REC layout decisions and physical coalescing decisions. docs/src/developer-docs/memory-management/runtime-and-backend-lowering/ owns the full plan contract and its validation invariants. It is produced once per target/profile physical variant, after build-owned target partition and target validation. The compiler-owned planner also settles obligation reclassification and concrete count transitions before lowering.
Last-use and capable-source-death facts first support retained-edge liveness and cleanup frontiers. The memory planner then uses them with validated topology for affine transfer, obligation reclassification and REC selection. Backends consume that settled plan rather than interpreting borrow facts or advisory drop sites directly.
Debug and GC-native representations may erase individual cleanup operations when their runtime owns storage. A capable full-control release backend must still lower without a tracing or reachability collector. It may retain storage under the proven region when optional transfer or a more precise physical optimisation does not apply.
ValidatedMemoryPlan is the single final physical authority for cleanup and count transitions. Borrow facts are validated context, not an alternate lowering authority.
Observable state that a template subscription can still see must remain live for that observation model. Borrow validation treats subscriptions as read-only dependencies, not active borrow lifetimes that freeze the whole heap.
Builder lifecycle roots later connect reactive observability to page, mount, request, frame or arena lifetimes. A backend may use a garbage-collected representation for those already-proven facts, but garbage collection does not define them.
Imagine two workers and one mutable place. If both obtain conflicting access, you have a race-shaped hazard. Moth's access rules reject the pattern at the language level even when today's runtime does not expose general threaded execution.
Channel send remains a separate accepted deferred boundary: a successful send transfers affine cleanup responsibility, a failed send preserves or returns it to the sender and arbitrary shared graphs do not cross task lifetimes.
Return-escape legality, retained-edge legality and cycle legality belong to lifetime-region validation, not optional-transfer proof.
Alternative: expose source lifetimes and move syntax.
Choice: mandatory HIR analysis, optional inferred transfers that back off to borrowing and a memory-plan-driven backend handoff.
Benefit: source APIs stay small while access safety and physical cleanup remain explicit to the compiler.
Cost: analysis precision can retain storage under its proven region longer than a more precise plan would.
~, optional inferred moves and mandatory lifetime topology.DropIfOwned path. They do not form the accepted backend input contract.You leave with the handoff in view: borrow validation proves access and last use, lifetime analysis proves topology, the memory planner chooses cleanup and backends lower that validated plan.