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