BFM-decomp/docs/concurrency-design.md

# Concurrency Contract — overlapping draft / gate / propagate / R22 without weakening the byte-gate

**Status:** design (P30), authored by a Fable-5 planning pass 2026-08-07. **Not yet implemented.**
**Scope:** the pipeline around `tools/gate_stage.py`, `tools/bulk_harvest.py`,
`tools/harvest_verify.py`, `tools/dedup_propagate.py`, `tools/wave_snapshot.py`, and the R22
clean-fleet verify.

**The one-sentence contract:** a byte-gate verdict is a property of a *(draft, tree-state)* pair;
concurrency is sound exactly when (1) no other actor writes any element of a gate's read-set while
that gate runs, and (2) the terminal claim ("matched") is only ever published for a **commit**
whose own clean R22 passed — because the R22 at a frozen state re-derives everything and is
therefore immune to every race that happened before it.

---

## 1. Resource / conflict map

Fleet today: ~213 binaries (main + resident + `OVERLAY_BINARIES` + `MODULE_BINARIES`,
`Makefile:54-59`). "Gate(b)" = `gate_stage.run_gate` → `harvest_verify` for binary *b*; "Prop" =
`dedup_propagate`; "Draft" = an agent wave + `match_one`; "R22" = `make clean && make extract-all
&& make check-all`.

