ocaml.cat

(*
 * Multicore OCaml memory model, from:
 *
 * "Bounding Data Races in Space and Time"
 *   Stephen Dolan, KC Sivaramakrishnan and Anil Madhavapeddy.
 *   (PLDI 2018)
 *
 * Compared to the previous proposal (in ocaml-old.cat), this
 * model has a simpler hb relation, weaker coherence rules,
 * and does not include fr on atomics in hb. (There is also
 * an operational model. See the paper referenced above).
 *
 *)

include "cos.cat"

let sync = [Ma]; (co | rf); [Ma]
let hb = (po | sync)+

acyclic (hb | rf | ([Ma]; fr; [Ma])) as Causality
irreflexive (hb; co) as CoWW
irreflexive (hb; fr) as CoWR