From 70f2a318e0812c0c86513f9b284adc8918413007 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 19 May 2026 03:07:40 +0200 Subject: [PATCH] =?UTF-8?q?iter=20embedding-abi-m5.tidy=20(DONE=203/3):=20?= =?UTF-8?q?milestone-close=20doc-honesty=20drift=20=E2=80=94=20pin-safe,?= =?UTF-8?q?=20doc/comment-only?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves the M5 milestone-close audit DRIFT (audit journal 28ab56a). Single cohesive commit, M2.tidy a80d495 / M3.tidy 63d7d60 precedent (pins are the coverage, no RED, no audit/fieldtest gate). - docs/DESIGN.md edit-1 §"Free (host side)": dropped the retired-M4 forward-reference ("an additive M4 concern, not a contradiction of this freeze"; M4 retired 2026-05-18) -> present-tense current fact (a boxed-field record is not an M3 embedding type, export-gate-rejected; the freeze covers exactly the all-scalar single-ctor record). - docs/DESIGN.md edit-2 §"Embedding ABI": reconciled the now- inaccurate "(no shared mutable runtime state - ... data-race-free, sanitiser-verified)" blanket with the real post-7bfa11e state: the per-allocation hot path (per-ctx counters + per-object refcount header) is non-atomic by design and never shared (Ctx:!Send, single-thread-per-ctx); the one shared datum is the atomic-relaxed global RC-stats fallback counter; "data-race-free, sanitiser-verified" retained (still true). - runtime/rc.c:88 comment-only: stale "two unconditional ++ operations" -> accurate "one counter bump per alloc/free ... relaxed atomic add on the global null-ctx fallback, a plain ++ on the per-ctx path" (consistent with the adjacent already- correct :93-106 atomic block + :45-55 Threading header). Boss-verified independently: all pins green (design_schema_drift 8/0, docs_honesty_pin 5/0, effect_doc_honesty_pin 4/0, embed_record_layout_pin 1/0) = mechanical proof no pinned/hashed byte moved; the adjacent separately-pinned bare-scalar sentence is byte-identical (shifted 2299->2305 by net-added lines; substring pin, passes); rc.c strictly comment-only (filter empty); cargo build --workspace Finished; git scope = only docs/DESIGN.md + runtime/rc.c + journal/stats. Clears the M5-audit doc-honesty debt; no new debt. FINAL M5 iteration. The M1-M5 Embedding ABI arc is functionally complete, audited, ratified, and doc-honest. Includes the per-iter journal, stats, and INDEX line. --- ...2026-05-19-iter-embedding-abi-m5.tidy.json | 12 +++ docs/DESIGN.md | 20 +++-- .../2026-05-19-iter-embedding-abi-m5.tidy.md | 81 +++++++++++++++++++ docs/journals/INDEX.md | 1 + runtime/rc.c | 6 +- 5 files changed, 111 insertions(+), 9 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-19-iter-embedding-abi-m5.tidy.json create mode 100644 docs/journals/2026-05-19-iter-embedding-abi-m5.tidy.md diff --git a/bench/orchestrator-stats/2026-05-19-iter-embedding-abi-m5.tidy.json b/bench/orchestrator-stats/2026-05-19-iter-embedding-abi-m5.tidy.json new file mode 100644 index 0000000..80a98fe --- /dev/null +++ b/bench/orchestrator-stats/2026-05-19-iter-embedding-abi-m5.tidy.json @@ -0,0 +1,12 @@ +{ + "iter_id": "embedding-abi-m5.tidy", + "date": "2026-05-19", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 3, + "tasks_completed": 3, + "reloops_per_task": { "1": 0, "2": 0, "3": 0 }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null +} diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 1e68f54..8ebc7d9 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2288,9 +2288,15 @@ typecheck*. Every exported entrypoint takes a mandatory leading `ailang_ctx_t*` (M2): a per-thread embedding context created by `ailang_ctx_new()` and released by `ailang_ctx_free()`, owned by the calling thread for its lifetime. The host links one `ailang_ctx_t` per OS worker thread -and the runtime accounts RC alloc/free into it (no shared mutable -runtime state — the swarm artefact is data-race-free, sanitiser- -verified). The staticlib swarm artefact is **RC-only**: +and the runtime accounts RC alloc/free into it: the per-allocation +hot path (the per-ctx counters and the per-object refcount header) +is non-atomic by design and never shared — a box never crosses a +thread (`Ctx: !Send`) and each `ailang_ctx_t` is +single-thread-per-ctx. The one datum a multi-threaded host shares +is the global RC-stats fallback counter (used when no ctx is +bound); it is atomic-relaxed so the swarm's leak accounting is +exact. The swarm artefact is data-race-free, sanitiser-verified. +The staticlib swarm artefact is **RC-only**: `ail build --emit=staticlib` rejects `--alloc=gc`/`--alloc=bump` (the shared Boehm collector is not swarm-safe). The value/record layout is **frozen as of M3** (see "Frozen value layout" below); the @@ -2354,10 +2360,10 @@ is always owned by the host. **Free (host side).** `ailang_rc_dec(payload)`. Leak-free for an M3 record because every field is a scalar — `ailang_rc_dec` is header-only and an M3 record has no boxed children. A record with -boxed fields (`Str`/`List`/nested record) is **not** an M3 type -(rejected by the export gate); a recursive typed-free for that -shape is an additive M4 concern, not a contradiction of this -freeze. +boxed fields (`Str`/`List`/nested record) is **not** an M3 +embedding type — the export gate rejects it, so the boundary +never crosses a value that would need a recursive typed-free. The +freeze covers exactly the all-scalar single-constructor record. ## Data model diff --git a/docs/journals/2026-05-19-iter-embedding-abi-m5.tidy.md b/docs/journals/2026-05-19-iter-embedding-abi-m5.tidy.md new file mode 100644 index 0000000..8a40e35 --- /dev/null +++ b/docs/journals/2026-05-19-iter-embedding-abi-m5.tidy.md @@ -0,0 +1,81 @@ +# iter embedding-abi-m5.tidy — milestone-close doc-honesty drift reconciliation + +**Date:** 2026-05-19 +**Started from:** e81fb90d88bda546829a35496a02ee9c79f80150 +**Status:** DONE +**Tasks completed:** 3 of 3 + +## Summary + +The M5 milestone-close audit (`2026-05-19-audit-embedding-abi-m5.md`) +found three doc-honesty drift items — two `docs/DESIGN.md` prose +inaccuracies and one `runtime/rc.c` stale performance-aside comment. +This tidy reconciles all three: DOC/COMMENT-ONLY, pin-safe, zero +language/checker/codegen/schema/runtime-behaviour change. Mirrors the +M2.tidy (`a80d495`) / M3.tidy (`63d7d60`) precedent — the existing pin +tests (`design_schema_drift`, `docs_honesty_pin`, +`effect_doc_honesty_pin`, `embed_record_layout_pin`) staying green +before AND after is the mechanical proof the edits moved no pinned +byte; that is the coverage, so no RED test, no audit/fieldtest gate. +This is the final M5 iteration; M5 closes after Boss-verify +(roadmap [~]→[x] + done-state are Boss-side). + +## Per-task notes + +- iter embedding-abi-m5.tidy.1: `docs/DESIGN.md` doc-honesty (edit-1 + + edit-2). edit-1 §"Free (host side)" (~:2356-2360): dropped the + retired-M4 forward-reference ("an additive M4 concern") — M4 was + retired 2026-05-18; the boxed-field record is simply + export-gate-rejected (present-tense current fact). edit-2 + §"Embedding ABI" (~:2290-2293): reconciled the stale "no shared + mutable runtime state … data-race-free, sanitiser-verified" claim + with the now-atomic global RC-stats fallback — the per-allocation + hot path (per-ctx counters + per-object refcount header) is + non-atomic and never shared (`Ctx: !Send`, single-thread-per-ctx); + the one shared datum is the atomic-relaxed global RC-stats fallback + counter. Pin-safety proof green (8/5/4 passed, 0 failed across the + three ailang-core pin suites); the adjacent separately-pinned + line (`Export parameters are written **bare**:`, + `docs_honesty_pin.rs:135`) is byte-identical, shifted line 2299→2305 + by the net-added lines above it but content unchanged (the pin is a + substring assertion, not a line-number assertion — it passes). +- iter embedding-abi-m5.tidy.2: `runtime/rc.c` 18g.0-block (~:88-89) + comment-only honesty fix. Replaced the stale "two unconditional + `++` operations" performance aside with the accurate "one counter + bump per alloc/free … relaxed atomic add on the global null-ctx + fallback, a plain `++` on the per-ctx path", consistent with the + adjacent already-correct :93-106 atomic paragraph and :45-55 + Threading header. Mechanical comment-only filter clean (every + changed line is a `*`-prefixed C comment); frozen-IR pin + `embed_record_layout_pin` byte-identical (1 passed, 0 failed — it + asserts generated IR, never rc.c comment text; M3.tidy precedent). +- iter embedding-abi-m5.tidy.3: consolidated doc-only + scope gate + (verification only, no files). All pins green across both crates + (`grep -c 'test result: ok'` == 3 + `embed_record_layout_pin` ok); + `git status --porcelain` shows ONLY `docs/DESIGN.md` + `runtime/rc.c` + as content changes (zero `crates/**`, `examples/**`, `ail-embed/**`, + `Cargo.toml`, `bench/baseline.json`); `cargo build --workspace` + Finished — confirms no behaviour change. + +## Concerns + +(none) + +## Known debt + +(none — this iteration *clears* the M5-audit doc-honesty debt; no new +debt introduced.) + +## Blocked detail + +(n/a — DONE) + +## Files touched + +- `docs/DESIGN.md` (§"Embedding ABI" edit-2 ~:2290-2293; §"Free (host + side)" edit-1 ~:2356-2360 — prose-only) +- `runtime/rc.c` (18g.0 comment block ~:88-89 — C-comment text only) + +## Stats + +bench/orchestrator-stats/2026-05-19-iter-embedding-abi-m5.tidy.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index c212360..5581e24 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -113,3 +113,4 @@ - 2026-05-19 — iter bugfix-swarm-rc-alloc-undercount (RED→GREEN, debug→implement mini, DONE 1/1): root-caused and fixed the m5.2-resume-attempt residual. The M5 swarm leak-proof was still non-deterministic after the atomic-counter runtime fix `7bfa11e` — NOT a second runtime bug and NOT test-methodology unsoundness, but a **build-dependency staleness gap**: `ail-embed/build.rs` declared `cargo:rerun-if-changed` only for the kernel `.ail` + `build.rs`, NOT the `runtime/` C sources `ail build --emit=staticlib` compiles into `libailang_rt.a`. So Cargo never re-ran `build.rs` after `7bfa11e`; `ail-embed` kept linking a stale pre-`7bfa11e` non-atomic `libailang_rt.a` whose `g_rc_alloc_count++` raced the swarm's concurrent TLS-NULL host allocs (explaining the frees-stable/allocs-jitter asymmetry, and why the isolated `crates/ail` RED — which rebuilds the staticlib fresh per run — was green while the `ail-embed` swarm was not). `runtime/rc.c` at HEAD was always correct; the entire production fix is one directory-level `cargo:rerun-if-changed=/runtime` line (preferred over a per-file list — the implementer inspected `crates/ail` `build_staticlib` confirming `libailang_rt.a = ar(rc.o,str.o)`, both under `runtime/`; directory tracking is future-proof against any new runtime source). RED (debugger, audit-trail `483117d`): `ail-embed/tests/rt_archive_freshness.rs` pins the *cause* deterministically (objdump the linked archive for `lock`-prefixed atomic increments + a fresh-build cross-check) since the *symptom* is non-deterministic by construction; Boss-verified RED = 0 lock insns ("STALE"). GREEN (implement mini, this commit): the build.rs fix + the cohesive consequence — `symbol_fan_swarm_leak_free` un-`#[ignore]`d (body byte-for-byte verbatim — it was always quarantined, never weakened; the three doc breadcrumbs rewritten to the resolved build-dep-staleness rationale), now the integration-level acceptance of both `7bfa11e` and this fix. Boss removed a pre-existing dead `DataFormat` import in swarm.rs inline (trivial; file committed this iter regardless). Boss-verified independently: RED→GREEN; **swarm determinism 5/5 — `symbol_fan_swarm_leak_free` + `symbol_fan_swarm_bit_exact` GREEN every run, 0 ignored, jitter gone, Σallocs==Σfrees==12000003**; isolated `embed_rc_global_stats_race` still GREEN (untouched); Invariant 1 data-server count 0; scope = `ail-embed/build.rs` + `ail-embed/tests/swarm.rs` + journal + stats only. The M5 swarm leak-proof bounce-back is now fully resolved end-to-end (bounce-back → Option A `7bfa11e` → resume-attempt "necessary-but-insufficient" → this build-dep root-cause+fix). RED `483117d` → GREEN this commit. M5 stays open `[~]`; m5.3 (time-shard + friction-harvest + close-out) remains. → 2026-05-19-iter-bugfix-swarm-rc-alloc-undercount.md - 2026-05-19 — iter embedding-abi-m5.3 (DONE 3/3): final functional M5 iteration — the time-shard boundary-invisibility proof + friction harvest. One symbol (EURUSD), three disjoint contiguous single-month windows (2017-03/04/05), each folded on its own thread owning its own `Kernel` (`Ctx: !Send` ⇒ one-ctx-per-thread compile-time-enforced). Adds the purely-additive windowed adapter sibling `fold_window` (same `MidPriceStream`+`Kernel` path as `fold_symbol`, differs only by `stream_tick_windowed`), a new single-responsibility `[[bin]] timeshard_runner`, `chrono` as a **dev-dep** (the time-shard test derives `(y,m)→Unix-ms` bounds via data-server's own `NaiveDate…timestamp_millis()` precedent and passes raw ms to the bin, keeping the bin date-math-free and Invariant 1 untouched), and `tests/timeshard.rs` carrying the spec §3 strength-ordered assertions: (a) each shard's `(acc,n)` **bit-exact** vs a single-thread host fold of THAT EXACT window in data-server stream order — the first actual proof of the chunk/window-boundary-invisibility claim the entire M4 retirement rests on; (b) host-summed partials bit-exact by construction; (c) the whole-window [2017-03..2017-05] single-thread total within `REL_TOL=1e-6` only (cross-shard f64 re-association is host arithmetic, NOT a kernel property — asserting it bit-exact would be the bug; tolerance derived from the recursive-summation error bound with ~4 orders of safety, shown in the test). Plus the now-deterministic global leak-Σ (post-`dbd76e5`) and a journal-only friction-timing capture (no bench gate, no timing assertion — flake-free). RED was a genuine deterministic compile failure (declared-but-absent `[[bin]] timeshard_runner` source; surfaced as Cargo's missing-source error rather than the plan's predicted `env!` error — same root cause, same trigger, no false-green; recorded as a benign plan-text imprecision in Concerns). The shipped m5.2 symbol-fan path (`swarm_runner.rs`, `swarm.rs`) and m5.1 core stay byte-untouched and green. Boss-verified independently: **timeshard determinism 5/5** (consistent ~2.7s, no jitter); full ail-embed suite **0 failed AND 0 ignored** across all binaries (lib 2, swarm 2 — the m5.2 leak-proof stays un-ignored & green, the whole saga's resolution intact —, smoke 1, rt_archive 1, timeshard 1); isolated `embed_rc_global_stats_race` still green; AILang workspace `cargo metadata` data-server count 0; compiler-surface diff empty (zero diff to crates/ailang-*, crates/ail/, runtime/, examples/*.ail, root Cargo.toml, DESIGN.md). **Friction-harvest deliverable (P2 flat-array-decision input): host-per-tick-FFI ≈ 658 ms / 3 192 562 ticks ≈ ~206 ns/tick at real EURUSD volume.** M5's functional work is complete; the milestone closes next via the mandatory `audit` (which also handles the pre-existing `docs/DESIGN.md:2358-2360` "additive M4 concern" drift, explicitly out of m5.3 scope). → 2026-05-19-iter-embedding-abi-m5.3.md - 2026-05-19 — audit embedding-abi-m5 (milestone close): DRIFT (one doc-honesty tidy) + RATIFY (gc_rss trio, evidenced) + causally-exonerated pre-existing P2 bench noise. Architect: **Invariant 1 PASS** (zero data-server in any compiler crate/runtime; ail-embed its own workspace root; only "finance" hits are the M3 ABI export *symbol name* — ABI not data-server knowledge), M3 frozen-layout SSOT unmoved (the lone rc.c change `7bfa11e` touched only the global stats counters), rc.c header-comment honesty accurate; drift = `[medium]` DESIGN.md:2358-2360 stale "additive M4 concern" (PRE-EXISTING, M4 retired, correctly scoped out of M5) + `[medium]` DESIGN.md §"Embedding ABI" silent-drift (it asserts "no shared mutable runtime state … data-race-free" but the now-atomic global RC-stats fallback IS shared mutable state under concurrency — M5 is AILang's first concurrent consumer) + `[low]` rc.c:88 "two unconditional ++" imprecise — one tidy, same honesty axis, not split. Bencher (my pre-audit "gc_rss is allocator-orthogonal → environmental" hypothesis was **refuted by evidence** — the verification discipline working): the 3× `*.gc_rss_kb +32%` are GENUINE, DETERMINISTIC, M5-attributable — `7bfa11e`'s atomic split a branch in `ailang_rc_alloc` (reached by GC programs via `str.c` int→str at `print`), spilling `%r14/%rbx`; a stale interior list pointer in the new spill slot is conservatively retained by Boehm, pinning a ~32 MB dead spine (Boehm collection #12 freed PRE 32 MB vs HEAD 32 B); bisects exactly on the commit, IR byte-identical, `ail` sha256-identical; RC/bump RSS dead-stable. `bump_s`/`max_us` = pre-existing tracked-P2 (bump RC-orthogonal; max_us 1-sample tail-jitter, PRE often worse, +65→+104% swing between runs minutes apart — dispositively noise), NOT M5. Adjudication: **RATIFY** the gc_rss trio — language reason (Decision 9: Boehm is explicitly transitional; the cost is purely a Boehm conservative-scan false-retention artifact on the transitional allocator of a *correct, necessary, user-approved swarm-safety fix*, codegen-layout-fragile, RC path the committed model and unaffected; chasing it with an out-of-scope codegen change invests in the path being removed) — selective baseline re-anchor `bench/baseline.json` lines 14/44/64 ONLY (137448/137768/137636, bencher-confirmed steady-state; every other metric byte-pristine — a wholesale --update-baseline would have absorbed the P2 noise and broken the established-envelope discipline); re-run confirms the 3 now `ok` at ±0.3%. **NO-ratify / causally exonerated** for bump_s×2 + max_us×2 — baseline pristine, identical disposition to the M2/M3/prelude-decouple closes. Friction-harvest recorded (P2 input): host-per-tick-FFI ≈ ~206 ns/tick at real EURUSD volume. M5 closes after the doc-honesty tidy lands + Boss-verified. Ratify discipline honored: updated baseline JSON + this paired JOURNAL ratify entry committed together. → 2026-05-19-audit-embedding-abi-m5.md +- 2026-05-19 — iter embedding-abi-m5.tidy (DONE 3/3): resolves the M5 milestone-close audit DRIFT (28ab56a). DOC/COMMENT-ONLY, recon-pin-verified, single cohesive commit (M2.tidy a80d495 / M3.tidy 63d7d60 precedent — pins are the coverage, no RED, no audit/fieldtest gate). `docs/DESIGN.md` edit-1 §"Free (host side)": dropped the retired-M4 forward-reference ("an additive M4 concern, not a contradiction of this freeze" — M4 retired 2026-05-18) → present-tense current fact (a boxed-field record is **not** an M3 embedding type, export-gate-rejected; the freeze covers exactly the all-scalar single-ctor record). edit-2 §"Embedding ABI": reconciled the now-inaccurate "(no shared mutable runtime state — … data-race-free, sanitiser-verified)" blanket with the real post-7bfa11e state — the per-allocation hot path (per-ctx counters + per-object refcount header) is non-atomic by design and never shared (`Ctx: !Send`, single-thread-per-ctx); the one datum a multi-threaded host shares is the global RC-stats fallback counter, atomic-relaxed so the swarm's leak accounting is exact; "data-race-free, sanitiser-verified" retained (still true). `runtime/rc.c:88` 18g.0-block comment-only: stale "two unconditional `++` operations" → accurate "one counter bump per alloc/free … relaxed atomic add on the global null-ctx fallback, a plain `++` on the per-ctx path" (consistent with the adjacent already-correct :93-106 atomic block + :45-55 Threading header). Boss-verified independently: all pins green (design_schema_drift 8/0, docs_honesty_pin 5/0, effect_doc_honesty_pin 4/0, embed_record_layout_pin 1/0) — the mechanical proof the edits moved no pinned/hashed byte; the adjacent separately-pinned bare-scalar sentence is byte-identical (shifted 2299→2305 by net-added lines; `docs_honesty_pin.rs:135` is a substring pin, passes); rc.c diff strictly comment-only (filter empty); `cargo build --workspace` Finished; git scope = only docs/DESIGN.md + runtime/rc.c + journal/stats. Clears the M5-audit doc-honesty debt; no new debt. This is the FINAL M5 iteration — M5 (the M1–M5 Embedding ABI arc) is now functionally complete, audited, ratified, and doc-honest. → 2026-05-19-iter-embedding-abi-m5.tidy.md diff --git a/runtime/rc.c b/runtime/rc.c index e6f31a4..07485af 100644 --- a/runtime/rc.c +++ b/runtime/rc.c @@ -85,8 +85,10 @@ static inline ailang_rc_header_t *header_of(void *payload) { * ailang_rc_stats: allocs=N frees=M live=K * * to stderr. The default-disabled path keeps production binaries quiet - * and adds only two unconditional `++` operations to the hot path — - * negligible relative to the libc malloc/free already on each path, + * and adds only one counter bump per alloc/free on the hot path — + * a relaxed atomic add on the global null-ctx fallback, a plain + * `++` on the per-ctx path — negligible relative to the libc + * malloc/free already on each path, * and the bench numbers in JOURNAL 18f.2 were taken with the counters * compiled in but disabled, so the figures are still valid. *