Thread Interleaving Explorer

Explore every permitted schedule of two or three short programs under sequential consistency. Choose an example, edit initial values or thread programs, then Explore. Editing clears old results. The lost-update example has 20 schedules: x=1 in 18, x=2 in 2. A mutex makes the read–increment–write sequence exclusive.

One instruction per line: r1 = x loads a shared variable, x = r1 stores a local register, x = 5 assigns a shared integer, r1 = r1 + 1 calculates in a local register. Addition, subtraction and multiplication accept integers or variable/register names. lock(m) waits for an unowned mutex; unlock(m) requires ownership. wait(x == 1) blocks until its shared-variable comparison is true; !=, <, >, <= and >= also work. Names are case-insensitive; r followed by digits is thread-local, other names shared. Uninitialized values are zero. Initial values use x = 0, y = 1; duplicate names are rejected. // starts a comment.

Results include shared values and every local register. Schedule share counts enumerated paths, never real-world timing probabilities. Thread order means the same result is possible by completing each thread in turn; Interleaved means it needs instruction interleaving. Neither label proves the presence or absence of a data race. Blocked means unfinished threads have no enabled next action, which may be a lock-order deadlock or an unsatisfied wait. Trace opens one actual witness and its intermediate global and local values.

Limits: 18 instructions total, 80,000 schedules before mutex/wait restrictions, 4,096 characters per input and 64 per name. Integers and calculations must stay within ±9,007,199,254,740,991. This local exhaustive teaching model excludes loops, real timing, compiler reordering, atomics and weak memory. Try broken versus fixed publication: writing ready before data permits reading 0; reversing the writes permits only 42.

Enumeration runs in a local worker so the page stays usable. The activity bar has no percentage: mutexes and waits can end paths early. The count is explored terminal schedules; Cancel stops the worker and keeps the inputs. Editing or leaving also stops it and discards late replies. The filter matches shared/register values, ignoring case; space-separated search terms must all match. Initial values not referenced by any thread appear once in Unused initial values and are omitted from repeated outcome/trace cells.

Programs, including a hidden third program, thread count, raw initial values, errors, result filter and selected/open trace stay in local browser storage. Cache structure, counts and input association are checked and a selected witness is replayed before display; this is not a tamper-proof result certificate. Imported completed results are always recomputed in the worker, so altered file counts are never trusted. No server calculation.

Only input values are remembered in this browser. Calculated results and experiment histories are not saved.