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.
Cat model
Expressible in cat author-extrapolated
Declarative transaction axioms over the ARMv8 base model — per-execution and cat-expressible, but published as inference rules rather than cat. Dongol 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
- 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