POWER + DJR Transactions POWER+DJR
The PPC (POWER) 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 POWER by construction.
Cat model
Expressible in cat author-extrapolated
Declarative transaction axioms over the POWER 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
- no Multicopy atomic
Ordering relationships
- Equivalent to
- IBM POWER Memory Model — Dongol, Jagadeesan & Riely (POPL 2018) also instantiate their transactional framework at PPC (POWER); the added transactional axioms only constrain transactional events, so on programs with no transactions the POWER instance coincides with POWER 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