Well-Justified Event Structures WJES
A model based on event structures with a notion of well-justification — inspired by game semantics — used to forbid thin-air values and prove the external DRF guarantee. The authors do not study the soundness of program transformations, but exhibit a load→load reordering counterexample, which also implies that the compilation mappings to ARMv7, ARMv8, and POWER are not optimal.
Ordering relationships
- Incomparable with
- C11/C++11 Memory Model — WJES uses a game-semantics-inspired notion of well-justification to forbid thin-air and prove external DRF. A load→load reordering counterexample shows its mappings to ARMv7/ARMv8/POWER are not optimal, so it is incomparable with C11.
References
- Alan Jeffrey, James Riely. On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory. LICS 2016, 2016. doi:10.1145/2933575.2934536
- 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