SC
include
"fences.cat"
include
"cos.cat"
(* Atomic *)
empty
rmw & (fre;coe)
as
atom
(* Sequential consistency *)
show
sm\id
as
si
acyclic
po | ((fr | rf | co);sm)
as
sc