"x86 TSO Mixed"
include "x86fences.cat"
include "cos.cat"
let ca = fr | co
let obs = rfe | fre | coe
let rec lob = po \ ([W]; po; [R])
| [W]; po; [MFENCE]; po; [R]
| [W]; po; [R & X]
| [W & X]; po; [R]
| lob; lob
let rec ob = obs; si
| lob
| ob; ob
acyclic po-loc | ca | rf
as internal
empty rmw & (fre;coe)
as atomic
irreflexive ob
as external