From 97e793dd62b0c7150fb211fe4e0f9bf920748063 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 8 May 2026 14:27:36 +0200 Subject: [PATCH] JOURNAL: Iter 18g.2 + post-18g.2 re-bench MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-runs the latency bench post-18g.2 and records the result: RC p99 = 311.6 µs (1.37× median), max = 348.2 µs (1.53× median); Boehm p99 = 7249 µs (69.65× median), max = 7923 µs. RC is 23× better on p99 and 23× better on max. RSS: RC 42 MB vs Boehm 66 MB — RC is now LOWER RSS, not higher. Median throughput: RC is 2.18× slower (alloc-path tax). Decision 10's real-time commitment has its evidence base. Boehm retirement is now an orchestrator call between (A) 'retire, accept the throughput tax until a slab allocator is built' and (B) 'build the slab allocator first, retire after'. No commit yet flips defaults. Documents the 18-arc as complete on the correctness property: explicit-mode RC reports live=0 on the canonical bench fixture (allocs=11068575 frees=11068575). Remaining open work is orchestrator-territory or queued (tag-conditional partial-drop, let-alias-aware mode propagation, tidy-iter). --- docs/JOURNAL.md | 166 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 166 insertions(+) diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 0b74aef..bea6c32 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -7939,3 +7939,169 @@ follow-up, not a regression introduced here. alias (the same carve-out as 18d.4 Iter A's fix) still evades the param-mode gate; the carve-out is unchanged and still queued as a propagation-pass iter. + +## 2026-05-08 — Iter 18g.2: let-binder drop for Own-returning App + +18g.1 closed the per-op leak (LCons outer cells in tail- +recursive arms) but `bench_latency_explicit` still reported +`live = 1048575` at exit — exactly the depth-19 Tree cache +(524287 TNode + 524288 TLeaf) that main holds across the +whole run. Diagnosis: the existing `is_rc_heap_allocated` +predicate returned `false` for any `Term::App`, citing the +doc-comment "later iters tied to (own) ret-mode contracts". +We have those contracts (Iter 18a); this iter delivers the +deferred case. + +### Fix shape + +`is_rc_heap_allocated` widens: an `App` whose callee carries +`ret_mode == Own` is now trackable. The signal is the +callee's own static contract — the typechecker gates `Own` +ret-modes through the same machinery that gates `(own T)` +parameter modes (Iter 18a / 18c.2's linearity check), so the +predicate is sound by construction. `Borrow`-returning calls +remain non-trackable (the callee retains ownership) and +`Implicit`-returning calls remain non-trackable (back-compat +lane, leaks rather than mis-decs). + +`drop_symbol_for_binder` gains an `App` arm: synthesise the +return type, resolve `Type::Con { name }` to +`drop__` with cross-module qualification through +`import_map`. Falls back to `ailang_rc_dec` for non-`Type:: +Con` returns (e.g. unresolved type vars on a polymorphic +call's pre-monomorphisation site — the monomorphised copies +get the right symbol). + +`emit_inlined_partial_drop` now defaults to shallow +`ailang_rc_dec` when `value` is not `Term::Ctor`, instead of +panicking. With Iter 18g.2's wider input set, a +pattern-match against an `App`-bound let-binder can populate +`moved_slots`; the partial-drop helper has no static ctor to +key off, so the dynamic-tag carve-out fires (same family as +18d.4's `(case (LCons h t) ...)` debt). Closing this +remaining leak path requires a tag-conditional helper; queued +for later. + +### TDD record + +Red: `alloc_rc_let_binder_for_owned_returning_app_drops_at_scope_close` +on `examples/rc_let_owned_app_leak.ail.json` — pre-fix +`live = 3` (a depth-1 Tree: 1 TNode + 2 TLeaf children), +post-fix `live = 0`. Kept as regression coverage. + +### End-to-end on bench_latency_explicit + +``` +arm | wall(s) | RSS(KB) | live (allocs/frees) +implicit @ gc (Boehm) | 0.245 | 66400 | n/a (no rc-stats) +explicit @ rc (pre-18g.1) | 0.348 | 511000 | 11048575 (11068575 / 20000) +explicit @ rc (post-18g.1) | n/a | 511000 | 1048575 (11068575 / 10020000) +explicit @ rc (post-18g.2) | 0.285 | 42336 | 0 (11068575 / 11068575) +implicit @ rc (control) | 0.359 | 511632 | (leaks: Implicit-mode debt) +``` + +`live = 0` end-to-end. Decision 10's "RC frees promptly" property +now holds on the canonical bench fixture without exception. + +### Re-bench on the latency axis (post-18g.2) + +``` +arm | median(µs) | p99(µs) | p99/med | max(µs) | max/med +implicit @ gc (Boehm) | 104.1 | 7249.4 | 69.65× | 7923.4 | 76.13× +explicit @ rc (post-18g.2) | 227.4 | 311.6 | 1.37× | 348.2 | 1.53× +implicit @ rc (control) | 295.9 | 412.7 | 1.39× | 432.0 | 1.46× +``` + +Compared to 18f.2 (pre-18g.1): + +- RC's median tightened slightly (280 → 227 µs). The added + per-op `rc_dec` is more than offset by the cache effects of + not retaining 11M live cells. +- RC's p99 tightened (453 → 312 µs) and p99/median dropped + (1.62× → 1.37×). Boehm's tail unchanged at ~7 ms (its STW + pauses don't depend on whether the comparator is leaking). +- RC RSS dropped from 511 MB to 42 MB; explicit-mode RC is + now LOWER RSS than Boehm (42 vs 66 MB). Boehm reserves + conservatively; RC frees promptly. The "RC pays an RSS + premium" intuition is wrong on this workload. + +### Implications for the Boehm retirement decision + +The 18f throughput bench failed its 1.3× target. The 18f.2 +latency bench supported the real-time claim but had to +caveat that explicit-mode RC was leaking. Post-18g.2, both +caveats lift: + +- **Tail latency**: RC is 23× better than Boehm on p99 (312 + vs 7249 µs) and 23× better on max (348 vs 7923 µs). RC's + p99/median is 1.37× — meets even a strict real-time + determinism criterion. Boehm's 70× p99/median is the STW + pause signature. +- **RSS**: RC is now LOWER than Boehm (42 vs 66 MB) on this + fixture — promptly-freed cells beat Boehm's conservative + heap reservation. +- **Median throughput**: RC is 2.18× slower than Boehm. This + is the `ailang_rc_alloc` (libc malloc + 8-byte header init) + vs Boehm's bulk-page allocation cost. Path B (slab/pool + allocator in `runtime/rc.c`) would close most of this; Path + A (lower the throughput threshold) accepts it as the price + of bounded latency. + +Decision 10's central commitment — RC + uniqueness for real- +time-grade memory management — has its evidence base. The +remaining gap between "evidence base exists" and "Boehm +retired" is an orchestrator call, no longer a measurement +question. The two open paths from 18f's entry: + +1. **Path A**: accept that RC is throughput-slower, retire + Boehm anyway because the latency + RSS wins are decisive + and the real-time property is the canonical reason this + project exists. +2. **Path B**: build a slab/pool allocator first to close + the throughput gap, then retire. + +Both are available. Path A's "lower the threshold" framing +from 18f no longer applies — it presumed RC was on par with +Boehm; in fact RC is decisively better on the relevant axis +and merely throughput-slower. Path A is now better described +as "retire Boehm; throughput-tax is acceptable until Path B +is built later." + +The mechanical work to flip the default and drop `-lgc` is +small (a few lines in `bench/run.sh`, `crates/ail/src/main.rs`, +and a README pass). The semantic decision — does AILang +commit to the throughput-tax-for-determinism trade — is +canonical Decision 10 territory. Recorded here for the +orchestrator's review; no commit yet flips defaults. + +### Iter status / 18-arc closure + +18-arc as originally scoped: + 18a (modes), 18b (rc runtime), 18c.1–4 (clone + linearity + + uniqueness + per-type drop), 18d.1–4 (reuse-as + move-aware + patterns + scope-close drops), 18e (drop-iterative + worklist), + 18f (bench). + +Post-rename: 18f decided not to decide. 18f.2 ran the right +bench and surfaced two implementation gaps, both now closed: + + 18g.0 (rc-stats counter for diagnosing leaks) + 18g.1 (outer-cell shallow-dec at tail-call sites) + 18g.2 (let-binder drop for Own-returning App) + +The 18-arc's correctness property — "explicit-mode RC matches +explicit-mode RC's documented contracts; no leaks on the +canonical fixture" — now holds. The arc is complete. The +remaining open items are: + + - Boehm retirement (orchestrator decision, see above). + - Tag-conditional partial-drop helper (the dynamic-tag + carve-out shared by 18d.4 and 18g.2; not load-bearing + for the canonical fixture; queue for later). + - Let-alias-aware param-mode propagation (the 18d.4 Iter + A carve-out; same as above). + - Tidy-iter (the 18-arc's mandatory family-boundary + tidy; queued as #80). + +After the orchestrator's Boehm-retirement decision lands, +the tidy-iter is the right next step.