tidy: 18g sub-arc — DESIGN ratification, latency bench, negative coverage
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).
This commit is contained in:
@@ -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"
|
||||
|
||||
@@ -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."
|
||||
);
|
||||
}
|
||||
|
||||
@@ -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_<owner>_<T>` (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
|
||||
|
||||
+135
@@ -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.
|
||||
|
||||
@@ -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"}
|
||||
@@ -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)))))
|
||||
)
|
||||
Reference in New Issue
Block a user