"Uniproc model" withoutco (**********************) (* Computes co and fr *) (**********************) (* NB: this model handles RMW *) let invrf=rf^-1 (* co observations in test *) let obsco = (WW(po-loc) |(rf;RW(po-loc)) |noid(WR(po-loc);invrf) |noid(rf;RR(po-loc);invrf)) let rmw = R & W let rmwco = (rf ; [rmw]) (* co observation by atomicity *) let cobase = obsco|rmwco|co0 let rec co = cobase (* initial observations *) | ([rmw];fr) (* by atomicity *) | (co ; co) (* transitivity *) and fr = noid(invrf;co) (* notice: avoid self fr (RMW) *) show fr show co (* a few additional shows *) show mfence lfence sfence show sync lwsync eieio show dmb dsb dsbst dmbst show isb isync (* uni check proper *) irreflexive co as uniproc