C++ Transactional Memory Extension C++TM
An axiomatic formalisation of the C++ transactional-memory technical specification (relaxed and atomic transactions) layered on the repaired C11/C++ memory model of Lahav et al. (RC11), chosen because it supports correct compilation to Power. The extension makes two amendments to the base model: the definition of a data race is unchanged, and conflicting transactions synchronise via a transaction order folded into happens-before. On programs without transactions the model coincides with its RC11 base. The authors prove atomic transactions are strongly isolated, that race-free programs with no non-SC atomics and no relaxed transactions enjoy 'transactional SC', and (up to a bound) that C++ transactions compile soundly to x86, Power, and ARMv8. Handling of programmer-invoked abort() is left to future work.
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
- yes Store→Store
- yes Load→Load
- no Load→Store
- Reasoning guarantees
- yes External DRF
- yes Coherence
- no No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Equivalent to
- Repaired C11 (RC11) — Chong, Sorensen & Wickerson (PLDI 2018, §7) build the C++ TM model on the baseline C++ model of Lahav et al. (RC11), making only two amendments (an unchanged race definition and transactional synchronisation folded into happens-before) that vanish when there are no transactions. On the non-transactional fragment it coincides with RC11 by construction.
- Compiles correctly to
- x86-TSO + Transactional Memory (x86-TSO+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.
- POWER + Transactional Memory (POWER+TM) — Chong, Sorensen & Wickerson (PLDI 2018) prove (up to a bound) that C++ transactions compile soundly to Power; the mapping targets the POWER transactional model.
- ARMv8 + Transactional Memory (proposed) (ARMv8+TM) — Chong, Sorensen & Wickerson (PLDI 2018) state a (bounded) sound compilation of C++ transactions to ARMv8. Caveat: the ARMv8+TM target is the untested/proposed model for which naive lock elision is unsound (Example 1.1), so this edge inherits that caveat.
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
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer. Repairing Sequential Consistency in C/C++11. PLDI 2017, 2017. doi:10.1145/3062341.3062352