Memory consistency models: Worked examples — Hardware deep dive

Intuition What this page is

The parent note gave you the rulebook. This page exercises every cell of that rulebook: each model (SC → TSO → Weak), each reordering pair (L→L, L→S, S→S, S→L), the degenerate cases (one core, no sharing), the limiting case (everything fenced), and the twists (transitivity, IRIW). By the end no litmus test can surprise you.

One vocabulary reminder before we start, so no symbol is unearned:

A load L = a read from memory. A store S = a write to memory.
Program order = the top-to-bottom order the instructions are written in for one core.
Globally visible = the moment every other core could observe the effect.
The notation $a <_{m} b$ read aloud is " $a$ happens before $b$ in the one true global order the memory system commits to." The subscript $m$ = "memory order".

The scenario matrix

Every litmus test we can face is one row of this table. The goal of the 8 examples below is to fill every cell at least once.

#	Case class	Concrete question	Models that differ here
A	S→L reorder (store buffer)	Store-Buffering: can both loads read stale 0?	SC=No, TSO/x86=Yes
B	S→S reorder	Message-passing flag: can consumer see flag but stale data?	SC/TSO=No, Weak=Yes
C	L→L reorder	Load-buffering: can two loads be reordered before their stores?	SC/TSO=No, Weak=Yes
D	Degenerate: single core	Does a core ever see its own ops out of order?	All models: No
E	Degenerate: no sharing	Two cores, disjoint addresses — any interaction?	All models: No
F	Cycle test (proof)	Prove SC forbids the SB bad outcome	SC only
G	Multi-copy atomicity (IRIW)	Do two readers agree on the order of two writes?	SC/TSO=Yes agree, POWER/ARM=No
H	Limiting case: full fences	Insert `MFENCE` — does TSO recover SC?	recovers SC
I	Real-world twist	Spin-lock acquire/release correctness	needs acquire/release
J	Exam twist: transitivity	WWC / cumulative barriers across 3 cores	Weak needs cumulative fence

Example A — Store→Load reorder (cell A)

Worked example Store-Buffering (Dekker core)

Init x = 0, y = 0.

Core 1	Core 2
`x = 1` (S1)	`y = 1` (S3)
`r1 = y` (L2)	`r2 = x` (L4)

On x86 (TSO), can we finish with r1 == 0 && r2 == 0?

Forecast: guess Yes or No before reading on.

Answer: Yes.

