x86-TSO + Transactional Memory x86-TSO+TM
An axiomatic (herd7-style) extension of the x86-TSO memory model with rules for hardware transactional memory (Intel TSX). Transactions are treated as atomic units bounded by implicit fences (a committed transaction has LOCK-prefix ordering semantics) with strong isolation. The additions only constrain transactional events, so on programs without transactions the model coincides with x86-TSO. Validated by synthesising 'minimally forbidden' litmus tests that were run on four Intel TSX implementations (Haswell, Broadwell, Skylake, Kabylake) and never observed.
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
Ordering relationships
- Equivalent to
- x86-TSO — 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).
- Compilation target of
- C++ Transactional Memory Extension (C++TM) — Chong, Sorensen & Wickerson (PLDI 2018) prove (up to a bound, model-checked) that C++ transactions compile soundly to x86; the mapping targets the x86-TSO transactional model.
References
- Nathan Chong, Tyler Sorensen, John Wickerson. The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++. PLDI 2018, 2018. doi:10.1145/3192366.3192373