PPC
include "cos.cat"
acyclic po-loc | rf | fr | co
as scperlocation
empty rmw & (fre;coe)
as atomic
let dd = addr | data
let rdw = po-loc & (fre;rfe)
let detour = po-loc & (coe ; rfe)
let addrpo = addr;po
include "ppcfences.cat"
show isync,ctrlisync
let ci0 = ctrlisync | detour
let ii0 = dd | rfi | rdw
let cc0 = dd | po-loc | ctrl | addrpo
let ic0 =
0
include "ppo.cat"
let lwsync = lwsync \ (W * R)
let eieio = eieio & (W * W)
let strong = sync
let light = lwsync|eieio
include "ppc-checks.cat"