Thread Interleaving Explorer

A data race is not a bug that happens; it is a bug that can happen. This tool settles the question by brute force: it runs every interleaving of the threads' instructions and collects the complete set of reachable results, together with how many interleavings lead to each one.

Why the programs look so low-level. x = x + 1 is not one step. It is a load, an addition and a store, and another thread can run in between. So loads and stores are written out explicitly: r1 = x reads the shared variable into a thread-local register, x = r1 writes it back. Registers are private to each thread; anything else is shared.

Instruction set

• r1 = x — load a shared variable
• x = r1 / x = 5 — store a register or a constant
• r1 = 5, r1 = r2, r1 = r1 + 1 (also - and *, with a register or a number on the right)
• lock(m) / unlock(m) — a mutex named m; a thread blocks while another holds it
• wait(ready == 1) — block until the condition on a shared variable holds (also !=, <, >, <=, >=)

Initial values go in the init field as x = 0, ready = 0. Anything not listed starts at 0. Lines after // are comments.

Reading the verdicts. An outcome is marked expected when some sequential order of whole threads produces it — that is what a programmer who ignores concurrency has in mind. Everything else is marked a race: only interleaving produces it. Deadlock means no thread could take another step while some still had work left.

The scenarios

• Lost update — two threads increment the same counter. Only 2 of the 20 interleavings end at x = 2: the two where one thread finishes completely before the other starts. In the other 18 an increment is lost. On real hardware the timing is nowhere near uniform, so the same code usually looks correct in testing and fails in production.
• Counter with a mutex — the same code inside lock/unlock. The bad interleavings become unreachable and only x = 2 remains.
• Broken publication — the flag is set before the data. A reader that waits for the flag can still read stale data.
• Correct publication — data first, then the flag. Now the reader always sees 42.
• Lock-order deadlock — one thread takes a then b, the other b then a. Some interleavings reach a state where both wait forever. Take the locks in the same order and it goes away.
• Three concurrent withdrawals — three threads each take 30 from a balance of 90. Run one after another the balance ends at 0; interleaved, the most likely single outcome by far is 60, as if two of the three withdrawals never happened. The same read-modify-write hazard as the counter, but with money.

What is modelled and what is not. Execution is sequentially consistent: every thread sees one global order of memory operations. Real CPUs and compilers are weaker — store buffering, load/store reordering and register caching create outcomes that cannot appear here (the classic “both read 0” in Dekker's example is one). So this tool proves a race exists; it can never prove code is safe on real hardware. There are no loops, branches, function calls, atomics or memory fences, and the state space is capped at 80,000 interleavings.