iter embedding-abi-m2.1 (PARTIAL 4/9 + Boss spec-defect repair): ctx ABI + de-globalisation
Tasks 1-4 land fully review-green and are the cohesive shippable
subset (the per-thread embedding ABI, fully wired + proven):
- T1: FIXED-FIRST alloc-guard baseline pin (RED captured -> GREEN at T4).
- T2: 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_...'. g_rc_* statics +
ailang_rc_stats_atexit + the constructor RETAINED VERBATIM as the
null-ctx (single-threaded executable) fallback. rc_accounting_tsan.c
+ driver: per-ctx 8x200000 tsan-clean (de-globalisation positive proof).
- T3: codegen Target::StaticLib forwarder gains a leading 'ptr %ctx'
+ one '@__ail_tls_ctx = external thread_local global ptr' decl +
TLS save/store/restore around the BYTE-UNCHANGED internal call;
_adapter/_clos + internal arg vector untouched (M1 decision held);
doc-comment provisionality narrowed to the value/record layout.
- T4: build_staticlib rejects --alloc != rc (RC-only swarm artefact).
Boss adjudication of the orchestrator's Task-5 BLOCKED (spec-defect,
correctly surfaced not hacked): swarm.c's -DSHARED_CTX negative
control is structurally impossible — examples/embed_backtest_step.ail
is a non-allocating scalar kernel that never writes a ctx field, and
__ail_tls_ctx is __thread, so a shared-ctx scalar swarm has no
shared-memory write to race on (the spec's OWN item-1 honesty point).
The de-globalisation teeth belong to the item-1 rc_accounting harness
(shared ctx genuinely races on ctx->alloc_count; orchestrator
independently confirmed tsan exit 66). Spec amended in lockstep
(Goal coherent-stop, must-fail-axis item 2, Testing item 3,
Acceptance) so item 3's negative control is item-1's by the
de-globalisation-proof / capability-demo split; plan Task 5
restructured (swarm.c per-ctx capability demo only; negative-control
standing test relocated into the item-1 harness driver) + Task 3's
plan-transcription error (@ail_backtest_step ->
@ail_embed_backtest_step_step) corrected. This is a Boss
consistency-repair of an internally-contradictory clause whose intent
is already correctly realised in the same spec — not a redesign; no
brainstorm bounce. Task-5 working files discarded (corrected plan
reproduces them; a structurally-RED test must not enter main).
INDEX.md + final journal land at iter completion (re-dispatch [5,9]).
This commit is contained in:
@@ -25,8 +25,9 @@
|
||||
- Modify: `crates/ail/tests/embed/host.c` — migrated to the ctx ABI (M1 value oracle, single-threaded).
|
||||
- Modify: `crates/ail/tests/embed_e2e.rs:17–46` — `c_host_calls_exported_scalar_kernel` migrated to drive the ctx-ABI `host.c`.
|
||||
- Create: `crates/ail/tests/embed/rc_accounting_tsan.c` — direct `ailang_rc_alloc`/`ailang_rc_dec`+`ailang_ctx_*` N-thread harness (links `libailang_rt.a` only; the de-globalisation teeth — item 1).
|
||||
- Create: `crates/ail/tests/embed/swarm.c` — N-pthread scalar-kernel swarm; per-thread-ctx mode + `-DSHARED_CTX` negative control (items 2, 3).
|
||||
- Create: `crates/ail/tests/embed_swarm_tsan.rs` — driver: builds the staticlib + the two new C harnesses under `-fsanitize=thread`, asserts the matrix.
|
||||
- Create: `crates/ail/tests/embed/swarm.c` — N-pthread scalar-kernel swarm, per-thread-ctx capability demo ONLY (no `SHARED_CTX`; a non-allocating scalar kernel cannot race even under a shared ctx — item 2).
|
||||
- Create: `crates/ail/tests/embed_swarm_tsan.rs` — driver: builds the staticlib, links `swarm.c` under `-fsanitize=thread`, asserts the per-ctx positive (item 2).
|
||||
- Modify: `crates/ail/tests/embed_rc_accounting_tsan.rs` (Task 5 Step 3) — add the `-DSHARED_CTX` de-globalisation negative-control standing test (item 3, in Task 2's rc-accounting harness where a shared ctx genuinely races).
|
||||
- Create: `crates/ail/tests/embed_staticlib_alloc_guard.rs` — RED-first pin: `--emit=staticlib --alloc=gc|bump` rejected (Task 1).
|
||||
- Test (regression, unmodified): `crates/ail/tests/print_no_leak_pin.rs`, `crates/ail/tests/e2e.rs` (leak-stat helper), `crates/ailang-core/tests/embed_export_hash_stable.rs`, `crates/ailang-core/tests/design_schema_drift.rs`, `crates/ailang-check/tests/embed_export_gate.rs`, `crates/ailang-core/tests/docs_honesty_pin.rs`.
|
||||
|
||||
@@ -325,7 +326,7 @@ In `crates/ailang-codegen/tests/embed_staticlib_lowering.rs`, in `staticlib_emit
|
||||
"forwarder must take a leading ptr %ctx;\nIR:\n{ir}");
|
||||
assert!(ir.contains("store ptr %ctx, ptr @__ail_tls_ctx"),
|
||||
"forwarder must publish ctx into the TLS slot;\nIR:\n{ir}");
|
||||
assert!(ir.contains("call i64 @ail_backtest_step(i64 %a0, i64 %a1)"),
|
||||
assert!(ir.contains("call i64 @ail_embed_backtest_step_step(i64 %a0, i64 %a1)"),
|
||||
"internal call must stay byte-unchanged (no ctx arg);\nIR:\n{ir}");
|
||||
```
|
||||
|
||||
@@ -434,27 +435,47 @@ two-archive build path unaffected by the guard.
|
||||
|
||||
---
|
||||
|
||||
## Task 5: Scalar-swarm capability harness + negative control (items 2, 3)
|
||||
## Task 5: Scalar-swarm capability demo (per-thread-ctx) + de-globalisation negative-control standing test
|
||||
|
||||
Depends on Tasks 2+3 GREEN (ctx ABI present). Links **both** archives (kernel + runtime). Separate file from Task 2's harness — different link surface, distinct spec role (capability demo vs de-globalisation proof).
|
||||
> **Boss correction (2026-05-18, post-first-dispatch):** the original
|
||||
> Task 5 paired a `-DSHARED_CTX` negative control onto `swarm.c`. That
|
||||
> is structurally impossible and was the spec defect the first
|
||||
> implement dispatch correctly surfaced: `examples/embed_backtest_step.ail`
|
||||
> is a non-allocating scalar kernel — 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), so a shared-ctx scalar swarm has no
|
||||
> shared-memory write to race on and tsan correctly stays clean
|
||||
> (exactly the §Testing-item-1 honesty point). The negative control
|
||||
> belongs to the **item-1 direct rc-accounting harness**
|
||||
> (`rc_accounting_tsan.c`, which *does* write `ctx->alloc_count`
|
||||
> concurrently under a shared ctx — a genuine race). `swarm.c` is the
|
||||
> per-thread-ctx capability demo ONLY. Spec amended in lockstep
|
||||
> (§Goal coherent-stop, §must-fail-axis item 2, §Testing item 3,
|
||||
> §Acceptance).
|
||||
|
||||
Two deliverables: (5a) the per-thread-ctx scalar-swarm capability demo (`swarm.c`, links **both** archives); (5b) the de-globalisation negative-control standing test, added to Task 2's item-1 `rc_accounting_tsan.c` harness (which already carries the `#ifdef SHARED_CTX` block) so the teeth are a reproducible CI test, not a one-off manual check.
|
||||
|
||||
**Files:**
|
||||
- Create: `crates/ail/tests/embed/swarm.c`
|
||||
- Create: `crates/ail/tests/embed_swarm_tsan.rs`
|
||||
- Create: `crates/ail/tests/embed/swarm.c` (per-thread-ctx capability demo, no `SHARED_CTX`)
|
||||
- Create: `crates/ail/tests/embed_swarm_tsan.rs` (one green positive test)
|
||||
- Modify: `crates/ail/tests/embed_rc_accounting_tsan.rs` (Task 2's driver — add the `-DSHARED_CTX` negative-control standing test)
|
||||
|
||||
- [ ] **Step 1: Write the swarm harness C file**
|
||||
- [ ] **Step 1: Write the capability-demo swarm C file (per-thread-ctx only)**
|
||||
|
||||
Create `crates/ail/tests/embed/swarm.c`:
|
||||
|
||||
```c
|
||||
/* M2 items 2+3: scalar-kernel swarm. Per-thread-ctx (default) must be
|
||||
* tsan-clean and every thread's result must match the serial oracle.
|
||||
* Built -DSHARED_CTX = negative control: all threads share one ctx;
|
||||
* tsan MUST report a race (proves the clean result is not vacuous). */
|
||||
/* M2 item 2: scalar-kernel capability demo. N threads, each owning
|
||||
* its own ailang_ctx_t, drive the headline scalar kernel; must be
|
||||
* -fsanitize=thread-clean with every thread's result == the serial
|
||||
* oracle. NO negative control here: a non-allocating scalar kernel
|
||||
* writes no shared mutable state even under a shared ctx, so a
|
||||
* shared-ctx variant cannot race (the de-globalisation negative
|
||||
* control lives in the rc_accounting harness — Task 5 Step 3). */
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
#include <pthread.h>
|
||||
#include <assert.h>
|
||||
|
||||
typedef struct ailang_ctx ailang_ctx_t;
|
||||
extern ailang_ctx_t *ailang_ctx_new(void);
|
||||
@@ -472,36 +493,20 @@ static int64_t serial_oracle(void) {
|
||||
return s;
|
||||
}
|
||||
|
||||
#ifdef SHARED_CTX
|
||||
static ailang_ctx_t *g_shared;
|
||||
#endif
|
||||
|
||||
static void *worker(void *out) {
|
||||
#ifdef SHARED_CTX
|
||||
ailang_ctx_t *ctx = g_shared;
|
||||
#else
|
||||
ailang_ctx_t *ctx = ailang_ctx_new();
|
||||
#endif
|
||||
int64_t s = 0;
|
||||
for (int i = 0; i < NITERS; i++) s = backtest_step(ctx, s, (i & 7));
|
||||
#ifndef SHARED_CTX
|
||||
ailang_ctx_free(ctx);
|
||||
#endif
|
||||
*(int64_t *)out = s;
|
||||
return NULL;
|
||||
}
|
||||
|
||||
int main(void) {
|
||||
#ifdef SHARED_CTX
|
||||
g_shared = ailang_ctx_new();
|
||||
#endif
|
||||
pthread_t t[NTHREADS];
|
||||
int64_t res[NTHREADS];
|
||||
for (int i = 0; i < NTHREADS; i++) pthread_create(&t[i], NULL, worker, &res[i]);
|
||||
for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], NULL);
|
||||
#ifdef SHARED_CTX
|
||||
ailang_ctx_free(g_shared);
|
||||
#endif
|
||||
int64_t oracle = serial_oracle();
|
||||
for (int i = 0; i < NTHREADS; i++) {
|
||||
if (res[i] != oracle) { fprintf(stderr, "thread %d: %lld != %lld\n",
|
||||
@@ -512,15 +517,16 @@ int main(void) {
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 2: Write the driver (per-thread-ctx GREEN; shared-ctx flagged)**
|
||||
- [ ] **Step 2: Write the capability-demo driver (one green positive test)**
|
||||
|
||||
Create `crates/ail/tests/embed_swarm_tsan.rs`:
|
||||
|
||||
```rust
|
||||
//! M2 items 2+3. Builds the staticlib (rc) via the `ail` CLI, then
|
||||
//! links swarm.c against lib<entry>.a + libailang_rt.a under
|
||||
//! -fsanitize=thread. Per-thread-ctx: tsan-clean, exit 0. Negative
|
||||
//! control (-DSHARED_CTX): tsan MUST report (non-zero / report text).
|
||||
//! M2 item 2 (capability demo). Builds the staticlib (rc) via the
|
||||
//! `ail` CLI, links swarm.c against lib<entry>.a + libailang_rt.a
|
||||
//! under -fsanitize=thread. Per-thread-ctx: tsan-clean, exit 0,
|
||||
//! every thread's result == serial oracle. (The de-globalisation
|
||||
//! negative control is in embed_rc_accounting_tsan.rs — item 1.)
|
||||
use std::process::Command;
|
||||
use std::path::PathBuf;
|
||||
|
||||
@@ -538,59 +544,80 @@ fn build_staticlib(outdir: &PathBuf) {
|
||||
assert!(st.success(), "ail build --emit=staticlib failed");
|
||||
}
|
||||
|
||||
fn link_swarm(outdir: &PathBuf, bin: &PathBuf, shared: bool) {
|
||||
let root = ws_root();
|
||||
let mut args: Vec<String> = vec![
|
||||
"-O1".into(), "-g".into(), "-fsanitize=thread".into(), "-pthread".into(),
|
||||
"-o".into(), bin.to_string_lossy().into(),
|
||||
root.join("crates/ail/tests/embed/swarm.c").to_string_lossy().into(),
|
||||
];
|
||||
if shared { args.push("-DSHARED_CTX".into()); }
|
||||
args.push(format!("-L{}", outdir.to_string_lossy()));
|
||||
args.push("-lembed_backtest_step".into());
|
||||
args.push("-lailang_rt".into());
|
||||
let st = Command::new("clang").args(&args).status().expect("clang");
|
||||
assert!(st.success(), "linking swarm.c failed (shared={shared})");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle() {
|
||||
let outdir = std::env::temp_dir().join("ail_m2_swarm_ok");
|
||||
build_staticlib(&outdir);
|
||||
let root = ws_root();
|
||||
let bin = outdir.join("swarm_ok");
|
||||
link_swarm(&outdir, &bin, false);
|
||||
let st = Command::new("clang").args([
|
||||
"-O1", "-g", "-fsanitize=thread", "-pthread",
|
||||
"-o", bin.to_str().unwrap(),
|
||||
root.join("crates/ail/tests/embed/swarm.c").to_str().unwrap(),
|
||||
&format!("-L{}", outdir.to_string_lossy()),
|
||||
"-lembed_backtest_step", "-lailang_rt",
|
||||
]).status().expect("clang");
|
||||
assert!(st.success(), "linking swarm.c failed");
|
||||
let out = Command::new(&bin).env("TSAN_OPTIONS", "halt_on_error=1")
|
||||
.output().expect("run swarm");
|
||||
assert!(out.status.success(),
|
||||
"per-thread-ctx swarm must exit 0 tsan-clean; stderr:\n{}",
|
||||
String::from_utf8_lossy(&out.stderr));
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 3: Add the de-globalisation negative-control standing test (item-1 harness)**
|
||||
|
||||
`crates/ail/tests/embed/rc_accounting_tsan.c` already carries the `#ifdef SHARED_CTX` block (Task 2). Append this test to the existing `crates/ail/tests/embed_rc_accounting_tsan.rs` (reuse its `ws_root()` + `cc()` helpers defined in Task 2):
|
||||
|
||||
```rust
|
||||
#[test]
|
||||
fn shared_ctx_negative_control_is_flagged_by_tsan() {
|
||||
let outdir = std::env::temp_dir().join("ail_m2_swarm_neg");
|
||||
build_staticlib(&outdir);
|
||||
let bin = outdir.join("swarm_neg");
|
||||
link_swarm(&outdir, &bin, true);
|
||||
fn rc_accounting_shared_ctx_is_flagged_by_tsan() {
|
||||
// Negative control: all N threads share one ailang_ctx_t* while
|
||||
// calling ailang_rc_alloc/ailang_rc_dec → concurrent
|
||||
// ctx->alloc_count++ is a genuine data race tsan MUST report.
|
||||
// Proves the de-globalisation property is not vacuous.
|
||||
let root = ws_root();
|
||||
let tmp = std::env::temp_dir().join("ail_m2_rcacct_neg");
|
||||
std::fs::create_dir_all(&tmp).unwrap();
|
||||
let rc_o = tmp.join("rc.o");
|
||||
let str_o = tmp.join("str.o");
|
||||
let rt_a = tmp.join("libailang_rt.a");
|
||||
cc(&["-O1", "-g", "-fsanitize=thread", "-c", "-o", rc_o.to_str().unwrap(),
|
||||
root.join("runtime/rc.c").to_str().unwrap()], "rc.c");
|
||||
cc(&["-O1", "-g", "-fsanitize=thread", "-c", "-o", str_o.to_str().unwrap(),
|
||||
root.join("runtime/str.c").to_str().unwrap()], "str.c");
|
||||
let st = Command::new("ar").args(["rcs", rt_a.to_str().unwrap(),
|
||||
rc_o.to_str().unwrap(), str_o.to_str().unwrap()]).status().unwrap();
|
||||
assert!(st.success(), "ar failed");
|
||||
let bin = tmp.join("rcacct_neg");
|
||||
cc(&["-O1", "-g", "-fsanitize=thread", "-pthread", "-DSHARED_CTX",
|
||||
"-o", bin.to_str().unwrap(),
|
||||
root.join("crates/ail/tests/embed/rc_accounting_tsan.c").to_str().unwrap(),
|
||||
rt_a.to_str().unwrap()], "link rc_accounting_tsan -DSHARED_CTX");
|
||||
let out = Command::new(&bin).env("TSAN_OPTIONS", "halt_on_error=1")
|
||||
.output().expect("run swarm neg");
|
||||
.output().expect("run rcacct neg");
|
||||
let stderr = String::from_utf8_lossy(&out.stderr);
|
||||
assert!(
|
||||
!out.status.success() || stderr.contains("WARNING: ThreadSanitizer"),
|
||||
"shared-ctx negative control MUST be flagged by tsan (the harness \
|
||||
has teeth); exit={:?} stderr:\n{stderr}", out.status.code()
|
||||
"shared-ctx rc-accounting negative control MUST be tsan-flagged \
|
||||
(the de-globalisation teeth); exit={:?} stderr:\n{stderr}",
|
||||
out.status.code()
|
||||
);
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 3: Run the swarm matrix**
|
||||
- [ ] **Step 4: Run both halves**
|
||||
|
||||
Run: `cargo test -p ail --test embed_swarm_tsan`
|
||||
Expected: PASS (`test result: ok. 2 passed`) —
|
||||
Expected: PASS (`test result: ok. 1 passed`) —
|
||||
`scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle` exits 0
|
||||
tsan-clean with every thread == oracle;
|
||||
`shared_ctx_negative_control_is_flagged_by_tsan` observes the tsan
|
||||
race report (teeth proven).
|
||||
tsan-clean, every thread == oracle.
|
||||
|
||||
Run: `cargo test -p ail --test embed_rc_accounting_tsan`
|
||||
Expected: PASS (`test result: ok. 2 passed`) — the per-ctx positive
|
||||
(Task 2) stays green AND `rc_accounting_shared_ctx_is_flagged_by_tsan`
|
||||
observes the genuine tsan race on `ctx->alloc_count` (teeth proven).
|
||||
|
||||
---
|
||||
|
||||
@@ -806,4 +833,4 @@ regression, not carry-on.)
|
||||
5. **No commit steps:** none present (Boss commits at iter end). ✓
|
||||
6. **Pin/replacement contiguity:** the only presence-pin paired with a verbatim doc edit is `docs_honesty_pin.rs:135` ↔ DESIGN.md §"Embedding ABI (M1)". Task 7 Step 1 edits ONLY `:2282–2285` and explicitly forbids touching `:2287–2289` (the pinned sentence) — the pinned substring is never inside the replacement body, so no soft-wrap split is possible; `norm()` additionally collapses whitespace. ✓
|
||||
7. **Compile-gate vs deferred-caller:** no task changes a Rust fn signature (`lower_workspace_staticlib*` unchanged; `build_staticlib` adds an internal guard, signature unchanged). The one cross-task RED interval (Task 3 leaves `embed_e2e` RED until Task 6) is a *link/runtime* gate, explicitly named in both Task 3's preamble and Task 6 Step 1, and Task 3's GREEN gate scopes to `embed_staticlib_lowering` only — no silent resequencing. ✓
|
||||
8. **Verification filter strings resolve:** existing-test filters use recon-verified names (`alloc_rc_print_int_does_not_leak_show_result_str`, `alloc_rc_explicit_mode_tail_sum_does_not_leak_outer_cells`, `staticlib_emits_forwarder_no_main`, `executable_target_still_emits_main`, `c_host_calls_exported_scalar_kernel`, `fn_without_export_hash_is_unchanged`); new-test filters resolve by construction (defined in the same task); the `-- rc_stats` filter (T8 S1) is backed by the unfiltered `print_no_leak_pin` run in the same step and `e2e.rs:2178` helper consumers are `*rc_stats*`-named (recon-confirmed) — and T8 S3 runs the unfiltered `cargo test --workspace` so "nothing ran" cannot masquerade as green. ✓
|
||||
8. **Verification filter strings resolve:** existing-test filters use recon-verified names (`alloc_rc_print_int_does_not_leak_show_result_str`, `alloc_rc_explicit_mode_tail_sum_does_not_leak_outer_cells`, `staticlib_emits_forwarder_no_main`, `executable_target_still_emits_main`, `c_host_calls_exported_scalar_kernel`, `fn_without_export_hash_is_unchanged`); new-test filters resolve by construction (defined in the same task: `scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle`, `rc_accounting_per_ctx_is_tsan_clean`, `rc_accounting_shared_ctx_is_flagged_by_tsan`, `staticlib_gc_is_rejected`/`staticlib_bump_is_rejected`); the `-- rc_stats` filter (T8 S1) is backed by the unfiltered `print_no_leak_pin` run in the same step and `e2e.rs:2178` helper consumers are `*rc_stats*`-named (recon-confirmed) — and T8 S3 runs the unfiltered `cargo test --workspace` so "nothing ran" cannot masquerade as green. The Task-5 split (capability demo with no negative control vs. de-globalisation teeth in the rc-accounting harness) is the resolution of the spec defect the first dispatch surfaced; no harness asserts a structurally-unreachable race. ✓
|
||||
|
||||
Reference in New Issue
Block a user