Operational Happens-Before Model OHMM
An operational happens-before model proposed to repair the Java Memory Model. Its abstract machine uses a global event buffer, where events may be reordered before propagating to a global history main memory, together with a replay mechanism to simulate speculative executions. To avoid thin-air outcomes it tracks syntactic dependencies between events and forbids reordering dependent events. The authors proved the external DRF theorem and the soundness of several transformations.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- yes Load/Store
- Other local transformations
- yes Irrelevant load elim.
- yes Speculative load intro.
- yes Roach motel
- no Trace preserving
- Reasoning guarantees
- yes External DRF
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
Ordering relationships
- Incomparable with
- Java Memory Model (JMM) — OHMM is an operational attempt to repair the JMM — a global event buffer with a replay mechanism, tracking syntactic dependencies to forbid thin-air. It restructures the JMM's semantics rather than strictly refining it, so the two are incomparable.
- Linux Kernel Memory Model (LKMM) — Both are syntactic-dependency-preserving models that forbid thin-air by respecting syntactic dependencies, but over different primitives (Linux-kernel barriers vs a JMM-style happens-before machine); neither subsumes the other.
References
- Yang Zhang, Xinyu Feng. An Operational Happens-Before Memory Model. Frontiers of Computer Science, 2016. doi:10.1007/s11704-015-4492-4
- 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