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.
Ordering relationships
- Strictly weaker than
- Sequential Consistency (SC) — x86-TSO is the formal model equivalent of TSO for x86.
- Equivalent to
- Total Store Order (TSO) — x86-TSO formalises TSO for x86; behaviourally equivalent for standard operations.
- Compilation target of
- 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