"Experimental model, with atomics"

(* Uniproc *)
let com =  rf | fr | co
acyclic po-loc | com

(* Atomic *)
empty atom & (fre;coe) as atomic

(* Utilities *)
let dd = addr | data
let rdw = po-loc & (fre;rfe)
let detour = po-loc & (coe ; rfe)
let addrpo = addr;po


(*******)
(* ppo *)
(*******)


(* Initial value *)
let ci0 = ctrlisync | detour
let ii0 = dd | rfi | rdw
let cc0 = dd | ctrl | addrpo | po-loc
let ic0 = 0

(* Fixpoint from i -> c in instructions and transitivity *)
let rec ci = ci0 | (ci;ii) | (cc;ci)
and ii = ii0 | ci | (ic;ci) | (ii;ii)
and cc = cc0 | ci | (ci;ic) | (cc;cc)
and ic = ic0 | ii | cc | (ic;cc) | (ii ; ic) (* | ci inclus dans ii et cc *)

let ppo = RW(ic) | RR(ii)


(**********)
(* fences *)
(**********)

(* Power *)
let lwsync_eff = RM(lwsync)|WW(lwsync)
let eieio_eff = WW(eieio)


(* ARM *)
let dmb.st_eff=WW(dmb.st)
let dsb.st_eff=WW(dsb.st)

(* Common, all arm barriers are strong *)
let strong = sync|dmb|dsb|dmb.st_eff|dsb.st_eff
let light = lwsync_eff|eieio_eff

let fence = strong|light


(* happens before *)
let hb = ppo | fence | rfe
acyclic hb as thinair

(* prop *)
let hbstar = hb*
let propbase = (fence|(rfe;fence));hbstar

let chapo = rfe|fre|coe|(fre;rfe)|(coe;rfe)

let prop = WW(propbase)
| (chapo? ; propbase*; strong; hbstar)

acyclic co|prop|AA(WW(po)) as propagation
irreflexive fre;prop;hbstar as causality