5.2 An Example Relaxed Consistency Model (XC)

For teaching purposes the book introduces an eXample relaxed Consistency model — XC — capturing the basic idea and implementation potential of relaxed models. Like SC and TSO (and the largely defunct Alpha and SPARC RMO models it resembles), XC assumes a global memory order exists.

5.2.1 The basic idea

By default, XC leaves loads and stores unordered. A FENCE — other models say barrier, memory barrier, membar, or sync — is how a programmer asks for order: if core Ci executes operations Xi, then a FENCE, then operations Yi, memory order puts all Xi before the FENCE and the FENCE before all Yi. Four properties are worth pinning down:

A FENCE specifies no address.
Two FENCEs by the same core stay ordered.
A FENCE does not affect other cores’ operations — which is why “fence” is a better name than “barrier.”
Real architectures offer multiple FENCE flavors with different ordering properties (§5.6’s RVWMO has six); this chapter uses only full FENCEs.

So XC’s memory order respects program order for:

Load → FENCE, Store → FENCE, FENCE → FENCE, FENCE → Load, FENCE → Store — the five FENCE rules, and
Load → Load, Load → Store, Store → Store to the same address only — TSO’s rules, kept to preserve sequential core semantics and prevent astonishment: without same-address Store→Store, a critical section running A = 1 then A = 2 could finish with A = 1; without same-address Load→Load, reading B twice could see B’s value go from new back to old.

Finally, like TSO’s write-buffer bypassing , XC ensures loads immediately see updates from their own stores — again preserving single-thread sequentiality.

5.2.2 Examples using FENCEs

Without FENCEs, XC demolishes §5.1’s flag idiom — all four outcomes appear:

Table 5.1's program under raw XC — no FENCEs

Core C1	Core C2
S1: data1 = NEW;	L1: r1 = flag;
S2: data2 = NEW;	L2: r2 = data1;
S3: flag = SET;	L3: r3 = data2;

Initially data1 = 0, data2 = 0, flag = 0. Table 5.1: what order ensures r2 and r3 always get NEW?

Model:

Possible outcomes (r2, r3) under XC (FENCEs only):

(NEW, NEW)SC

90 executions — show one

S1 → S2 → S3 → L1 → L2 → L3

(0, NEW)not SC

90 executions — show one

L2 → S1 → S2 → S3 → L1 → L3

(NEW, 0)not SC

90 executions — show one

S1 → L3 → S2 → S3 → L1 → L2

(0, 0)not SC

90 executions — show one

L3 → L2 → S1 → S2 → S3 → L1

XC enumeration reorders each thread freely EXCEPT across a FENCE and for same-address Load→Load / Load→Store / Store→Store; (bypass) = the load read its own thread's program-order-earlier store even though that store enters memory order later (the extended value rule).

Only executions where C2's spin loop has exited (r1 = SET) are shown — the book's L1/B1 loop repeats until flag reads SET.

Table 5.3 repairs it. One FENCE orders the data stores before the flag store; one orders the flag observation before the data loads:

Table 5.3: Table 5.1 with the FENCEs XC needs

Core C1	Core C2
S1: data1 = NEW;	L1: r1 = flag;
S2: data2 = NEW;	F2: FENCE
F1: FENCE	L2: r2 = data1;
S3: flag = SET;	L3: r3 = data2;

Initially data1 = 0, data2 = 0, flag = 0. Table 5.3: Table 5.1's program with the FENCEs XC needs.

Model:

Possible outcomes (r2, r3) under XC (FENCEs only):

(NEW, NEW)SC

4 executions — show one

S1 → S2 → F1 → S3 → L1 → F2 → L2 → L3

Only executions where C2's spin loop has exited (r1 = SET) are shown — the book's L1/B1 loop repeats until flag reads SET.

The chain is now S1, S2 → F1 → S3 → L1 loads SET → F2 → L2, L3. The store-side FENCE F1 surprises no one; the load-side FENCE F2 does. But allowing loads to execute out of order can make in-order stores look out of order: run L2 early — L2, S1, S2, S3, L1, L3 — and r2 reads 0. The trap is sharpest for a program without B1’s control dependence, where L1 and L2 are just consecutive loads to different addresses and reordering them “seems reasonable, but is not.”

For the critical-section program, Table 5.4 conservatively surrounds every acquire and release with FENCEs (the book notes some are removable — §5.5’s release consistency makes that precise):

