4.3A Little TSO/x86 Formalism

Three edits to SC’s definition

TSO’s formal definition is SC’s definition with exactly three changes.

Change 1 — drop Store→Load (enable the FIFO write buffer). All cores still insert their loads and stores into $<_m$ respecting program order for the other three cases, same or different addresses:

(The fourth rule, $S(a) <_p L(b) \Rightarrow S(a) <_m L(b)$, is gone.)

Change 2 — extend the value rule (need bypassing bypassing A load returning the value of its own core's latest program-order-earlier buffered store, overriding memory order. defined in Chapter 4 — open in glossary ). Every load gets its value from:

The book rightly calls this equation mind-bending: a load returns the last same-address store that is either (a) before it in memory order or (b) before it in program order — though possibly after it in memory order — with option (b) taking precedence. In one clause, write-buffer bypassing overrides the rest of the memory system. This is what forced r1 = NEW in §4.2’s Table 4.3.

Change 3 — define FENCEs fence Instruction forcing all program-order-earlier memory operations into memory order before all later ones (a.k.a. memory barrier). defined in Chapter 4 — open in glossary (order everything):

Because TSO already enforces everything except Store→Load, one could define TSO FENCEs minimally — only Store→FENCE and FENCE→Load. The book chooses the redundant all-ordering definition: it doesn’t hurt, and it makes TSO’s FENCE identical to the FENCEs of chapter 5’s relaxed models.

The ordering table

Is x86 really TSO?

It is widely believed that the x86 memory model is equivalent to TSO (for normal cacheable memory and normal instructions) — but to the book’s knowledge, neither AMD nor Intel has guaranteed it or released a formal x86 model. The vendors define x86’s model with prose and examples: all the examples conform to TSO, and the prose seems consistent with it, but equivalence could only be proven against a public formal spec (none exists) and could be disproven by a counterexample (none found).

The constructive answer is Sewell et al.’s x86-TSO x86-tso Sewell et al.'s formal model of the x86 memory model (abstract machine ≡ labeled transition system). defined in Chapter 4 — open in glossary : a model in two provably equivalent forms — an abstract machine (essentially §4.4’s write-buffered switch plus a single global lock for x86 LOCK’d instructions), accessible to practitioners, and a labeled transition system that eases formal proofs. x86-TSO is consistent with the vendors’ informal rules and litmus tests, and empirical testing on AMD and Intel platforms revealed no violations — support, though never proof. The book joins Sewell et al. in urging x86 hardware and software creators to adopt the unambiguous, accessible x86-TSO model.