09 — TOCTOU / control_epoch Review (SUPERTRACK I)

Source: 08-control-epoch-toctou-spec.md.

#	Requirement	Spec answer	Verdict
I.1	control_epoch storage	exactly one qt001_cp.control_epoch row, owned by NOLOGIN owner	PASS
I.2	increment events	enumerated: activation/rollback, principal/evidence revoke, owner/ACL cutover/rollback, writer/gateway/readiness repoint, scheduler/verifier authority change, protected source/target/entrypoint change	PASS (explicit list)
I.3	writer reads epoch at start	writer txn locks row FOR SHARE, captures epoch + control + manifest hashes	PASS
I.4	writer checks epoch before commit	rereads/asserts epoch+hashes before commit	PASS (the actual TOCTOU closure — explicit)
I.5	activation lock specified	activation/cutover locks FOR UPDATE	PASS
I.6	activation writes epoch	applies atomically, recomputes hashes, increments epoch	PASS
I.7	stale epoch fails	race/stale/mismatch tests required; reread mismatch aborts	PASS
I.8	evidence binds epoch	evidence/approval bound to epoch; post-activation verifier required	PASS
I.9	rollback behavior	rollback never decrements epoch	PASS

Adversarial probes

• Deadlock risk between FOR SHARE (writer) and FOR UPDATE (activation)? Single-row lock, consistent acquisition order (both lock the one epoch row first) → no lock-ordering cycle. FOR UPDATE waits for FOR SHARE holders; writer's reread-before-commit then observes the new epoch and aborts. Sound, low deadlock risk (doc 15 feasibility).
• Can a writer commit on a stale set? No — FOR SHARE is held for the whole writer txn and epoch+hashes are reread/asserted before commit; if activation advanced the epoch, the writer aborts. Closes the prior-round "lock-hold scope / pre-commit predicate unspecified" gaps.
• Is post-activation evidence epoch-bound? Yes — evidence binds epoch and a fresh verifier is required within 15 min; readiness stays false until then. Closes the prior-round "fresh evidence not epoch-bound" gap.

Verdict: CONTROL_EPOCH_SPEC_COMPLETE

The control_epoch protocol is concretely and correctly specified (single owner row, enumerated increments, FOR SHARE/FOR UPDATE, reread-before-commit, epoch-bound evidence, no-decrement). No writer/activation race in the design. Implementation check (doc 15): a concurrency test harness proving stale-epoch abort + no deadlock.