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.
Cat model
Expressible in cat author-extrapolated
The framework is declarative: transactions are a per-execution axiom set parametric in the base model, so this instance is 'sc.cat plus transaction axioms'. No cat files accompany the paper. 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
- 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