What: S1 writes x=1 but the value first lands in Core 1's store buffer, not memory. Why this step? TSO's only relaxation is that a store can sit buffered while the core races ahead — this is the S→L cell.
What: L2 reads y. Memory still holds y=0 (S3 is also stuck in Core 2's buffer). So r1 = 0. Why: the buffered store on the other core is not yet globally visible.
What: Symmetrically, L4 reads x=0, so r2 = 0. Why: both cores did the same trick at once — this is the whole point of a store buffer.

Verify: Under SC this is impossible (Example F proves it). Under TSO the two buffered stores plus two early loads give exactly (r1,r2) = (0,0). This matches the parent's canonical claim. ✅

Example B — Store→Store reorder (cell B)

Worked example Message passing on weak hardware

Init data = 0, flag = 0.

Core 1 (producer)	Core 2 (consumer)
`data = 42` (S1)	`while(flag==0){}` (L3)
`flag = 1` (S2)	`r = data` (L4)

On ARM (weak), after the consumer sees flag==1, can r == 0?

Forecast: Yes or No?

Answer: Yes — r can be the stale 0.

What: On weak hardware S1 and S2 have no S→S ordering — flag=1 may reach Core 2 before data=42. Why this step? This is the S→S cell; TSO forbids it, ARM does not.
What: Consumer's loop L3 sees flag==1, exits, then L4 reads data — but data=42 hasn't propagated yet, so r=0. Why: the two writes traveled independently.
Fix: producer inserts a release fence between S1 and S2; consumer inserts an acquire fence after L3. See Memory Barriers and Fences and C++ Memory Model (acquire-release). Why: a release-acquire pair recreates the S→S / L→L ordering the algorithm needs.

Verify: On TSO/x86 S→S is preserved, so r is guaranteed 42 — the pattern works fence-free there. On ARM without fences r ∈ {0, 42}. Both outcomes are legal on weak, only 42 on TSO. ✅

Example C — Load→Load reorder (cell C)

Answer: Only on Weak (ARM/POWER); No on SC and TSO.

What: r1==1 means L1 read the value written by S4. r2==1 means L3 read the value written by S2. Why this step? We are asking whether a load can effectively slide after the store below it — the L→S / L→L relaxation.
What: For this to happen, S4 must be visible before L1, and S2 visible before L3 — but program order has L1<S2 and L3<S4. Why: on SC/TSO loads never bypass later stores of the same core, so no core can publish its store before completing its earlier load.
What: On ARM the load may be delayed / speculated past the store, allowing both 1s. Why: weak models drop L→L and L→S ordering by default.

Verify: SC/TSO table rows both show L→S = ✅, so LB's (1,1) is impossible there; ARM's row is all ❌ so it is allowed. ✅

Example D — Single core sees itself in order (cell D)

Worked example A core reading its own writes

x = 5     (S1)
r = x     (L2)

What is r?

Forecast: could a store buffer ever hand back the old value here?

Answer: r = 5, always, on every model.

What: Even in TSO the store x=5 sits in the buffer, but a later load of the same address checks the buffer first — store forwarding. Why this step? This is the degenerate single-core case; consistency models only govern what other cores see, never a core's view of itself.
What: So L2 sees the freshest value 5 regardless of drain timing. Why: every model preserves per-core, per-address program order — that is the Cache Coherence guarantee plus store forwarding, see Store Buffers and Write Buffering.

Verify: r = 5. No model permits r = 0 here. This is the invariant that keeps single-threaded code correct. ✅

Answer: (1, 1) on every model.

What: Each core reads only its own address, which it just wrote. Why this step? With no shared address there is nothing for a consistency model to constrain — it degenerates to two independent single-core programs (cell D twice).
What: Store forwarding gives each r its own core's fresh write. Why: cross-core ordering rules never fire when no location is shared.

Verify: (r1, r2) = (1, 1). Reordering is invisible without sharing. ✅

Example F — Cycle proof: SC forbids SB's bad outcome (cell F)

What: r1==0 ⇒ in the single total order $<_{m}$ , load L2 (read y) came before store S3 (write y). So $L 2 <_{m} S 3$ . Why this step? SC gives one total order consistent with each program order; a load returning the initial 0 must precede the store that would change it.
What: r2==0 ⇒ likewise $L 4 <_{m} S 1$ .
What: Program order forces $S 1 <_{m} L 2$ (Core 1) and $S 3 <_{m} L 4$ (Core 2). Why: SC never reorders a core's own operations.
What: Chain them: $S 1 <_{m} L 2 <_{m} S 3 <_{m} L 4 <_{m} S 1$ . Why: substitute the four facts head-to-tail.
What: That says $S 1 <_{m} S 1$ — a cycle. A total order is antisymmetric, so this is a contradiction. ∎

Verify: The dependency graph has a 4-node directed cycle, so no total order exists ⇒ SC forbids (0,0). This is why store buffers (TSO) are strictly weaker than SC. ✅

Example G — Do two readers agree? IRIW (cell G)

Worked example Independent Reads of Independent Writes

Init x=0, y=0.

C1	C2	C3	C4
`x=1` (S1)	`y=1` (S2)	`r1=x` (L3)	`r3=y` (L5)
		`r2=y` (L4)	`r4=x` (L6)

Can r1=1, r2=0, r3=1, r4=0 (C3 sees x first, C4 sees y first)?

Forecast: Yes or No?

Answer: No on SC and TSO. Yes on POWER/ARM (non-multi-copy-atomic).

What: The outcome asks whether two independent writes are observed in different orders by different readers. Why this step? This is a stronger property than any single-core reordering — it is about whether a single global store order even exists.
What: SC/TSO both commit stores to one total store order, so all readers agree ⇒ the outcome is impossible. Why: "single total order" is exactly what SC/TSO promise about stores.
What: POWER/ARM may propagate x=1 to C3 early while y=1 reaches C4 early — writes are not multi-copy-atomic. Why: weak interconnects deliver writes to different cores at different times.

Verify: SC/TSO forbid the split-observation (1,0,1,0); POWER/ARM allow it. Recovering agreement on weak hardware needs a cumulative barrier (cell J). ✅

Example H — Limiting case: fences recover SC (cell H)

Worked example SB with a fence on each core

Take SB (Example A) and insert an MFENCE between each store and load:

Core 1	Core 2
`x = 1` (S1)	`y = 1` (S3)
`MFENCE`	`MFENCE`
`r1 = y` (L2)	`r2 = x` (L4)

On x86, can r1==0 && r2==0 now?

Answer: No — the fences restore SC for this test.

What: MFENCE drains the store buffer, forcing S1 to become globally visible before L2 executes. Why this step? This is the limiting case: turning the one TSO relaxation (S→L) back on gives full SC ordering locally. See Memory Barriers and Fences and Atomic Operations and Locks.
What: Now at least one store is truly first in the global order, so both loads cannot both read 0 — reuse the cycle argument of Example F. Why: with S→L re-enforced, the SB ordering graph is acyclic-impossible for (0,0).

Verify: With fences, TSO's L→L, L→S, S→S, and S→L are all enforced ⇒ table row equals SC ⇒ (0,0) forbidden. The fence is the "dial" from TSO back to SC. ✅

Example I — Real-world twist: a spin-lock (cell I)

Worked example Acquire/release lock

// acquire:  while ( test_and_set(lock) ) {}      // ACQUIRE
//   ... critical section reads/writes shared data ...
// release:  store(lock, 0)                        // RELEASE

On ARM, will the critical section's memory ops stay inside the lock?

Forecast: does the lock alone guarantee it?

Answer: Only if test_and_set has acquire semantics and the release store has release semantics.

What: A plain load/store lock on ARM lets critical-section reads hoist above the acquire (L→L relaxed) or writes sink below the release (S→S relaxed). Why this step? Without ordering, another thread could observe the "unlocked" state while our writes are still in flight — corrupting shared data.
What: Acquire = no later op may be reordered before it. Release = no earlier op may be reordered after it. Why: together they form a one-way fence pair that boxes the critical section — exactly the C++ Memory Model (acquire-release) guarantee.
What: On x86/TSO a LOCK-prefixed test-and-set already drains the buffer, so the lock works with weaker source annotations. Why: TSO only lacked S→L, which the locked atomic fixes.

Verify: Acquire on lock-in + release on lock-out ⇒ every critical-section op is ordered between them ⇒ no leak. This is the standard correctness proof for mutual exclusion under weak models. ✅

Example J — Exam twist: transitivity / cumulativity (cell J)

Worked example Write-to-Read Causality across 3 cores (WRC)

Init x=0, y=0.

C1	C2	C3
`x = 1` (S1)	`r1 = x` (L2)	`r2 = y` (L4)
	`y = 1` (S3)	`r3 = x` (L5)

If r1==1 and r2==1, must r3==1?

Forecast: does causality chain through the middle core?

Answer: On SC/TSO yes. On plain ARM/POWER, not unless C2's fence is cumulative.

What: r1==1 means C2 saw C1's x=1; then C2 published y=1; r2==1 means C3 saw that y. Why this step? Intuitively causality should carry x=1 along the chain C1→C2→C3.
What: On non-multi-copy-atomic hardware, x=1 may still not have reached C3 even though y=1 has, so r3 can be 0. Why: ordinary barriers order only the fencing core's own ops; they don't force previously observed writes to also propagate — that stronger property is cumulativity.
What: A cumulative release fence (e.g. ARM dmb ish / release store) forces C1's x=1 to propagate before C2's y=1, so r3 must be 1. Why: cumulativity extends the fence's reach to writes the core has read, not just written.

Verify: SC/TSO: single store order ⇒ r3 forced to 1. Plain weak: r3 ∈ {0,1}. Cumulative fence on C2 ⇒ r3 = 1. This is the classic "barriers aren't automatically transitive" exam trap. ✅

Recall Which cell does each example hit?

Example A hits which reordering pair? ::: S→L (store buffer) Example B relaxes which pair, and on which model only? ::: S→S, on Weak/ARM only Example C (Load-Buffering) is impossible on which models? ::: SC and TSO Example F proves impossibility using what graph property? ::: a directed cycle in the memory order IRIW (G) distinguishes which hardware property? ::: multi-copy atomicity (single vs. per-core store propagation) Example H shows a fence dials TSO up to which model? ::: Sequential Consistency (SC) Example J's trap is that ordinary barriers lack what property? ::: cumulativity (transitivity across cores)

Back to Memory consistency models · prerequisite recap: Out-of-Order Execution, Store Buffers and Write Buffering.

Core 1	Core 2
`r1 = x` (L1)	`r2 = y` (L3)
`y = 1` (S2)	`x = 1` (S4)

Core 1	Core 2
`a = 1` (S1)	`b = 1` (S3)
`r1 = a` (L2)	`r2 = b` (L4)