ARMv8 + DJR Transactions ARMv8+DJR
The ARMv8 instance of the unified declarative transactional framework of Dongol, Jagadeesan & Riely (POPL 2018), which adds transactions to a relaxed-memory architecture parametric in the base model (the paper instantiates it at SC, TSO, ARMv8 and PPC/POWER). It treats relaxed memory as a restricted distributed system with no global real-time clock and uses observation-based 'observable serializability' rather than strict serializability, admitting flexible STM-style abort. A genuine sibling to the Chong-Sorensen-Wickerson TM cluster with a distinct construction and authorship. The added transactional axioms only constrain transactional events, so on programs with no transactions this instance coincides with ARMv8 by construction.
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
- Equivalent to
- ARMv8 / AArch64 Memory Model — Dongol, Jagadeesan & Riely (POPL 2018) instantiate their transactional framework at ARMv8; the added transactional axioms only constrain transactional events, so on programs with no transactions the ARMv8 instance coincides with ARMv8 by construction. fragment_restricted: the coincidence holds only on the non-transactional fragment.
References
- Brijesh Dongol, Radha Jagadeesan, James Riely. Transactions in Relaxed Memory Architectures. PACMPL 2(POPL), Article 18, 2018. doi:10.1145/3158106