Ownership Analyses That Ride the IR: Unique Accumulation and Owned/Borrowed Teardown Obligations

Pitch

Decide once, in the frontend, whether a name uniquely owns its object, stamp that fact on the IR, and let each backend choose what to do with it. On the Python backend this took accumulation loops from quadratic to linear copying, and three of six backends read the marker today.

Abstract

Compilers that target several runtimes face a repeated problem: a source-level aliasing fact is needed on every target, and each backend re-derives it. In revl, a language compiled to six targets, out = out.push(x) is a persistent write that copies its receiver, so the loop a programmer wrote as linear was emitted as quadratic on each audited target that copies on write (Python, Go and TypeScript). Two backends had independently written the same unsoundness-prone aliasing proof. We moved it into the frontend as a flow-sensitive forward dataflow with a fixpoint on loop back edges, plus a whole-program retention summary for calls, and stamp the result on the IR as a fact (unique: true or "copy"), not an instruction. On the Python backend, element copies when building a 1000-element list drop from 500500 to 1000, growth per doubling from x4.0 to x2.0, and the library list_sort and list_dedup reach the hand-written baseline in copy count. The TypeScript and Go backends read the same marker; Rust discharges the obligation with its borrow checker; Java and WebAssembly decline it for named representation reasons. We also describe a second ownership analysis on the same pattern, over the resource teardown accumulator: acquired handles are nominal opaque types (R0), the declared inverse cannot be hand-called (O1), and a seven-clause check keeps borrows from escaping (B1). The first analysis is on main and measured by deterministic element-copy counts (no timings); the second ships for owned and borrowed modes, with shared handles specified and deferred.

Problem and claim

Two separate ownership questions recur in revl. For accumulation: is the object this local names reachable through any other name at this write? For resources: which component owns the inverse of an acquired handle, and can any other position close it or keep it? Both are questions about the source program, not about a target language, and both have a wrong answer that is silent: an aliasing bug that changes a value, or a double close.

The claim of the first half: computing the uniqueness fact once, flow-sensitively and per write, in src/revl/ownership.py, is designed to fail safe, with every uncertainty resolving to not owned. That safety is argued from the fallback and the test suite, not proved. The analysis gives backends a shared fact in place of per-backend proofs. Ignoring the marker is always correct, which is what lets backends adopt it independently. The claim of the second half: owned and borrowed modes can be inferred over the teardown accumulator with no new grammar, and a does-not-escape check over the existing scope structure is enough for v1.

These are two analyses with different machinery (a dataflow over locals, a nominal-type and escape discipline over handles). They share a design principle (compute in the frontend, ride the IR or the checker, keep the conservative direction) but not code beyond a common statement of aliasing. The paper either leads with the first half and treats the second as a second application, or is split.

Contributions

1. A flow-sensitive forward dataflow (lattice FRESH < COPY < absent, join is maximum, births kill escapes, escapes gen) that decides per write whether a self-rebinding assign owns its object (src/revl/ownership.py:1-111).
2. A marker protocol that carries a fact and not an instruction: unique: true, unique: "copy" with unique_birth on the introducing let; absent when no write qualifies, so IR for other programs is byte-identical (src/revl/ownership.py:27-47).
3. A whole-program retention summary (least fixpoint over the call graph, optimistic start) that answers whether a callee retains a parameter, closing the list_dedup case (src/revl/ownership.py:617-678).
4. Measurements on the Python backend with a deterministic element-copy counter that rewrites the emitted module's AST (bench/codegen/python/copycount.py:1-30): 500500 to 1000 at n=1000, list_sort 171700 to 5050 at n=100 and 1353400 to 20100 at n=200, list_dedup 5050 to 100 at n=200.
5. A backend-by-backend account of what the marker buys and where it is declined: TypeScript and Go read true only, Python also reads "copy", Rust relies on its borrow checker, Java's list container is immutable, and Wasm's list header has no capacity field.
6. For resources: R0 (acquire returns are nominal opaque handles), O1 (no hand-call of a declared inverse, owner or borrower), B1 (a borrow does not escape, seven clauses), with owned and borrowed landed and shared teardown specified for a counted-grant ledger and deferred (docs/design/308-effect-ownership-modes.md:1-22, :130-220, :398-440).

