x86-TSO
A rigorous formal model for x86 multiprocessor memory, validated against AMD and Intel hardware. Captures FIFO store buffers, lock prefixes, and MFENCE barriers precisely.
Cat model
Specified in cat cat file identified
herd7's x86tso.cat is the standard cat rendering; Herding cats proves it equivalent to Sewell et al.'s store-buffer machine, and x86tso-mixed.cat covers mixed-size accesses. Alglave et al. 2014
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reordering sound
- yes Store→Load
- no Store→Store
- no Load→Load
- no Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic Sewell et al. 2010
Ordering relationships
- Strictly weaker than
- Sequential Consistency (SC) — x86-TSO is the formal model equivalent of TSO for x86.
- Equivalent to
- Persistent TSO (PTSO) — Raad & Vafeiadis (OOPSLA 2018): PTSO layers epoch persistency on TSO; on the crash-free fragment its behaviour coincides with x86-TSO. fragment_restricted because the equivalence holds only crash-free — persistency adds an orthogonal persist-order dimension the consistency model does not see.
- Persistent x86 (Px86) — Raad, Wickerson, Neiger & Vafeiadis (POPL 2020): Px86's crash-free behaviour coincides with x86-TSO. fragment_restricted because the equivalence holds only on the crash-free fragment; the persist-order axiom is orthogonal.
- x86-TSO + Transactional Memory (x86-TSO+TM) — Chong, Sorensen & Wickerson (PLDI 2018) present the TM model as a set of rules added on top of the x86-TSO consistency axioms (their Fig. 5) that only constrain transactional events. On the non-transactional fragment (programs with no transactions) it coincides with x86-TSO by construction. The extension was validated against four Intel TSX implementations (no forbidden test observed).
- x86-TSO + DJR Transactions (x86-TSO+DJR) — Dongol, Jagadeesan & Riely (POPL 2018) instantiate their transactional framework at TSO; the added transactional axioms only constrain transactional events, so on programs with no transactions the TSO instance coincides with (x86-)TSO by construction. fragment_restricted: the coincidence holds only on the non-transactional fragment.
- Total Store Order (TSO) — x86-TSO formalises TSO for x86; behaviourally equivalent for standard operations.
- ClightTSO — Ševčík et al. 2013 §1.2, §4.4: ClightTSO is defined to mirror the x86-TSO model at the language level (loads, stores, compare-and-swap, barriers with TSO behaviour), with a single TSO abstract machine shared across all compiler levels — the same store→load relaxation by construction, not a restricted fragment.
- Compilation target of
- Persistent Sequential Consistency (PSC) — Khyzha & Lahav (POPL 2021) develop a sound mapping from the stronger SC-based persistency model PSC down to x86; the mapping targets the x86-TSO consistency model.
- Intermediate Memory Model (IMM) — IMM compiles correctly to x86-TSO.
- Linux Kernel Memory Model (LKMM) — Linux kernel primitives compile correctly to x86; LKMM is designed to be no stronger than the hardware it runs on.
References
- Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Communications of the ACM, 2010. doi:10.1145/1785414.1785443
- Sarita V. Adve, Kourosh Gharachorloo. Shared Memory Consistency Models: A Tutorial. IEEE Computer 29(12), 1996. doi:10.1109/2.546611
- Jade Alglave, Luc Maranget, Michael Tautschnig. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM TOPLAS, 2014. doi:10.1145/2627752