Memory Models and the Happens-Before Relation

Source code suggests a simple world: statements execute in order, writes immediately become visible, and every thread observes one shared memory. Concurrent programs run in a less intuitive world. Compilers reorder independent operations, processors execute and retire memory operations through caches and buffers, and language runtimes define which observations programs are allowed to make.

A memory model is the contract that connects those layers. It does not merely describe hardware. It says which executions a language considers valid, which operations are atomic, and when one thread is guaranteed to observe another thread’s writes. The most useful reasoning tool in that contract is the happens-before relation. If a write happens-before a read, the read must be compatible with that ordered history. If there is no such edge, source order and elapsed wall time do not create visibility by themselves.

The thesis is practical: correct concurrent code establishes an explicit happens-before path for every cross-thread invariant. Atomics and synchronization are ways to create that path. They are not magic markers that make surrounding code safe without a proof.

Separate Program Order from Observable Order #

Within one thread, code has a required single-threaded meaning. A compiler may swap, combine, or eliminate operations as long as the thread cannot distinguish the transformed execution under the language rules. This is often called the as-if rule. In concurrent code, another thread can distinguish memory order, so the memory model defines which transformations remain legal.

Consider two ordinary assignments:

data = 42
ready = true

The author may intend ready to publish data. But if the variables are accessed concurrently without synchronization, several layers can defeat that inference. A compiler may move the independent stores, a processor may make them visible in a different order, or the reading core may hold an older cached value. More importantly, some language models classify the conflicting non-atomic accesses as a data race, making the program invalid or allowing behavior broader than any one hardware explanation.

Three orders must not be conflated:

• Program order describes sequenced operations within one thread as defined by the language.
• Modification order orders writes to one atomic object.
• Happens-before order connects operations whose effects must become visible across threads.

Wall-clock order is not on the list. Sleeping one thread before reading does not establish synchronization. A debugger pause may make a failure disappear by changing timing and cache traffic, but it creates no proof.

Hardware mechanisms explain why weak observations are possible, while the language model determines whether code may rely on them. Store buffers let a core continue before a write is globally visible. Out-of-order execution overlaps independent instructions. Coherent caches generally agree on the order of writes to one location, but coherence alone does not impose one order across different locations. Portable code should reason from the language contract and use its synchronization operations, not depend on an accidental property of one processor family.

Build Proofs with Happens-Before Edges #

Happens-before is a partial order. It need not choose an order between every pair of events. It is built from local sequencing and synchronization rules, then closed transitively.

Suppose operation $A$ is sequenced before $B$ in thread 1. Suppose $B$ synchronizes-with $C$ in thread 2, and $C$ is sequenced before $D$. Then:

and, by transitivity, $A$ happens-before $D$. This path is what publishes effects from the first thread to the second.

Different languages provide different synchronizes-with edges. Common examples include releasing a mutex followed by another thread acquiring it, starting a thread followed by its first action, a thread’s completion followed by a successful join, sending and receiving through a specified channel, and a release atomic operation observed by an acquire operation. The exact rule matters; similar-looking APIs may promise different ordering.

The relation gives a review method. For each shared non-atomic field:

1. Identify every thread that writes it and every thread that reads it.
2. Find the synchronization operation after the producer’s writes.
3. Find the matching synchronization operation before the consumer’s reads.
4. Trace the complete happens-before path, including program-order edges.
5. Confirm that object lifetime also spans every access.

If the path cannot be drawn, “the producer normally runs first” is not a replacement. Either add synchronization, make the state immutable and publish it correctly, confine it to one thread, or change the design so it is not shared.

Happens-before does not mean physically earlier. It is a semantic ordering relation. Nor does it make a compound operation indivisible. A synchronized publication can make an object visible, while later unsynchronized mutation of that object still races.

Distinguish Atomicity, Visibility, and Ordering #

These properties solve different problems.

Atomicity means an operation is observed as one indivisible action with respect to the guarantees of that atomic object. A 64-bit atomic load will not see half of one stored value and half of another. A read-modify-write operation such as atomic increment prevents two updates from collapsing into one.

Visibility means a thread is guaranteed to observe relevant effects from another thread. An atomic flag can carry that guarantee when used with the right ordering and when the consumer actually observes the producer’s value.

Ordering constrains which operations may move across a synchronization point and which observations are permitted. It can be one-way: release constrains earlier operations from moving after publication, while acquire constrains later operations from moving before consumption.

