Memory models — sequential consistency, TSO, relaxed: Worked examples

Before we start, three words we will use constantly, defined from zero:

Definition The reordering table (our reference for every example)

This is the same table the parent note gave; we reproduce it here so every example below is self-contained. Each row is a reordering $A \to B$ : an op of type $A$ (Store/Load) becoming globally visible after a later op of type $B$ .

Reordering	SC	TSO	Relaxed
Store → Load ( $S \to L$ )	forbidden	allowed	allowed
Store → Store ( $S \to S$ )	forbidden	forbidden	allowed
Load → Load ( $L \to L$ )	forbidden	forbidden	allowed
Load → Store ( $L \to S$ )	forbidden	forbidden	allowed

Figure — Memory models — sequential consistency, TSO, relaxed

Look at the board: the yellow vertical arrow on the far left shows program-text order (top box "op 1" down to bottom box "op 4"). A reordering is when the hardware lets a lower box finish before a higher box — a curved arrow jumping backwards up the column. The blue curved arrow from "op 2 (Load y)" up past "op 1 (Store x)" is the single $S \to L$ jump TSO allows. The two pink curved arrows (a store leaping past a store, a load leaping past a store) are the extra jumps only Relaxed allows.

The scenario matrix

Every cell below is covered by a worked example (Ex-N in the last column).

Cell class	Concrete question	SC	TSO	Relaxed	Example
$S \to L$ reorder	SB test, outcome $0, 0$	✗	✓	✓	Ex-1, Ex-2
$S \to S$ / $L \to L$	MP test, stale read	✗	✗	✓	Ex-3, Ex-4
$L \to S$ + coherence	LB (load-buffer) test	✗	✗	✓	Ex-5
Degenerate: one thread	any single-thread reorder	(invisible)	(invisible)	(invisible)	Ex-6
Same address (coherence only)	many ops, one location	✗ always	✗	✗	Ex-7
Limiting: fence everywhere	SB + `MFENCE` restores SC	✗	✗	✗	Ex-8
Real-world word problem	producer/consumer queue	—	✓ safe	needs rel/acq	Ex-9
Exam twist	IRIW (4-thread)	✗	✗(!)	✓	Ex-10

Ex-1 — $S \to L$ under SC (forbidden)

Worked example SB test, can

$r 1 = 0 \land r 2 = 0$ under Sequential Consistency? Shared $x = y = 0$ .

T1:  x = 1;   r1 = y;
T2:  y = 1;   r2 = x;

Forecast: guess yes or no before reading on.

Recall SC's promise. There is one total order of all four operations, and each thread's two operations keep their program order in it. Why this step? SC = "as if one interleaving", so we just have to search all interleavings.
List who must come first. For $r 1 = 0$ , T1's load of $y$ must land before T2's store $y = 1$ . For $r 2 = 0$ , T2's load of $x$ must land before T1's store $x = 1$ . Why? A load returns the last write to that address earlier in the total order; to read $0$ it must precede the write of $1$ .
Add program order. In T1, $x = 1 ≺ r 1 = y$ . In T2, $y = 1 ≺ r 2 = x$ . Why this step? Step 2 only pinned down cross-thread order; SC also forces each thread's own two ops to keep their text order, and we need those links to close the loop.
Follow the chain. From step 2+3: $x = 1 ≺ r 1 = y ≺ y = 1 ≺ r 2 = x ≺ x = 1$ The last link ( $r 2 = x ≺ x = 1$ ) closes a cycle: $x = 1$ must come before itself. Why this matters: a total order has no loops (see the $≺$ definition), so no such interleaving exists.

Verify: brute-force all $6$ interleavings that respect both threads' order — in every one, at least one load reads a $1$ . Outcome $0, 0$ never appears. ✅ Forbidden under SC.

Ex-2 — $S \to L$ under TSO (allowed)

Worked example Same SB test, same outcome, but on

TSO / x86. Forecast: SC said no — does the store buffer change the answer?

Follow the figure left to right. The blue box on the left is Core T1, the pink box on the right is Core T2, the small inner boxes labelled "SB: [...]" are the two store buffers, and the yellow box at the bottom is global memory holding x=0, y=0.

