"Power model, with read-after-read hazard allowed"

(* Uniproc *)
let complus = fr | rf | co | (co;rf) | (fr;rf)
let poi = WW(po-loc) | WR(po-loc) | RW(po-loc)
irreflexive poi ; complus

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

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

(* Initial value *)
let ci0 = ctrlisync | detour
let ii0 = dd | rfi | rdw
let cc0 = dd | po-loc | ctrl | addrpo
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 ppoR = RR(ii)
and ppoW = RW(ic)
let ppo = ppoR | ppoW
show ppo

(* fences *)
let dmbst=WW(dmbst)
let dsbst=WW(dsbst)
show dmb dsb dmbst dsbst

(* All arm barriers are strong *)
let strong = dmb|dsb|dmbst|dsbst
let light = 0
let fence = strong|light

(* extensions *)
let ppoext = (rfe;ppo)|(ppo;rfe)|(rfe;ppo;rfe)
let fenceext = (rfe;fence)|(fence;rfe)|(rfe;fence;rfe)

(* happens before *)
let hb = ppo | ppoext | fence | fenceext
let GHB = hb
show GHB
acyclic hb

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

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

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

#show prop
acyclic co|prop
irreflexive fre;prop;hbstar