cpp11.cat

C CPP11

(*
 * Same as RC11 but:
 * - without the no-thin-air axiom.
 * - external writes break release sequences.
 *
 * Simon Cooksey, Gonzalo Brito. 2025.
 *)

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)]) \ (coe; coe); (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

show hb, eco, psc, rmw