Relaxed Memory Models: an Operational Approach RMMOA
An operational approach to the semantics of relaxed memory, built on an abstract machine with a main memory and a hierarchical structure of store buffers in which writes to different locations may propagate to memory out of order — the same store→store relaxation as PSO. The authors prove the external 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
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- no Load→Load
- no Load→Store
- Reasoning guarantees
- yes External DRF
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Total Store Order (TSO) — Like PSO, RMMOA's hierarchical store buffers additionally permit store→store reordering to distinct addresses, which TSO forbids.
- Equivalent to
- Partial Store Order (PSO) — RMMOA is an operational model whose out-of-order propagation of writes to different locations matches PSO's store→store relaxation.
References
- Gérard Boudol, Gustavo Petri. Relaxed Memory Models: An Operational Approach. POPL 2009, 2009. doi:10.1145/1480881.1480930
- 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