Sequential Consistency and the Cost of One Global Memory Order

Two threads, two variables, no locks. Thread 1 stores 1 to x and then reads y. Thread 2 stores 1 to y and then reads x. Each store is a single aligned machine word, each load reads a value that some thread wrote, and no value is torn. Both loads may still return 0 on real hardware. Nothing in the code is racy in the sense of touching the same byte, and yet the outcome where both reads see zero is permitted on x86, on Arm, and on PowerPC. Sequential consistency forbids it, and no commercial processor implements sequential consistency for ordinary loads and stores.

That gap between the intuitive model and the implemented one is the subject of this whole cluster. It starts with a definition precise enough to reason about, because “the memory behaves as if there were one copy” is not precise enough to tell which outcomes are legal.

Lamport’s definition, and the two conditions inside it

Leslie Lamport defined the model in 1979 for multiprocessors built from uniprocessors: a system is sequentially consistent if the result of any execution is the same as if the memory operations of all processors were executed in some single sequential order, and the operations of each individual processor appear in that sequence in the order specified by its program. Two separate requirements hide in that sentence.

The first is program order per processor. Within one thread, the loads and stores must take effect in the order the instructions appear. A compiler that hoisted a load above a store to a different address, or a machine that retired the store after a later load had already read memory, violates this condition even if every individual access is atomic.

The second is a single total order over all accesses. There must exist one interleaving of every processor’s operations that explains every value observed. This is the expensive part. It is not enough for each location to be consistent on its own; the orders of different locations must be compatible with one shared sequence. A machine can be perfectly coherent, in the sense that all processors agree on the order of writes to each individual byte, and still fail to be sequentially consistent, because there is no single interleaving that produces the observed combination of values across locations. That distinction is the subject of Cache Coherence Is Per Location, Consistency Is Not.

Read operations return the value of the most recent write to that location in the total order. Writes become visible at the point they occupy in the sequence, not before. There is no notion of a write being “in flight” or “partially visible”: the model has no time dimension at all, only an order.

Why one total order is expensive in hardware

A sequentially consistent machine must make every memory operation globally visible before the next one from the same processor begins, or at least appear to. Three hardware techniques that every modern core uses are exactly the ones this forbids.

Store buffers. A core that writes to a cache line it does not own must send a request and wait for ownership. Rather than stall, the core parks the store in a small buffer and continues. The buffer is the mechanism behind Store Buffers and the Total Store Order That Replaces Sequential Consistency, and it directly breaks the single-order requirement: the store exists in the issuing core’s buffer while other cores still see the old value, so two cores can each have a pending store that the other has not observed.

Speculative and out-of-order loads. A core issues a load as soon as its address is known, before older stores have resolved and before it knows whether an older store to the same line is still pending elsewhere. If the load retires and its value is later invalidated, the core must either squash the dependent work or prevent the load from retiring. Both are possible; both cost area, power, and verification effort.

Non-blocking caches. A cache that can service a miss without stalling the pipeline issues several misses concurrently, so the order in which they complete is not the order in which they were requested. That is fine for performance and incompatible with a per-processor order unless completion is forced to match issue order.

The canonical way to build a sequentially consistent multiprocessor without those restrictions is to serialize: route every memory operation through a single point, or use a directory protocol in which a location cannot change hands until the previous owner has acknowledged. Both approaches work and both put a full memory round trip, on the order of a hundred nanoseconds on a modern machine, on the critical path of every miss. Amdahl’s argument applies immediately: a core that can execute several instructions per cycle spends the whole interval waiting.

There is a subtle alternative, sometimes called speculative sequential consistency: run the fast, relaxed hardware and check after the fact. A core speculatively satisfies loads early, records the lines it read, and invalidates its speculation if a conflicting write arrives before the load retires. This preserves the appearance of a total order without serializing, at the cost of a validation mechanism on every load and a squash path. It appears in research machines and in restricted forms in real designs, but it is not what mainstream cores do, because the simpler relaxation is nearly free.

The litmus test that separates the model from its neighbours

Small concurrent programs with a fixed number of threads and a small set of outcomes are called litmus tests. They are the working tool for telling models apart, and Litmus Tests and How Allowed Outcomes Are Decided covers the family in detail. The one that matters here is store buffering:

// x = 0, y = 0 initially; both threads run concurrently
void *t1(void *_) {
    x = 1;            // plain store
    int r1 = y;       // plain load
    return NULL;
}
void *t2(void *_) {
    y = 1;
    int r2 = x;
    return NULL;
}

Sequential consistency forbids r1 == 0 && r2 == 0. Suppose the total order places x = 1 before y = 1. Then thread 2’s load of x follows its own store of y, which follows x = 1, so r2 must read 1. Symmetrically, if y = 1 comes first, thread 1’s load of y must read 1. Only one of the two loads can miss.

On a machine with store buffers, both misses happen routinely. Each core executes its store into its own buffer, then its load hits the line still holding zero, then the stores drain. Each core’s own program order is intact: the store precedes the load in that core’s instruction stream. What is missing is the single total order, because the two stores were never ordered with respect to each other at the moment the loads read.

That observation generalises into a compact statement of what weaker models give up. They keep per-location coherence and per-processor program order for some classes of accesses, and they discard the global interleaving. The question a memory model answers is precisely which cross-location orderings survive.

What remains when the total order goes away

Even the weakest models retain properties that programs depend on, and it is worth being explicit about them because they are what makes lock-free code possible at all.

Every model in practical use preserves single-copy atomicity for aligned accesses no wider than the machine’s guaranteed width: a store becomes visible to all observers at once, never half-applied, and a load returns one value, not a mixture. A 64-bit aligned store on a 64-bit machine is atomic; an unaligned or wider access may not be, and a program that relies on it is relying on nothing.

Every model also preserves coherence per location: all processors agree on the order of writes to a single address, and a processor never sees a value go backwards for one address. A load that observes write A never subsequently observes an older write B to the same address. This is enforced by the cache coherence protocol, not by the consistency model, which is why coherence and consistency are separate layers.

What varies is the treatment of orderings between different addresses, and that variation is where the performance lives. A model that permits a load to be satisfied from a store buffer, or a store to be visible before an earlier store to another line, saves the core from waiting. The bill arrives in the form of fences that the programmer or the compiler must insert, and in the reasoning burden of proving that the fences are in the right places. The rest of the cluster is about paying that bill precisely rather than generously: one-way ordering instead of full barriers, atomic instructions that carry their own ordering, and formal tests that say exactly which outcomes a model permits.

The reference model stays useful even though nothing implements it. It is the model a programmer imagines when writing code with no synchronisation, the model a compiler is allowed to assume for single-threaded code, and the yardstick against which every relaxation is described.