Relaxed Memory Calculus RMC
The Relaxed Memory Calculus, an alternative approach in which ordering constraints between memory accesses are specified directly in the source code rather than derived from per-access annotations. The approach is highly generic and subsumes the traditional annotation style of C11. The resulting model is very weak and permits thin-air values, but the authors prove the internal DRF theorem.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- yes x86
- yes POWER
- yes Armv7
- yes Armv8
- Reasoning guarantees
- no External DRF
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- no No out-of-thin-air
Ordering relationships
- Incomparable with
- C11/C++11 Memory Model — The Relaxed Memory Calculus specifies ordering constraints directly in source code rather than deriving them from access annotations. It is very weak and permits thin-air values (only internal DRF is proved); its primitives differ from C11's, so the two are incomparable.
References
- Karl Crary, Michael J. Sullivan. A Calculus for Relaxed Memory. POPL 2015, 2015. doi:10.1145/2676726.2676984
- 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