JOURNAL: Iter 18g.2 + post-18g.2 re-bench
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).
This commit is contained in:
+166
@@ -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_<owner>_<T>` 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.
|
||||
|
||||
Reference in New Issue
Block a user