"Uniproc, no co generated" (* Utilities *) let invrf = rf^-1 let WW(r) = r & (W * W) let RW(r) = r & (R * W) (* Collect constraints on U order *) let U0 = po-loc | rf | co0 let rec U = U0 | WW(U;invrf)\id (* WR observation of co *) | RW(invrf;U)\id (* RW observation of co *) | U;U when acyclic U as sc-per-location let co = WW(U) and fr = RW(U) show fr,co (* a few additional shows *) include "fences.cat"