iter embedding-abi-m2.1 (DONE 5-9): swarm-safe ctx ABI complete + sanitiser-verified
Completes Embedding ABI — M2.1 (Tasks 1-4 committed c9a84b3 as the
known-good subset; this commit lands Tasks 5-9 from the re-dispatch
against the Boss-corrected plan).
- T5: swarm.c per-thread-ctx scalar-swarm capability demo (no
SHARED_CTX) + rc_accounting_shared_ctx_is_flagged_by_tsan added to
the item-1 harness driver (de-globalisation negative-control teeth,
where a shared ctx genuinely races on ctx->alloc_count).
- T6: M1 host.c migrated to the ctx ABI; embed_e2e green (s==25
through the ctx-threaded forwarder).
- T7: DESIGN.md current-state update (provisional-until-M3 narrowed
to the value/record layout; Decision-10 per-thread-ctx note);
docs_honesty-pinned sentence + (con Int) snippet preserved verbatim.
- T8: regression gate — workspace green; null-ctx fallback
byte-behaviour preserved.
- T9: bench-trio — compile_check/cross_lang clean; check.py
tracked-P2 noise only, causally exonerated (zero codegen/runtime
diff vs HEAD), NO baseline ratified.
Boss-verified directly (not on report trust): docs_honesty_pin 5/0,
design_schema_drift 8/0, embed_export_hash_stable 1/0,
embed_export_gate 6/0, embed_e2e 1/0, embed_staticlib_alloc_guard
2/0, print_no_leak_pin 1/0 + e2e rc_stats 4/0; the tsan coherent-stop
proven by hand — per-ctx clean (exit 0, 0 warnings), shared-ctx a
real ThreadSanitizer data race at rc.c:157/:208 (exit 66).
Known debt (journal + roadmap): DESIGN.md '## Embedding ABI (M1)'
header still says (M1) while the body mirrors M2 — out of Task 7's
scope-limited regions by design; post-audit doc-honesty tidy.
Milestone-close audit next.
This commit is contained in:
+15
-5
@@ -1526,7 +1526,10 @@ acyclicity invariant.
|
||||
`(con T)` is treated as `(own T)`. Existing JSON hashes
|
||||
stay bit-identical until the fixture is intentionally updated.
|
||||
- **Does not commit to atomic refcounts.** AILang is
|
||||
single-threaded; refcounts are non-atomic.
|
||||
single-threaded; refcounts are non-atomic. The embedding ABI's
|
||||
per-thread `ailang_ctx_t` keeps this correct under a host swarm:
|
||||
each thread's allocations are private to its ctx, no RC cell
|
||||
crosses a thread, so non-atomic refcounts stay sound.
|
||||
- **Does not introduce regions.** Regions were considered and
|
||||
rejected; see "Why not other memory models" above.
|
||||
|
||||
@@ -2279,10 +2282,17 @@ parameter and the return type must be `Int` (lowered `i64`) or
|
||||
`Float` (lowered `double`), and the fn's effect set must be empty.
|
||||
These are enforced at `ail check` (`export-non-scalar-signature`,
|
||||
`export-has-effects`) — an effectful or non-scalar export *fails to
|
||||
typecheck*. M1 ships no runtime lifecycle API: the per-thread
|
||||
context parameter that M2 threads through every exported call will
|
||||
change this C signature; do not treat the M1 signature as frozen.
|
||||
The value/record layout freeze is M3.
|
||||
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**:
|
||||
`ail build --emit=staticlib` rejects `--alloc=gc`/`--alloc=bump`
|
||||
(the shared Boehm collector is not swarm-safe). Only the value/record
|
||||
layout remains provisional until M3; the ctx-threaded C signature is
|
||||
the M2 shape.
|
||||
|
||||
Export parameters are written **bare**: a scalar type carries no
|
||||
`own`/`borrow` mode (modes apply only to heap-shaped types, which the
|
||||
|
||||
@@ -1,134 +1,213 @@
|
||||
# iter embedding-abi-m2.1 — per-thread runtime context + concurrency safety
|
||||
|
||||
**Date:** 2026-05-18
|
||||
**Started from:** b3388c83506a314fbd87f3354f80ae8cc212f501
|
||||
**Status:** PARTIAL
|
||||
**Tasks completed:** 4 of 9
|
||||
**Started from:** c9a84b33b3e7806491153a5bd3037be1b8ef9d31 (Tasks 1–4 committed)
|
||||
**Original start (first dispatch):** b3388c83506a314fbd87f3354f80ae8cc212f501
|
||||
**Status:** DONE
|
||||
**Tasks completed:** 9 of 9 (Tasks 1–4 in the first dispatch, committed at c9a84b3; Tasks 5–9 in this re-dispatch)
|
||||
|
||||
## Summary
|
||||
|
||||
Tasks 1–4 land fully green: the FIXED-FIRST alloc-guard baseline pin
|
||||
(RED→GREEN across the iter), the de-globalised `ailang_ctx_t` runtime
|
||||
(per-thread TLS slot + conditional accounting, `g_rc_*`+atexit retained
|
||||
verbatim as the null-ctx fallback), the codegen forwarder gaining a
|
||||
leading `ptr %ctx` + `@__ail_tls_ctx` save/store/restore around the
|
||||
byte-unchanged internal call, and the CLI RC-only guard. Task 2's direct
|
||||
rc-accounting tsan harness proves the de-globalisation teeth: per-ctx
|
||||
clean, and its `-DSHARED_CTX` negative control genuinely races at
|
||||
`rc.c` `ailang_rc_alloc` (validated separately). Task 5 is implemented
|
||||
faithfully to the plan but BLOCKED on a plan-design contradiction: the
|
||||
swarm.c shared-ctx negative control cannot be flagged by tsan because
|
||||
`embed_backtest_step` is a non-allocating scalar kernel that never
|
||||
writes any ctx field, and `@__ail_tls_ctx` is `__thread` (per-thread,
|
||||
never shared even when the `ailang_ctx_t*` value is). Tasks 6–9 not
|
||||
run (ordering dependencies are the Boss's to resequence).
|
||||
The per-thread embedding-ctx ABI is complete. Tasks 1–4 (first
|
||||
dispatch, committed at c9a84b3): the FIXED-FIRST alloc-guard baseline
|
||||
pin, the de-globalised `ailang_ctx_t` runtime (per-thread TLS slot +
|
||||
conditional accounting, `g_rc_*`+atexit retained verbatim as the
|
||||
null-ctx fallback), the codegen forwarder gaining a leading
|
||||
`ptr %ctx` + `@__ail_tls_ctx` save/store/restore around the
|
||||
byte-unchanged internal call, and the CLI RC-only guard. Tasks 5–9
|
||||
(this re-dispatch): the per-thread-ctx scalar-swarm capability demo
|
||||
(`swarm.c`, no SHARED_CTX, GREEN), the de-globalisation
|
||||
negative-control standing test in the rc-accounting harness
|
||||
(`rc_accounting_shared_ctx_is_flagged_by_tsan` — shared-ctx genuinely
|
||||
raced under tsan, teeth proven), the M1 `host.c` migration to the ctx
|
||||
ABI (`s == 25` holds through the ctx-threaded forwarder), the
|
||||
DESIGN.md current-state update (provisional-until-M3 narrowed to
|
||||
value/record layout; Decision-10 per-thread-ctx note; pinned
|
||||
"Export parameters are written **bare**…" sentence + `(con Int)`
|
||||
snippet preserved verbatim), and the full regression + bench gate
|
||||
(workspace 0 failed; bench-trio causally exonerated). The milestone's
|
||||
concurrency-safety invariant is sanitiser-verified.
|
||||
|
||||
## Boss spec-defect repair (2026-05-18)
|
||||
|
||||
The first dispatch (Tasks 1–4 clean) correctly **BLOCKED on Task 5**,
|
||||
surfacing a genuine spec defect: the original Task 5 paired a
|
||||
`-DSHARED_CTX` negative control onto `swarm.c`. That is structurally
|
||||
impossible — `examples/embed_backtest_step.ail` is a non-allocating
|
||||
scalar kernel (`state += sample*sample`); it never calls
|
||||
`ailang_rc_alloc`/`ailang_rc_dec`, never writes a `ctx` field, and
|
||||
`@__ail_tls_ctx` is `__thread` (per-thread, never shared even when the
|
||||
`ailang_ctx_t*` value is passed to a shared ctx). A shared-ctx scalar
|
||||
swarm therefore has no shared-memory write to race on; tsan correctly
|
||||
stays clean. Asserting a structurally-unreachable race would have been
|
||||
a vacuous (and dishonest) test. The Boss adjudicated: the
|
||||
de-globalisation negative-control teeth belong to the **item-1
|
||||
rc-accounting harness** (`rc_accounting_tsan.c -DSHARED_CTX`, where a
|
||||
shared ctx genuinely races on `ctx->alloc_count`), NOT `swarm.c`. The
|
||||
spec was amended in lockstep and the plan's Task 5 restructured:
|
||||
`swarm.c` is the per-thread-ctx capability demo ONLY (one green
|
||||
positive test); the negative control became
|
||||
`rc_accounting_shared_ctx_is_flagged_by_tsan` added to the committed
|
||||
`embed_rc_accounting_tsan.rs`. This re-dispatch implemented the
|
||||
corrected Task 5 — no swarm.c negative control reintroduced. The
|
||||
plan's Task 3 expected-string transcription error (recorded below)
|
||||
was likewise Boss-corrected (`@ail_embed_backtest_step_step`, the
|
||||
module-qualified convention-correct symbol).
|
||||
|
||||
## Per-task notes
|
||||
|
||||
- iter embedding-abi-m2.1.1: FIXED-FIRST alloc-guard pin. New
|
||||
`crates/ail/tests/embed_staticlib_alloc_guard.rs` (verbatim from
|
||||
plan); RED captured (build currently succeeds), the deliverable.
|
||||
- iter embedding-abi-m2.1.2: `runtime/rc.c` gains `ailang_ctx_t`
|
||||
{alloc_count, free_count} + `ailang_ctx_new`/`ailang_ctx_free` +
|
||||
`__thread __ail_tls_ctx`; the two increment sites become
|
||||
`if (_ctx) _ctx->… else g_rc_…`. `g_rc_*` statics + atexit +
|
||||
constructor retained verbatim. New `rc_accounting_tsan.c` +
|
||||
`embed_rc_accounting_tsan.rs`: RED (link error) → GREEN
|
||||
(per-ctx, 8×200000, tsan-clean).
|
||||
- iter embedding-abi-m2.1.3: codegen `Target::StaticLib` arm emits
|
||||
`@__ail_tls_ctx = external thread_local global ptr` once; forwarder
|
||||
signature gains leading `ptr %ctx`; body does load-save / store-ctx
|
||||
/ unchanged `call @ail_<mname>_<fn>(args)` / store-restore.
|
||||
`_adapter`/`_clos` + internal arg vector byte-untouched. Doc-comment
|
||||
narrowed to value/record-layout provisionality. `embed_e2e` left
|
||||
RED by design (Task 6 migrates it).
|
||||
- iter embedding-abi-m2.1.4: `crates/ail/src/main.rs build_staticlib`
|
||||
rejects `--alloc != Rc` after the has_export check, before lowering.
|
||||
Task-1 pin RED→GREEN; `embed_staticlib_cli` default path unaffected.
|
||||
- iter embedding-abi-m2.1.5: `swarm.c` + `embed_swarm_tsan.rs`
|
||||
written verbatim. `scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle`
|
||||
PASSES (capability proven). `shared_ctx_negative_control_is_flagged_by_tsan`
|
||||
FAILS structurally — see Blocked detail.
|
||||
- iter embedding-abi-m2.1.6–9: not run (Task 5 BLOCKED; downstream
|
||||
resequencing is a Boss decision).
|
||||
- iter embedding-abi-m2.1.1 (first dispatch, committed): FIXED-FIRST
|
||||
alloc-guard pin. New `crates/ail/tests/embed_staticlib_alloc_guard.rs`
|
||||
(verbatim from plan); RED captured (build currently succeeds), the
|
||||
deliverable. RED→GREEN across the iter (Task 4 closes it).
|
||||
- iter embedding-abi-m2.1.2 (first dispatch, committed): `runtime/rc.c`
|
||||
gains `ailang_ctx_t` {alloc_count, free_count} + `ailang_ctx_new`/
|
||||
`ailang_ctx_free` + `__thread __ail_tls_ctx`; the two increment
|
||||
sites become `if (_ctx) _ctx->… else g_rc_…`. `g_rc_*` statics +
|
||||
atexit + constructor retained verbatim. New `rc_accounting_tsan.c` +
|
||||
`embed_rc_accounting_tsan.rs`: RED (link error) → GREEN (per-ctx,
|
||||
8×200000, tsan-clean).
|
||||
- iter embedding-abi-m2.1.3 (first dispatch, committed): codegen
|
||||
`Target::StaticLib` arm emits `@__ail_tls_ctx = external
|
||||
thread_local global ptr` once; forwarder signature gains leading
|
||||
`ptr %ctx`; body does load-save / store-ctx / unchanged
|
||||
`call @ail_<mname>_<fn>(args)` / store-restore. `_adapter`/`_clos`
|
||||
+ internal arg vector byte-untouched. Doc-comment narrowed to
|
||||
value/record-layout provisionality. `embed_e2e` left RED by design
|
||||
(Task 6 migrates it).
|
||||
- iter embedding-abi-m2.1.4 (first dispatch, committed):
|
||||
`crates/ail/src/main.rs build_staticlib` rejects `--alloc != Rc`
|
||||
after the has_export check, before lowering. Task-1 pin RED→GREEN;
|
||||
`embed_staticlib_cli` default path unaffected.
|
||||
- iter embedding-abi-m2.1.5 (this re-dispatch): per-thread-ctx
|
||||
capability demo. New `crates/ail/tests/embed/swarm.c` (no
|
||||
SHARED_CTX) + `crates/ail/tests/embed_swarm_tsan.rs`;
|
||||
`scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle` GREEN
|
||||
(8 threads × 200k, tsan-clean, every result == serial oracle).
|
||||
De-globalisation negative control
|
||||
`rc_accounting_shared_ctx_is_flagged_by_tsan` appended to the
|
||||
committed `embed_rc_accounting_tsan.rs` (reuses its `ws_root()`/
|
||||
`cc()` helpers); GREEN — shared-ctx build genuinely raced under
|
||||
tsan (teeth proven, not vacuous). No swarm.c negative control
|
||||
reintroduced (the Boss spec-defect repair).
|
||||
- iter embedding-abi-m2.1.6 (this re-dispatch): `crates/ail/tests/
|
||||
embed/host.c` replaced with the ctx-ABI version (opaque
|
||||
`ailang_ctx_t`, `ailang_ctx_new`/`_free` lifecycle, ctx-prefixed
|
||||
`backtest_step`). Confirmed expected RED post-Task-3 first
|
||||
(`s != 25` from the garbage-ctx arg shift). `embed_e2e.rs`
|
||||
intentionally NOT modified: the M1 harness already links
|
||||
`libailang_rt.a` by absolute path (`.arg(outdir.join(
|
||||
"libailang_rt.a"))`), so the ctx symbols resolve without an
|
||||
`-lailang_rt` add — the task block's own "no change is needed
|
||||
beyond Step 2" conditional branch. GREEN, `s == 25` holds.
|
||||
- iter embedding-abi-m2.1.7 (this re-dispatch): `docs/DESIGN.md` —
|
||||
provisional-until-M3 sentence (~:2282) replaced with the M2 ctx
|
||||
prose (mandatory leading `ailang_ctx_t*`, per-thread, RC-only
|
||||
swarm artefact, value/record layout still provisional);
|
||||
Decision-10 atomicity bullet (~:1528) gains the per-thread-ctx
|
||||
soundness note. Pinned "Export parameters are written **bare**…"
|
||||
sentence + canonical `(con Int)` snippet preserved verbatim (the
|
||||
edit ends before them; no soft-wrap split risk). `docs_honesty_pin`
|
||||
GREEN unmodified (5 passed), `design_schema_drift` GREEN (8
|
||||
passed) — edits outside the `## Data model` scan window.
|
||||
- iter embedding-abi-m2.1.8 (this re-dispatch): regression gate, no
|
||||
code. `print_no_leak_pin` (1) + `e2e -- rc_stats` (4) GREEN —
|
||||
null-ctx fallback prints unchanged. `embed_export_hash_stable`
|
||||
(1, `fn_without_export_hash_is_unchanged`) + `embed_export_gate`
|
||||
(6, all pass) GREEN — no schema field, export gate unchanged.
|
||||
Full `cargo test --workspace`: every suite ok, 0 failing suites.
|
||||
- iter embedding-abi-m2.1.9 (this re-dispatch): bench gate, no code.
|
||||
`compile_check.py` exit=0 (24/24 stable); `cross_lang.py` exit=0
|
||||
(25/25 stable); `check.py` exit=1 on exactly 4 tracked-P2 noise
|
||||
metrics (`bench_list_sum.bump_s` +16.53%,
|
||||
`latency.explicit_at_rc.max_us` +40.41%,
|
||||
`latency.implicit_at_rc.p99_9_us` +31.66%,
|
||||
`latency.implicit_at_rc.max_us` +92.35%). Causally exonerated by
|
||||
the source-level invariant (see Concerns); no baseline ratified.
|
||||
|
||||
## Concerns
|
||||
|
||||
- iter embedding-abi-m2.1.3: PLAN TRANSCRIPTION ERROR. Task 3 Step 1's
|
||||
plan code block asserts
|
||||
- iter embedding-abi-m2.1.3 (first dispatch — carried forward):
|
||||
PLAN TRANSCRIPTION ERROR. Task 3 Step 1's plan code block asserted
|
||||
`ir.contains("call i64 @ail_backtest_step(i64 %a0, i64 %a1)")`.
|
||||
The internal symbol is `@ail_embed_backtest_step_step`
|
||||
(module-qualified `@ail_<mname>_<fn>`), which the plan's own Step-4
|
||||
parenthetical and Boss constraint 3 require to stay byte-unchanged.
|
||||
`@ail_backtest_step` is not a substring of the actual emission, so
|
||||
the verbatim assertion would fail even with a correct implementation,
|
||||
contradicting the plan's own invariant. Written instead with the
|
||||
convention-correct symbol (`@ail_embed_backtest_step_step`), which
|
||||
the pre-existing line-30 assertion in the same file already uses.
|
||||
Recorded, not silently substituted. The plan file should be
|
||||
corrected if re-run.
|
||||
- iter embedding-abi-m2.1.3: removing the now-dead `let params` vector
|
||||
binding in the StaticLib arm was strictly required for the requested
|
||||
Step-4 change to compile without an unused-variable warning / dead
|
||||
vector construction; not an unrequested scope extra.
|
||||
Written instead with the convention-correct symbol (Boss-corrected
|
||||
in the re-dispatched plan). The plan file should remain corrected.
|
||||
- iter embedding-abi-m2.1.6: `embed_e2e.rs` is in the task's `Files:`
|
||||
block but was intentionally left unchanged — the M1 harness already
|
||||
links `libailang_rt.a` by absolute path, so the ctx symbols resolve
|
||||
without an `-lailang_rt` add. This is the task block's own sanctioned
|
||||
"no change is needed beyond Step 2" conditional branch, not a missed
|
||||
requirement (observation, not correctness).
|
||||
- iter embedding-abi-m2.1.7: the section header is still
|
||||
`## Embedding ABI (M1)` while the body now describes the M2 ctx ABI
|
||||
as current state — a header/content honesty mismatch. NOT fixed:
|
||||
renaming the header is outside the task block's named edit regions
|
||||
(`:2282–2285`, `:1528–1529`) and could perturb a doc-honesty pin
|
||||
tracking the `(M1)` token; the controller curates scope, not the
|
||||
implementer. Routed here for Boss adjudication — a candidate
|
||||
follow-up (header rename + fieldtest/pin audit) but explicitly NOT
|
||||
in this iter's plan scope.
|
||||
- iter embedding-abi-m2.1.8: the task block expected
|
||||
`embed_export_gate` to be "8 passed"; the suite at HEAD c9a84b3 has
|
||||
exactly 6 tests, all passing, 0 filtered. The literal "8" is a
|
||||
plan-transcription artefact (pre-existing — M2 added/removed no test
|
||||
in this suite). The protected invariant (export gate unchanged by
|
||||
M2) holds unambiguously; the implementer correctly did NOT pad the
|
||||
suite to 8 (that would fabricate coverage). Plan number vs reality,
|
||||
not a regression.
|
||||
- iter embedding-abi-m2.1.9: `check.py` exit=1 on 4 metrics, all in
|
||||
the tracked-P2 noise families (`*.bump_s`, `latency.*.max_us`,
|
||||
`latency.*.p99_9_us`). CAUSALLY EXONERATED by a source-level
|
||||
invariant stronger than the plan's binary `cmp`: this re-dispatch's
|
||||
entire working-tree footprint is test fixtures + test drivers +
|
||||
`docs/DESIGN.md` — ZERO files under `crates/*/src/` or `runtime/`.
|
||||
The `ail` codegen binary and the linked `rc.c`/`str.c` runtime are
|
||||
byte-identical to HEAD c9a84b3 by construction, so the firing
|
||||
metrics cannot be caused by this iter. The plan's `git stash`/
|
||||
`git stash pop` recipe was deliberately NOT run: on a re-dispatch
|
||||
it would discard the iter's uncommitted Tasks 5–8 work and violate
|
||||
the working-tree-as-handoff contract. No baseline ratified
|
||||
(consistent with roadmap-P2 noise policy + the 2026-05-14 audit-pd
|
||||
"baseline pristine, Nth consecutive observation" envelope).
|
||||
|
||||
## Known debt
|
||||
|
||||
- Task 5 `swarm.c` shared-ctx negative control: no race surface for a
|
||||
non-allocating scalar kernel. The meaningful de-globalisation
|
||||
negative control (a genuine tsan race on `ctx->alloc_count`) already
|
||||
exists with teeth in Task 2's `rc_accounting_tsan.c -DSHARED_CTX`
|
||||
(validated: races at `rc.c` `ailang_rc_alloc`).
|
||||
- `## Embedding ABI (M1)` section header in DESIGN.md still says
|
||||
"(M1)" though its body is now M2 current-state. Out of this iter's
|
||||
plan scope (Task 7 named only `:2282–2285` and `:1528–1529`).
|
||||
Candidate follow-up: header rename with a doc-honesty-pin audit
|
||||
for any `(M1)` token dependency. Not touched to keep the diff
|
||||
scope-compliant and avoid perturbing a pin.
|
||||
|
||||
## Blocked detail
|
||||
|
||||
Task: 5
|
||||
Reason: spec-ambiguous (plan-design contradiction at task level)
|
||||
Worker's verbatim finding: Task 5's `shared_ctx_negative_control_is_flagged_by_tsan`
|
||||
asserts that sharing one `ailang_ctx_t*` across 8 threads driving
|
||||
`backtest_step` makes tsan report a race. It does not, and cannot:
|
||||
`examples/embed_backtest_step.ail` is `state += sample*sample` — a
|
||||
non-allocating scalar kernel. It never calls `ailang_rc_alloc`/
|
||||
`ailang_rc_dec`, so no `ctx->alloc_count`/`free_count` field is ever
|
||||
written by any thread. The forwarder's TLS transport uses
|
||||
`@__ail_tls_ctx`, a `__thread` global — per-thread storage that is
|
||||
never shared across threads even when the `ailang_ctx_t*` value is
|
||||
passed to a shared ctx. There is therefore no shared-memory write to
|
||||
race on. `swarm_neg` runs clean, exits 0, prints `swarm: ok (3500000)`.
|
||||
This is structural: the chosen M2 scalar kernel cannot exhibit the
|
||||
asserted behaviour. The implementer-faithful diff is correct; the
|
||||
plan's premise for this one test is wrong. The real
|
||||
de-globalisation race surface (concurrent `ctx->alloc_count++`) is the
|
||||
rc primitives, which `swarm.c` never calls directly — that surface IS
|
||||
covered with teeth by Task 2's `rc_accounting_tsan.c -DSHARED_CTX`
|
||||
(independently confirmed to race at `rc.c` in `ailang_rc_alloc`,
|
||||
tsan exit 66). Weakening the swarm negative control to make it pass
|
||||
is forbidden (voids the coherent-stop proof; Boss constraint 8).
|
||||
Suggested next step: Boss decision — either (a) drop
|
||||
`shared_ctx_negative_control_is_flagged_by_tsan` from Task 5 (the
|
||||
de-globalisation negative control is Task 2's job by the plan's own
|
||||
"distinct spec role" split; swarm.c is the capability demo only —
|
||||
keep only the per-ctx positive test, which passes), or (b) re-spec
|
||||
Task 5's negative control to exercise an *allocating* exported kernel
|
||||
so the shared ctx genuinely races (requires a new fixture + spec
|
||||
amendment via brainstorm, since M2's scope is scalar-only). Option (a)
|
||||
preserves the plan's own item-1-vs-item-2/3 separation and ships the
|
||||
already-green capability proof.
|
||||
None. All 9 tasks completed (Tasks 1–4 committed at c9a84b3 in the
|
||||
first dispatch; Tasks 5–9 in this re-dispatch, all reaching
|
||||
`approved` quality with zero review re-loops). The first dispatch's
|
||||
Task-5 BLOCK was a genuine spec defect, Boss-adjudicated and repaired
|
||||
before this re-dispatch (see "Boss spec-defect repair").
|
||||
|
||||
## Files touched
|
||||
## Files touched (this re-dispatch — Tasks 5–9 working tree)
|
||||
|
||||
Modified:
|
||||
- `runtime/rc.c` (Task 2: ctx struct + lifecycle + TLS + accounting split)
|
||||
- `crates/ailang-codegen/src/lib.rs` (Task 3: forwarder + doc)
|
||||
- `crates/ailang-codegen/tests/embed_staticlib_lowering.rs` (Task 3: IR pin)
|
||||
- `crates/ail/src/main.rs` (Task 4: RC-only guard)
|
||||
- `crates/ail/tests/embed/host.c` (Task 6: ctx-ABI migration)
|
||||
- `crates/ail/tests/embed_rc_accounting_tsan.rs` (Task 5: +
|
||||
`rc_accounting_shared_ctx_is_flagged_by_tsan` negative control)
|
||||
- `docs/DESIGN.md` (Task 7: M2 current-state + Decision-10 note)
|
||||
|
||||
Created:
|
||||
- `crates/ail/tests/embed_staticlib_alloc_guard.rs` (Task 1)
|
||||
- `crates/ail/tests/embed/rc_accounting_tsan.c` (Task 2)
|
||||
- `crates/ail/tests/embed_rc_accounting_tsan.rs` (Task 2)
|
||||
- `crates/ail/tests/embed/swarm.c` (Task 5)
|
||||
- `crates/ail/tests/embed_swarm_tsan.rs` (Task 5)
|
||||
- `crates/ail/tests/embed/swarm.c` (Task 5: per-thread-ctx
|
||||
capability demo, no SHARED_CTX)
|
||||
- `crates/ail/tests/embed_swarm_tsan.rs` (Task 5: one green
|
||||
positive test)
|
||||
|
||||
(Tasks 1–4's files — `embed_staticlib_alloc_guard.rs`, `rc.c`,
|
||||
codegen `lib.rs`, `embed_staticlib_lowering.rs`, `main.rs`,
|
||||
`rc_accounting_tsan.c`, the Task-2 `embed_rc_accounting_tsan.rs`
|
||||
base — are already committed at c9a84b3.)
|
||||
|
||||
## Stats
|
||||
|
||||
|
||||
@@ -98,3 +98,4 @@
|
||||
- 2026-05-18 — fieldtest embedding-abi-m1 (milestone CLOSE, surface-touch — thesis substantiated, 3 non-blocking follow-ups routed): post-audit downstream-LLM-author field test of M1's `(export "<sym>")` + `ail build --emit=staticlib` + scalar/effect-free gate, DESIGN.md + public examples only (never compiler source). 4 fresh programs: Int fixed-point EMA `(State,Sample)->State` fold + Float leaky integrator (both author→`--emit=staticlib`→C-host link→typed scalar return, `s==67`/`s==1.875`, exit 0 — **clause-1 confirmed first-try**), IntList-param export (correctly rejected `export-non-scalar-signature`), `!IO` scalar-clean export (correctly rejected `export-has-effects`) — **clause-3 confirmed, both diagnostics precise+self-correcting**. **0 bugs**; the M1 capability + gate are sound and the milestone thesis ("an LLM author makes a scalar fold callable") is empirically substantiated. 3 working + 1 friction + 2 spec_gap. The friction + spec_gap#1 share a root: `crates/ailang-core/specs/form_a.md` "Schema invariants" item 1 + Pitfalls state an *unconditional* "every fn param MUST be `(own/borrow T)`" but scalars require **bare** `(con Int)` (`(own (con Int))`→`use-after-consume`, `(borrow)`→`consume-while-borrowed`); the doc the LLM reads first misdirects M1's headline task into a body-pointing linearity diagnostic — a **pre-existing form_a.md docs-honesty defect M1 made acute, not introduced** (the positive examples only succeeded because the fieldtester imitated the public `embed_*` corpus over the form_a.md prose rule). spec_gap#2: no public `emit-ir --emit=staticlib` though Decision 5 makes kernel-IR readability load-bearing. Boss independently re-verified via the public CLI (positive E2E builds both archives; both rejections fire the documented codes). Orchestrator routing (own judgement, not the fieldtester's recommended-action column): friction+spec_gap#1 → ONE P1 `[todo]` docs-honesty tidy (form_a.md scalar-param carve-out symmetric with the existing return-type carve-out + DESIGN.md mirror; behaviour settled → tidy, no brainstorm; ahead of M2 because it undermines the clause-1 ergonomics of the surface M2–M5 extend); spec_gap#2 → P1 `[feature]` add `--emit=staticlib` to `ail emit-ir` (restore the affordance, NOT narrow DESIGN.md). None are bugs (no debug); none M1-blocking. **embedding-abi-m1 fully ratified and CLOSED**: spec (grounding-check PASS) + plan (Boss-Repaired) + iter (`818177d` partial+Repair / `e406d07` DONE) + audit `425c4eb` CLEAN + fieldtest thesis-substantiated; roadmap P1 `[~]`→`[x]`, 2 follow-ups added P1-ahead-of-M2. Next *milestone* is Embedding ABI — M2 (no spec) = a `/boss` new-milestone bounce-back (not auto-started); the 2 P1 follow-ups are autonomous-eligible tidies/feature but the session is context-deep — surfaced to the user for the session-shape/next-item call. → 2026-05-18-fieldtest-embedding-abi-m1.md
|
||||
- 2026-05-18 — iter form-a-scalar-param-mode-carveout (M1-fieldtest follow-up #1, docs-honesty tidy in the docs-honesty-lint class, DONE): resolved the M1 fieldtest `[friction]` + `[spec_gap]#1` shared root. `crates/ailang-core/specs/form_a.md` stated an *unconditional* "every `(fn ...)` param MUST carry an `(own/borrow)` mode" rule in four places (`### Function` prose L97, grammar-block comment L230, "Schema invariants" item 1 L347, Pitfalls bullet L382) that contradicts shipped checker behaviour — scalar `Int`/`Bool`/`Unit`/`Str` params take **and require** bare `(con Int)` (a mode on a scalar makes the linearity pass hold the primitive to linear discipline → body-pointing `use-after-consume`/`consume-while-borrowed`, the exact fieldtest misdirection). All four sites rewritten symmetric to the pre-existing return-type carve-out; site 5 (L521 few-shot annotation) already correct, left verbatim by design (carve-out reuses its heap-shaped/primitive vocabulary for end-to-end internal consistency). `docs/DESIGN.md` §"Embedding ABI (M1)" gained the bare-scalar export-param rule + a corpus-grounded `step` Form-A snippet (byte-identical to `examples/embed_backtest_step.ail:3-11`). RED-first anti-regrowth pin `form_a_scalar_param_carveout_present_and_old_rule_absent` in `crates/ailang-core/tests/docs_honesty_pin.rs` (reads the canonical `ailang_core::FORM_A_SPEC` `include_str!` const — single-source, compile-checked — + `read("docs/DESIGN.md")`; `norm()` whitespace-collapse structurally discharges the grep/contains line-wrap family; 4 ABSENT + 4 PRESENT form_a + 1 PRESENT DESIGN). Boss scope calls: 4 form_a sites not 2 (internal-consistency, on the merits — a tidy whose thesis is "consistent current-state mirror" cannot fix some and leave others contradicting); pin idiom = `FORM_A_SPEC` const (semantic single-source, not effort). `spec_drift.rs` recon-confirmed NOT a lockstep partner (anchors are short keyword tokens; `(own`/`(borrow` survive an additive carve-out). Zero language/checker/codegen change by construction; independent Boss verification: docs_honesty_pin 5/0, spec_drift 8/8, ailang-core 112/0, workspace 622→623 (+1 = the pin), zero `crates/**/src/**` diff. spec carrier `docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md` + roadmap P1 entry → plan `docs/plans/form-a-scalar-param-mode-carveout.md` (`4c266a6`). Pure docs+pin tidy — no audit/fieldtest gate (zero authoring-behaviour change; the pin IS the regression coverage). → 2026-05-18-iter-form-a-scalar-param-mode-carveout.md
|
||||
- 2026-05-18 — iter emit-ir-staticlib (M1-fieldtest follow-up #2, scoped [feature], DONE): resolved M1 fieldtest [spec_gap]#2 — `ail emit-ir` had no `--emit=staticlib` (only `ail build` did) and on a `main`-free kernel hit the executable-path `MissingEntryMain` rejection, so an author could not read the generated `@<sym>` forwarder for an exported kernel — the exact Decision-5 IR-readability affordance, for the exact artefact M1 introduced. Added a one-line symmetric codegen convenience `lower_workspace_staticlib(ws)` (mirrors `lower_workspace`: `--emit=exe`↔`lower_workspace`, `--emit=staticlib`↔`lower_workspace_staticlib`; delegates to the M1-audited unchanged `Target::StaticLib` forwarder path), an `emit: String` clap field on `Cmd::EmitIr` symmetric with `Cmd::Build`'s, and a zero-export guard byte-identical to `build_staticlib`'s (so the error is symmetric across both subcommands and the existing `embed_staticlib_cli.rs` substring assertion holds for both). Recon resolved the only integration risk negative (both codegen entrypoints return `Result<String>`, the emit-ir printer already consumes `String` — no adapter). DESIGN.md *widened* not narrowed (roadmap resolution honoured): a present-tense affordance sentence in §"Embedding ABI (M1)" + a CLI-synopsis correction that also discharges a pre-existing M1 omission (`ail build --emit=staticlib` was never in the synopsis). Boss editorial calls: synopsis fixes BOTH lines (docs-as-current-state-mirror consistency, on the merits); NO new docs pin (the E2E pins behaviour; the architect's mandatory DESIGN.md read at milestone close catches stale prose — pinning every feature sentence is noise); Decision-5 prose left untouched (already present-tense correct). New E2E `crates/ail/tests/emit_ir_staticlib_cli.rs` (3 tests: positive — IR contains external `@backtest_step(` + internal `@ail_embed_backtest_step_step`, NOT `@main(`, NOT `has no main def`; zero-export guard symmetric with build's, reusing the identical `embed_noentry_baseline.ail` fixture; default-exe regression — `--emit` defaults to `exe`, a `main`-free kernel without the flag still hits `MissingEntryMain`, so the new branch cannot silently reroute the default path). RED-first observed exactly ("1 passed; 2 failed" pre-edit — the default-exe test passes because that IS the spec_gap behaviour). Independent Boss verification: the 3 new tests 3/0, `embed_staticlib_cli` 2/0 (build-side untouched), `docs_honesty_pin` 5/0 (no regression), `ail` suite 186/0, workspace 623→626 (+3 = exactly the new tests), zero diff outside the 4 in-scope paths, no fixture minted. Functional spot-check from the user-facing CLI: `ail emit-ir examples/embed_backtest_step.ail --emit=staticlib` emits `define i64 @backtest_step(...)` (the readable external forwarder) + `@ail_embed_backtest_step_step` (internal), no `@main` — the affordance is genuinely delivered. spec carrier `docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md` [spec_gap]#2 + roadmap P1 entry → plan `docs/plans/emit-ir-staticlib.md` (`03493c9`) → iter this commit. Scoped feature, no audit/fieldtest gate (the E2E is the coverage; no authoring-surface or invariant change — reuses the M1-audited codegen path). → 2026-05-18-iter-emit-ir-staticlib.md
|
||||
- 2026-05-18 — iter embedding-abi-m2.1 (Embedding ABI — M2, DONE 9/9 across one Boss-repaired split dispatch): per-thread runtime context + concurrency safety. No authoring-surface change (the `.ail` is byte-identical to M1); the deliverable is a swarm-safe generated C ABI + de-globalised runtime, sanitiser-verified. Shipped: `runtime/rc.c` gains `ailang_ctx_t {alloc_count,free_count}` + `ailang_ctx_new`/`_free` + `__thread __ail_tls_ctx`, the two increment sites become `if (_ctx) _ctx->… else g_rc_…` (the `g_rc_*` statics + `ailang_rc_stats_atexit` + constructor RETAINED VERBATIM as the null-ctx single-threaded executable fallback — `print_no_leak_pin`/`e2e` rc_stats stay green unmodified); codegen `Target::StaticLib` forwarder gains a mandatory leading `ptr %ctx` + one `@__ail_tls_ctx = external thread_local global ptr` decl + TLS save/store/restore around the BYTE-UNCHANGED internal `@ail_<mod>_<fn>` call (`_adapter`/`_clos` + internal arg vector untouched — M1 decision held; the frozen-at-M3 surface is the C `@<sym>(ctx,…)` signature, internal convention free); `build_staticlib` rejects `--alloc != rc` (RC-only swarm artefact, no shared Boehm collector by construction; default already rc; P2 Boehm-retirement untouched); DESIGN.md §"Embedding ABI (M1)" updated to post-M2 current state (provisional-until-M3 narrowed to the value/record layout; Decision-10 per-thread-ctx atomicity note) with the docs_honesty-pinned "Export parameters are written **bare**…" sentence + `(con Int)` snippet preserved verbatim; M1 `host.c`/`embed_e2e` migrated to the ctx ABI (`s==25` holds). Coherent stop sanitiser-verified by the Boss directly (not inferred): per-thread-ctx scalar swarm `-fsanitize=thread`-clean with every thread == serial oracle (capability demo); direct rc-accounting per-ctx exit 0 / 0 tsan warnings (de-globalisation positive); shared-ctx negative control a genuine `ThreadSanitizer: data race` at `rc.c:157` (`_ctx->alloc_count++` in `ailang_rc_alloc`) + `rc.c:208` (`_ctx->free_count++` in `ailang_rc_dec`), exit 66 — teeth non-vacuous, precisely targeting the de-globalised counters. Process note: the first dispatch (Tasks 1–4 clean, committed `c9a84b3` as the known-good subset) correctly BLOCKED on Task 5 having surfaced a genuine spec defect — the original Task 5 paired a `-DSHARED_CTX` negative control onto `swarm.c`, structurally impossible because a non-allocating scalar kernel writes no ctx field and `__ail_tls_ctx` is `__thread` (the spec's OWN item-1 honesty point). Boss adjudication (not a brainstorm bounce — a consistency-repair of an internally-contradictory clause whose intent is already realised by item 1): spec amended in lockstep (Goal coherent-stop, must-fail-axis item 2, Testing item 3, Acceptance) so the negative-control teeth are item-1's by the de-globalisation-proof / capability-demo split; plan Task 5 restructured (`swarm.c` per-ctx capability demo only; negative control relocated into the item-1 `rc_accounting` harness driver) + Task-3 plan-transcription error corrected (`@ail_backtest_step`→`@ail_embed_backtest_step_step`); re-dispatch `[5,9]` DONE. spec `docs/specs/2026-05-18-embedding-abi-m2.md` (user-approved, grounding-check PASS 9/9, `1c58055`) → plan `docs/plans/embedding-abi-m2.1.md` (`b3388c8`, Boss-corrected) → iter `c9a84b3` (PARTIAL 4/9 + Boss repair) + this commit (DONE 5–9). Known debt routed: DESIGN.md `## Embedding ABI (M1)` section header still says "(M1)" while the body now mirrors M2 — out of Task 7's scope-limited edit regions by design (preserve the docs_honesty_pin), a post-audit doc-honesty tidy candidate. Milestone-close `audit` next. → 2026-05-18-iter-embedding-abi-m2.1.md
|
||||
|
||||
Reference in New Issue
Block a user