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.
Cat model
Specified in cat cited
The proposed transactional rules are given in cat on top of the ARMv8 model and run in the authors' transaction-aware herd7. Chong et al. 2018
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