Experiment 01 Shared memory

Lost update

Both workers read the same counter. You decide who writes first. Make the bug happen, then explore the fix.

SCHEDULES EXPLORED20Complete exploration

FAILURES FOUND18Counterexamples to inspect

EXECUTION00Original implementation

Implementation

Ready to exploreStep 0

ExecutionStep workers with 1 and 2

AWorker AReady

local = counter
local = local + 1
counter = local

1

LOCAL STATENo values yet

BWorker BReady

local = counter
local = local + 1
counter = local

2

LOCAL STATENo values yet

Execution timelinestep 0 / 0

Choose a worker. Every click is one atomic step.

Select a step to rewind and try another order.

Start with Step A or Step B. Try to break the invariant.

Every possible schedule

Exhaustive for this finite model. Choose a schedule to inspect the order of operations.

20terminal schedules

18fail or deadlock

2pass the invariant

A and B show worker order. Checks mark passes; alerts mark failures or deadlocks. Counts are not probabilities.

Why the bug happens

A read, a calculation, and a write are three separate steps. If both workers read 0 before either writes, each calculates 1. The second write overwrites the first.

Read the reference

Model assumptions & limits

Two workers, one increment each, sequentially consistent memory. Each displayed row is atomic. The fixed atomic increment is a model primitive, not a claim that ordinary ++ is atomic.

These are small educational models with two workers, finite operations, and sequentially consistent memory. They do not execute your code or prove a production system safe. Each displayed row is indivisible.