x86-TSO + DJR Transactions x86-TSO+DJR
The TSO 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 (x86-)TSO 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
- no Store→Store
- no Load→Load
- no Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- x86-TSO — Dongol, Jagadeesan & Riely (POPL 2018) instantiate their transactional framework at TSO; the added transactional axioms only constrain transactional events, so on programs with no transactions the TSO instance coincides with (x86-)TSO 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