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.
Cat model
Expressible in cat author-extrapolated
An abstract machine with a global reorderable event buffer; the happens-before discipline it enforces is per-execution, but no declarative characterisation has been published. Zhang & Feng 2016
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