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.
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
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- no Load→Load
- Elimination sound
- no Load/Load
- no Load/Store
- Reasoning guarantees
- yes External DRF
- no Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
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