Weakestmo (Event-Structure Model) WMO
A semantic-dependency-preserving model that grounds thin-air reads using event structures, which can simultaneously encode multiple conflicting executions in order to model speculation. It admits the optimal compilation mappings, many program transformations, and the external DRF guarantee, and — unlike the Promising semantics — it also supports sequentially consistent accesses. It descends from a formalisation of an LLVM concurrency fragment by the same authors.
Ordering relationships
- Strictly stronger than
- C11/C++11 Memory Model — Weakestmo grounds thin-air reads with event structures and is, in the authors' words, 'stronger than C11 (which allows OOTA) and weaker than RC11': every separating outcome (the OOTA load-buffering test and the 'RNG' bogus-value example) is allowed by C11 and forbidden by Weakestmo, with no behaviour Weakestmo allows that C11 forbids. So C11 is strictly weaker. (Reclassified from incomparable; see litmus/strictly-weaker/Weakestmo-vs-C11.)
- Incomparable with
- Promising Semantics (PS) — Both are semantic-dependency-preserving models that forbid out-of-thin-air, admit the optimal compilation mappings, and give external DRF. Weakestmo is built on event structures (vs Promising's promises/certification) and, unlike the Promising semantics, supports sequentially consistent accesses; neither is a subset of the other.
References
- Soham Chakraborty, Viktor Vafeiadis. Grounding Thin-Air Reads with Event Structures. POPL 2019 (PACMPL vol. 3), 2019. doi:10.1145/3290383
- Soham Chakraborty, Viktor Vafeiadis. Formalizing the Concurrency Semantics of an LLVM Fragment. CGO 2017, 2017. doi:10.1109/CGO.2017.7863732
- 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