Races, deadlocks, and lost updates resist normal debugging because the failure depends on interleaving, not input. Extended-reasoning models are unusually good at systematically enumerating interleavings across two or three code paths — the mental simulation humans do badly under fatigue.
Tier: Advanced · Workflow area: Debugging & Performance
The discipline: the model proposes the interleaving, you encode it as a deterministic or statistical stress test, and only a reproducing test counts as a diagnosis.
pytest + threads/asyncio.gather, Go's -race detector, JCStress (JVM), or a small script hammering two connections at a DB.Assemble the minimal concurrent world. Extract every code path that reads or writes the shared state into one paste — not the whole service. Include the infrastructure semantics, which decide everything:
Context: two uvicorn workers, Postgres, isolation level READ COMMITTED.
Path A (HTTP handler): get_balance(); if balance >= amount: debit(amount)
Path B (webhook consumer): credit(amount) in its own transaction
[full code of both paths + the transaction decorator pasted here]
Ask for exhaustive interleaving analysis, not a verdict.
Enumerate the interleavings of Path A and Path B that can violate the
invariant "balance never goes negative". For each candidate:
- Number each atomic step (S1, S2, ...) in both paths first.
- Show the schedule as an ordered step list (A:S1 -> B:S1 -> A:S2 ...).
- State the resulting bad state and WHY the isolation level / lock / GIL
does not prevent it.
- Mark it POSSIBLE or IMPOSSIBLE under the stated runtime semantics, with
the rule that makes it impossible.
Think step by step through the memory/transaction semantics; do not stop
at the first bug found.
The POSSIBLE/IMPOSSIBLE column with cited semantics is where reasoning models earn their cost — and where you audit them, because they sometimes forget the GIL, connection pooling, or that READ COMMITTED rereads within a transaction.
Audit the winning interleaving by hand. Take the single most plausible schedule and walk it yourself against the actual code, line by line. Check the model's semantic claims: is that read really outside the transaction? Is that check-then-act really two separate awaits? If you cannot follow the schedule, the diagnosis is not usable regardless of correctness.
Encode the interleaving as a test. Ask the model to generate a stress test that forces or statistically provokes the schedule:
async def test_concurrent_debit_credit_never_negative():
await set_balance(account_id, 100)
# 50 concurrent debit(30) attempts racing 50 credit(10)s
results = await asyncio.gather(
*[debit(account_id, 30) for _ in range(50)],
*[credit(account_id, 10) for _ in range(50)],
return_exceptions=True,
)
assert await get_balance(account_id) >= 0
assert successful_debits(results) * 30 <= 100 + 50 * 10
For finer control, inject sync points (an Event the test controls, a sleep(0) at the suspected boundary) so the bad schedule happens every run, not one in ten thousand. On the JVM use JCStress; in Go run the scenario under go test -race -count=100.
Fix, then prove the fix with the same test. The test must fail reliably before the fix and pass after (run it 100+ iterations both times). Then ask the model to re-run the interleaving enumeration against the fixed code — a common outcome is the fix (e.g., SELECT ... FOR UPDATE) introducing a new deadlock schedule, which the model should catch in round two.
An interleaving analysis without a reproducing test is a plausible story, not a diagnosis. Models produce convincing but wrong schedules; the stress test is the only referee.
grep for every call site touching accounts.balance) and run the stress loop repeatedly — useful because assembling the minimal world is half the work.-race, ThreadSanitizer) are clean after the fix where the toolchain supports them.sleep(0.1) schedules rot into flakiness. Prefer controlled sync points or detector tooling; keep statistical tests at high iteration counts in a separate slow suite.transfer_funds → op_a) and business context removed — interleaving logic survives sanitization almost perfectly.go test -race, TSan, JCStress) and the stress-test loop are fully local; in no-external-LLM environments, do the enumeration on a whiteboard using the same numbered-step + schedule format — the format is the transferable skill.