Related work

Evidence on main

Numbers that exist

• Python element copies at n=1000: build, doubled, fill 500500 to 1000; drop_keys 499500 to 2000; shift_all 503500 to 4000 (docs/v2.0-roadmap.md:1754). Five of six probes match the hand-written column; growth x4.0 to x2.0 per doubling. Deterministic counts, one program per probe, one machine-independent counter.
• list_sort: 171700 to 5050 at n=100, 1353400 to 20100 at n=200, growth x7.9 to x4.0; bytes 1.50x to 1.00x; ops 1.26x to 1.27x (the stated cost) (docs/v2.0-roadmap.md:1857).
• list_dedup: 5050 to 100 at n=200, 20100 to 200 at n=400, x4.0 to x2.0 (docs/v2.0-roadmap.md:1858).
• TypeScript: 79800 to 0 elements copied at n=400 (docs/v2.0-roadmap.md:1862).
• Java list_push: 221224 B/op emitted against 286760 hand-written (docs/v2.0-roadmap.md:1723); line 1861 calls the hand-written Java file a persistent yardstick, so the win needs a mutable-arm case.
• Test counts: 16 (Python accumulation), 49 (ownership modes), 5 (runtime), counted from def test_ lines.
• No timings exist, on purpose; the audit states none were taken because the host was under load (docs/v2.0-roadmap.md:1753).
• No numbers for how many real programs have a qualifying write, analysis compile-time cost, or the false-positive rate of B1 on real code.

Paper outline

1. Introduction: one aliasing proof written twice, six backends; why a fact on the IR.
2. The marker protocol: unique, "copy", unique_birth; why a fact and not an instruction; byte-identical IR when absent.
3. The analysis: lattice, birth, escape, self-rebind kills, loop fixpoint, conservative fallback list.
4. Calls: retention summary as a least fixpoint; extern, host root and function-value callees always retain.
5. Backends: what each does with the marker (Python, TypeScript, Go lower it; Rust relies on rustc; Java and Wasm blockers).
6. Evaluation: copy counts, growth curves, timings (to be added), real-code coverage, fuzzing.
7. Resource ownership as a second application: R0, O1, B1, owned and borrowed, shared deferred; closure capture decision (by value only) as the rule that keeps both analyses simple.
8. Related work and limits.

Threats to validity and limits

• Soundness is not proved. The module docstring says "a wrong answer here is a wrong ANSWER and not a crash" (src/revl/ownership.py:16-18); safety is the conservative fallback plus tests.
• Measured improvements are element-copy counts from an instrumented rewrite of the emitted Python module, not time. The audit chose this deliberately; ops got slightly worse for list_sort (1.26x to 1.27x).
• Only Python and TypeScript have measured wins; Go's lowering predates the frontend marker; Rust, Java and Wasm are unmeasured or declined. Three of six backends read the marker, so "six backends share a fact" is not what main shows.
• concat is never marked because its receiver type is unknown at the node and no tier can mutate a Str in place (src/revl/ownership.py:115-119). A common string-building loop is therefore not helped.
• A local born from a call result is refused; it needs a freshness summary that "was not attempted" (docs/v2.0-roadmap.md:1860).
• Resource half: the inference is positional and the design doc accepts false positives; a legitimate checkout/checkin shape is "deliberately inexpressible in v1" (docs/design/308-effect-ownership-modes.md:164-171). Shared and transfer are not implemented. B1's closure clause was chosen as an outright refusal ("a strictly smaller check", design doc line 417), not because the closure-taint alternative was shown unnecessary.
• The self-host agreement is equality of the parsed IR functions sections on the corpus, not a proof.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 50 checked, 11 corrected.

Cite this draft

@misc{revlp04,
  author       = {Thomas Moussajee},
  title        = {Ownership Analyses That Ride the IR: Unique Accumulation and Owned/Borrowed Teardown Obligations},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P04.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.