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:
@@ -0,0 +1,14 @@
|
|||||||
|
{
|
||||||
|
"iter_id": "embedding-abi-m2.1",
|
||||||
|
"date": "2026-05-18",
|
||||||
|
"mode": "standard",
|
||||||
|
"outcome": "PARTIAL",
|
||||||
|
"tasks_total": 9,
|
||||||
|
"tasks_completed": 4,
|
||||||
|
"reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 0 },
|
||||||
|
"review_loops_spec": 0,
|
||||||
|
"review_loops_quality": 0,
|
||||||
|
"blocked_reason": "spec-ambiguous",
|
||||||
|
"blocked_task": 5,
|
||||||
|
"notes": "Tasks 1-4 fully green (zero review re-loops). Task 5 implemented faithfully but BLOCKED: shared-ctx swarm negative control is structurally unable to race for a non-allocating scalar kernel (@__ail_tls_ctx is __thread; no ctx field is written by the kernel). Real de-globalisation negative control already has teeth in Task 2's rc_accounting_tsan.c -DSHARED_CTX (tsan exit 66 at rc.c ailang_rc_alloc). Task 3 carried one DONE_WITH_CONCERNS plan-transcription-error fix (assertion symbol @ail_backtest_step -> @ail_embed_backtest_step_step to match the byte-unchanged @ail_<mname>_<fn> invariant). Tasks 6-9 not run (downstream resequencing is a Boss decision)."
|
||||||
|
}
|
||||||
@@ -2490,6 +2490,12 @@ fn build_staticlib(
|
|||||||
"staticlib target needs at least one `(export \"<sym>\")` fn"
|
"staticlib target needs at least one `(export \"<sym>\")` fn"
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
if !matches!(alloc, ailang_codegen::AllocStrategy::Rc) {
|
||||||
|
anyhow::bail!(
|
||||||
|
"staticlib (swarm) artefact is RC-only — `--alloc=gc` links the \
|
||||||
|
shared Boehm collector, which is not swarm-safe; use `--alloc=rc`"
|
||||||
|
);
|
||||||
|
}
|
||||||
let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(&ws, alloc)?;
|
let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(&ws, alloc)?;
|
||||||
|
|
||||||
let tmpdir = std::env::temp_dir().join(format!("ailang-{}", std::process::id()));
|
let tmpdir = std::env::temp_dir().join(format!("ailang-{}", std::process::id()));
|
||||||
|
|||||||
@@ -0,0 +1,59 @@
|
|||||||
|
/* M2 item 1: the de-globalisation teeth. Exercises ailang_rc_alloc /
|
||||||
|
* ailang_rc_dec DIRECTLY (not through any kernel) from N threads, each
|
||||||
|
* owning its own ailang_ctx_t. Per-ctx counters must be individually
|
||||||
|
* correct and -fsanitize=thread-clean. Build -DSHARED_CTX for the
|
||||||
|
* global-hammering negative control (must make tsan report a race). */
|
||||||
|
#include <stdint.h>
|
||||||
|
#include <stdio.h>
|
||||||
|
#include <stdlib.h>
|
||||||
|
#include <pthread.h>
|
||||||
|
#include <assert.h>
|
||||||
|
|
||||||
|
typedef struct ailang_ctx ailang_ctx_t;
|
||||||
|
extern ailang_ctx_t *ailang_ctx_new(void);
|
||||||
|
extern void ailang_ctx_free(ailang_ctx_t *);
|
||||||
|
extern void *ailang_rc_alloc(size_t);
|
||||||
|
extern void ailang_rc_dec(void *);
|
||||||
|
/* set the per-call ctx the runtime accounts into (defined in rc.c) */
|
||||||
|
extern __thread ailang_ctx_t *__ail_tls_ctx;
|
||||||
|
|
||||||
|
#define NTHREADS 8
|
||||||
|
#define NCYCLES 200000
|
||||||
|
|
||||||
|
#ifdef SHARED_CTX
|
||||||
|
static ailang_ctx_t *g_shared; /* negative control: one ctx, all threads */
|
||||||
|
#endif
|
||||||
|
|
||||||
|
static void *worker(void *_a) {
|
||||||
|
(void)_a;
|
||||||
|
#ifdef SHARED_CTX
|
||||||
|
ailang_ctx_t *ctx = g_shared;
|
||||||
|
#else
|
||||||
|
ailang_ctx_t *ctx = ailang_ctx_new();
|
||||||
|
#endif
|
||||||
|
__ail_tls_ctx = ctx;
|
||||||
|
for (int i = 0; i < NCYCLES; i++) {
|
||||||
|
void *p = ailang_rc_alloc(16);
|
||||||
|
ailang_rc_dec(p); /* refcount 1 -> 0, frees, free_count++ */
|
||||||
|
}
|
||||||
|
#ifndef SHARED_CTX
|
||||||
|
/* per-ctx balance must hold exactly */
|
||||||
|
/* (read via the same struct layout the runtime defines) */
|
||||||
|
ailang_ctx_free(ctx);
|
||||||
|
#endif
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
|
||||||
|
int main(void) {
|
||||||
|
#ifdef SHARED_CTX
|
||||||
|
g_shared = ailang_ctx_new();
|
||||||
|
#endif
|
||||||
|
pthread_t t[NTHREADS];
|
||||||
|
for (int i = 0; i < NTHREADS; i++) pthread_create(&t[i], NULL, worker, NULL);
|
||||||
|
for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], NULL);
|
||||||
|
#ifdef SHARED_CTX
|
||||||
|
ailang_ctx_free(g_shared);
|
||||||
|
#endif
|
||||||
|
printf("rc_accounting_tsan: ok\n");
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
@@ -0,0 +1,43 @@
|
|||||||
|
//! M2 item 1: direct rc-accounting de-globalisation proof. Compiles
|
||||||
|
//! runtime/rc.c + runtime/str.c into libailang_rt.a, links the
|
||||||
|
//! rc_accounting_tsan.c harness against it under -fsanitize=thread.
|
||||||
|
//! Per-thread-ctx build: tsan-clean + exit 0. RED until rc.c gains
|
||||||
|
//! ailang_ctx_* + __ail_tls_ctx (link error: undefined symbols).
|
||||||
|
use std::process::Command;
|
||||||
|
use std::path::PathBuf;
|
||||||
|
|
||||||
|
fn ws_root() -> PathBuf {
|
||||||
|
PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../..").canonicalize().unwrap()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn cc(args: &[&str], ctx: &str) {
|
||||||
|
let st = Command::new("clang").args(args).status().expect("spawn clang");
|
||||||
|
assert!(st.success(), "clang failed: {ctx}");
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn rc_accounting_per_ctx_is_tsan_clean() {
|
||||||
|
let root = ws_root();
|
||||||
|
let tmp = std::env::temp_dir().join("ail_m2_rcacct");
|
||||||
|
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");
|
||||||
|
cc(&["-O1", "-g", "-fsanitize=thread", "-pthread",
|
||||||
|
"-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");
|
||||||
|
let out = Command::new(&bin).env("TSAN_OPTIONS", "halt_on_error=1")
|
||||||
|
.output().expect("run harness");
|
||||||
|
assert!(out.status.success(),
|
||||||
|
"per-ctx rc-accounting harness must exit 0 tsan-clean; stderr:\n{}",
|
||||||
|
String::from_utf8_lossy(&out.stderr));
|
||||||
|
}
|
||||||
@@ -0,0 +1,46 @@
|
|||||||
|
//! M2: `ail build --emit=staticlib` is RC-only. `--alloc=gc`/`--alloc=bump`
|
||||||
|
//! must fail the build (the shared Boehm collector / bench stub are not
|
||||||
|
//! swarm-safe). RED until the Task-4 CLI guard lands: today the alloc
|
||||||
|
//! strategy is passed straight through and the build SUCCEEDS.
|
||||||
|
use std::process::Command;
|
||||||
|
|
||||||
|
fn ail_bin() -> &'static str { env!("CARGO_BIN_EXE_ail") }
|
||||||
|
|
||||||
|
fn build_staticlib_with_alloc(alloc: &str, outdir: &str) -> std::process::Output {
|
||||||
|
Command::new(ail_bin())
|
||||||
|
.args([
|
||||||
|
"build", "examples/embed_backtest_step.ail",
|
||||||
|
"--emit=staticlib", &format!("--alloc={alloc}"), "-o", outdir,
|
||||||
|
])
|
||||||
|
.current_dir(env!("CARGO_MANIFEST_DIR").to_string() + "/../..")
|
||||||
|
.output()
|
||||||
|
.expect("spawn ail build")
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn staticlib_gc_is_rejected() {
|
||||||
|
let out = build_staticlib_with_alloc("gc", "/tmp/ail_m2_guard_gc");
|
||||||
|
assert!(
|
||||||
|
!out.status.success(),
|
||||||
|
"expected `--emit=staticlib --alloc=gc` to FAIL the build; exit was success"
|
||||||
|
);
|
||||||
|
let stderr = String::from_utf8_lossy(&out.stderr);
|
||||||
|
assert!(
|
||||||
|
stderr.contains("staticlib (swarm) artefact is RC-only"),
|
||||||
|
"expected the RC-only diagnostic; stderr was:\n{stderr}"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn staticlib_bump_is_rejected() {
|
||||||
|
let out = build_staticlib_with_alloc("bump", "/tmp/ail_m2_guard_bump");
|
||||||
|
assert!(
|
||||||
|
!out.status.success(),
|
||||||
|
"expected `--emit=staticlib --alloc=bump` to FAIL the build; exit was success"
|
||||||
|
);
|
||||||
|
let stderr = String::from_utf8_lossy(&out.stderr);
|
||||||
|
assert!(
|
||||||
|
stderr.contains("staticlib (swarm) artefact is RC-only"),
|
||||||
|
"expected the RC-only diagnostic; stderr was:\n{stderr}"
|
||||||
|
);
|
||||||
|
}
|
||||||
@@ -171,7 +171,11 @@ pub enum Target {
|
|||||||
/// `--emit=staticlib`: suppress the `@main` trampoline AND the
|
/// `--emit=staticlib`: suppress the `@main` trampoline AND the
|
||||||
/// `MissingEntryMain` shape-check (a kernel module is a library);
|
/// `MissingEntryMain` shape-check (a kernel module is a library);
|
||||||
/// emit one external C entrypoint per `(export …)` fn forwarding
|
/// emit one external C entrypoint per `(export …)` fn forwarding
|
||||||
/// to `@ail_<module>_<fn>`. Provisional signature until M3.
|
/// to the internal `@ail_<module>_<def>`. M2: the entrypoint takes
|
||||||
|
/// a mandatory leading `ptr %ctx` (per-thread embedding context)
|
||||||
|
/// published via `@__ail_tls_ctx` around the unchanged internal
|
||||||
|
/// call. The ctx-threaded C signature is the M2 shape; only the
|
||||||
|
/// value/record layout remains provisional until M3.
|
||||||
StaticLib,
|
StaticLib,
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -606,6 +610,11 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy, target: Target) -
|
|||||||
// the internal callee takes the scalars positionally
|
// the internal callee takes the scalars positionally
|
||||||
// (confirmed against `emit_fn`'s signature emission,
|
// (confirmed against `emit_fn`'s signature emission,
|
||||||
// `lib.rs:1087`).
|
// `lib.rs:1087`).
|
||||||
|
// M2: the per-thread embedding ctx slot. Defined by
|
||||||
|
// runtime/rc.c (__thread ailang_ctx_t *__ail_tls_ctx);
|
||||||
|
// the forwarder publishes its explicit ctx param here for
|
||||||
|
// the synchronous duration of the internal call.
|
||||||
|
out.push_str("\n@__ail_tls_ctx = external thread_local global ptr\n");
|
||||||
for (mname, m) in &ws.modules {
|
for (mname, m) in &ws.modules {
|
||||||
for d in &m.defs {
|
for d in &m.defs {
|
||||||
if let Def::Fn(f) = d {
|
if let Def::Fn(f) = d {
|
||||||
@@ -617,17 +626,21 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy, target: Target) -
|
|||||||
(check-side gate should have rejected it)"))),
|
(check-side gate should have rejected it)"))),
|
||||||
};
|
};
|
||||||
let cret = llvm_scalar(&ret_ty);
|
let cret = llvm_scalar(&ret_ty);
|
||||||
let params: Vec<String> = param_tys.iter().enumerate()
|
|
||||||
.map(|(i, t)| format!("{} %a{i}", llvm_scalar(t)))
|
|
||||||
.collect();
|
|
||||||
let args: Vec<String> = param_tys.iter().enumerate()
|
let args: Vec<String> = param_tys.iter().enumerate()
|
||||||
.map(|(i, t)| format!("{} %a{i}", llvm_scalar(t)))
|
.map(|(i, t)| format!("{} %a{i}", llvm_scalar(t)))
|
||||||
.collect();
|
.collect();
|
||||||
|
let mut sig_params = vec!["ptr %ctx".to_string()];
|
||||||
|
sig_params.extend(
|
||||||
|
param_tys.iter().enumerate()
|
||||||
|
.map(|(i, t)| format!("{} %a{i}", llvm_scalar(t))));
|
||||||
out.push_str(&format!(
|
out.push_str(&format!(
|
||||||
"\ndefine {cret} @{sym}({}) {{\n \
|
"\ndefine {cret} @{sym}({}) {{\n \
|
||||||
|
%saved = load ptr, ptr @__ail_tls_ctx\n \
|
||||||
|
store ptr %ctx, ptr @__ail_tls_ctx\n \
|
||||||
%r = call {cret} @ail_{mname}_{}({})\n \
|
%r = call {cret} @ail_{mname}_{}({})\n \
|
||||||
|
store ptr %saved, ptr @__ail_tls_ctx\n \
|
||||||
ret {cret} %r\n}}\n",
|
ret {cret} %r\n}}\n",
|
||||||
params.join(", "),
|
sig_params.join(", "),
|
||||||
f.name,
|
f.name,
|
||||||
args.join(", "),
|
args.join(", "),
|
||||||
));
|
));
|
||||||
|
|||||||
@@ -30,6 +30,17 @@ fn staticlib_emits_forwarder_no_main() {
|
|||||||
assert!(ir.contains("@ail_embed_backtest_step_step("),
|
assert!(ir.contains("@ail_embed_backtest_step_step("),
|
||||||
"the forwarder must call the internal \
|
"the forwarder must call the internal \
|
||||||
@ail_embed_backtest_step_step (module embed_backtest_step)");
|
@ail_embed_backtest_step_step (module embed_backtest_step)");
|
||||||
|
|
||||||
|
// M2: forwarder takes a leading ptr %ctx and routes it through TLS
|
||||||
|
// around the UNCHANGED internal call.
|
||||||
|
assert!(ir.contains("@__ail_tls_ctx = external thread_local global ptr"),
|
||||||
|
"staticlib module must declare the external thread-local ctx slot;\nIR:\n{ir}");
|
||||||
|
assert!(ir.contains("define i64 @backtest_step(ptr %ctx, i64 %a0, i64 %a1)"),
|
||||||
|
"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_embed_backtest_step_step(i64 %a0, i64 %a1)"),
|
||||||
|
"internal call must stay byte-unchanged (no ctx arg);\nIR:\n{ir}");
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
|
|||||||
@@ -0,0 +1,135 @@
|
|||||||
|
# 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
|
||||||
|
|
||||||
|
## 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).
|
||||||
|
|
||||||
|
## 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).
|
||||||
|
|
||||||
|
## Concerns
|
||||||
|
|
||||||
|
- iter embedding-abi-m2.1.3: PLAN TRANSCRIPTION ERROR. Task 3 Step 1's
|
||||||
|
plan code block asserts
|
||||||
|
`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.
|
||||||
|
|
||||||
|
## 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`).
|
||||||
|
|
||||||
|
## 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.
|
||||||
|
|
||||||
|
## Files touched
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
## Stats
|
||||||
|
|
||||||
|
bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m2.1.json
|
||||||
@@ -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/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`.
|
- 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/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.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 + the two new C harnesses under `-fsanitize=thread`, asserts the matrix.
|
- 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).
|
- 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`.
|
- 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}");
|
"forwarder must take a leading ptr %ctx;\nIR:\n{ir}");
|
||||||
assert!(ir.contains("store ptr %ctx, ptr @__ail_tls_ctx"),
|
assert!(ir.contains("store ptr %ctx, ptr @__ail_tls_ctx"),
|
||||||
"forwarder must publish ctx into the TLS slot;\nIR:\n{ir}");
|
"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}");
|
"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:**
|
**Files:**
|
||||||
- Create: `crates/ail/tests/embed/swarm.c`
|
- Create: `crates/ail/tests/embed/swarm.c` (per-thread-ctx capability demo, no `SHARED_CTX`)
|
||||||
- Create: `crates/ail/tests/embed_swarm_tsan.rs`
|
- 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`:
|
Create `crates/ail/tests/embed/swarm.c`:
|
||||||
|
|
||||||
```c
|
```c
|
||||||
/* M2 items 2+3: scalar-kernel swarm. Per-thread-ctx (default) must be
|
/* M2 item 2: scalar-kernel capability demo. N threads, each owning
|
||||||
* tsan-clean and every thread's result must match the serial oracle.
|
* its own ailang_ctx_t, drive the headline scalar kernel; must be
|
||||||
* Built -DSHARED_CTX = negative control: all threads share one ctx;
|
* -fsanitize=thread-clean with every thread's result == the serial
|
||||||
* tsan MUST report a race (proves the clean result is not vacuous). */
|
* 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 <stdint.h>
|
||||||
#include <stdio.h>
|
#include <stdio.h>
|
||||||
#include <pthread.h>
|
#include <pthread.h>
|
||||||
#include <assert.h>
|
|
||||||
|
|
||||||
typedef struct ailang_ctx ailang_ctx_t;
|
typedef struct ailang_ctx ailang_ctx_t;
|
||||||
extern ailang_ctx_t *ailang_ctx_new(void);
|
extern ailang_ctx_t *ailang_ctx_new(void);
|
||||||
@@ -472,36 +493,20 @@ static int64_t serial_oracle(void) {
|
|||||||
return s;
|
return s;
|
||||||
}
|
}
|
||||||
|
|
||||||
#ifdef SHARED_CTX
|
|
||||||
static ailang_ctx_t *g_shared;
|
|
||||||
#endif
|
|
||||||
|
|
||||||
static void *worker(void *out) {
|
static void *worker(void *out) {
|
||||||
#ifdef SHARED_CTX
|
|
||||||
ailang_ctx_t *ctx = g_shared;
|
|
||||||
#else
|
|
||||||
ailang_ctx_t *ctx = ailang_ctx_new();
|
ailang_ctx_t *ctx = ailang_ctx_new();
|
||||||
#endif
|
|
||||||
int64_t s = 0;
|
int64_t s = 0;
|
||||||
for (int i = 0; i < NITERS; i++) s = backtest_step(ctx, s, (i & 7));
|
for (int i = 0; i < NITERS; i++) s = backtest_step(ctx, s, (i & 7));
|
||||||
#ifndef SHARED_CTX
|
|
||||||
ailang_ctx_free(ctx);
|
ailang_ctx_free(ctx);
|
||||||
#endif
|
|
||||||
*(int64_t *)out = s;
|
*(int64_t *)out = s;
|
||||||
return NULL;
|
return NULL;
|
||||||
}
|
}
|
||||||
|
|
||||||
int main(void) {
|
int main(void) {
|
||||||
#ifdef SHARED_CTX
|
|
||||||
g_shared = ailang_ctx_new();
|
|
||||||
#endif
|
|
||||||
pthread_t t[NTHREADS];
|
pthread_t t[NTHREADS];
|
||||||
int64_t res[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_create(&t[i], NULL, worker, &res[i]);
|
||||||
for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], NULL);
|
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();
|
int64_t oracle = serial_oracle();
|
||||||
for (int i = 0; i < NTHREADS; i++) {
|
for (int i = 0; i < NTHREADS; i++) {
|
||||||
if (res[i] != oracle) { fprintf(stderr, "thread %d: %lld != %lld\n",
|
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`:
|
Create `crates/ail/tests/embed_swarm_tsan.rs`:
|
||||||
|
|
||||||
```rust
|
```rust
|
||||||
//! M2 items 2+3. Builds the staticlib (rc) via the `ail` CLI, then
|
//! M2 item 2 (capability demo). Builds the staticlib (rc) via the
|
||||||
//! links swarm.c against lib<entry>.a + libailang_rt.a under
|
//! `ail` CLI, links swarm.c against lib<entry>.a + libailang_rt.a
|
||||||
//! -fsanitize=thread. Per-thread-ctx: tsan-clean, exit 0. Negative
|
//! under -fsanitize=thread. Per-thread-ctx: tsan-clean, exit 0,
|
||||||
//! control (-DSHARED_CTX): tsan MUST report (non-zero / report text).
|
//! 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::process::Command;
|
||||||
use std::path::PathBuf;
|
use std::path::PathBuf;
|
||||||
|
|
||||||
@@ -538,59 +544,80 @@ fn build_staticlib(outdir: &PathBuf) {
|
|||||||
assert!(st.success(), "ail build --emit=staticlib failed");
|
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]
|
#[test]
|
||||||
fn scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle() {
|
fn scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle() {
|
||||||
let outdir = std::env::temp_dir().join("ail_m2_swarm_ok");
|
let outdir = std::env::temp_dir().join("ail_m2_swarm_ok");
|
||||||
build_staticlib(&outdir);
|
build_staticlib(&outdir);
|
||||||
|
let root = ws_root();
|
||||||
let bin = outdir.join("swarm_ok");
|
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")
|
let out = Command::new(&bin).env("TSAN_OPTIONS", "halt_on_error=1")
|
||||||
.output().expect("run swarm");
|
.output().expect("run swarm");
|
||||||
assert!(out.status.success(),
|
assert!(out.status.success(),
|
||||||
"per-thread-ctx swarm must exit 0 tsan-clean; stderr:\n{}",
|
"per-thread-ctx swarm must exit 0 tsan-clean; stderr:\n{}",
|
||||||
String::from_utf8_lossy(&out.stderr));
|
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]
|
#[test]
|
||||||
fn shared_ctx_negative_control_is_flagged_by_tsan() {
|
fn rc_accounting_shared_ctx_is_flagged_by_tsan() {
|
||||||
let outdir = std::env::temp_dir().join("ail_m2_swarm_neg");
|
// Negative control: all N threads share one ailang_ctx_t* while
|
||||||
build_staticlib(&outdir);
|
// calling ailang_rc_alloc/ailang_rc_dec → concurrent
|
||||||
let bin = outdir.join("swarm_neg");
|
// ctx->alloc_count++ is a genuine data race tsan MUST report.
|
||||||
link_swarm(&outdir, &bin, true);
|
// 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")
|
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);
|
let stderr = String::from_utf8_lossy(&out.stderr);
|
||||||
assert!(
|
assert!(
|
||||||
!out.status.success() || stderr.contains("WARNING: ThreadSanitizer"),
|
!out.status.success() || stderr.contains("WARNING: ThreadSanitizer"),
|
||||||
"shared-ctx negative control MUST be flagged by tsan (the harness \
|
"shared-ctx rc-accounting negative control MUST be tsan-flagged \
|
||||||
has teeth); exit={:?} stderr:\n{stderr}", out.status.code()
|
(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`
|
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
|
`scalar_swarm_per_ctx_is_tsan_clean_and_matches_oracle` exits 0
|
||||||
tsan-clean with every thread == oracle;
|
tsan-clean, every thread == oracle.
|
||||||
`shared_ctx_negative_control_is_flagged_by_tsan` observes the tsan
|
|
||||||
race report (teeth proven).
|
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). ✓
|
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. ✓
|
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. ✓
|
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. ✓
|
||||||
|
|||||||
@@ -31,9 +31,11 @@ otherwise.
|
|||||||
**Coherent stop:** N host threads, each owning its own
|
**Coherent stop:** N host threads, each owning its own
|
||||||
`ailang_ctx_t`, each driving the scalar kernel in a `while
|
`ailang_ctx_t`, each driving the scalar kernel in a `while
|
||||||
let next_chunk`-shaped loop, run `-fsanitize=thread`-clean with every
|
let next_chunk`-shaped loop, run `-fsanitize=thread`-clean with every
|
||||||
thread's result matching the serial oracle — *and* a deliberately
|
thread's result matching the serial oracle — *and* the
|
||||||
ctx-sharing negative control that tsan correctly flags (the harness
|
de-globalisation proof's deliberately ctx-sharing negative control
|
||||||
has teeth), *and* `--emit=staticlib --alloc=gc` failing to build.
|
(the direct rc-accounting harness, where a shared ctx genuinely races
|
||||||
|
on `ctx->alloc_count`) that tsan correctly flags (the teeth), *and*
|
||||||
|
`--emit=staticlib --alloc=gc` failing to build.
|
||||||
|
|
||||||
### Position in the M1–M5 arc (load-bearing)
|
### Position in the M1–M5 arc (load-bearing)
|
||||||
|
|
||||||
@@ -225,11 +227,18 @@ is at the build/runtime layer, and there are two teeth:
|
|||||||
(Same wording shape for `--alloc=bump`.) RED today (`build_staticlib`
|
(Same wording shape for `--alloc=bump`.) RED today (`build_staticlib`
|
||||||
passes the strategy through and succeeds); GREEN after the guard.
|
passes the strategy through and succeeds); GREEN after the guard.
|
||||||
|
|
||||||
2. **Negative control proves the harness has teeth** — a harness
|
2. **Negative control proves the teeth** — the `-DSHARED_CTX`
|
||||||
variant where all N threads share one `ailang_ctx_t*` must make
|
variant of the *direct rc-accounting harness* (Testing item 1,
|
||||||
tsan report a race on `ctx->alloc_count` (the analogue of M1's
|
below): all N threads share one `ailang_ctx_t*` while calling
|
||||||
must-fail fixture: a test that the safety mechanism is real, not
|
`ailang_rc_alloc`/`ailang_rc_dec`, so the concurrent
|
||||||
vacuous).
|
`ctx->alloc_count++` is a genuine data race tsan must report (the
|
||||||
|
analogue of M1's must-fail fixture: the safety mechanism is real,
|
||||||
|
not vacuous). The negative control lives in the rc-accounting
|
||||||
|
harness because that is the only M2 surface that *writes* a ctx
|
||||||
|
field — the scalar capability kernel (`swarm.c`) allocates
|
||||||
|
nothing, so a shared ctx there has no shared-memory write to race
|
||||||
|
on (the same honesty point Testing item 1 makes; do not place a
|
||||||
|
negative control on `swarm.c`).
|
||||||
|
|
||||||
### Implementation shape (secondary — supporting, not the point)
|
### Implementation shape (secondary — supporting, not the point)
|
||||||
|
|
||||||
@@ -392,9 +401,19 @@ fixtures = the gate's teeth):
|
|||||||
*capability* (the headline use case runs swarm-safe through the
|
*capability* (the headline use case runs swarm-safe through the
|
||||||
new ABI end-to-end). Honestly recorded: it is the capability
|
new ABI end-to-end). Honestly recorded: it is the capability
|
||||||
proof, not the de-globalisation proof (which is item 1).
|
proof, not the de-globalisation proof (which is item 1).
|
||||||
3. **Negative control.** The ctx-shared variant of the item-2
|
3. **Negative control (belongs to item 1, not item 2).** The
|
||||||
harness must make tsan report a race — proves item 2's clean
|
`-DSHARED_CTX` variant of the *item-1 direct rc-accounting
|
||||||
result is not vacuous.
|
harness* must make tsan report a race on the concurrent
|
||||||
|
`ctx->alloc_count++` — proving the de-globalisation property is
|
||||||
|
not vacuous. It is **not** a variant of the item-2 swarm harness:
|
||||||
|
`examples/embed_backtest_step.ail` is a non-allocating scalar
|
||||||
|
kernel that never writes a ctx field, and `__ail_tls_ctx` is
|
||||||
|
`__thread` (per-thread storage, 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 honesty point item 1 makes. `swarm.c` therefore ships
|
||||||
|
the per-thread-ctx positive demonstration only; its teeth are
|
||||||
|
item 1's by the de-globalisation-proof / capability-demo split.
|
||||||
4. **Forwarder shape.** `embed_staticlib_lowering.rs` extended:
|
4. **Forwarder shape.** `embed_staticlib_lowering.rs` extended:
|
||||||
`@<sym>` now `define i64 @sym(ptr %ctx, …)` with the TLS
|
`@<sym>` now `define i64 @sym(ptr %ctx, …)` with the TLS
|
||||||
save/store/restore around an *unchanged* `call @ail_<mod>_<fn>`;
|
save/store/restore around an *unchanged* `call @ail_<mod>_<fn>`;
|
||||||
@@ -459,9 +478,12 @@ Milestone-close ("coherent stop") is met when **all** hold:
|
|||||||
- The §"changed C host" N-thread harness on
|
- The §"changed C host" N-thread harness on
|
||||||
`examples/embed_backtest_step.ail` is `-fsanitize=thread`-clean
|
`examples/embed_backtest_step.ail` is `-fsanitize=thread`-clean
|
||||||
and every thread's result matches the serial oracle.
|
and every thread's result matches the serial oracle.
|
||||||
- The direct rc-accounting N-thread+tsan test (item 1) is green;
|
- The direct rc-accounting N-thread+tsan test (item 1) is green in
|
||||||
its global-hammering RED variant and the ctx-shared negative
|
its per-ctx form; its `-DSHARED_CTX` negative control (item 3, in
|
||||||
control (item 3) both demonstrate the teeth.
|
the same rc-accounting harness) is tsan-flagged — demonstrating the
|
||||||
|
de-globalisation teeth are not vacuous. (`swarm.c` carries no
|
||||||
|
negative control by construction — a scalar kernel has no shared
|
||||||
|
mutable state; see Testing item 3.)
|
||||||
- `ail build --emit=staticlib --alloc=gc` fails with the RC-only
|
- `ail build --emit=staticlib --alloc=gc` fails with the RC-only
|
||||||
diagnostic; `--alloc=rc` (default) builds and links.
|
diagnostic; `--alloc=rc` (default) builds and links.
|
||||||
- `embed_e2e.rs` migrated and green on the ctx ABI; the M1 value
|
- `embed_e2e.rs` migrated and green on the ctx ABI; the M1 value
|
||||||
|
|||||||
+35
-2
@@ -86,6 +86,37 @@ static inline ailang_rc_header_t *header_of(void *payload) {
|
|||||||
static uint64_t g_rc_alloc_count = 0;
|
static uint64_t g_rc_alloc_count = 0;
|
||||||
static uint64_t g_rc_free_count = 0;
|
static uint64_t g_rc_free_count = 0;
|
||||||
|
|
||||||
|
/* M2: per-thread embedding context. A scalar kernel allocates nothing,
|
||||||
|
* so this carries only the de-globalised RC accounting. Set by the
|
||||||
|
* generated C `@<sym>` forwarder into __ail_tls_ctx for the synchronous
|
||||||
|
* duration of one call (never held across a suspension point). The
|
||||||
|
* g_rc_* statics + atexit below are RETAINED as the null-ctx
|
||||||
|
* (single-threaded executable) fallback. */
|
||||||
|
typedef struct ailang_ctx {
|
||||||
|
uint64_t alloc_count;
|
||||||
|
uint64_t free_count;
|
||||||
|
} ailang_ctx_t;
|
||||||
|
|
||||||
|
__thread ailang_ctx_t *__ail_tls_ctx = NULL;
|
||||||
|
|
||||||
|
ailang_ctx_t *ailang_ctx_new(void) {
|
||||||
|
return (ailang_ctx_t *)calloc(1, sizeof(ailang_ctx_t));
|
||||||
|
}
|
||||||
|
|
||||||
|
void ailang_ctx_free(ailang_ctx_t *ctx) {
|
||||||
|
if (ctx != NULL) {
|
||||||
|
const char *flag = getenv("AILANG_RC_STATS");
|
||||||
|
if (flag != NULL && flag[0] != '\0') {
|
||||||
|
fprintf(stderr,
|
||||||
|
"ailang_rc_stats: allocs=%llu frees=%llu live=%lld\n",
|
||||||
|
(unsigned long long)ctx->alloc_count,
|
||||||
|
(unsigned long long)ctx->free_count,
|
||||||
|
(long long)(ctx->alloc_count - ctx->free_count));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
free(ctx);
|
||||||
|
}
|
||||||
|
|
||||||
static void ailang_rc_stats_atexit(void) {
|
static void ailang_rc_stats_atexit(void) {
|
||||||
fprintf(stderr,
|
fprintf(stderr,
|
||||||
"ailang_rc_stats: allocs=%llu frees=%llu live=%lld\n",
|
"ailang_rc_stats: allocs=%llu frees=%llu live=%lld\n",
|
||||||
@@ -122,7 +153,8 @@ void *ailang_rc_alloc(size_t size) {
|
|||||||
*hdr = 1;
|
*hdr = 1;
|
||||||
void *payload = (uint8_t *)block + HEADER_SIZE;
|
void *payload = (uint8_t *)block + HEADER_SIZE;
|
||||||
memset(payload, 0, size);
|
memset(payload, 0, size);
|
||||||
g_rc_alloc_count++;
|
ailang_ctx_t *_ctx = __ail_tls_ctx;
|
||||||
|
if (_ctx != NULL) _ctx->alloc_count++; else g_rc_alloc_count++;
|
||||||
return payload;
|
return payload;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -172,7 +204,8 @@ void ailang_rc_dec(void *payload) {
|
|||||||
*hdr -= 1;
|
*hdr -= 1;
|
||||||
if (*hdr == 0) {
|
if (*hdr == 0) {
|
||||||
free(hdr);
|
free(hdr);
|
||||||
g_rc_free_count++;
|
ailang_ctx_t *_ctx = __ail_tls_ctx;
|
||||||
|
if (_ctx != NULL) _ctx->free_count++; else g_rc_free_count++;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user