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.
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