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.

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.