From 95e6d8b698d2165b4455b68c419a3709c8f0901e Mon Sep 17 00:00:00 2001 From: Jongsun Suh Date: Fri, 31 Jul 2026 06:46:39 -0400 Subject: [PATCH 1/4] Add `race-condition-proof` skill for ordering guarantees under concurrency The falsifier for a concurrency claim is a test that never interleaved: a sequential run exercises no race and produces a green indistinguishable from a real pass. The skill therefore treats showing the interleaving occurred as the proof obligation, not the assertion passing. Lands in `stability/` beside `memory-leak-hunt`, the other defect-class engine `pr-validate` delegates to. --- .../skills/race-condition-proof/skill.md | 110 ++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 domains/stability/skills/race-condition-proof/skill.md diff --git a/domains/stability/skills/race-condition-proof/skill.md b/domains/stability/skills/race-condition-proof/skill.md new file mode 100644 index 0000000..3ff6d2d --- /dev/null +++ b/domains/stability/skills/race-condition-proof/skill.md @@ -0,0 +1,110 @@ +--- +name: race-condition-proof +description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /race-condition-proof, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by pr-validate as the engine behind its B7 deterministic-interleaving evidence category, and named by falsifying-test as its sibling for ordering bugs. +maturity: experimental +--- + +# /race-condition-proof + +A race is nondeterministic in the wild, so you cannot validate "the stale retry was canceled" by +running the code and hoping the interleaving occurs. The evidence has to **make the race +deterministic** — force the exact interleaving, then assert the outcome. + +The claim shape is distinctive: not a value, not a behavior, but an *ordering guarantee*. "When a +newer write supersedes a pending retry, the stale retry is dropped." No screenshot, benchmark, or +value assertion touches that. + +> **Falsifier.** A test that never interleaved. If the operations ran to completion in sequence, +> no race was exercised and the green is vacuous — and it looks identical to a real pass. The +> proof obligation is to show **the interleaving happened**, not that the assertion passed. + +This is the reward-hack specific to the category, and it is easy to write by accident: `await` +the first operation, then start the second, then assert. Every assertion passes. Nothing was +tested. + +## Method + +1. **State each guarantee separately, in interleaving terms.** Not "retries work" but "when B + arrives during A's pending window, A's recovery event does not fire." One sentence per + guarantee, each naming the arriving operation, the window, and the expected outcome. + + **Asymmetric guarantees are usually the crux.** Two paths that deliberately behave differently + — a primary retry that *is* cancelable by a newer write, a backup retry that is *not* because a + split write could leave backed-up keys stale — need one forced interleaving each. A harness + that proves the symmetric half and assumes the other has proven the easy one. + +2. **Force the interleaving.** Control time and ordering rather than waiting for them: + + | technique | purpose | + |---|---| + | `jest.useFakeTimers()` + `advanceTimersByTimeAsync(DELAY)` | fire the delayed action at a known point | + | `Promise.all([opA, opB])` | overlap operations rather than sequencing them | + | `advanceTimersByTimeAsync(0)` | step to a precise interleaving point between overlapping ops | + + The shape that matters: launch A, advance time *into* its pending window, inject B *during* + that window, then assert. Never `await opA` before starting `opB`. + +3. **Verify the interleaving before believing the assertion.** This is step 2's trust-gate and it + is not optional — confirm time was advanced into the pending window and the superseding op was + launched concurrently. Reading the assertion tells you nothing; a sequential test asserts the + same things and passes. + + The cheap check: **break the implementation and confirm the test fails.** Revert the ordering + logic, keep the test file byte-identical, re-run. A test that still passes never exercised the + race. Show both runs — that mutation pair is the evidence, not the green run alone. + +4. **Assert the negative side explicitly.** Cancellation guarantees are proven by absence: + `expect(recoveryEvent).not.toHaveBeenCalled()`. A suite that only asserts things happened + cannot detect a stale operation that ran when it should have been dropped. Pair every + "must complete" (`.toHaveBeenCalledWith(...)`) with its "must not" counterpart. + +5. **Corroborate the integration path if the claim reaches beyond the unit.** The deterministic + harness is a *model* — exhaustive and fast, but a model. For a high-stakes claim, add one live + forced-race capture in the real runtime (CDP/injection, the force-the-unobservable technique) + to show the race exists where the model says it does. Unit harness for coverage, live capture + for reality; use both when the cost of being wrong is high. + +6. **Report transition telemetry with enough labeling to distinguish branches.** `retry-recovered` + is ambiguous when there are two retry paths; `set-retry-recovered` vs + `set-backup-retry-recovered` is not. If the observable can't tell the branches apart, it can't + witness an asymmetric guarantee. + +## Output + +``` +Ordering guarantees — + +| guarantee | forced how | assertion | result | +|---|---|---|---| +| B during A's window cancels A | advance , inject B via Promise.all | recovery .not.toHaveBeenCalled() | pass | +| backup completes despite newer write | advance , inject B | .toHaveBeenCalledWith(...) | pass | + +Interleaving verified: +Mutation check: → , test file unchanged +Live corroboration: | not run +``` + +Lead with the guarantee table — one row per guarantee, each naming how the interleaving was +forced. A row without a forcing mechanism is a sequential test wearing the category's clothes. +Report the mutation pair (head green / reverted red) as the evidence that the harness discriminates. + +## Scope — what this is NOT + +- **Not the generic falsifying test.** These *are* falsifying tests, but the category is the + *technique* (forced deterministic interleaving) and the *claim shape* (ordering, not values). + `falsifying-test` names this skill as its sibling for ordering bugs; use that one when the claim + is a value or a behavior and the base/head arms are the whole story. +- **Not flake diagnosis.** A test that fails intermittently is a different problem from a + guarantee that needs proving. Determinism here is the *method*, not the goal. +- **Not performance under load.** Throughput and contention are timing questions; this is about + ordering correctness at a specific interleaving. + +## Notes + +Correctness of the *reasoning* about a race is not something to assert from reading. Where the +guarantee depends on runtime semantics — what an `AbortController` actually cancels, whether a +microtask runs before a timer callback — cite the behavior or demonstrate it in the harness rather +than describing it. + +Engine for `pr-validate` category **B7 (deterministic interleaving)**; the full category note +lives at `exogram-daemon/artifacts/evidence-taxonomy/category-concurrency-temporal-ordering.md`. From 81dcf484656b0d01285a411286451a6daa631cfd Mon Sep 17 00:00:00 2001 From: Jongsun Suh Date: Fri, 31 Jul 2026 10:20:19 -0400 Subject: [PATCH 2/4] fix(race-condition-proof): name the evidence category instead of indexing it The description read "the engine behind evidence's B7 deterministic-interleaving evidence category". "B7" is an address into evidence-catalog.md, not a name: it carries no meaning to a reader who has not opened the catalog, and a frontmatter description cannot link out to one. - Drop the lane id from the description; name the role instead. - Replace the trailing Notes reference with a Related section that links the catalog by URL. A relative path would not survive installation, which flattens skills to mms-/. - Drop the exogram-daemon path, which is a private repo the reader cannot open. - Update the stale pr-validate name to evidence. --- .../stability/skills/race-condition-proof/skill.md | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/domains/stability/skills/race-condition-proof/skill.md b/domains/stability/skills/race-condition-proof/skill.md index 3ff6d2d..5c8b790 100644 --- a/domains/stability/skills/race-condition-proof/skill.md +++ b/domains/stability/skills/race-condition-proof/skill.md @@ -1,6 +1,6 @@ --- name: race-condition-proof -description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /race-condition-proof, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by pr-validate as the engine behind its B7 deterministic-interleaving evidence category, and named by falsifying-test as its sibling for ordering bugs. +description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /race-condition-proof, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by `evidence` as its deterministic-interleaving engine, and named by `falsifying-test` as its sibling for ordering bugs. maturity: experimental --- @@ -106,5 +106,12 @@ guarantee depends on runtime semantics — what an `AbortController` actually ca microtask runs before a timer callback — cite the behavior or demonstrate it in the harness rather than describing it. -Engine for `pr-validate` category **B7 (deterministic interleaving)**; the full category note -lives at `exogram-daemon/artifacts/evidence-taxonomy/category-concurrency-temporal-ordering.md`. +## Related + +- `evidence` — this skill is its deterministic-interleaving engine: `evidence` decides that a + concurrency claim needs an interleaving proof, and calls here to produce one. The category note + is [`deterministic interleaving` in the evidence catalog](https://github.com/MetaMask/skills/blob/main/domains/pr-workflow/skills/evidence/references/evidence-catalog.md). + A relative path would not survive installation — skills flatten to `mms-/`, so a link + out of one skill into another only resolves as a URL. +- `falsifying-test` — the sibling engine for ordering bugs that reproduce without a forced + interleaving. From 6a9343423cace346504e9daae3cf40ef1a42b4ba Mon Sep 17 00:00:00 2001 From: Jongsun Suh Date: Fri, 31 Jul 2026 11:53:15 -0400 Subject: [PATCH 3/4] Rename `race-condition-proof` to `race-condition-repro` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit As a noun suffix, `-proof` is privative in English — waterproof, bulletproof, tamper-proof all mean "immune to". So `race-condition-proof` parses as "immune to race conditions" rather than "produces a proof about ordering", and that misreading is plausible enough not to self-correct. `-repro` names what the harness produces and carries no such inversion. --- .../{race-condition-proof => race-condition-repro}/skill.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) rename domains/stability/skills/{race-condition-proof => race-condition-repro}/skill.md (98%) diff --git a/domains/stability/skills/race-condition-proof/skill.md b/domains/stability/skills/race-condition-repro/skill.md similarity index 98% rename from domains/stability/skills/race-condition-proof/skill.md rename to domains/stability/skills/race-condition-repro/skill.md index 5c8b790..47b8de1 100644 --- a/domains/stability/skills/race-condition-proof/skill.md +++ b/domains/stability/skills/race-condition-repro/skill.md @@ -1,10 +1,10 @@ --- -name: race-condition-proof -description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /race-condition-proof, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by `evidence` as its deterministic-interleaving engine, and named by `falsifying-test` as its sibling for ordering bugs. +name: race-condition-repro +description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /race-condition-repro, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by `evidence` as its deterministic-interleaving engine, and named by `falsifying-test` as its sibling for ordering bugs. maturity: experimental --- -# /race-condition-proof +# /race-condition-repro A race is nondeterministic in the wild, so you cannot validate "the stale retry was canceled" by running the code and hoping the interleaving occurs. The evidence has to **make the race From 43b5e920d05b6463f655b5665ebae790b90d2dbc Mon Sep 17 00:00:00 2001 From: Jongsun Suh Date: Tue, 4 Aug 2026 08:01:24 -0400 Subject: [PATCH 4/4] Name the installed command in `race-condition-repro`'s description The installer emits `mms-race-condition-repro`; the description advertised `/race-condition-repro`. --- domains/stability/skills/race-condition-repro/skill.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/domains/stability/skills/race-condition-repro/skill.md b/domains/stability/skills/race-condition-repro/skill.md index 47b8de1..72cf2ca 100644 --- a/domains/stability/skills/race-condition-repro/skill.md +++ b/domains/stability/skills/race-condition-repro/skill.md @@ -1,6 +1,6 @@ --- name: race-condition-repro -description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /race-condition-repro, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by `evidence` as its deterministic-interleaving engine, and named by `falsifying-test` as its sibling for ordering bugs. +description: Prove an ordering guarantee under concurrency — that when B arrives during A's pending window, A is canceled, or completes first, or the two commit in a defined order. Covers race conditions, retries, cancellation, supersession, debounce/throttle, locks, queues, and async state machines, where correctness IS the interleaving rather than a value. Builds a deterministic interleaving harness (fake timers advanced into the pending window, concurrent launch, microtask stepping) and asserts each guarantee separately, including asymmetric ones where two paths deliberately differ. The falsifier is a test that never interleaved — operations run to completion in sequence exercise no race and produce a vacuous green indistinguishable from a real pass, so the proof obligation is to show the interleaving occurred, not that the assertion passed. Triggers on /mms-race-condition-repro, or when asked to prove a race condition is fixed, test cancellation or supersession, validate retry or debounce ordering, write a deterministic interleaving test, or check whether a concurrency test actually exercises the race. Callable by `evidence` as its deterministic-interleaving engine, and named by `falsifying-test` as its sibling for ordering bugs. maturity: experimental ---