x86tso.cat

"X86 TSO"

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

(* DJL: for some reason, herd omits some po edges... *)
let po_workaround = RR(po) | RW(po) | WR(po) | WW(po)
show po_workaround as po

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

(* GHB *)
#ppo
let po_ghb = WW(po) | RM(po)

#mfence
let mfence = (po & (_ * MFENCE)) ; po

#implied barriers
let poWR = WR(po)
let i1 = PA(poWR)
let i2 = AP(poWR)
let implied = i1 | i2

let GHB = mfence | implied | po_ghb | rfe | fr | co
show mfence
show implied
acyclic GHB