Relaxed Memory Model Zoo

Memory model
← Back to the map

OCaml Memory Model OCaml MM

2018 · Dolan, Sivaramakrishnan, Madhavapeddy · language, formal

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.

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.

Open OCaml MM in the interactive map →