Core C1	Core C2	Comments
`F11: FENCE` `A11: acquire(lock)` `F12: FENCE`
Some loads L1i interleaved with some stores S1j		/* Arbitrary interleaving of L1i's & S1j's */
`F13: FENCE` `R11: release(lock)` `F14: FENCE`	`F21: FENCE` `A21: acquire(lock)` `F22: FENCE`	/* Handoff from critical section 1 to 2 */
	Some loads L2i interleaved with some stores S2j	/* Arbitrary interleaving of L2i's & S2j's */
	`F23: FENCE` `R22: release(lock)` `F24: FENCE`

FENCEs F13 and F22 carry the handoff: All L1i, All S1j → F13 → R11 → A21 → F22 → All L2i, All S2j.

5.2.3 Formalizing XC

Using chapter 3’s notation, an XC execution requires:

1. FENCE rules — all cores insert loads, stores, and FENCEs into $<_m$ respecting:

\begin{aligned} L(a) <_p \text{FENCE} &\Rightarrow L(a) <_m \text{FENCE} \\ S(a) <_p \text{FENCE} &\Rightarrow S(a) <_m \text{FENCE} \\ \text{FENCE} <_p \text{FENCE} &\Rightarrow \text{FENCE} <_m \text{FENCE} \\ \text{FENCE} <_p L(a) &\Rightarrow \text{FENCE} <_m L(a) \\ \text{FENCE} <_p S(a) &\Rightarrow \text{FENCE} <_m S(a) \end{aligned}

2. Same-address rules — loads and stores to the same address stay ordered:

\begin{aligned} L(a) <_p L'(a) &\Rightarrow L(a) <_m L'(a) \\ L(a) <_p S(a) &\Rightarrow L(a) <_m S(a) \\ S(a) <_p S'(a) &\Rightarrow S(a) <_m S'(a) \end{aligned}

3. Value rule — exactly TSO’s extended rule, bypassing included:

\text{val}(L(a)) = \text{val}\big(\operatorname{MAX}_{<_m}\{\, S(a) \mid S(a) <_m L(a) \ \textbf{or}\ S(a) <_p L(a) \,\}\big)

Table 5.5 summarizes the rules with one new letter — A, an ordering enforced only if the operations target the same address:

Op 1 ↓ \ Op 2 →	Load	Store	RMW	FENCE
Load	A	A	A	X
Store	B	A	A	X
RMW	A	A	A	X
FENCE	X	X	X	X

X = ordering enforced · B = bypassing required if same address · A = ordering enforced only if same address · hover any cell

Table 5.5 (recreated): XC ordering rules. The nine A entries are where XC differs from TSO’s Table 4.4 — every X outside the FENCE row and column weakened to same-address-only.

An implementation that allows only XC executions is an XC implementation.

5.2.4 The examples, operating correctly

Why do the FENCEd programs work? Figure 5.1a shows an XC execution of Table 5.3 in which C1’s stores S1/S2 swapped in memory order, as did C2’s loads L2/L3 — watch the program-order arrows cross:

Figure 5.1a (recreated): an XC execution of Table 5.3. S2 enters memory order before S1, and L3 before L2 — legal, and harmless.

Figure 5.1b (recreated): an SC execution of the same program. As far as any programmer can tell, the two executions are equivalent.

The same holds for the critical-section program (the book’s Figure 5.2): within each “arbitrary interleaving” block, XC may shuffle the loads L1i and stores S1j against each other — but the lock handoff chain F13 → R11 → A21 → F22 pins everything a second thread could observe, so the XC execution is again equivalent to an SC execution in which nothing reordered.

These examples demonstrate the chapter’s pivotal claim: with sufficient FENCEs, a relaxed model like XC can appear to programmers as SC — generalized properly in §5.4’s “SC for data-race-free.”

Check yourself

1.Which orderings does XC enforce WITHOUT the programmer asking?

2.In Table 5.3, most readers accept the store-side FENCE F1 — why is the LOAD-side FENCE F2 also necessary?

3.Table 5.5 introduces the entry "A" alongside X and B. What does A mean?

4.In Table 5.4's conservatively FENCEd critical sections, which FENCEs make the handoff from critical section 1 to critical section 2 correct?

5.Figure 5.1a shows an XC execution where C1's stores S1/S2 swapped and C2's loads L2/L3 swapped. Why does the book call it EQUIVALENT to the SC execution of Figure 5.1b?

5 questions