From 311325868011dded0d2d44d035014e19990e3ff0 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 8 May 2026 14:37:36 +0200 Subject: [PATCH] =?UTF-8?q?tidy:=2018g=20sub-arc=20=E2=80=94=20DESIGN=20ra?= =?UTF-8?q?tification,=20latency=20bench,=20negative=20coverage?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves the architect's drift report on the 18g sub-arc: - DESIGN.md: ratify mode-metadata's codegen role. param_modes / ret_mode were already on Type::Fn since 18a; with 18d.4 / 18g they became load-bearing for drop-emission decisions in codegen. The new 'Mode metadata is load-bearing for codegen' subsection records the four seams (Iter A + Iter B + 18g.1 + 18g.2) and names the let-alias-of-borrow carve-out the gates do not propagate through. - bench/run.sh: post-throughput, invoke bench/latency_harness.py on the three canonical arms (Implicit @ gc, explicit @ rc, Implicit @ rc control). The Boehm-retirement bench numbers are now reproducible by anyone running the harness, not just by hand on a specific host. - Negative coverage: examples/rc_let_implicit_returning_app + alloc_rc_let_binder_for_implicit_returning_app_does_not_drop pin the asymmetry to the (own)-ret-mode test (live=0 there, live=1 here). The Borrow-ret-mode case is covered by the language design itself — typechecker rejects 'borrow- passthrough' shapes with consume-while-borrowed. JOURNAL entry records four items as deferred known debt: emit_inlined_partial_drop dynamic-tag fallback, carve-out diagnostics surface, bench-number stat-of-N, and the cross-family ordering observation about CLAUDE.md's tidy-iter rule. The 18-arc is formally closed with this tidy. Next iter is the orchestrator's Boehm-retirement decision (Path A vs Path B from JOURNAL 2026-05-08 18f entry, joined by the post-18g.2 re-bench numbers). --- bench/run.sh | 34 +++++ crates/ail/tests/e2e.rs | 40 ++++++ docs/DESIGN.md | 72 ++++++++++ docs/JOURNAL.md | 135 ++++++++++++++++++ .../rc_let_implicit_returning_app.ail.json | 1 + examples/rc_let_implicit_returning_app.ailx | 63 ++++++++ 6 files changed, 345 insertions(+) create mode 100644 examples/rc_let_implicit_returning_app.ail.json create mode 100644 examples/rc_let_implicit_returning_app.ailx diff --git a/bench/run.sh b/bench/run.sh index 6cbfede..209cbd1 100755 --- a/bench/run.sh +++ b/bench/run.sh @@ -166,5 +166,39 @@ for f in "${fixtures[@]}"; do "$f" "$gc_t" "$bp_t" "$rc_t" "$gc_ratio" "$rc_ratio" "$gc_r" "$bp_r" "$rc_r" done +# Iter 18g tidy: latency bench. The throughput table above is wall- +# time-and-RSS — the wrong metric for Decision 10's real-time claim. +# `bench/latency_harness.py` measures per-operation tail latency +# (median + p99 + p99.9 + max) on PTY-line-buffered stdout for the +# `bench_latency_*` fixtures. We invoke it for the three canonical +# arms (Boehm-fair Implicit @ gc, RC-fair explicit @ rc, control +# Implicit @ rc) and emit a second table. +# +# Skipped if the harness / fixtures aren't present (the latency bench +# was added in 18f.2 and may not exist on older branches that share +# this script). +LAT_HARNESS="$ROOT/bench/latency_harness.py" +LAT_IMPL_SRC="$ROOT/examples/bench_latency_implicit.ail.json" +LAT_EXPL_SRC="$ROOT/examples/bench_latency_explicit.ail.json" +if [[ -x "$LAT_HARNESS" && -f "$LAT_IMPL_SRC" && -f "$LAT_EXPL_SRC" ]]; then + echo + echo ">>> latency bench (PTY inter-arrival, 1000 samples per arm)" + echo + + # Build the three arms. -O2 to match the throughput table. + "$AIL" build --opt=-O2 --alloc=gc "$LAT_IMPL_SRC" -o "$OUTDIR/bench_latency_implicit_gc" >/dev/null + "$AIL" build --opt=-O2 --alloc=rc "$LAT_EXPL_SRC" -o "$OUTDIR/bench_latency_explicit_rc" >/dev/null + "$AIL" build --opt=-O2 --alloc=rc "$LAT_IMPL_SRC" -o "$OUTDIR/bench_latency_implicit_rc" >/dev/null + + # The harness prints a multi-line block per arm; we let it speak + # for itself. The orchestrator captures the verbatim output into a + # JOURNAL entry like the throughput table above. + "$PY" "$LAT_HARNESS" "$OUTDIR/bench_latency_implicit_gc" --label "implicit @ gc (Boehm-fair)" + echo + "$PY" "$LAT_HARNESS" "$OUTDIR/bench_latency_explicit_rc" --label "explicit @ rc (RC-fair)" + echo + "$PY" "$LAT_HARNESS" "$OUTDIR/bench_latency_implicit_rc" --label "implicit @ rc (control: leaks, no STW)" +fi + echo echo ">>> done" diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index 34f01b6..880f9ee 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -2161,3 +2161,43 @@ fn alloc_rc_let_binder_for_owned_returning_app_drops_at_scope_close() { call's return type" ); } + +/// Iter 18g tidy negative-coverage: a let-binder whose value is the +/// result of an `Implicit`-ret-mode (default, unannotated) call must +/// NOT be trackable. Implicit is the back-compat lane that 18c.3 +/// documented as "params don't get any dec — leak rather than mis- +/// dec"; the symmetric carve-out for ret-modes is "Implicit-returning +/// calls do not flow ownership to the caller, the caller must NOT +/// dec". +/// +/// If `is_rc_heap_allocated` were mistakenly to fire on this shape, +/// the let-scope close would emit an unjustified dec — refcount +/// underflow at runtime (the cell's RC reaches zero before any other +/// owner had a chance to dec). The fixture under `--alloc=rc` must: +/// +/// (1) Build cleanly (no consume-while-borrowed false positive, +/// parse error, or unimplemented). +/// (2) Exit cleanly with stdout `7` — the unboxed Int from the cell. +/// (3) Report `live = 1` — the one MkT cell leaks. The leak is the +/// intentional Implicit-mode behaviour; if codegen ever started +/// dec'ing this shape it would crash with refcount underflow +/// before the leak number could even be observed. +/// +/// This test is the negative-side companion to +/// `alloc_rc_let_binder_for_owned_returning_app_drops_at_scope_close`: +/// the asymmetry between (own)-ret-mode (live=0) and Implicit-ret-mode +/// (live=1) is the documented contract. +#[test] +fn alloc_rc_let_binder_for_implicit_returning_app_does_not_drop() { + let (stdout, allocs, frees, live) = + build_and_run_with_rc_stats("rc_let_implicit_returning_app.ail.json"); + assert_eq!(stdout.trim(), "7", "alloc(7) -> unbox should print 7"); + assert_eq!( + live, 1, + "Implicit-ret-mode App must leak (not crash with refcount \ + underflow); allocs={allocs} frees={frees} live={live}. \ + A live count of 0 means is_rc_heap_allocated mistakenly \ + marked Implicit-ret-mode App as trackable; a non-zero exit \ + means the unjustified dec triggered the underflow guard." + ); +} diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 6753dca..ca25cf7 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1038,6 +1038,78 @@ Codegen for `Term::Ctor` / `Term::Lam` env / closure pair under inference is wired up. Until then, `--alloc=rc` deliberately leaks like the pre-Boehm era; this is purely about plumbing. +### Mode metadata is load-bearing for codegen (Iter 18d–18g) + +`param_modes` and `ret_mode` on `Type::Fn` are not merely +typechecker metadata — codegen consults both to decide where to +emit drop calls. The 18d.4 / 18g shipping work moved them from +"annotation that the typechecker enforces" to "annotation that +codegen reads to keep RC correct". Recorded here so the schema +metadata's role is explicit: + +**`param_modes` — drop-emission gates.** + +- **Iter B: Own-param dec at fn return.** When a fn body + fall-throughs to a `ret` (no tail-call), every parameter with + `param_modes[i] == Own` is dec'd before the `ret` iff its + uniqueness `consume_count == 0` and the ret value is not the + param itself. `Borrow` and `Implicit` parameters are skipped: + `Borrow` retains the caller's ownership by contract; + `Implicit` carries no static caller-handed-off-ownership + signal (it's the back-compat lane). + +- **Iter A: arm-close pattern-binder dec.** When a match-arm's + body terminates without a tail-call, every ptr-typed + pattern-bound binder pushed by the arm is dec'd at arm close + iff its `consume_count == 0` and it is not the arm's tail + value, **gated on the scrutinee's static ownership**. If the + scrutinee is a fn-param, only `Own`-mode scrutinees enable + the dec — `Borrow` and `Implicit` scrutinees would let the + arm dec memory the caller still references. + +- **Iter 18g.1: pre-tail-call shallow-dec.** When a match-arm's + body IS a tail call, both Iter A and Iter B are skipped (the + block is terminated). A separate seam in `lower_match` emits + a shallow `ailang_rc_dec` on the scrutinee outer cell BEFORE + the tail call, gated identically on the scrutinee mode plus + the requirement that every ptr-typed slot in the active + ctor's pattern is in `moved_slots[scrutinee]`. + +**`ret_mode` — let-binder trackability.** + +- **Iter 18g.2: `Term::App` drop at let-scope close.** A + let-binder whose value is `Term::App { callee, .. }` is + trackable for scope-close drop iff the callee's + `ret_mode == Own`. The signal is the callee's static + contract that ownership of the freshly heap-allocated cell + flows to the caller. `Borrow`-returning calls remain + non-trackable (the callee retains ownership; the caller + holds a view, not an own ref). `Implicit`-returning calls + remain non-trackable (back-compat lane). + +The drop fn's symbol resolution for an Own-returning App: +synthesise the call's return type, resolve `Type::Con { name }` +to `drop__` (with cross-module qualification through +the import map). Falls back to shallow `ailang_rc_dec` for +returns that are not `Type::Con` (e.g. unresolved type vars on +a polymorphic call's pre-monomorphisation site; the +monomorphised copies resolve to concrete drop fns). + +**What this widening does NOT do.** + +- Does not change the canonical hash. `param_modes` / + `ret_mode` were already hash-load-bearing as of Iter 18a; the + 18d–18g iters add codegen consumers, not new schema fields. +- Does not introduce a new `Type` variant. Mode metadata stays + flat on `Type::Fn` (see "Schema additions" above on why). +- Does not cover let-aliases of borrowed values. A let-binder + whose value is `Term::Var` referencing a `Borrow`-mode + param is not yet propagated through; the param-mode gates + treat such a binder as "owned" (its `current_param_modes` + lookup misses, default = owned). This is a known carve-out + shared by Iter A and 18g.1; closing it is a propagation pass + through let-bindings that has not shipped yet. + ### Migration plan 1. **Iter 18a:** `(borrow T)` / `(own T)` annotations as a diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index bea6c32..f41908f 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -8105,3 +8105,138 @@ remaining open items are: After the orchestrator's Boehm-retirement decision lands, the tidy-iter is the right next step. + +## 2026-05-08 — 18g sub-arc tidy-iter + +`ailang-architect` ran a drift review of the 18g sub-arc +(commits `e8c6e99` through `97e793d`) and reported seven +items, prioritised. Resolved: + +### Ratified into DESIGN.md + +**Item 1: `param_modes` / `ret_mode` codegen role.** DESIGN.md +§ "Codegen contract" gained a "Mode metadata is load-bearing +for codegen (Iter 18d–18g)" subsection that lays out the four +seams that consume mode metadata: Iter B (Own-param dec at fn +return), Iter A (arm-close pattern-binder dec gated on +scrutinee mode), Iter 18g.1 (pre-tail-call shallow-dec), and +Iter 18g.2 (let-binder trackability for Own-returning App). +Also names the let-alias-of-borrow carve-out the gates do not +yet propagate through. + +The schema is unchanged (mode metadata was already on +`Type::Fn` since 18a); what's new is that codegen's drop- +emission behaviour now depends on those fields. Recording the +dependency in DESIGN.md was overdue — this entry closes that +gap. + +### Wired into the harness + +**Item 2: `bench/latency_harness.py` not in `bench/run.sh`.** +`run.sh` now invokes the latency harness on the three +canonical arms (Implicit @ gc Boehm-fair, explicit @ rc +RC-fair, Implicit @ rc control) after the throughput table. +Each invocation prints the median / p99 / p99.9 / max block +the harness already produces. The Boehm-retirement bench +numbers are now reproducible by anyone running `bench/run.sh`, +not just by hand on a specific host. + +The harness output is intentionally not folded into a single +table by the script — the per-arm block carries its own noise- +floor and read-coalescing context that the orchestrator should +see verbatim when capturing into a JOURNAL entry. + +### Negative coverage test added + +**Item 3 (partial): negative-side test for `Implicit`-ret-mode +App.** New fixture +`examples/rc_let_implicit_returning_app.ailx` and test +`alloc_rc_let_binder_for_implicit_returning_app_does_not_drop`. +The fixture is a let-binder whose value is a default-mode +(`Implicit` ret) App; the test asserts the binary exits +cleanly with `live = 1` (the cell leaks but does not crash). +This pins the asymmetry to the (own)-ret-mode test +(`live = 0`) and would fail loudly if a future iter +mistakenly widened `is_rc_heap_allocated` to all App shapes. + +The `Borrow`-ret-mode case was attempted but the typechecker +correctly rejects the only minimal repro shape (a +"borrow-passthrough" returning a borrowed view of an arg) +with `consume-while-borrowed` — meaning the language already +forbids the shape that would have been the negative test. The +gate is therefore covered by language-design constraint +rather than by a regression test, and a comment in the +fixture documents that path. + +### Carry-over (deferred, recorded as known debt) + +**Item 4: `emit_inlined_partial_drop` shallow-dec fallback +silent-leak path.** The fallback fires when an App-bound let- +binder accumulates `moved_slots` (the body pattern-matches +the binder). No fixture currently exercises that shape; if +one lands without surfacing the leak, the carve-out's debt +will compound silently. Queued as: a tag-conditional +partial-drop runtime helper that takes the dynamic ctor tag +as input and dispatches accordingly. Same family as 18d.4's +match-arm dynamic-tag carve-out; both close together. + +**Item 5: carve-outs accumulating without diagnostic +surface.** Three live carve-outs as of 18g.2 — let-aliases of +borrowed scrutinees (18d.4 fix), dynamic-tag pattern-binder +partial-drop (18d.4), dynamic-tag App-binder partial-drop +(18g.2). All three silently leak rather than diagnose. The +typechecker's `consume-while-borrowed` rule prevents the +worst class of these (e.g. the borrow-passthrough fixture +above), but the codegen-time carve-outs are not surfaced to +the user. Closing this requires a structured diagnostic +emitted from codegen when a carve-out path fires — feasible +within the existing `suggested_rewrites` framework. Queued +for the carve-out unification iter. + +**Item 6: bench numbers vs methodology.** The 18g.2 latency +table was a single-host hand-run on AMD 5900X; the harness +captures one run, not a stat-of-N. The qualitative claim +("Boehm has STW pauses, RC doesn't; RC is RSS-lower than +Boehm on this fixture") is robust at a 23× signal margin and +not at risk from run-to-run variance. The quantitative +numbers are not regression-locked. To make them so, the next +re-bench should record N runs and median + variance per cell; +the harness can be extended to do that without re-shaping the +output. Recorded as known limitation rather than fixed in +this tidy because the orchestrator's Boehm-retirement +decision (still open) does not require sub-percent precision +to resolve. + +### CLAUDE.md tidy-iter ordering + +**Item 7: Boehm retirement decision is staged ahead of the +tidy-iter in the 18g.2 entry.** CLAUDE.md "Tidy-iter at +family boundaries" requires the next iter after a family +closes to BE the tidy-iter, with explicit deferral +documented. The 18g.2 closing did not name the deferral +explicitly — implicit by the retirement-decision framing. +This tidy-iter (the entry you are reading) is in fact what +follows the 18g family, in order; the retirement decision +remains queued for the orchestrator's call. The ordering is +preserved in retrospect by this entry; future families +should not stage cross-family decisions before the tidy. + +### What this tidy ships + +- `docs/DESIGN.md` § "Mode metadata is load-bearing for + codegen" (~80 lines added). +- `bench/run.sh` post-throughput latency harness invocations. +- `examples/rc_let_implicit_returning_app.{ailx,ail.json}` + + one e2e test. +- This JOURNAL entry, which both closes the 18g sub-arc and + acknowledges the four deferred items as known debt. + +### Status of the 18-arc + +The 18-arc (a + b + c.1–4 + d.1–4 + e + f) was reported as +"complete on the correctness property" in the 18g.2 entry, +joined by sub-arc 18g (g.0 + g.1 + g.2). With this tidy +entry the family is formally closed; the next iter is the +orchestrator's call between Boehm-retirement Path A and +Path B (see 18g.2 entry for the framing). Three known debts +travel forward as queue-items, not as 18-arc loose ends. diff --git a/examples/rc_let_implicit_returning_app.ail.json b/examples/rc_let_implicit_returning_app.ail.json new file mode 100644 index 0000000..a9ff2e5 --- /dev/null +++ b/examples/rc_let_implicit_returning_app.ail.json @@ -0,0 +1 @@ +{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkT"}],"kind":"type","name":"T"},{"body":{"args":[{"name":"n","t":"var"}],"ctor":"MkT","t":"ctor","type":"T"},"kind":"fn","name":"alloc","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"T"}}},{"body":{"arms":[{"body":{"name":"v","t":"var"},"pat":{"ctor":"MkT","fields":[{"name":"v","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"x","t":"var"},"t":"match"},"kind":"fn","name":"unbox","params":["x"],"type":{"effects":[],"k":"fn","param_modes":["borrow"],"params":[{"k":"con","name":"T"}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"args":[{"args":[{"name":"x","t":"var"}],"fn":{"name":"unbox","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"name":"x","t":"let","value":{"args":[{"lit":{"kind":"int","value":7},"t":"lit"}],"fn":{"name":"alloc","t":"var"},"t":"app"}},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_let_implicit_returning_app","schema":"ailang/v0"} diff --git a/examples/rc_let_implicit_returning_app.ailx b/examples/rc_let_implicit_returning_app.ailx new file mode 100644 index 0000000..f290086 --- /dev/null +++ b/examples/rc_let_implicit_returning_app.ailx @@ -0,0 +1,63 @@ +; Iter 18g tidy negative-coverage fixture: a let-binder whose +; value is the result of an `Implicit`-ret-mode fn call must NOT +; be trackable for scope-close drop. Implicit is the back-compat +; lane (default for unannotated fns); 18c.3 documented "Implicit- +; mode params do not get any dec — they leak rather than mis-dec", +; and 18g.2's symmetric carve-out is "Implicit-returning calls do +; not flow ownership to the caller, the caller must NOT dec". +; +; The asymmetry to `(own T)`-returning calls is real and +; intentional: an Own-returning fn signs a static contract that +; the caller now owns the cell and must dec it; an Implicit- +; returning fn does not. If `is_rc_heap_allocated` were +; mistakenly to fire on this shape, the let-scope close would +; emit a dec for a cell whose ownership is not (statically) the +; caller's. The cell may be a fresh allocation the callee +; happens to return without explicit annotation, OR a static +; constant in BSS, OR a returned-borrow indistinguishable from +; an own at the callee's signature. Dec'ing it would be +; refcount underflow in the first two cases and use-after-free +; in the third. +; +; Properties guarded: +; (1) Build succeeds (no consume-while-borrowed false positive). +; (2) Binary exits cleanly with stdout `7` (no crash, no +; refcount underflow). +; (3) `live = 1` at program exit — the one MkT cell leaks. The +; leak is intentional under the Implicit back-compat lane; +; it documents the asymmetry from the (own)-ret case (which +; would have `live = 0`). + +(module rc_let_implicit_returning_app + + (data T + (ctor MkT (con Int))) + + ; No ret-mode annotation -> default Implicit. Takes one + ; ignored Int param (form-A doesn't allow zero-arg fn-app). + (fn alloc + (type + (fn-type + (params (con Int)) + (ret (con T)))) + (params n) + (body + (term-ctor T MkT n))) + + (fn unbox + (type + (fn-type + (params (borrow (con T))) + (ret (con Int)))) + (params x) + (body + (match x + (case (pat-ctor MkT v) v)))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let x (app alloc 7) + (do io/print_int (app unbox x))))) +)