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