SC + DJR Transactions SC+DJR
The SC 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). Following Alglave et al.'s vocabulary it treats relaxed memory as a restricted distributed system with no global real-time clock, and replaces strict serializability with an observation-based 'observable serializability' criterion (a committed-transaction order need only respect the observable coherence and causal orders), 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 SC 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
- no 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
- Sequential Consistency (SC) — Dongol, Jagadeesan & Riely (POPL 2018) give a transactional framework parametric in the base architecture and instantiate it at SC; its added transactional axioms only constrain transactional events, so on programs with no transactions the SC instance coincides with SC by construction. fragment_restricted: they coincide only on the non-transactional fragment — the framework adds an orthogonal transactional layer with observable-serializability guarantees.
References
- Brijesh Dongol, Radha Jagadeesan, James Riely. Transactions in Relaxed Memory Architectures. PACMPL 2(POPL), Article 18, 2018. doi:10.1145/3158106