OCaml Memory Model OCaml MM
Memory model for OCaml multicore. Based on a 'local DRF' guarantee. Provides strong guarantees for well-typed programs without data races, and well-defined (though weak) semantics for racy accesses.
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
- yes x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- no Load/Store
- Other local transformations
- yes Trace preserving
- yes Common subexpr. elim.
- Reasoning guarantees
- yes External DRF
- no Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
Ordering relationships
- Incomparable with
- Java Memory Model (JMM) — Both are language-level models providing DRF-SC but with different treatments of racy accesses.
References
- Stephen Dolan, KC Sivaramakrishnan, Anil Madhavapeddy. Bounding Data Races in Space and Time. PLDI 2018, 2018. doi:10.1145/3192366.3192421
- Robin Morisset. The OCaml Memory Model. Unpublished manuscript / SIGPLAN blog, 2019. kcsrk.info/papers/memory_model_ocaml19.pdf