Relaxed Atomic + Ordering RAO
The 'Relaxed Atomic + Ordering' model, in which relaxed behaviours are explained through transformations applied over a sequentially consistent execution. The authors claim the external DRF guarantee while still permitting thin-air values — two properties known to be incompatible in general (Batty et al., ESOP 2015) — which the survey attributes to restrictions on the supported input language (for example, the absence of general conditional statements).
Cat model
Not expressible in cat cited
Allowed behaviours are those obtainable by applying a sequence of program transformations to an SC execution: a rewriting derivation, not a predicate on the candidate execution. Saraswat et al. 2007
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Reasoning guarantees
- no Coherence
- yes No undefined behaviour
- no In-order execution
- no No out-of-thin-air
Ordering relationships
- Incomparable with
- C11/C++11 Memory Model — RAO explains relaxed behaviour via transformations over an SC execution. Its authors claim external DRF while still permitting thin-air values — two properties known to be incompatible in general (Batty et al., ESOP 2015) — which the survey attributes to restrictions on the input language (no general conditionals). Incomparable with C11.
References
- Vijay A. Saraswat, Radha Jagadeesan, Maged Michael, Christoph von Praun. A Theory of Memory Models. PPoPP 2007, 2007. doi:10.1145/1229428.1229469
- Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell. The Problem of Programming Language Concurrency Semantics. ESOP 2015, 2015. doi:10.1007/978-3-662-46669-8_12
- Evgenii Moiseenko, Anton Podkopaev, Dmitrii Koznov. A Survey of Programming Language Memory Models. Programming and Computer Software 47(6), pp. 439–456, 2021. doi:10.1134/S0361768821060050