| Resource | Read by | Written by | Notes |
|---|---|---|---|
| `asm/<bin>/**` (regenerated, gitignored) | Gate(b) via `INCLUDE_ASM` `.include`; Draft (or its snapshot); `match_one` | `make extract BINARY=b` (Gate(b)'s jtbl prep, `harvest_verify.py:344,404,419`); R22's `extract-all`; **deleted whole by `make clean`** (`Makefile:842`) | Per-binary disjoint. Waves already decoupled via `wave_snapshot.py` (immutable sha1-manifested copy). |
| `src/<bin>/*.c` | Gate(b) (splice base, `harvest_verify.py:178-214`); Prop (member sites); Draft (ambient-decl context, read-only); `OBJS` glob at build parse | Gate(b) (splice/revert, jtbl carve region files); Prop (stub→`DEFINE_…()` rewrites, fleet-wide) | Per-binary disjoint **between gates**; Gate(b) vs Prop genuinely conflict on every member overlay. |
| `src/shared/engine_core.h`, `engine_types.h` | **every** binary's build (via `common.h`) | Prop (`dedup_propagate` macro author); **and — contrary to `bulk_harvest.py:16-17`'s isolation claim — the arity pre-pass inside every gate** (`gate_stage.py:316-335` → `fix_arity_callers.py:39`) | **Finding F1**: phase-B parallel workers each run the arity pre-pass unless `GATE_NO_ARITY` is set, and bulk_harvest does **not** set it. Two workers can concurrently edit + journal-undo the fleet-shared header. |
| `config/overlays.mk`, `config/splat.<bin>.yaml` | every build parse; corpus | Gate(b)'s jtbl prep (`jtbl_carve`/`jr_isolate_all`, snapshotted at `harvest_verify.py:305-310`); onboarding tools | **Finding F2**: `config/overlays.mk` is **one shared file**; two concurrent binaries' jtbl preps race on it, and each restores *its own* snapshot — a lost update on the other's carve. |
| `include/*.inc`, `include/include_asm.h` (generated) | every compile | `make extract` for **any** binary (identical content; `Makefile:762-764` — extract-all seeds them via main serially for exactly this reason) | Concurrent re-writes are content-identical but **tearable**: a reader mid-write gets a truncated macro file → spurious CC1-FAIL (never a false pass — see §2). |
| `build/{src,asm}/<bin>/**`, `build/<bin>/*` | Gate(b) link/check; asm-differ | Gate(b); Prop's per-member `make build` (`dedup_propagate.py:343`); R22 | Per-binary disjoint (`Makefile:757-765`). Prop's write-set spans **many** `build/<bin>` dirs ⇒ conflicts with any concurrent gate. |
| `expected/**` | asm-differ | operator `make expected` (`Makefile:827-837`); deleted by `make clean` | Off the hot path. |
| `config/check.<bin>.sha` | Gate(b) (`gate_stage.py:205`), `make check` | **nobody** during operation | Load-bearing: the only false-bank vector (§2.1). Add a cheap guard. |
| `config/dedup.us.yaml` | `_dedup_group_count`, `dedup_integrate --check` | Prop only (`dedup_propagate.py:315`) | Serial-lane only. |
| git index / worktree | everything | `gate_stage.py:481-495`, `bulk_harvest.git_commit` | Single-writer: `sh()` swallows a `git add` loser of an `index.lock` race → silently short commit (R32 class). |
| `.run` scratch | many | `match_one` (private per-pid, `match_one.py:30-52`); per-binary verified/failed (`gate_stage.py:517-525`); `.run/auto/bulk/*` (cleared wholesale, `bulk_harvest.py:209-210`) | One bulk/sweep driver at a time. |
| `.run/auto/gate[.<bin>].lock` | — | flock at `gate_stage.py:181` | Per-binary when `lock_path` passed; global otherwise. `harvest_verify` invoked **directly** takes no lock. |

**Genuinely conflicting pairs:** Gate(b) ∥ Gate(b) · Gate(*) ∥ Prop · Gate(*) ∥ Gate(*) when
either runs a shared-state stage (F1, F2, extract's include seeding) · anything ∥ `make clean` in
the same tree · two committers.

**Non-conflicting (the free parallelism):** Draft ∥ everything · Gate(b₁) ∥ Gate(b₂) with
shared-state stages disabled · main tree ∥ verify worktree.

---

## 2. The correctness argument (can any of this cause a FALSE BANK?)

### 2.1 The structure that makes the oracle race-proof

1. **The verdict compares against an immutable constant.** `make check` compares the built image's
   SHA1 against `config/check.<bin>.sha` (`Makefile:811-823`) — the hash of the *original retail
   bytes*, written once at onboarding, written by no pipeline stage. `INCLUDE_ASM` pastes the
   original assembly, so a wrong draft always changes some bytes (`harvest_verify.py:173-177`).
2. **The terminal R22 re-derives everything from the state it certifies.** `make clean` deletes all
   derived state (`Makefile:841-844`); `extract-all` structurally invalidates objects
   (`Makefile:571-590`); `check-all` asserts coverage, not absence-of-failure (`Makefile:801-807`).

⇒ **For a wrong draft to be *terminally* accepted, a clean rebuild of the final claimed state would
have to reproduce the original bytes with wrong C in the tree — contradicting (1).** No interleaving
of earlier stages can manufacture that. Races produce only false *failures*, wasted drafts, dirty
intermediate trees, and **verdict decay** — all fail closed at the terminal R22, loudly.

The one surviving false-bank vector is corruption of the comparison constant itself: a write to
`config/check.<bin>.sha`, or `--good-sha` pointing at the wrong hash (the Bug-A/DEF_SHA family,
`gate_stage.py:536-546`). No stage writes these; Stage 1 adds a guard asserting they are clean vs HEAD.

### 2.2 The four required sub-questions

**(a) Target staleness — draft authored against T, gated against T′.** *Sound.* The verdict is
computed entirely at T′. A stale draft can only fail to bank. Staleness is a **throughput**
variable, never a soundness one.

**(b) Concurrent propagation changing a TU's ambient declarations.** *Between* draft and gate: same
as (a), sound. *During* the gate's build: the real hazard. A mid-build write to `engine_core.h` or a
member `.c` can tear a read (fail-to-bank, safe) **or** let the gate compute a verdict true of a
**transient** tree state that will never exist again — **verdict decay**. It cannot put wrong bytes
into a green terminal state, but it mints a bank whose C is not byte-correct against the committed
state; the commit then fails R22 and someone bisects a batch that "all gated green." So Gate ∥ Prop
stays **mutually exclusive** — for verdict *hygiene*, not byte-gate soundness. Mechanism: every gate
holds `.run/auto/shared_state.lock` **SHARED**; propagation, `fix_arity_callers --apply`, and any
jtbl config edit hold it **EXCLUSIVE**. F1 and F2 must be closed for the same reason: in parallel
mode gates run `GATE_NO_ARITY=1` and **defer** (not drop — R32: report a `deferred:` count)
jtbl/arity drafts to the serial lane. Stage 0 (`gate_stage.py:222-247`) already banks byte-correct
drafts with no transforms, so the parallel lane keeps most of its yield.

**(c) `compute_fleet=False` workers vs the serial fleet metric.** *Sound*, already correct
(`bulk_harvest.py:81`, `sweep_parallel.py:22`). Fleet % is telemetry parsed from a moving tree, never
an input to accept/reject. A racy value causes a false **number** (an R32 defect in its own right),
not a false bank. Rule: workers never compute it; the serial lane computes it once, post-commit.

**(d) Can a worktree clean-verify certify the MAIN tree?** **Only its own checked-out commit — and
that is the correct object to certify.** Green at commit C proves *"a pristine checkout of exactly
C's tracked content rebuilds all ~213 binaries byte-identical."* Consequences:
- Claims attach to commit SHAs, never to "the tree": *"R22 213/213 at `<sha>`"*.
- **This is strictly stronger than current practice.** A main-tree R22 verifies the working state
  including untracked files — the `OBJS` glob compiles any stray `src/<ov>/*.c` — so main-tree green
  does **not** certify the commit. Documented at `gate_stage.py:483-491`: `git add -u` cannot stage
  created files, and "a clone of such a bank commit failed to build." The worktree verify detects
  omitted-from-commit files by construction.

**Verdict:** none of the proposed concurrency admits a false bank, **provided** (i) the shared-state
RW lock is honored, (ii) claims are published only per R22-verified commit, (iii)
`config/check.*.sha` stays unwritten. **Dropped idea:** overlapping propagation with gating on
"non-member" binaries — the arity-reconcile path (`dedup_propagate.py:350-359`) can widen the
write-set mid-run (the half-propagated-fleet incident, `gate_stage.py:377-396`); a write-set that can
grow during the run cannot be safely partitioned. Propagation stays globally exclusive.

---

## 3. Recommended architecture — four lanes

- **Lane D — draft (wave N+1), always-on.** Drafts against a `wave_snapshot`, writes only
  `.run/<wave>/`, `match_one` in private per-pid scratch. No locks. Overlaps **everything**.
- **Lane G — parallel gate (wave N).** `bulk_harvest` phase-B / `sweep_parallel` farm verbatim
  (ProcessPool over **distinct** binaries, per-binary lock, per-worker paths,
  `propagate=False, commit=False, compute_fleet=False`) **plus**: hold `shared_state.lock` SHARED;
  `GATE_NO_ARITY=1`; jtbl/arity drafts deferred-and-reported to lane P.
- **Lane P — serial integrate.** Holds `shared_state.lock` EXCLUSIVE. (1) re-gate the deferred queue
  with the full ladder; (2) `dedup_propagate --auto-from` per banking binary; (3) merge backlogs,
  fleet %, **one** commit.
- **Lane V — verify worktree.** Async clean R22 at the latest committed SHA. Green ⇒ publish claims
  (`r22/<shortsha>` tag + `.run/verify/<sha>.json`). Red ⇒ **stop-the-line**.

**Overlap matrix:** D ∥ {G,P,V} ✓ · G ∥ V ✓ · G ∥ P ✗ · P ∥ V ✓ · G(b) ∥ G(b) ✗ · two P ✗ · two V: queue.

**Where `bulk_harvest` already suffices:** phase separation, per-binary locks, per-worker scratch,
round-robin spread, serial commit, resumable tried-set. **Where it falls short:** (1) phase A welded
to local-LLM drafting → extract phases B+C into a shared `gate_farm` module; (2) its isolation
*claim* (`bulk_harvest.py:15-17`) is stale against F1/F2 — true only after Stage 1; (3) no
cross-cycle pipelining; (4) no verify integration.

---

## 4. The verification worktree

**Mechanism.** `tools/verify_worktree.py`: `git worktree add ../bfm-verify <sha>`, provision the
untracked build deps — cc1 from the **committed** tarball verified against
`tools/bin/CHECKSUMS.sha256`; `.venv` (symlink acceptable, read-only at build time);
`git submodule update --init tools/maspsx` (verify `git submodule status` clean — `.gitmodules` has
`ignore = dirty`). Then `make extract-all && make check-all`, writing `.run/verify/<sha>.json`.

**Soundness.** Green certifies **commit C**, full stop. The oracle is output bytes, not the
toolchain: a "wrong" cc1 that still reproduces the bytes does not invalidate a match; one that diffs
produces a false **failure** — hence the checksum preflight (R35). Sparse-checkout excluding
`ghidra/`, `dumps/`, `datasets/` is safe **fail-closed only** (an excluded load-bearing file can only
shrink `OBJS` and diff the image); validate once against a full checkout at the same SHA (R34).

**Cost.** ~1.1 GB sparse. Warm-up: full `extract-all` per verified SHA. **Needs measuring** at 213
binaries with lane G contending for cores.

**Sync.** Verifies **coalesce** — R22 verifies *states, not deltas*, so verifying the newest SHA
certifies the cumulative state. The main tree never runs `make clean` during operations again.

**What green licenses, verbatim:** *"Commit `<sha>`: clean-fleet 213/213 byte-identical from a
pristine checkout; every non-stub function in `<sha>` is matched (G3/P9). No claim about any later
commit or any working tree."*

---

## 5. New silent-failure classes and their detectors

| # | Class | Detector |
|---|---|---|
| 1 | Shared-header mid-air edit during parallel gates (F1) → verdict decay | RW flock + `GATE_NO_ARITY`; **bracketing assertion**: `git status --porcelain src/shared config` identical before/after phase G (R32); backstop = lane V |
| 2 | jtbl config lost-update (F2) | Defer jtbl drafts out of G; `jr_inventory`'s 1:1 ownership assertion as second oracle (R34) |
| 3 | Torn `include/*.inc` → spurious CC1-FAILs booked as walls, poisoning the backlog | R35: any CC1-FAIL naming a generated include gets ONE serial re-probe before a backlog record is written. Deferring jtbl prep removes the only in-G `make extract` |
| 4 | Commit-vs-claim skew: totals published from an unverified commit | Report tooling prints the last `r22/<sha>` tag + a loud `UNVERIFIED: N commits ahead` |
| 5 | Double-gating one binary from two drivers | Per-binary flock + per-binary result paths; extend the flock to direct `harvest_verify` invocations |
| 6 | Worktree provenance drift (stale submodule / wrong cc1) → false failures | Checksum + `submodule status` preflight; provenance in the verdict JSON; a red with bad provenance is an instrument failure (R35) |
| 7 | Silent shrink/widen of the parallel input set (deferred drafts vanishing) | R32: `drafts == banked + near + failed + deferred`, and lane P consumes exactly the deferred list |

---

## 6. Staged implementation plan

**Stage 1 — close F1/F2 and land the RW lock (pure safety; makes today's phase-B claim true).**
`shared_state.lock` (SH in `run_gate`; EX in `dedup_propagate`, `fix_arity_callers --apply`, lane-P
gates); parallel callers set `GATE_NO_ARITY` and `defer_shared=True`.
*Negative controls:* (a) with a gate holding SH, `dedup_propagate` with `LOCK_NB` must refuse loudly
naming the holder; (b) a known arity-needing draft gated in parallel mode must come back `deferred`,
then bank serially; (c) R22 unchanged 213/213.

**Stage 2 — `tools/verify_worktree.py` (lane V).** Sparse first run validated against one full
checkout. *Negative control:* a throwaway commit splicing a known-wrong draft must go red naming
exactly its binary; then delete the commit. Proves the detector fires before any green is trusted.

**Stage 3 — the wave dispatcher (formalize D∥G).** Generalize `split_drafts_by_binary`; extract the
shared `gate_farm`. *Control + measurement:* run a wave while a worktree R22 and one propagation run
mid-wave; assert manifest coverage (R32) and compare bank-rate against a quiet-tree control (R34).

**Stage 4 — pipelined loop + claim ledger.** Publish claims only on green. *Negative control:* kill
the loop between P's commit and V's green; on restart it must refuse to publish and re-enqueue.

**Stage 5 (measure first) — verify coalescing + auto-bisect on red.**

---

## 7. Explicit uncertainties (probes, not assertions)

- R22 wall-clock at 213 binaries in the worktree, with/without a concurrent gate farm.
- Arity/jtbl incidence in cheap-tier waves (sizes lane P's serial tail): count `PLUMBING`-arity +
  jtbl classes in `.run/backlog.jsonl` over recent waves.
- Staleness cost of D∥P: the Stage-3 A/B bank-rate comparison. If real, re-snapshot ambient decls at
  staging time — a throughput fix, never a soundness one.
- `git worktree` + submodule + sparse-checkout interplay on this git version — a 10-minute dry run.
- Whether any current wave prompt reads live `asm/` instead of a snapshot; Stage 3 should assert
  snapshot-only inputs (the manifest makes this checkable).