Marking one field atomic does not make a multi-field invariant atomic. Suppose a producer updates x, y, and an atomic version. A consumer can use version to detect a stable snapshot only if the protocol accounts for concurrent writers and uses appropriate ordering. Atomic individual reads of x and y would still not guarantee that both came from the same logical update.

Likewise, volatile is not a portable synonym for synchronization. In some languages it has defined cross-thread visibility semantics; in others it primarily controls optimization or device access and does not make a race safe. Always use the definition from the language at hand.

The right mechanism follows from the invariant, not from a desire to avoid a particular primitive.

Use Acquire and Release for Publication #

Acquire and release form a directional handshake. A release operation publishes all operations sequenced before it. An acquire operation that observes that release, or an appropriate later value in the atomic object’s ordering as defined by the language, makes those earlier effects visible to operations after the acquire.

Here is a language-neutral publication pattern using pseudocode with explicit atomic order names:

shared payload: ordinary immutable object reference
shared ready: atomic boolean = false

producer:
    local = buildCompletePayload()
    payload = local
    atomicStore(ready, true, release)

consumer:
    if atomicLoad(ready, acquire) == true:
        use(payload)

The release store is not valuable because ready itself is difficult to write. Its purpose is to publish the preceding ordinary write to payload. When the acquire load observes true, the proof is:

By transitivity, building and publishing the object happen-before its use. The object must not be mutated concurrently afterward unless a separate protocol protects that mutation.

A relaxed atomic operation provides atomicity and participates in the atomic object’s modification order, but generally does not publish unrelated ordinary memory. Relaxed ordering is useful for independent counters, statistics, or algorithms whose ordering proof comes from other operations. Replacing the release store and acquire load above with relaxed operations destroys the publication edge even though ready itself remains atomic.

Sequentially consistent atomics add a single global order for sequentially consistent operations, consistent with each thread’s program order. They are often easier to reason about and can be the right default. They still do not automatically group multiple operations into a transaction, and ordinary shared accesses still need a happens-before justification.

Performance arguments for weaker ordering should follow a correctness proof and measurement. Acquire/release can reduce constraints on some targets, but the maintenance cost of a subtle protocol may exceed any benefit. An unproven weak-memory optimization is not an optimization; it is a latent correctness defect.

Work Through the Message-Passing Litmus Test #

A litmus test is a tiny concurrent program that asks whether a particular outcome is allowed. It strips away application detail so the memory-order question can be stated precisely.

Start with two shared variables initialized to zero:

x = 0                 // ordinary
flag = 0              // atomic

Thread P:             Thread C:
x = 1                 r1 = load(flag, ?)
store(flag, 1, ?)     if r1 == 1:
                          r2 = x

The desired invariant is r1 == 1 implies r2 == 1.

Case 1: release store and acquire load. If the acquire load reads the value from the release store, the write x = 1 happens-before r2 = x. The invariant holds. This is the worked publication protocol from the previous section.

Case 2: relaxed store and relaxed load. The flag operations are atomic, but no synchronizes-with edge publishes x. In a model where concurrent ordinary access without happens-before is a data race, the program is invalid. In a model that assigns weak semantics rather than undefined behavior, observing the new flag with stale data may be allowed. Either way, the intended invariant is not established.

Case 3: release store and relaxed load. Release on one side is insufficient. The consumer needs a matching operation with acquire semantics to import the preceding writes.

Case 4: relaxed store and acquire load. Acquire cannot manufacture a release sequence from an operation that did not publish preceding work. Again, there is no complete edge.

This test exposes a common mistake: placing a strong operation somewhere in each thread is not enough. The consumer’s acquire must observe the producer’s release through a relation recognized by the memory model.

Another classic test, store buffering, uses two atomic variables initially zero:

Thread A:             Thread B:
store(x, 1, relaxed)  store(y, 1, relaxed)
r1 = load(y, relaxed) r2 = load(x, relaxed)

Can both r1 and r2 equal zero? Under many weak-memory contracts, yes. Each thread’s store can remain unobserved by the other when its load occurs. Sequential consistency would forbid that outcome because no single interleaving can place both loads before both program-order-prior stores. The point is not to memorize outcomes, but to derive them from the chosen ordering rules.

Understand Data Races and Their Failure Modes #

