AILang/design/models/rc-uniqueness.md

RC + Uniqueness — memory model whitepaper

Dual allocator — RC canonical, Boehm parity oracle

AILang ships two allocator backends with an asymmetric role:

• RC is canonical. --alloc=rc is the CLI default for ail build and ail run (see pipeline). The runtime AILang's memory model (RC + uniqueness inference) is designed for. New examples, benches, and corpus tests run under RC unless they explicitly pin GC.
• Boehm stays as a parity oracle. --alloc=gc remains reachable. Its load-bearing job is differential diagnosis: when RC produces a segfault, refcount underflow, or wrong stdout, the GC build of the same module is the cheap "memory bug or logic bug?" probe. The end-to-end suite includes per-example parity tests that run both backends and assert byte-identical stdout — those tests are what make the oracle real.
• --alloc=bump is unchanged: a leak-only bench instrument, not a production target.

Full Boehm retirement (drop libgc, remove the gc backend) reopens when the parity oracle stops paying its keep — concretely, when a few iter families ship without the gc arm catching anything that the rc arm did not already catch. Until then, the cost of keeping libgc as a build dependency is accepted in exchange for diagnostic leverage. The RC + uniqueness memory model, built on the language constraints, holds as the specification of the canonical runtime; the rest of this section documents the Boehm half, retained as the oracle.

Choice: Boehm-Demers-Weiser conservative GC. The simplest working option:

• Replace malloc(...) with GC_malloc(...) in every IR site (currently lower_ctor's ADT box, lower_lambda's env block and closure pair).
• Replace the IR-level declare ptr @malloc(i64) with declare ptr @GC_malloc(i64).
• Add -lgc to the clang link command (in crates/ail/src/main.rs's Build / Run paths).
• No language-level change. No AST change. No schema change.

Rationale:

• Mature. Boehm has been the default conservative GC for decades. Linux distros ship it as libgc / libgc-dev / gc (Arch).
• No language work. Conservative scan of the C stack handles AILang's stack frames without LLVM stack-map infrastructure (which is its own multi-iter design).
• Single-iter integration. Lift-and-shift of the four allocation sites; all existing tests must still pass with identical output.

Trade-offs accepted:

• Conservative over-retention. A user-supplied Int field whose value happens to coincide with a heap address will pin that allocation. In practice, vanishingly rare for typical values; survivable.
• Pause time non-deterministic. Boehm uses stop-the-world mark-sweep. For LLM-author-written stdlib code at MVP scale, pause times are not the bottleneck.
• Build-time dependency. libgc must be installed on the build host. Users without it get a link-time error from clang, not a silent failure.

Per-fn arena via stack alloca

This optimisation is layered on top of Boehm in its simplest form. ailang-codegen runs an escape-analysis pre-pass over every fn body (and every lifted lambda thunk body); allocations the pass proves do not outlive the fn frame are lowered to LLVM alloca instead of @GC_malloc. Allocations that may escape continue to use @GC_malloc. The Boehm collector is still linked and unchanged; this is purely an optimisation above the floor.

Allocation mechanism: LLVM alloca (not a heap arena). Stack allocation matches the "freed at fn return" lifetime exactly, needs no malloc/free pair, and integrates with LLVM's existing optimiser (mem2reg / SROA may further promote the alloca'd box to registers if the box is small and its uses are simple). No new runtime is introduced; no language-level change; no AST or schema change.

Escape rule (conservative). A Term::Ctor or Term::Lam allocation is non-escaping iff (1) it is the value of a Term::Let { name = X, value = ALLOC, body = B }, and (2) the body B does not let any value derived from X flow past the fn frame. "Derived from" follows two propagation rules:

• A Term::Match whose scrutinee is a Var referring to a tainted name propagates taint to every pattern-bound name in every arm. (Pattern bindings hold field projections of the scrutinee, which live inside the same allocation.)
• A Term::Let { name = Y, value = Var(t), ... } where t is tainted makes Y tainted in the let's body.

