"C++11" withinit

(* MB: This file includes a version of the C/C++11 memory model. It
   follows the Lem model, but differs in some details. The main one is
   initialisation: in C/C++11, one can introduce undefined behaviour
   by reading from an uninitialised variable. In Herd, all-location
   intialisation is built in. That simplifies some of the model
   somewhat. Finally, program order is total in Herd, whereas sb can
   be partial in the Lem model.

   Where possible, restrictions are expressed in a way that is natural
   for Herd. This can look quite different to the Lem definitions that
   make up the C/C++11 model. Throughout the file, definitions carry
   comments that name the definitons of the Lem model that most
   closely relate.
*)

(* SC atomics have acquire and release semantics. *)
let cacq = acq | (sc & (R | F)) | acq_rel | (F & con)
let crel = rel | (sc & (W | F)) | acq_rel
let ccon = R & con

let dd = (data | addr)+

(* These are useful auxilliary definitions. The constraints that arise
   from memory orders can usually be applied to a single action, or to
   a fence-action pair. These definitions allow us to combine those
   cases.
*)
let idf = (po; [F])?
let fid = ([F]; po)?


(*C: release_acquire_fenced_synchronizes_with, hypothetical_release_sequence_set, release_sequence_set *)
let rs = [crel]; fid; [A & W]; (((co ; [rmw]) | coi) & ~(coe ; [!rmw] ; co))?
let swra = ext (rs; rf; [A]; idf; [cacq])
let swul = ext ([ul]; lo; [lk])
let pp_asw = asw \ (asw;po)
let sw = pp_asw | swul | swra

(* C: with_consume_cad_set, dependency_ordered_before

   Note that the consume memory order does not support fence-style
   synchronisation.
*)
let cad = ((rf & po) | dd)+
let dob = (ext ([W]; rs; rf; [ccon])); cad?


(* C: happens_before, inter_thread_happens_before, consistent_hb *)
let ithbr = sw | dob | sw;po
let ithb = (ithbr | po;ithbr)+
let hb = po | ithb
acyclic hb as hbAcyclic

(* C: coherent_memory_use *)
(* Uniproc/Coherence check *)
let hbl = hb & loc
let pol = po & loc

let corr = fr;rf;hbl
let corw = co;rf;hbl
let cowr = fr;hbl
let coww = co;hbl


irreflexive (corr | cowr | corw | coww) as coherence

let rmwv = rf;[rmw] | (co;fr) | (co;rf)

irreflexive rmwv as rmwAtomicity

(* C: visible_side_effect_set *)
let vse = ([W];hbl;[R]) & ~(hbl; [W]; hbl)

(* C: consistent_non_atomic_rf -- must read from vse: *)
let narf = rf; [nonatomicloc]

(* narf included in vse *)
empty narf \ vse as nonAtomicRfConsistent

(* C: det_read

   We assume there are initialisation writes at every location. That
   means we don't need a det-read style restriction.
*)


(* C: consistent_atomic_rf -- acyclicity of hb union rf for atomic reads: *)
let arf = rf; [atomicloc]

let hbarf = hb;arf
irreflexive hbarf as atomicRfConsistent


(*
(* C: sc_fenced_sc_fences_heeded, sc_accesses_sc_reads_restricted,
      sc_accesses_consistent_sc *)
let scco = [sc]; fid; co; idf; [sc]

(* For SC fr, the picture is more complicated. We'd like to have: *)
let scfr = ~[_] &
           ( ([sc]    ; rf^-1; hbl  ; [W & sc]) |
             ([sc]    ; rf^-1; [sc] ; co; [sc]) |
             ([sc & F]; po; fr;     [sc]    ) |
             (    [sc];     fr; po; [sc & F]) |
             ([sc & F]; po; fr; po; [sc & F])
           )

(* SC atomics have to respect happens-before: *)
let schb = [sc]; hb; [sc]

let scp = schb | scco | scfr

acyclic scp as scConsistent
show scp
*)

(* C: locks_only_consistent_lo *)
irreflexive lo;hb as hbAgreesLo

(* C: locks_only_consistent_locks *)
let mv = [ls]; lo^-1; [ls]; ~(lo; [ul]; lo)
irreflexive mv as consistentLo

(* C: data_races *)
let dr = ext((W * _) | (_ * W)) &
         loc & 
         (~(A * A)) &
         ~hb & ~(hb^-1)

(* C: unsequenced_races *)
let ur = int((W * M) | (M * W)) &
         loc &
         ~[_] &
         ~(po+) & ~((po+)^-1)

(* C: locks_only_good_mutex_use, locks_only_bad_mutexes *)
let bl = ([ls]; (po & lo); [lk]) & ~(lo; [ul]; lo)

let lopowoul = (po & lo & ~(lo; [ul]; lo))
let lu = [ul] & ~([ul];lopowoul^-1;[ls];lopowoul;[ul])

undefined_unless empty dr as dataRace 
undefined_unless empty ur as unsequencedRace 
undefined_unless empty bl as badLock
undefined_unless empty lu as badUnlock