Race condition: follow every read, add and write

Exact schedule state

An increment contains several operations

An unsynchronized increment is represented by three instructions: read the shared counter into a private register, add one to that register, then write the register back. Another thread can run between those instructions. The shared counter, private registers, next instructions and completed-operation counts are all explicit states. The model never subtracts a random percentage of updates. A write can overwrite a value based on a newer read because this chosen schedule permits it. The final discrepancy is a consequence of the trace, not an invented collision probability.

Choose the interleaving

Threads and Increments per thread determine the finite workload. Round-robin instructions alternates among unfinished threads after every instruction, making conflicting reads easy to inspect. Finish each thread in order completes one thread before moving to the next. Seeded instruction choices selects the next runnable thread from a reproducible pseudo-random sequence; Schedule seed affects that mode only. Use indivisible atomic increment replaces the three separate instructions with one protected counter update. It represents atomicity as an assumption, not a generated machine instruction or a hardware benchmark. Every input change recomputes the schedule and pauses at the start.

Reproduce one lost update exactly

Select two threads, one increment each, round-robin scheduling and disable atomic increments. Thread zero reads zero, thread one reads zero, both private registers become one, and both eventually write one. The final counter is one although two increments completed. Turn on atomic increments: the same workload finishes with two. With three increments per thread and the round-robin non-atomic schedule, each round repeats the conflict and the final counter is three instead of six. Select serial scheduling while leaving atomic disabled; the particular non-overlapping trace reaches six. That successful run does not make the unsynchronized program safe under other schedules.

Inspect a trace, not a language memory model

Play reveals the finite instruction sequence over sixty inspection seconds. Pause holds it; Next state advances one instruction; Restart rewinds; Speed changes viewing pace; Inspect time selects an exact recorded step. Restore defaults resets all controls. The inspector shows the counter before and after the current instruction, the active thread and every private register. Completed increments count writes or atomic operations, not individual reads or additions. This model assumes sequentially consistent individual reads and writes and omits compiler reordering, weak memory, cache visibility, overflow and language-specific undefined behavior. It explains a logical lost-update race; it does not claim to emulate the Java, C++ or processor memory model.