A tainted name "escapes" if it appears in any of: the tail position of B, the arg list of any Term::App / Term::Do, the field list of a Term::Ctor, or the free-var capture set of a Term::Lam. The closure-pair-callee position of Term::App where the callee is a bare Var to the tainted name is NOT an escape (calling locally is fine).

What this is not. Not a region-inference system. Not flow-sensitive within an arm. Not field-sensitive (pattern bindings are tainted wholesale). Precision can be improved later; correctness is the priority for this iter. A pessimistic answer (claiming an allocation escapes when it does not) only loses optimisation, never correctness.

Codegen integration. Three sites in ailang-codegen/src/lib.rs:

• lower_ctor — ADT box.
• lower_lambda env block (when there are captures).
• lower_lambda closure pair (always 16 bytes).

Each site queries the per-fn non_escape: BTreeSet<usize> (raw pointer addresses of Term::Ctor / Term::Lam AST nodes flagged as non-escaping). On a hit the emitter writes alloca i8, i64 <size>, align 8; on a miss it writes call ptr @GC_malloc(i64 <size>). The rest of the lowering (tag store, field stores, closure-pair packing) is identical.

The closure-pair and its env share an escape verdict — they have parallel lifetimes. If the closure pair is non-escaping, the env is too.

Memory model — RC + Uniqueness with LLM-author annotations

The GC bench (bench/run.sh) showed Boehm contributing a substantial fraction of runtime on allocation-heavy workloads that hold the heap fully live (bench notes in JOURNAL). The mainstream "RC + inference" position is extended with mandatory LLM-author mode annotations (borrow / own), explicit clone, first-class reuse-as, and drop-iterative data attrs.

The cost of GC is structurally in the allocate path — Boehm's GC_malloc is structurally slower than a bump pointer, and the bench workloads exercised allocate cost without collection cost. Tracing GC's irreducible variability cannot be tuned away; RC's costs are bounded and analysable per program point. A corpus committed to one memory model is expensive to switch — pre- stdlib is the cheapest moment to commit.

Choice. AILang's canonical memory model is reference counting with static uniqueness inference and explicit LLM-author annotations on fn signatures, in the lineage of Lean 4 / Roc / Koka. Boehm becomes a transitional allocator (see the dual-allocator section above) and is retired when the RC pipeline matches the bump-allocator floor within an acceptable margin (target 1.3× on bench/run.sh).

Workload scope of the 1.3× target. The 1.3× target was calibrated on the original bench/run.sh corpus: linear list sum (bench_list_sum) and tree walk (bench_tree_walk) — uniform single-allocation-per-step workloads where one inc/dec pair amortises against one allocation. The corpus was later extended with bench_closure_chain (closure-pair allocation: each step allocates two heap objects, the closure cell and its captured env struct) and bench_hof_pipeline (poly-ADT + indirect dispatch). The closure-chain fixture measures wider than the 1.3× linear/tree target: each step pays two allocs and two decs against one bump-pointer bump, doubling the allocation tax on closure construction (current ratio recorded in JOURNAL bench entries). This is a representational cost of the closure-pair layout, not a defect in the RC implementation; a future slab/pool allocator for fixed-shape pair cells (a Boehm-retirement follow-up) would compress this ratio without changing semantics.

The 1.3× retirement target therefore applies to the linear / tree / poly-ADT subset of the corpus. Closure-heavy workloads are tracked under a wider band (the closure-chain baseline records its rc/bump ratio as the rc_over_bump reference value with ±15% tolerance) and are explicitly excluded from the Boehm-retirement gate until a slab/pool answer ships. The memory model's RC commitment is unchanged; what is scoped is the quantitative retirement criterion, not the choice of memory model.

The architecture has two layers:

1. Inference. A post-typecheck pass produces a per-node uniqueness side table. Codegen uses it to elide inc/dec wherever provably redundant.
2. LLM-author annotations. Fn signatures carry mandatory (borrow T) / (own T) mode markers. Authors mark sharing-vs-consumption explicitly. The compiler verifies rather than guesses.

The combination plays to what LLMs are good at (writing slightly more annotation per definition) and avoids what compilers are bad at (proving sharing absent in the face of recursion + closures + match).

The LLM-aware sharpening

