"Generate co's" (* generates possible co's, optimized version *) (* co observations in test *) let invrf = rf^-1 (* Relation pco is computed by herd7 code let obsco = let po-loc = [Exp];po-loc;[Exp] in let ww = po-loc & (W * W) and rw = rf ; (po-loc & (R * W)) and wr = ((po-loc & (W * R)) ; invrf) \ id and rr = (rf ; (po-loc & (R * R)) ; invrf) \ id in (ww|rw|wr|rr) let pco = obsco|co0 *) (* The following applies to C only, where RMW is both R and W *) let rmwco = let _RMW = R & W in rf & (W * _RMW) (* co observation by atomicity *) let cobase = rmwco|pco (* Catch uniproc violations early *) acyclic cobase as ConsCo include "cross.cat" with co from generate_cos(cobase) (* From now, co is a coherence order *) let coi = co & int let coe = co \ coi (* Compute fr *) let fr = (invrf ; co) \ id let fri = fr & int let fre = fr \ fri show co,fr