THE ORRERY

A model checker asks what can happen when threads take turns in every possible order.

All exported tree nodes and edges are drawn. Pale wisps are a sampled density encoding of measured omitted completions, not reconstructed paths.

Follow a measured schedule

Choose a witness. The comet follows its numeric endpoints through the matching run.

Dekker with one missing wait · SC · race17 stepsSchedule-derived continuation beyond a pruned boundary

Six programs, six machines

Diameter scales with naive-equivalent schedules.

  1. The smallest raceSC · 2
  2. Dekker's algorithmSC · 93,884
  3. Dekker with one missing waitSC · 336,153
  4. Lost wakeupSC · 8
  5. Test-and-set spin lassoSC · 842
  6. PSO message-passing discriminatorPSO · 210SC 2 · PSO 6

Intact and wounded Dekker

Removing one wait opens dangerous interleavings.

Intact algorithm

naive-equivalent schedules
93,884
DPOR schedules explored
269
prefix states
1,317

primary verdictnontermination

One missing wait

naive-equivalent schedules
336,153
DPOR schedules explored
281
prefix states
1,492

primary verdictrace

SC and PSO: what actually flips

Only assertion reachability changes.

SC

Primary verdict
race
Assertion reachability
holds

PSO

Primary verdict
race
Assertion reachability
violated
ACT II · THE MERIDIAN BENCH

TAKE THE BATON.

The sky maps every timeline. Here, build one.

THE ORRERY / DPOR / SC

WOUNDED DEKKER

Press A or D. Each press executes one instruction; cells, registers, and the rail update from the program.

PROGRAM / SCdekker_counter_broken_drop_turn_wait

THREAD0
Next instructionset r7 1endpoint 0:0
  1. 00set r7 1
  2. 01atomic_store flag0 1
  3. 03atomic_load flag1 -> r0
  4. 04bnz r0 p0_check_turn
  5. 05bnz r7 p0_enter
Local registers
r0
0
r1
0
r2
0
r7
0
Your schedule00 steps

No instruction has executed.

Shared cells
flag0
0
flag1
0
turn
0
counter
0
THREAD1
Next instructionset r7 1endpoint 1:0
  1. 00set r7 1
  2. 01atomic_store flag1 1
  3. 03atomic_load flag0 -> r0
  4. 04bnz r0 p1_check_turn
  5. 05bnz r7 p1_enter
Local registers
r0
0
r1
0
r2
0
r7
0

RACE · counter · unordered cross-thread access

Checker atlas

Five more state spaces.

  1. 01

    Two unprotected writes

    model
    SC
    DPOR schedules
    2
    primary verdict
    race
  2. 02

    Dekker, intact

    model
    SC
    DPOR schedules
    269
    primary verdict
    nontermination
  3. 03

    Lost wakeup

    model
    SC
    DPOR schedules
    4
    primary verdict
    deadlock
  4. 04

    Test-and-set spinlock

    model
    SC
    DPOR schedules
    85
    primary verdict
    nontermination
  5. 05

    Message passing / SC → PSO

    model
    SC
    DPOR schedules
    2
    primary verdict
    race
    model
    PSO
    DPOR schedules
    6
    primary verdict
    race

    Primary verdict: race under SC and PSO; assertion reachability: holds under SC, violated under PSO.