ARMv8 + Transactional Memory (proposed) ARMv8+TM
An axiomatic extension of the ARMv8 memory model with (unofficial) transactional-memory rules based on a proposal considered within ARM Research: strong isolation, implicit transaction fences, transaction ordering, and RMW cancellation. ARM hardware did not support TM, so the model could not be tested directly, but the generated test suites revealed a TxnOrder violation in an RTL prototype. The paper's headline result is that combining any reasonable TM extension with the recommended ARMv8 spinlock makes lock elision UNSOUND (Example 1.1): a critical region can begin executing after the lock is observed free but before it is taken. No behavioural-equivalence edge to ARMv8 is asserted; the fix proposed is to append a DMB to the lock() implementation, after which lock elision becomes sound.
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
- yes Multicopy atomic
Ordering relationships
- Compilation target of
- C++ Transactional Memory Extension (C++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