Happens-before and memory orderings

3.5 The contract: the memory model, happens-before and the orderings

No programmer can reason about every compiler pass on every chip, and no compiler can know which of a program’s accesses another thread is watching. The two sides need an agreement. This section is that agreement, what it lets a program say, and what saying it costs on each architecture.

The memory model

A memory model is a set of rules, written for an abstract machine rather than any real one, that says for every load in a multi-threaded program which stores it is allowed to return. It binds both sides. The programmer marks which accesses must be ordered, and how. The compiler, for each target, emits whatever instructions and barriers make the real chip produce only outcomes the rules allow, and is free to optimise everything else. Rust uses the model of C++20, so its vocabulary is shared with C and C++. Two consequences follow. An outcome the rules allow is a legal outcome even if no chip made today produces it. And a program is correct only if every outcome the rules allow is acceptable to it.

Happens-before

The model’s central relation is happens-before, and it is built from two simpler links. Within one thread, each operation is sequenced before the next, in program order. Between threads, a store with Release ordering synchronises with a load with Acquire ordering that reads the value the store wrote. Happens-before is any chain of those two links, followed in order.

One rule makes it useful. If a store happens-before a load of the same location, the load returns that store’s value or a later one, never an earlier one. If two accesses to one location, at least one of them a write, are not ordered by happens-before either way, there are two cases. When both are atomic, each load must still obey modification order and the model’s coherence rules; it cannot choose an arbitrary value. When either is non-atomic, the program contains a data race, and its behaviour is undefined.

The chain runs from the store of data to the load of data, so the load cannot return the old value. Remove either the Release or the Acquire and the middle link is gone. Nothing then orders the two accesses to data, and 0 is a legal answer.

The orderings

Every atomic operation in Rust takes an Ordering, and each ordering says what the compiler and the CPU may not move across that operation.

• Relaxed gives atomicity and one more thing: all threads agree on a single order of the writes to that one variable, its modification order, so atomic RMW increments are not lost. A sequence of separate loads and stores can still lose an update; wraparound or deliberate stores can also reduce a counter. Relative to other variables it orders nothing.
• Release applies to a store, or the store half of an RMW. No load or store that comes before it in program order may be moved after it. Everything the thread did before the store is visible to any thread that acquires it.
• Acquire applies to a load, or the load half of an RMW. No load or store that comes after it in program order may be moved before it. If it reads a value stored with Release, everything before that store is visible after this load.
• AcqRel applies to an RMW and is both at once.
• SeqCst, sequentially consistent, is Acquire on loads, Release on stores and AcqRel on RMWs, plus one more rule: all SeqCst operations, on every variable, fall into one total order that every thread agrees on. Among the per-access orderings, it supplies the total order needed to forbid the two-flag both-zero outcome, which is exactly the reordering the store buffer performs.

Rust rejects meaningless combinations when the program runs: a store with Acquire, or a load with Release, panics.

AArch64 needs no extra instruction for SeqCst because the architecture forbids an ldar from overtaking an earlier stlr: the pair was designed to give exactly this. The ldapr that newer cores use for plain Acquire drops that one restriction, which is why SeqCst loads stay on ldar.

Fences

A fence supplies ordering without a memory access of its own. For example, a release fence before a relaxed flag store can synchronise with an acquire fence after a relaxed load that reads that store; the accesses to the same atomic flag are still essential. A fence does not publish unrelated data by itself. A SeqCst fence between each store and load also forbids the both-zero outcome of the store-buffering example. x86 acquire/release fences commonly emit no hardware instruction, whereas a sequentially consistent fence needs a barrier such as mfence or a locked operation. AArch64 uses dmb variants. compiler_fence constrains the compiler without providing hardware inter-core ordering. The Rust fence contract gives the precise synchronisation conditions.

Why a passing test proves nothing

A test runs one compiler version, on one chip, under one schedule of threads. On x86 it can never see three of the four reorderings, because the hardware never performs them. It sees the compiler’s reorderings only when an optimisation happens to fire, which can change with an unrelated edit, a new inlining decision or a compiler upgrade. It sees store buffering only when two threads collide within a few nanoseconds. The model allows all of them. A test that passes a billion rounds shows that one machine did not produce a bad outcome in those billion rounds, which is evidence about the machine and not about the program. Correctness is a property of the program measured against the model, so it has to be checked against the model.

What it costs

On x86-64, total store order already keeps loads in order, stores in order, and loads ahead of later stores, which is everything Acquire and Release ask for. In hardware they cost nothing: the same mov as Relaxed. Their only cost is in the compiler, which may no longer move accesses across them, usually a few instructions of lost scheduling. The one ordering with a hardware price on x86 is a SeqCst store or a SeqCst fence, because it must forbid the one reordering the hardware does. xchg and mfence wait for the store buffer to drain: about 20–40 cycles when it is nearly empty, and as long as the slowest pending store when it is not, which can be a line transfer or a DRAM miss. RMWs cost their lock whatever ordering they carry.

On AArch64 the orderings cost in hardware. A stlr cannot complete until every earlier access has. An ldar holds back every later access until it completes. In a quiet loop each costs a few cycles more than a plain access, and more when it stops the core from overlapping misses. A dmb costs tens of cycles, more with stores outstanding. So on ARM, Relaxed instead of Acquire is a measurable saving, while on x86 it saves nothing in hardware and changes only what is correct.

Worked example: the quote, published properly

The quote and its flag are ordered by one pair: Release on the strategy’s last store, Acquire on the gateway’s spin.

When the gateway’s Acquire load reads the strategy’s sequence number, the strategy’s stores of px and qty happen-before the gateway’s loads, and the loads return those values or later ones. The words or later ones are the catch. If the strategy publishes again while the gateway is reading, the gateway can get the new price with the old quantity. One pair orders a single hand-over; a value overwritten while it is being read is more than one pair can order.

On x86-64 the ordered code is the broken code, instruction for instruction: three movs on each side. The Release/Acquire pair compiles to plain movs there, and what it removes is the compiler’s freedom to reorder. On AArch64, stlr replaces one str and ldar or ldapr replaces the ldr in the spin: a few cycles a publish. For the two-flag example, SeqCst on all four accesses is a straightforward way to forbid both loads returning zero. Properly placed SeqCst fences are another; this litmus test alone is not a complete mutual-exclusion or position-limit algorithm. There each store becomes xchg on x86-64, 20–40 cycles plus the drain, and stlr on AArch64, where the ldar that follows can no longer overtake it.

Seeing it

loom is a model checker for concurrent Rust. A test written against loom’s versions of the atomic, cell and thread types, inside loom::model, is run again and again, each time with a different interleaving of the threads and, for each load, any value the memory model lets it return.

Model a single publication with two loom atomics and a joined producer: if an acquiring reader sees flag == 1, assert data == 42. That model should pass with Release/Acquire; replacing both with Relaxed permits the assertion to fail. Use RUSTFLAGS="--cfg loom" cargo test --release when the exercise’s conditional imports are wired for it; the flag alone does not instrument standard atomics. loom is exhaustive only for small tests, LOOM_MAX_PREEMPTIONS caps how many thread switches it tries in one execution, it treats SeqCst loads and stores as AcqRel, and it misses some Relaxed behaviours; Miri (cargo +nightly miri test) complements it by catching data races in ordinary tests. cargo asm for both targets shows the price: on x86, between Relaxed and Release there is no instruction to see, and between Release and SeqCst on a store there is exactly one, the xchg that drains the buffer.