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).
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