A mainstream RC implementation (think Lean 4 in default mode) infers everything from naked AST plus a few optional hints. The inference is conservative; whatever it can't prove unique becomes shared and pays runtime inc/dec. AILang exploits its target audience to push that conservative ceiling higher.

Five mechanisms.

(1) Mandatory (borrow T) / (own T) on fn signatures.

(fn list_length
  (type (fn-type (params (borrow (List Int))) (ret (con Int))))
  ...)

(fn sum_list_consume
  (type (fn-type (params (own (List Int))) (ret (con Int))))
  ...)

(borrow T) declares the parameter is read-only and lives at most until the call returns; the caller still owns it; the callee performs no inc/dec on it. (own T) declares ownership transfer; the callee consumes the value and is responsible for its end-of-life. The declaration is structural (visible in JSON) and binding (the typechecker rejects bodies that contradict it).

For a Lean 4 / Roc author this is all optional and inferred when omitted. AILang makes it mandatory because the LLM author can carry the cognitive cost trivially, and the compiler gains a precise contract at every call site instead of a probabilistic guess.

(2) Linear-by-default consumption with explicit (clone X) (the Term::Clone schema entry lives in Data model).

In bodies, every binder is consumed by exactly one own-mode use. If the LLM writes:

(let p (expensive_fn x)
  (let r1 (consume_a p)        ; consume_a takes (own); consumes p
    (let r2 (consume_b p)      ; ERROR: p already consumed
      ...)))

the compiler emits a structured non-linear-use diagnostic with concrete suggested_rewrites:

• "make consume_a borrow": refactor consume_a's signature, no body change at the call site;
• "explicit clone": insert (clone p) at the first use;
• "fuse traversal": replace the two separate calls with a fused fn.

The LLM picks one. There is no implicit clone — sharing always costs visible source.

(3) Reuse hints as first-class.

(fn map_inc
  (type (fn-type (params (own (List Int))) (ret (own (List Int)))))
  (params xs)
  (body
    (match xs
      (case Nil Nil)
      (case (Cons h t)
        (reuse-as xs (term-ctor List Cons (app + h 1) (app map_inc t)))))))

(reuse-as SRC NEW-CTOR) asks the codegen to allocate NEW-CTOR in SRC's memory slot. Compiler verifies: SRC is owned, this is its last use, sizes match. On a hit: no malloc, no free — the box is overwritten in place. On a miss: structured diagnostic explains which precondition failed; the LLM either adjusts the surrounding code or removes the hint.

This matches Lean 4 / Roc reuse analysis but lifts it from "compiler-inferred when possible" to "author-asserted, compiler- verified". The LLM applies it everywhere it expects to fire and lets the compiler bounce the request when it can't.

(4) (drop-iterative) annotation on data declarations.

(data Tree (vars a)
  (ctor Leaf)
  (ctor Node a (Tree a) (Tree a))
  (drop-iterative))

When the refcount of a Tree value reaches zero, the synthesised dec-on-zero traversal is iterative (worklist + heap-allocated stack) instead of recursive. Avoids stack overflow on deep structures. The LLM adds the annotation where appropriate; the compiler refuses to emit recursive dec-cascade on annotated types.

(5) Structured compiler diagnostics with suggested_rewrites.

Every RC-mode error (use-after-consume, mode-mismatch, reuse-as-fail, drop-cascade-too-deep) emits a JSON object containing the failure kind, the source span, and a list of concrete rewrite suggestions in form-A AILang. The LLM consumes these without prose-parsing. This is the missing half of the LLM-as-author story: the language spec defines not only what compiles, but what the compiler tells the author when it doesn't.

Inference algorithm

Post-typecheck, post-lift_letrecs (see pipeline), pre-codegen pass over the elaborated module. For each Term node that produces or binds a boxed value, the pass computes a uniqueness flag:

• Unique: at this program point, the reference is the only outstanding reference to its referent.
• Shared: there may be multiple outstanding references.

A reference is unique if every path from its allocation to the current program point passes through exactly one binding. The inference is a forward dataflow over the AST. The annotations (borrow / own) provide the inter-fn contract; the inference fills in intra-fn detail.