T1 issues $x = 1$ . In the figure this fills T1's store buffer SB: [x=1] (the small box under the blue core), not yet global memory. Why this step? TSO's one relaxation: a store can wait in the buffer.
T1 issues $r 1 = y$ . The curved chalk arrow from T1 down to the yellow global-memory box shows the load reading global $y$ (T1's buffer only holds $x$ , not $y$ ). Global $y$ is still $0$ , so $r 1 = 0$ . Why allowed? This is exactly the permitted $S \to L$ jump — the load overtakes the still-buffered store.
T2 does the mirror: the pink core buffers SB: [y=1] and then its load reads global $x = 0 \Rightarrow r 2 = 0$ . Why does this follow? TSO gives every core an identical, independent store buffer, so the same rule that let T1's load overtake its store lets T2's do the same — the situation is symmetric.
Both buffers drain later. The two dashed arrows in the figure show x=1 and y=1 flowing from the buffers down into global memory after the loads already ran. Why does the drain order not matter? Both loads finished in steps 2–3 while global memory still read $0$ ; whatever order the buffers drain in afterwards cannot rewrite a value already returned.

Verify: on any real x86, this outcome is observed with nonzero frequency — that is the famous TSO fact. Compared to Ex-1: SC forbids $0, 0$ , TSO allows it. See Store Buffers and Out-of-Order Execution for the microarchitecture. ✅ Allowed under TSO.

This is why Peterson and Dekker Locks need an explicit fence on x86.

Ex-3 — $S \to S$ under TSO (still forbidden → publication is free)

Worked example MP test, can consumer see

$f l a g = 1$ but stale $r = 0$ on TSO?

T1:  data = 42;  flag = 1;
T2:  while(flag==0){}  r = data;

Forecast: TSO allowed $0, 0$ above — will it also allow stale data here?

Which reordering would be needed? For T2 to see $f l a g = 1$ but $r = 0$ , either T1's two stores got reordered ( $S \to S$ : $f l a g$ visible before $d a t a$ ), or T2's two loads got reordered ( $L \to L$ ). Why this step? Identify the exact relaxation the bad outcome demands.
Check the reordering table above. Look at the $S \to S$ and $L \to L$ rows in the reference table: both read forbidden under TSO. Why? Store buffers drain in FIFO order, so stores hit memory in program order; loads also stay ordered.
Conclude. If T2 sees $f l a g = 1$ , then $f l a g = 1$ was drained, which means $d a t a = 42$ (earlier in the same FIFO) was already drained → $r = 42$ . Why does seeing $f l a g = 1$ force this? $d a t a = 42$ entered T1's FIFO buffer before $f l a g = 1$ ; a FIFO drains in insertion order, so the moment $f l a g = 1$ reaches global memory, $d a t a = 42$ must already be there — T2's later load cannot find the old $0$ .

Verify: the only outcome forbidden here would be $(f l a g seen = 1, r = 0)$ ; TSO makes it impossible → $r$ is always $42$ . ✅ Safe on TSO without a fence.

Ex-4 — $S \to S$ under Relaxed (allowed → stale read appears)

Worked example Same MP test on

ARM / POWER (relaxed). Forecast: same code, weaker chip — safe or broken?

Relaxed permits $S \to S$ . T1's write to $f l a g$ may propagate to T2's core before the write to $d a t a$ . Why? No FIFO guarantee across addresses; stores travel independently through the interconnect.
Consumer proceeds early. T2 exits its while because it sees $f l a g = 1$ , then loads $d a t a$ — still $0$ . So $r = 0$ . Why this step? Nothing tied the two propagations together.
Fix. Put a release on the store to $f l a g$ and an acquire on the load of $f l a g$ (or a DMB ISH barrier). Why does this tool force the needed ordering? A release-store publishes everything the thread wrote before it as a single package; an acquire-load that reads the released value is guaranteed to also see that whole package. So the release forbids $f l a g = 1$ from overtaking $d a t a = 42$ (killing the $S \to S$ reorder), and the matching acquire forbids T2's load of $d a t a$ from floating above its load of $f l a g$ (killing the $L \to L$ reorder) — exactly the two relaxations Ex-3 identified. This is the synchronizes-with edge.

Verify: with the fix, the outcome $(f l a g = 1, r = 0)$ becomes impossible; without it, real ARM hardware produces it. Matches Memory Barriers and Fences. ✅ Broken on relaxed unless fenced.

Ex-5 — $L \to S$ under Relaxed (the Load-Buffer test)

Worked example LB test — can

both loads read $0$ after both stores fired? Shared $x = y = 0$ .

T1:  r1 = x;   y = 1;
T2:  r2 = y;   x = 1;

Forecast: each thread reads then writes — can $r 1 = 0 \land r 2 = 0$ happen?

What outcome is interesting? $r 1 = 0 \land r 2 = 0$ : both loads see the initial value even though both stores of $1$ occur.
Under SC/TSO it is forbidden. Both models keep $L \to S$ in order, so in the single global order each thread's load precedes its own store: $r 1 = x ≺ y = 1$ and $r 2 = y ≺ x = 1$ . For a load to read $0$ it must come before the other thread's store of that variable: reading $r 2 = 0$ needs $r 2 = y ≺ y = 1$ , and reading $r 1 = 0$ needs $r 1 = x ≺ x = 1$ . Chain them: $r 2 = y ≺ y = 1$ , and program order gives $r 1 = x ≺ y = 1$ as well — but to force a cycle we combine the store→load observations. Concretely $r 1 = x ≺ y = 1 ≺ r 2 = y ≺ x = 1 ≺ r 1 = x$ closes a loop only if $y = 1 ≺ r 2 = y$ , i.e. if $r 2$ read the $1$ — contradiction with $r 2 = 0$ . The clean statement: forbidding $L \to S$ means each load is globally ordered before its own store, and one checks by enumeration that no total order lets both loads read $0$ . Why forbidden? Same "no total order works" fact as Ex-1, verified below by brute force.
Under Relaxed it is allowed. A core may let its store become globally visible before its own earlier load has committed — the store address ( $y$ for T1) is independent of the load address ( $x$ ), so the interconnect can publish $y = 1$ while T1's load of $x$ is still in flight and ends up reading the old $0$ . This is the physical $L \to S$ reorder: not speculation, but the store propagating to memory ahead of the prior load's completion. Why this step? Relaxed hardware places no ordering between a load and a later independent store.

Verify: on x86/TSO the $(0, 0)$ outcome is never observed; on POWER it is documented and observed. The distinguishing reordering is exactly $L \to S$ . ✅ Only Relaxed allows it.

Ex-6 — Degenerate case: a single thread (nothing is visible)

Worked example One thread reorders itself — does anyone notice?

T1:  a = 1;  b = 2;  r = a;   // no other threads

Forecast: the CPU may reorder $a = 1$ and $b = 2$ . Can $r$ ever be wrong?

Same-address dependency. $r = a$ depends on $a = 1$ . Hardware must honor this: a load sees the most recent same-address store from its own core (store forwarding). Why? Per-location coherence + single-thread program-order illusion are guaranteed by every model.
Cross-address reorder is invisible. Swapping $a = 1$ and $b = 2$ changes no observable single-thread result, since no one else reads them. Why this step? The whole reason reordering is legal is that a lone thread cannot tell.

Verify: $r = 1$ under SC, TSO, and Relaxed alike — the degenerate row of the matrix. Reordering only bites with $\geq 2$ threads. ✅

Ex-7 — Same-address case (coherence only)

Worked example Many accesses to the

same location — can a reader see them out of order?

T1:  x = 1;
T2:  x = 2;
T3:  r1 = x;  r2 = x;

Forecast: can T3 read $r 1 = 2$ then $r 2 = 1$ (going "backwards")?

This is coherence, not the memory model. All accesses hit one address, so the four-reordering table doesn't apply. Why? The parent note said single-location ordering is handled by Cache Coherence (MESI) and assumed everywhere.
Coherence rule (CoRR): there is a single global order of writes to $x$ , and no thread reads them out of that order. If T3 saw $2$ then $1$ , it read $x$ backwards in the write order — forbidden. Why? MESI (Modified / Exclusive / Shared / Invalid — the four states a cache line can be in) serializes writes to a line: before any core writes, it takes the line into the Modified state with exclusive ownership, so writes to that one line are globally sequenced. See Cache Coherence (MESI).

Verify: $(r 1, r 2) = (2, 1)$ is impossible on every model including relaxed; only $(1, 1), (1, 2), (2, 2)$ (and $(0, \cdot)$ if it reads before either) occur. ✅ Same-address ⇒ always ordered.

Ex-8 — Limiting case: fence everywhere restores SC

Worked example SB test with an

MFENCE inserted — recompute the answer.

T1:  x = 1;  MFENCE;  r1 = y;
T2:  y = 1;  MFENCE;  r2 = x;

Forecast: Ex-2 allowed $0, 0$ . Does the fence kill it?

Read the figure top to bottom on the left: the three stacked boxes are x = 1, then the yellow MFENCE (drain) box, then r1 = y. The yellow arrow on the right shows the fence pushing x=1 out into the blue global-memory box.

What MFENCE does. It drains the store buffer: no later load may execute until the earlier store is globally visible. In the figure this is the yellow "fence forces x to memory" arrow that must complete before control reaches the r1 = y box. Why this tool? It surgically removes the only TSO relaxation ( $S \to L$ ) exactly where we need SC.
Re-establish the ordered links. The fence forces $x = 1 ≺ r 1 = y$ in T1 (the store is global before the load runs), and symmetrically $y = 1 ≺ r 2 = x$ in T2. Why this step? Ex-2's escape depended entirely on the load overtaking the still-buffered store; killing the $S \to L$ jump reinstates program order between each thread's store and its own load — exactly the links Ex-1 used.
Re-run the cycle argument. For the bad outcome we still need $r 1 = y ≺ y = 1$ (so $r 1$ reads $0$ ) and $r 2 = x ≺ x = 1$ (so $r 2$ reads $0$ ). Combine with step 2: $x = 1 ≺ r 1 = y ≺ y = 1 ≺ r 2 = x ≺ x = 1$ This is the same cycle as Ex-1 — $x = 1$ before itself. Why this matters? A total order has no loops, so $0, 0$ is now impossible; the fence has restored SC for this pattern.
Cost. Each fence forces a global round trip (the store must reach memory before the load proceeds); that is why we fence only where correctness needs it, not everywhere. Why note this? The limiting "fence everywhere" corner is correct but slow — the whole point of weak models is to avoid paying it when unneeded.

Verify: with fences the outcome set equals SC's set → $0, 0$ impossible (brute-force below over all fence-respecting interleavings). This is the maximally-fenced corner of the matrix, and the fix Dekker/Peterson need. ✅ See Memory Barriers and Fences.

Ex-9 — Real-world word problem: a one-slot mailbox

Worked example A logger thread hands a message pointer to a printer thread.

Producer:  msg->text = "hi";  ready = true;
Consumer:  while(!ready){}  print(msg->text);

The team ships on x86 and it works. They port to an ARM phone and sometimes print garbage. Explain, and give the portable fix.

Forecast: which model change caused garbage, and what one annotation fixes it everywhere?

On x86 (TSO): this is the MP pattern (Ex-3). $S \to S$ is forbidden, so text is published before ready. Works — but by luck of the chip. Why? The code has no explicit ordering.
On ARM (Relaxed): $S \to S$ allowed (Ex-4). ready=true reaches the consumer before msg->text, so print dereferences stale/garbage. Why? Independent store propagation.
Portable fix in C++: make ready a std::atomic<bool>; store it with memory_order_release, load it with memory_order_acquire. The release→acquire pair makes everything before the release happen-before everything after the acquire. Why this tool and not MFENCE? The language model lets the compiler emit the minimum barrier per target (nothing on x86, dmb on ARM).

Verify: after the fix the stale-read outcome is impossible on both targets; before it, only ARM shows garbage. This is the lock-free publication idiom. ✅

Ex-10 — Exam twist: IRIW (Independent Reads of Independent Writes)

Worked example Four threads. Two writers, two readers — can the readers

disagree on the order of two independent writes? Shared $x = y = 0$ .

T1:  x = 1;
T2:  y = 1;
T3:  r1 = x;  r2 = y;
T4:  r3 = y;  r4 = x;

Forecast: can $r 1 = 1, r 2 = 0$ (T3 saw $x$ first) and $r 3 = 1, r 4 = 0$ (T4 saw $y$ first) at once?

What the outcome means. T3 thinks " $x$ became $1$ before $y$ "; T4 thinks " $y$ became $1$ before $x$ " — the two writes have no agreed global order.
Under SC: impossible. A single total order fixes which of $x = 1, y = 1$ came first; both readers must respect it. Why? SC = one total order for everyone.
Under TSO: also impossible(!) — this is the exam trap. TSO has per-core store buffers, but once a store leaves the buffer it enters one shared memory that all cores agree on (TSO is "multi-copy atomic"). Why does this kill the outcome? If there is a single shared memory, the moment $x = 1$ and $y = 1$ land they land in some order, and every reader that observes both must observe that same order — so T3 and T4 cannot disagree.
Under Relaxed (POWER, old ARM): allowed — writes can propagate to different readers in different orders (non-multi-copy-atomic). Why? There is no single global memory; each core gets its own view as messages arrive, so $x = 1$ can reach T3 first while $y = 1$ reaches T4 first, and the two readers genuinely disagree.

Verify: IRIW forbidden by SC and TSO, allowed by non-MCA relaxed models — the sharpest line between "TSO" and "truly weak". ✅ This is why "x86 is strong" does not generalise to "all reorderings are the same on every strong chip."

Wrap-up

Recall Which single reordering distinguishes each pair of models?

SC vs TSO ::: store→load (SB test, Ex-1/Ex-2) TSO vs Relaxed ::: store→store or load→load (MP test, Ex-3/Ex-4) and load→store (LB, Ex-5) The IRIW surprise ::: TSO still forbids it (multi-copy atomic); only non-MCA relaxed allows it (Ex-10)

Related: parent topic · Hinglish version.