A data race usually means two potentially concurrent accesses to the same memory location, at least one a write, with no required ordering and without the synchronization the language demands. Exact definitions vary, especially around atomic objects, but the engineering response is consistent: races are specification defects, not merely unlucky timings.

In languages where a data race yields undefined behavior, the compiler need not preserve intuitive “last writer wins” behavior. It may hoist a load out of a loop, assume a value cannot change concurrently, or remove branches based on single-threaded reasoning. Testing on one machine cannot constrain executions the language does not promise.

Even a race-free program can be logically wrong. Atomics can prevent data races while allowing invalid operation ordering. Two atomic withdrawals from separate fields may preserve each field’s integrity but violate a combined account invariant. Conversely, benign-looking races, such as an approximate debug counter, can still invalidate the program in a strict language; use a relaxed atomic if approximate ordering is acceptable.

Common failure modes include:

• Publishing a pointer before construction is complete.
• Reusing memory while another thread may still hold a reference.
• Mixing atomic and non-atomic access to the same location.
• Assuming a successful compare-and-swap orders unrelated memory under every ordering mode.
• Reading several atomics and treating the values as one coherent snapshot.
• Replacing synchronization with sleeps, logging, or debugger timing.
• Copying a protocol from a different language whose memory model differs.

Object lifetime is part of memory safety. A perfect ordering proof for a load is useless if the referenced object has been freed and reused. Reclamation techniques add another protocol; they should be reviewed separately from the logical update algorithm.

Verify Memory-Ordering Claims Systematically #

Begin with a written invariant and an edge diagram, not a stress loop. For the publication example, state: after a consumer’s acquire load observes ready == true, every payload field equals the value established before the producer’s release store. Identify the exact read-from relation that activates the synchronizes-with edge.

Use several complementary tools:

Static review traces shared locations, access modes, and happens-before paths. An annotation can record which lock protects a field or which atomic publishes it. Reviewers should challenge every transition between ordinary and atomic state.

Race detectors instrument memory accesses and synchronization to find executions with missing ordering. They are powerful for ordinary data races, but they observe only executed paths, add overhead, and may not diagnose a race-free ordering bug such as an invalid multi-variable snapshot.

Litmus runners and model checkers enumerate or symbolically explore small executions under a specified memory model. Keep tests tiny: a few locations, threads, and events. Ask whether a forbidden outcome is reachable, then verify that strengthening or moving an ordering operation removes it for the reason expected.

Seeded stress tests increase schedule diversity and can expose lifetime or integration errors. Record seeds, runtime versions, processor architecture, and iteration counts so a failure can be replayed. A billion passing iterations are evidence about those runs, not a proof that an unmodeled weak outcome is impossible.

Compiler and runtime tests should cover every supported target because mappings from language atomics to machine instructions differ. Inspect generated assembly only as a diagnostic; the source-level proof remains authoritative. A compiler can change instruction selection while preserving the same memory-model guarantee.

When optimizing an ordering, make one change at a time. Re-run model checks, race detection, invariant tests, and representative performance measurements. If the team cannot state why the weaker order preserves every edge, revert to the clearer order.

Review and Operate Concurrent State with Discipline #

Production telemetry can reveal symptoms but rarely prove a memory-order defect directly. Watch invariant violations, impossible state combinations, duplicate ownership, corrupted queue links, and process crashes by runtime and architecture. Preserve enough version information to compare code generation and deployment targets. Avoid “repairing” impossible states silently; count and surface them even if a safe fallback contains user impact.

Code review should maintain a small synchronization vocabulary. Prefer immutable handoff, established mutexes, channels, and well-documented atomic protocols over bespoke mixtures. Encapsulate atomics behind an abstraction whose public methods state their concurrency contract. The caller should not need to know that a field uses release semantics to use the component safely.

For every custom atomic protocol, keep a proof sketch near its tests or design documentation:

• Shared locations and their initial states.
• Allowed writers and readers.
• The invariant being protected.
• The operation that publishes each update.
• The operation that acquires it and the value it must observe.
• Lifetime and reclamation rules.
• Permitted weak outcomes and why they are harmless.

Memory models become manageable when treated as contracts rather than folklore. Program order explains one thread, atomics define indivisible operations and per-object order, and happens-before carries visibility across threads. Draw the edge from every produced value to every consumer. If the path exists under the language’s actual rules, the code has a defensible foundation. If it does not, no amount of favorable timing can supply it.