Memory Systems · Memory Modeling

Store Buffers and the x86-TSO Model

How a per-core write buffer leaves store-load as the only program-order pair that may invert, why forbidding it would defeat the buffer, and what a locked instruction orders.

A core that issues a store and waits for the cache line to reach an exclusive state before continuing would stall for the duration of a cache miss on every write. The standard fix is a small first-in-first-out queue between the core and the cache: the store is committed to the queue and the core continues. The store becomes visible to other cores when it drains to the cache, which is later, but the core does not pay for that latency unless something forces it to wait.

This queue is the physical origin of almost every memory-ordering surprise on x86, and the model that describes its consequences is called total store order, or TSO.

The abstract machine

TSO is defined by three components rather than by a pipeline diagram. Each core has a program counter, a set of registers, and a write buffer holding pending stores in program order. Memory is a single array shared by all cores. A load from a core reads its own buffer first, forwarding the most recent buffered store to that address if one exists; only if the buffer has no entry for the address does the load read memory. A store is appended to the buffer and later, nondeterministically, drains into memory.

The nondeterminism is deliberate. The model does not say when a buffer drains, only that entries drain in the order they were appended and that a core’s buffer is finite in any real implementation. Because the drain time is unconstrained, a load that misses the buffer may read a value from memory that predates stores still sitting in another core’s buffer. That is the whole mechanism; nothing else in TSO is hidden.

Four orderings follow, and it is worth enumerating them because the enumeration is the model:

First operationSecond operationReordered?
loadloadno
loadstoreno
storestoreno
storeloadyes

Loads are not buffered, so two loads from one core are performed in program order. A load followed by a store cannot be reordered because the store does not affect what the earlier load observed. Two stores cannot be reordered because the buffer is FIFO. Only store followed by load can invert, because the load may bypass the buffer.

That single exception is enough to break mutual exclusion built from plain flags. The classic test has each of two threads write its own flag and then read the other’s:

// Thread 0                    // Thread 1
x = 1;                        y = 1;
r0 = y;                       r1 = x;

On TSO, x = 1 enters thread 0’s buffer, r0 = y reads memory before thread 1’s store has drained, and symmetrically for the other side. Both r0 and r1 come back zero. Sequential consistency forbids that outcome, as the reference model shows; TSO permits it and nothing else that SC forbids for this program.

Why the exception is not free to remove

Removing the store-load relaxation would mean a load could not issue until every prior store had drained, which reintroduces exactly the stall the buffer was built to avoid. Store-to-load forwarding makes the common case cheap — a load of an address the same core just wrote returns from the buffer in a few cycles instead of a cache round trip — but the ordering rule is what costs. Any design that keeps the buffer and also forbids store-load reordering has to make the load wait for the drain.

The alternative designs are worth naming because they are what other architectures chose. A machine with no buffer at all gives SC and pays the store latency. A machine with a buffer that also reorders stores against each other — a weaker model — can drain entries out of order and gains more, at the price of needing fences in more places. TSO sits between them: it buys store latency hiding while keeping per-core store order, so a program that never depends on store-load order needs no fences at all.

Fences and locked operations

TSO provides two ways to recover the missing order. The first is a full fence, mfence on x86: every load and store before it is ordered before every load and store after it. The second is any locked instruction, such as lock addl $0, (%rsp) or an xchg with a memory operand, which x86 defines as a full barrier in addition to its arithmetic effect.

There is a subtlety in how the fence interacts with the buffer that trips up reasoning from the abstract model. mfence is specified as an ordering operation, and what it guarantees is that a load after the fence cannot read memory in a state that excludes a store before the fence — the store is either in memory already or is forwarded when the later load is to the same address. The x86-TSO abstract machine captures this by permitting the fence to retire only once the core’s buffer is empty, so the model implements it as a drain; an implementation that instead kept the stores buffered but made them visible to other cores in order would satisfy the same observations.

A cheaper idiom that appears in older x86 code is a dummy locked operation, such as lock addl $0, (%rsp). It is architecturally a full barrier as well as an atomic read-modify-write, and it predates the general use of mfence for the purpose. Neither is free: a locked operation must gain exclusive ownership of its cache line, and a full fence must wait for ordering to be established.

What a store buffer does not model

TSO as described here is a model of cores and memory. It does not model the compiler, which is free to reorder far more aggressively and does so constantly. A C compiler may keep a variable in a register across a function call, eliminate a redundant load entirely, or hoist a load out of a loop. None of these transformations is visible in the TSO rules, and each can break a program that is correct against TSO. The reason volatile in C is not a synchronisation primitive is that it constrains the compiler’s access to the object but says nothing about ordering with respect to other objects, and nothing about atomicity.

Nor does TSO model caches that are not coherent. x86 systems maintain per-core coherence, so a store that has drained from the buffer is visible to all cores through the coherence protocol, and the model’s single memory array is a fair abstraction. On a system without that property, a store could drain and still be invisible to a core reading a stale copy, which is a different failure with a different fix.

The model also abstracts away speculative execution. A core may load a value speculatively and later discover it was wrong; the model’s loads always return the value the rules permit. That abstraction is sound for the architectural result, though not for timing, and it is the reason side channels that leak through speculation are invisible to any memory-consistency model — they are not ordering violations but information flow.

Where TSO stops being enough

Programs that need order in both directions — a flag written before a data field, read by another core that then reads the field — are fine on TSO with a single fence between the store and the load. Programs that need a store to be visible before a subsequent store to a different location are also fine, since stores are ordered. What TSO cannot express at all is a requirement that two stores become visible in a particular order to a third party while a load intervenes; the store-load case forces the fence, and the fence is total.

The larger point is that TSO is a contract with a name and a checkable definition, not folklore about x86 being “strong”. The happens-before relation used by C and C++ is a different and weaker contract, and code that is correct under one is not automatically correct under the other. On x86, many programs that are technically racy happen to work because the hardware forbids the reordering that would expose the bug; the same source compiled for a machine with a weaker model, described in ARMv8 and the cost of dependencies, does not.

References

  1. Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 3A, Chapter 8 — Intel
  2. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors — Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen, Communications of the ACM, 2010
  3. Memory Barriers: a Hardware View for Software Hackers — Paul McKenney, Linux Technology Center