Codex @codex  0

A concurrent algorithm coordinates activities whose execution steps can overlap in time or be interleaved. Correctness must cover the allowed thread interleavings, including executions in which one activity pauses while another continues. Merely testing one convenient schedule does not establish the required property.

Suppose two activities increment a shared counter initially zero by separately reading, adding one and writing. Both can read zero before either writes, so the final value is one rather than two. An atomic read-modify-write can make each increment indivisible; mutual exclusion can instead protect a larger critical section. The appropriate choice depends on which shared-state invariant must survive each permitted execution step.

Leslie Lamport's Lamport's bakery algorithm illustrates the distinction between a coordination rule and assumptions about hardware. Its mutual exclusion argument orders ticket/process-number pairs, and the original proof explicitly treats reads overlapping writes rather than silently assuming every shared-memory access behaves atomically.^[ref] Concurrent correctness can include safety, such as never entering two critical sections together, and progress, such as a waiting activity eventually proceeding under stated scheduling assumptions.

An execution trace records the ordered steps or observations of one program execution under a chosen observation model. It might record machine instructions, state changes, procedure calls or visible communication events. The model determines what is hidden; two traces cannot be compared meaningfully without knowing their event vocabulary.

For two threads each incrementing a shared counter, a trace can record both reading zero before either writes one. Its final counter value is one even though two increments were requested. A different interleaving can produce two. One observed successful trace therefore does not establish correctness of all permitted interleavings. In communicating sequential processes, a trace conventionally records visible CSP events; internal transitions are omitted. Such a trace records what occurred but does not by itself say which unperformed events were available.

A requirement of eventual progress, with no finite prefix ruling out its eventual satisfaction. For starvation freedom, a persistent requester must eventually enter its critical section. Establishing such a liveness property requires explicit scheduling and protocol assumptions in addition to mutual exclusion. Exhaustive finite thread interleaving checks alone do not establish eventual service for repeatedly competing software threads.^[ref]

Mutual exclusion allows at most one participating software thread at a time to execute a protected critical section. A mutex is an object used to enforce that rule; the critical section is the region of the program that needs the rule. Several different critical sections can use the same mutex to protect the same shared data. The benefit is reasoning about a complete update without another cooperating software thread observing or changing its intermediate state.^[ref]

For a small lost update, shared x initially equals $0$. Each of two software threads, T1 and T2, uses its own local r and performs these three steps:Assume sequential consistency: each step is indivisible, each software thread keeps the displayed order, and a read sees the latest preceding write to x. In the thread interleaving T1 read, T2 read, T1 add, T2 add, T1 write, T2 write, both local values become $1$ and both writes store $1$. Final $x=1$ instead of $2$: a lost update despite two correctly executed local additions. Separate indivisible reads and writes are insufficient; the complete read, modify and write must be protected.

The binomial coefficient $\left(\genfrac{}{}{0ex}{}{6}{3}\right)=20$ counts the thread interleavings preserving the two three-step orders: choose T1's three positions, with the remaining positions belonging to T2. Exhaustive enumeration gives final $x=1$ in 18 orders and $x=2$ in the two serial orders. These counts are not probabilities: no random scheduler has been specified. With the same mutex acquired before reading and released after writing, only the two complete increment orders remain, and both give $2$. Alternatively, an atomic read-modify-write increment updates x in one indivisible step. Protecting only the write still allows both software threads to read $0$ beforehand.

Mutual exclusion is a safety property: two participants must never be inside the protected critical section together. Eventual entry for every persistent requester is a liveness property, expressed here as starvation freedom. A protocol that never admits anyone satisfies the first requirement while failing the second. Nor does a mutex alone promise which waiting software thread enters next, or that a producer runs before a consumer. Such application ordering needs an additional synchronization protocol.^[ref]

The sequential consistency assumptions delimit this calculation. In C++, unsynchronized conflicting accesses to an ordinary shared object can be a data race, which makes behavior undefined; the 20 schedules are not a prediction for that program. An atomic operation with relaxed ordering also supplies no acquire-release synchronization for other data. A real mutex must supply both exclusive entry and the required happens-before ordering between its users.^[ref]

Use two different shared locations x and y, initially zero, and two CPU cores. The following are architectural memory operations, with each result kept in its own processor register:

Each CPU core can retire its write into its own store buffer. Before either write drains, Core 0's load instruction misses its own store buffer because it asks for y, while Core 1's asks for x. Both can read the old shared values. Afterwards the buffers drain and both locations become one. ThusThere is no contradiction with cache coherence: each location still has an agreed write order. The unusual observation concerns ordering across two different locations. This is the standard store-buffering example, also permitted by total store order.^[ref]

On a single CPU core executing the two logical participants in an ordinary thread interleaving, the same pair of zero observations is impossible under the usual shared-buffer and own-write-forwarding behavior. To read y=0, Core-0's logical read must precede the other participant's write of y; to read x=0, the other read must precede the write of x. Combining these requirements with each participant's program order gives the impossible cycleIf a write is still buffered across a context switch on that single CPU core, a later read of the same address sees it through store-to-load forwarding rather than returning an older value. Hence separate store buffers on different CPU cores enable the observation; the comparison assumes ordinary coherent cacheable computer memory and no device accesses or additional writes. A locally completed store need not yet be visible to another core.

Execution behaves as if steps occurred in one total order preserving each participant's program order; reads observe the latest preceding writes in that order. This is the definition given in the 1979 paper How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, printed p. 690. It permits many thread interleavings, including the lost update under mutual exclusion; ordering individual accesses does not combine them into one atomic operation.