"Generate co's igoring load-load hazards" (* generates possible co's *) (* co observations in test *) let invrf = rf^-1 let obsco = let ww = po-loc & (W * W) and rw = rf ; (po-loc & (R * W)) and wr = (po-loc & (W * R)) ; invrf and rr = 0 in (ww|rw|wr|rr) \ id let RMW = R & W let rmwco = rf & (W * RMW) (* co observation by atomicity *) let cobase = obsco|rmwco|co0 (* Catch uniproc violations early *) acyclic cobase as ConsCo include "cross.cat" with co from generate_cos(cobase) let coe = co & ext let coi = co & int let fr = (invrf ; co) \ id let fre = fr & ext let fri = fr & int show co,fr