Happens-Before, Data Races, and the Memory Model Contract

Every concurrent language must state which of the program’s written operations the machine is required to perform in the written order. That statement is a memory model, and it is a contract between the programmer, the compiler, and the processor. Break it and the program is not merely slow or surprising; it is undefined.

The contract is stated in one relation. Two operations are ordered by happens-before if one must be visible to the other; operations unordered by it may be reordered, eliminated, or interleaved at will. Everything else in the model is machinery for establishing that relation.

Sequenced-before is the cheap half

Within a single thread, operations are sequenced-before in program order. This is the part programmers already believe. It is also the part a compiler is most willing to violate, because the observable behaviour of a single thread is preserved by any transformation that keeps the data dependencies intact. A store to a local that is never read again can be deleted. Two independent loads can be hoisted above an unrelated store. The compiler is allowed to do this because a single thread cannot observe its own reordering.

The machine does the same. Out-of-order cores execute loads and stores as their operands become available, with a reorder buffer and store buffer hiding the latency. A load may be satisfied from a speculative path and retired later; a store may sit in a store buffer and become visible to other cores long after the instruction retired. None of this changes single-thread behaviour, so none of it is constrained by sequenced-before alone.

The gap that produces the classic example: a flag store written after a data store can become globally visible before it.

int data = 0;
int ready = 0;

// thread 1
data = 42;
ready = 1;      // may be visible before the data store

// thread 2
if (ready) {
    use(data);  // may observe 0
}

On a machine with store buffers, thread 2 can see ready == 1 while data is still 0. Nothing in the language forbids it, because the two threads share no synchronisation.

Synchronises-with is the half that must be built

The second edge is established only by specific operations. In the C++ and Java models, a release store and an acquire load on the same atomic variable create an edge: the release store happens-before the acquire load that reads its value, and therefore everything sequenced before the release is visible to everything sequenced after the acquire. That is the entire purpose of the release/acquire pair, and it is why using them correctly makes the naive example above safe.

The edges compose transitively. If thread 1 releases a lock and thread 2 acquires it, everything thread 1 did before the release is ordered before everything thread 2 does after the acquire. If thread 2 then releases a second lock acquired by thread 3, the edge extends. This is how a chain of mutexes or a chain of channels produces a total order over a chain of stages without any global clock.

In Java the same relation is expressed through the monitor rules: an unlock happens-before every subsequent lock of the same monitor, a write to a volatile field happens-before every subsequent read of that field, and thread start and join create edges of their own. The JLS chapter 17 states these as a set of rules from which the rest follows, which is the right way to read it: not as a list of prohibitions, but as a generation grammar for the happens-before relation.

A further consequence in Java is that a final field’s value, as set in the constructor, is visible to any thread that sees the object after construction completes without further synchronisation, provided the constructor did not leak the reference. That guarantee exists because otherwise immutable objects would be unsafe to publish, and the whole point of an immutable object is to be publishable.

Why a data race is undefined and not just a bug

Two accesses to the same memory location, at least one a write, unordered by happens-before, constitute a data race. In C and C++ the standard makes such a program undefined: not “may produce a stale value”, but no requirements at all. The distinction matters because it licenses the compiler to assume races do not occur.

That assumption is the basis of ordinary optimisations. If a loop reads a global twice and nothing in the loop can modify it under the model, the compiler may read it once. If a compiler had to preserve the behaviour of racy programs, every such hoist would need to be checked against an unbounded set of possible interleavings, and optimisation would collapse. The undefined-behaviour rule is the price of the optimiser, and it is not negotiable.

Java takes a different position: a data race does not make the program undefined, but the read may observe a value that no sequentially consistent execution of the same program would produce, and for a non-volatile long or double the specification permits a torn read that mixes two writes. The result is still wrong, just in a bounded way. This is a deliberate difference in the contract, and it is why code written against Java’s rule can behave quite differently when the same race is ported to a language where it is undefined behaviour instead.

The atomics spectrum

A sequentially consistent atomic is the simplest to reason about: all such operations appear in a single total order consistent with program order, and every thread observes them in that order. It is also the most expensive, because it constrains the machine’s ability to reorder around the operation.

Weaker orderings relax specific edges. A relaxed atomic guarantees atomicity and a single modification order per variable but no happens-before edge at all; it is useful for counters where only the final total matters, and useless for publishing data. A release store orders prior writes before itself. An acquire load orders subsequent reads after itself. Consume ordering, present in the C++ model, was intended to carry a dependency only along data that the loaded value was used to address; carrying that dependency through the optimiser proved impractical, and the standard’s own notes discourage it in favour of acquire.

The practical rule is that the weakest ordering that establishes the needed edge should be used, and that the edge must be justified in a comment. A relaxed load used where acquire was needed produces a bug that appears only under specific hardware or specific compiler versions, and its usual symptom is a null dereference after a check.

The hardware underneath

The model is written to permit implementation on machines that behave quite differently. x86-64 is strongly ordered for ordinary loads and stores: it preserves load-to-load, load-to-store, and store-to-store order, and the one relaxation it allows is a load passing an older store to a different address. The name “total store order” comes from the store buffer rather than from the loads: a core’s stores leave that buffer in program order and become visible to every other core in one agreed order, so a fence is needed only to wait for the buffer to drain. ARM and POWER are weaker: they permit more reordering and require explicit barrier instructions for the patterns x86 gets for free.

This is why code that is correct on one architecture can fail on another, and why the memory model has to be the contract rather than any particular machine’s behaviour. A program validated only against the x86 ordering is validated against one implementation of the model, not against the model.

McKenney’s treatment of barriers from the hardware side is the clearest explanation of why each fence exists: a store buffer is a queue, a fence drains it, and the cost of the fence is the cost of waiting for the queue to empty. On the software side the corresponding discipline is to make every shared field either atomic or protected by a happens-before edge, and to be able to name that edge.

Where the model meets the concurrency abstractions

Higher-level constructs are, from the model’s perspective, edge generators. A channel send and its matching receive generate a happens-before edge, which is why channel-based handoff needs no additional fence; see Rendezvous and Buffering in CSP-Style Channels. A future’s completion and the observer that takes the value generate an edge too, which is the guarantee that makes Futures as Write-Once Cells safe to use for publishing results. An actor’s mailbox generates an edge between the sender’s work and the handler’s execution, so state confined to the actor is protected without any atomic operation inside the handler.

Each abstraction is therefore a promise about which edges exist, and a program’s correctness rests on the edges it can name. The remaining question, what happens when two edges are needed but the operations providing them sit inside a library, is where reasoning about concurrency stops being local, and it is the reason the memory model is specified in terms of the whole program’s execution rather than of individual functions.