POWER + Transactional Memory POWER+TM
An axiomatic extension of the IBM POWER memory model with rules for its hardware transactional memory. Successful transactions create cumulative memory barriers at their boundaries, contain an integrated barrier ordering observed writes before transactional writes, and appear atomic to other threads (strong isolation). The additions only constrain transactional events, so on programs without transactions the model coincides with POWER. Validated by synthesising forbidden litmus tests run 10M times each on an 80-core POWER8 machine, none of which were observed. The work also flagged an ambiguity in the Power TM specification and showed that coalescing transactions is unsound in Power.
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
- yes Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Equivalent to
- IBM POWER Memory Model — Chong, Sorensen & Wickerson (PLDI 2018) add TM rules on top of the POWER consistency axioms (their Fig. 6) that only constrain transactional events; on the non-transactional fragment it coincides with POWER by construction. Validated on a POWER8 machine (no forbidden test observed).
- Compilation target of
- C++ Transactional Memory Extension (C++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.
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