let fence.r.r = [R];fencerel(Fence.r.r);[R]
let fence.r.w = [R];fencerel(Fence.r.w);[W]
let fence.r.rw = [R];fencerel(Fence.r.rw);[M]
let fence.w.r = [W];fencerel(Fence.w.r);[R]
let fence.w.w = [W];fencerel(Fence.w.w);[W]
let fence.w.rw = [W];fencerel(Fence.w.rw);[M]
let fence.rw.r = [M];fencerel(Fence.rw.r);[R]
let fence.rw.w = [M];fencerel(Fence.rw.w);[W]
let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M]
let fence.tso =
let f = fencerel(Fence.tso) in
([W];f;[W]) | ([R];f;[M])
let fence =
fence.r.r | fence.r.w | fence.r.rw |
fence.w.r | fence.w.w | fence.w.rw |
fence.rw.r | fence.rw.w | fence.rw.rw |
fence.tso
let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc)
let rsw = rf^-1;rf
let AcqRel = AcqRel|Sc
let AQ = (Acq|AcqRel)
and RL = (Rel|AcqRel)
let AMO = try AMO with (R & W)
let RCsc = (Acq|Rel|AcqRel|AMO) & (AMO|X)
let r1 = [M];po-loc;[W]
and r2 = ([R];po-loc-no-w;[R]) \ rsw
and r3 = [AMO|X];rfi;[R]
and r4 = fence
and r5 = [AQ];po;[M]
and r6 = [M];po;[RL]
and r7 = [RCsc];po;[RCsc]
and r8 = rmw
and r9 = [M];addr;[M]
and r10 = [M];data;[W]
and r11 = [M];ctrl;[W]
and r12 = [M];(addr|data);[W];rfi;[R]
and r13 = [M];addr;[M];po;[W]
and r14 = [R];po;[M]
and r15 = [M];po;[W]
let ppo =
r1
| r2
| r3
| r4
| r5
| r6
| r7
| r8
| r9
| r10
| r11
| r12
| r13
| r14
| r15