Sequential Consistency as the Reference Memory Model

Two threads each store to a private flag and then load the other thread’s flag. Every outcome of that program is unremarkable except one: both loads returning zero. On a machine that executes each thread’s operations in program order and interleaves them one at a time without overlap, at least one thread must see the other’s store, because whichever store lands first in the global order is already visible when the other thread’s load runs. The all-zero outcome means a store was reordered past a later load, and the programmer’s assumption — that memory operations take effect one at a time in some order — is false for that machine.

That assumption has a name and a formal definition. It is the reference point against which every weaker model is described, including the store-buffered model of x86-TSO and the language-level rules built on happens-before.

A model is a set of permitted executions

A memory model does not describe a processor’s pipeline. It is a predicate over executions: given a program, the model says which observations that program is allowed to make. This framing matters because it separates two questions that are easy to confuse — what the hardware does, and what the program is entitled to assume. A model is useful precisely when it is weaker than the hardware, so that a program correct under the model stays correct on a machine that reorders more aggressively than the one it was tested on.

An execution, in the form used throughout these models, is a set of events (reads, writes, read-modify-writes, fences) with three relations over them:

• program order (po), a total order per thread, fixed by the program text and the compiler’s output;
• reads-from (rf), mapping each read to the write whose value it returns;
• modification order (mo), a total order per memory location.

Different models constrain these three relations differently. Sequential consistency constrains them the most of any model that is still implementable: it requires that po and rf be jointly embeddable in a single total order over all events, one order shared by every location in the system. Per-location orders are not enough; the orders must be mergeable into one.

Lamport’s 1979 definition states the requirement in two clauses. First, the result of any execution is the same as if the operations of all processors were executed in some sequential order. Second, the operations of each individual processor appear in that sequence in the order specified by its program. The first clause is the strong one. It says there is one history, not one history per location and not one history per observer.

What the total order excludes

The two-clause definition can be tested mechanically. Enumerate every interleaving of the two threads that respects each thread’s program order, run each interleaving against a flat memory, and collect the register values.

import itertools

def interleavings(t0, t1):
    # Every shuffle of two traces that preserves each trace's internal order.
    n = len(t0) + len(t1)
    for positions in itertools.combinations(range(n), len(t0)):
        positions = set(positions)
        out, i, j = [], 0, 0
        for k in range(n):
            if k in positions:
                out.append(t0[i]); i += 1
            else:
                out.append(t1[j]); j += 1
        yield out

def run(trace):
    mem, regs = {'x': 0, 'y': 0}, {}
    for op, *args in trace:
        if op == 'st':
            mem[args[0]] = args[1]
        else:
            regs[args[0]] = mem[args[1]]
    return tuple(sorted(regs.items()))

t0 = [('st', 'x', 1), ('ld', 'r0', 'y')]
t1 = [('st', 'y', 1), ('ld', 'r1', 'x')]
print(len({run(t) for t in interleavings(t0, t1)}))   # 3

Three distinct outcomes out of four possible register combinations. The absent one is r0 = 0, r1 = 0. This is the store-buffer litmus test, and its all-zero outcome is the canonical signature of a machine that lets a store sit in a private buffer while a later load bypasses it. A model that permits the all-zero outcome is not sequentially consistent; a model that forbids it may still be weaker than SC in other ways.

A second test separates “one order per location” from “one order for the whole system”. Two threads each write two locations, and two independent readers each read both locations in opposite orders. Under per-location coherence alone, reader 0 can see the first thread’s write to x but not its write to y, while reader 1 sees the opposite. Under sequential consistency the readers cannot disagree about the relative order of the two writes, because that order is a single fact about the execution. This is the IRIW pattern, and it is where coherence and consistency visibly come apart; the per-location axioms are the subject of modification order and coherence.

Why nobody builds it

Sequential consistency forbids overlapping a store with anything that follows it. A store cannot be retired into a buffer and acknowledged early, because the next load must observe a state in which the store has already taken effect globally. In a machine with a shared coherence point, that means the store’s completion — at minimum a round trip to the point where all cores agree on the order of writes — sits on the critical path of every subsequent operation. Loads and stores from one core could no longer be pipelined past each other.

The cost is not a constant factor that better engineering removes. It is structural: SC requires that the order in which operations become visible be the same order for every observer, and any per-core buffering that hides store latency breaks exactly that. Real designs therefore keep the buffer and weaken the model, exposing the weakening to software as a small set of allowed reorderings. TSO allows a store to be delayed past a later load but not past a later store; weaker models allow almost everything and require explicit fences at the points where the program needs order.

This is the trade every weaker model makes: the model is a contract that lets the hardware reorder, and each relaxation is a specific permission granted to the implementation in exchange for a specific piece of performance.

Reading the definition as a constraint on rf

The single-total-order clause can be restated without mentioning time. An execution is SC if there exists a total order S over all events such that S extends po and, for every read r reading from write w, no write to the same location lies between w and r in S. The order is a witness, not a schedule; nothing requires that the hardware ever materialise it. This existential form is the one used by the automated checkers described in litmus tests as executable specifications, which search for a witness and report a violation when none exists.

Stated this way, two properties become visible. First, SC constrains reads only through the values they return; it says nothing about how long an operation takes, whether two operations to different locations happen simultaneously, or whether a load can be speculated. Second, SC is a property of a whole execution, so it does not follow from a property of each location taken alone — the per-location axioms can hold of every location while the whole execution fails to have a single order. Composition is a property worth checking separately rather than assuming; linearizability, unlike per-location coherence, is compositional by construction, which is why it is the correctness condition of choice for concurrent objects.

Assumptions that survive on weaker hardware

Sequential consistency is not what any current multiprocessor provides, but most correct programs never notice. The reason is the subject of the DRF-SC guarantee: a program whose conflicting accesses are all ordered by synchronisation behaves as if it ran on an SC machine, on hardware that provides SC for such programs. Dekker’s algorithm and Peterson’s algorithm, which depend on store-load ordering, fall outside that class, and both fail on a store-buffered machine unless the stores are fenced.

The practical rule that follows is narrower than “assume SC”. Assume SC for the accesses that are protected by a lock or by an acquire-release pair, and assume nothing at all about accesses that are not. That second half is not a stylistic warning. In C and C++, an unsynchronised pair of conflicting accesses is a data race and the program has no defined behaviour, which is a stronger statement than “the value is unpredictable” and is worth separating from the hardware question. The hardware question — which reorderings are physically possible — is answered by the model; the language question is answered by the contract, and the two are related but not identical.