C RC11
include "cos.cat"
let mo = co
let sb = po
let myrmw = [RMW] | rmw
let rb = (rf^-1; mo) \ id
let eco = (rf | mo | rb)+
let rs = [W]; (sb & loc)?; [W & (RLX | REL | ACQ_REL | ACQ | SC)]; (rf; myrmw)*
let sw = [(REL | ACQ_REL | SC)]; ([F]; sb)?; rs; rf; [R & (RLX | REL | ACQ | ACQ_REL | SC)]; (sb; [F])?; [(ACQ | ACQ_REL | SC)]
let hb = (sb | sw)+
let sbl = sb \ loc
let hbl = hb & loc
let scb = sb | sbl; hb; sbl | hbl | mo | rb
let pscb = ([SC] | [F & SC]; hb?); scb; ([SC] | hb? ; [F & SC])
let pscf = [F & SC]; (hb | hb; eco; hb); [F & SC]
let psc = pscb | pscf
let cnf = ((W *
_) | (
_ * W)) & loc \ ((IW *
_) | (
_ * IW))
let dr = (cnf & ext) \ (hb | hb^-1 | A * A)
undefined_unless empty dr
as Dr
irreflexive hb; eco?
as coherence1
irreflexive (myrmw; eco)
as coherencermw
empty (myrmw & (rb; mo))
as atomicity
acyclic psc
as SC
acyclic (sb | rf)
as no-thin-air
show hb, eco, psc, rmw