Two threads run on two cores. Thread 0 sets x = 1 and then reads y; thread 1 sets y = 1 and then reads x. Both start with x = y = 0. Can both reads return 0? Intuition says no: one of the stores must have happened first, so at least one thread must see a 1. On an x86 processor, and on Arm, both reads can return 0. Nothing is broken; the processors follow their memory models.
Which orders of memory accesses may a processor show, and how do protocols underneath affect it?
The obvious model is that memory accesses happen one at a time, in some interleaving of each thread's program order. That model, sequential consistency (SC), forbids both reads returning 0. But every core has a store buffer (lesson 7.8) so that stores need not wait for memory, and a load may complete while an earlier store is still in that buffer. Unless the hardware hides it, a load can pass an earlier store, and SC is gone. Each architecture states precisely which such reorderings software may see: its memory consistency model.
Model | Reorderings software may see | Examples |
|---|---|---|
Sequential consistency | None: one global interleaving of all program-order accesses | A reference model; few processors implement it for performance reasons |
Total Store Order (TSO) | Only a later load passing an earlier store to a different address (store buffering) | x86; RISC-V with the Ztso extension |
Weak (relaxed) models | Loads and stores to different addresses may be reordered unless a barrier or dependency forbids it | Arm, Power, RISC-V (RVWMO, its default) |
Two short litmus tests tell them apart:
SB (store buffering): T0: x = 1; r1 = y. T1: y = 1; r2 = x. Is r1 = r2 = 0 possible? SC: no. TSO and weak: yes.
MP (message passing): T0: x = 1; y = 1 (data, then flag). T1: r1 = y; r2 = x. Is r1 = 1, r2 = 0 possible (flag seen, data not)? SC and TSO: no. Weak: yes, unless barriers are added.
The model runs both tests under three models: SC (every interleaving in program order), TSO (each thread's stores wait in a FIFO store buffer; its loads read its own buffer first), and a relaxed model (a thread's two accesses to different addresses may happen in either order). It collects every possible outcome.
"""Enumerate the outcomes of two litmus tests under three memory models.
SB (store buffering): T0: x=1; r1=y T1: y=1; r2=x (x = y = 0 at start)
MP (message passing): T0: x=1; y=1 T1: r1=y; r2=x
SC: every interleaving of the two threads, each in program order
TSO: like SC, but each thread's stores wait in a FIFO store buffer; its loads
read its own buffer first; buffers drain to memory at any time
relaxed: a thread may perform its two accesses in either order (they are to
different addresses), then SC on the result
"""
from itertools import permutations
SB = ([("st", "x"), ("ld", "y", "r1")], [("st", "y"), ("ld", "x", "r2")])
MP = ([("st", "x"), ("st", "y")], [("ld", "y", "r1"), ("ld", "x", "r2")])
def interleavings(a, b):
if not a or not b:
yield list(a) + list(b)
return
for rest in interleavings(a[1:], b):
yield [a[0]] + rest
for rest in interleavings(a, b[1:]):
yield [b[0]] + rest
def sc(test):
out = set()
tagged = [[(t, op) for op in ops] for t, ops in enumerate(test)]
for order in interleavings(*tagged):
mem, regs = {"x": 0, "y": 0}, {}
for _, op in order:
if op[0] == "st":
mem[op[1]] = 1
else:
regs[op[2]] = mem[op[1]]
out.add((regs["r1"], regs["r2"]))
return out
def tso(test):
out = set()
def step(pcs, bufs, mem, regs):
moved = False
for t, ops in enumerate(test):
if pcs[t] < len(ops): # execute the thread's next instruction
op = ops[pcs[t]]
np, nb, nr = list(pcs), [list(b) for b in bufs], dict(regs)
np[t] += 1
if op[0] == "st":
nb[t].append(op[1])
else:
nr[op[2]] = 1 if op[1] in nb[t] else mem[op[1]]
step(np, nb, dict(mem), nr)
moved = True
if bufs[t]: # or drain the oldest buffered store
nb = [list(b) for b in bufs]
addr = nb[t].pop(0)
nm = dict(mem); nm[addr] = 1
step(list(pcs), nb, nm, dict(regs))
moved = True
if not moved:
out.add((regs["r1"], regs["r2"]))
step([0, 0], [[], []], {"x": 0, "y": 0}, {})
return out
def relaxed(test):
out = set()
for a in permutations(test[0]):
for b in permutations(test[1]):
out |= sc((list(a), list(b)))
return out
for name, test, bad in (("SB", SB, (0, 0)), ("MP", MP, (1, 0))):
for model in (sc, tso, relaxed):
outs = sorted(model(test))
flag = "allowed" if bad in outs else "forbidden"
print(f"{name} {model.__name__:7s}: outcomes {outs}; (r1, r2) = {bad} {flag}")
assert (0, 0) not in sc(SB) and (0, 0) in tso(SB) and (0, 0) in relaxed(SB)
assert (1, 0) not in sc(MP) and (1, 0) not in tso(MP) and (1, 0) in relaxed(MP)
print("PASS: TSO adds only the store-buffering outcome; a relaxed model also breaks message passing")It prints:
SB sc : outcomes [(0, 1), (1, 0), (1, 1)]; (r1, r2) = (0, 0) forbidden
SB tso : outcomes [(0, 0), (0, 1), (1, 0), (1, 1)]; (r1, r2) = (0, 0) allowed
SB relaxed: outcomes [(0, 0), (0, 1), (1, 0), (1, 1)]; (r1, r2) = (0, 0) allowed
MP sc : outcomes [(0, 0), (0, 1), (1, 1)]; (r1, r2) = (1, 0) forbidden
MP tso : outcomes [(0, 0), (0, 1), (1, 1)]; (r1, r2) = (1, 0) forbidden
MP relaxed: outcomes [(0, 0), (0, 1), (1, 0), (1, 1)]; (r1, r2) = (1, 0) allowed
PASS: TSO adds only the store-buffering outcome; a relaxed model also breaks message passingTSO adds exactly one outcome to SC: store buffering, (0, 0) in SB. It still forbids the stale message (1, 0) in MP, which is why data-then-flag code works on x86 without barriers. The relaxed model allows both, which is why the same code on Arm needs a barrier (or release and acquire) between the data and the flag on the writing side, and between the flag and the data on the reading side.
The interconnect must not be weaker than the processor's model promises. If an x86-style core relies on TSO for message passing, the fabric must not let its stores reach memory out of order: stores from one core must become visible in order.
Barriers must reach the fabric. A processor barrier is only as good as the fabric's ability to drain or order the accesses before it (lesson 7.5).
Devices see the same rules. A device reading memory that processors write sees the memory model's guarantees only if the protocol carries them, for example through ordering rules and coherence (Part 13).
A lock-free queue (illustrative) written and tested on x86 used plain stores to write an entry and then publish its index. Ported to Arm, consumers occasionally read entries that had not been written yet: MP's (1, 0) outcome, allowed on a weak model. Adding release semantics to the index store and acquire semantics to the index load fixed it, at almost no cost.
No: TSO keeps stores in order (the store buffer is FIFO), which is why message passing works under TSO.
A barrier (or a release store) between the data store and the flag store, and a barrier (or acquire load) between the flag load and the data load.
A memory consistency model states which access reorderings software may observe.
SC allows none; TSO (x86) allows only store buffering; weak models (Arm, Power, RISC-V RVWMO) allow more unless barriers forbid it.
The fabric underneath must be at least as strong as the processors' model promises, and must honour their barriers.