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