"Simple C11"
let CACQ = ACQ | (SC & R) | ACQ_REL
let CREL = REL | (SC & W) | ACQ_REL
let Access = R | W
let a_id = toid(A)
let rmw_id = toid(RMW)
let crel_id = toid(CREL)
let cacq_id = toid(CACQ)
let sc_id = toid(SC)
let asw = IW * (M \ IW)
include "filters.cat"
include "cos.cat"
let rsElem = coi | (co;rmw_id)
let breakRseq = (co \ rsElem)
let rseq = id | (rsElem \ (breakRseq;co))
let fence_id = toid(F)
let fid = (fence_id;po)?
let idf = (po;fence_id)?
let sw =
ext &
(crel_id ; fid ; rseq ;
rf ;
a_id ; idf ; cacq_id)
show sw
let Y = po
let hb = (po | asw | sw)+
let hb-loc = hb & loc
let scp = hb|co
acyclic scp
as ConsSC
with S
from linearisations(SC,scp)
show S
let rfNA = rf \ AA(rf)
empty rfNA \ hb-loc
as ConsRFna
let S-loc = MM(S) & loc
let minWRSC =
let aux = WR(S-loc)
in
aux \ (WW(S-loc);aux)
let rfSCSC = sc_id ; rf ; sc_id
let rfXSC = (rf;sc_id) \ rfSCSC
let X = hb ; minWRSC
let badRFSC= (rfSCSC \ minWRSC) | (rfXSC & (hb ; minWRSC))
empty badRFSC
as SCReads
irreflexive hb
as IrrHB
let chapo = rf|fr|co|(co;rf)|(fr;rf)
acyclic hb-loc | chapo
as Coh
let cosucc = co \ (co;co)
empty (rf;rmw_id) \ (cosucc)
as AtRMW
let locSomeW = loc \ RR(loc)
let dr =
let r1 = locSomeW & ext
in
let r2 = r1 \ AA(r1)
in
r2 \ (hb | hb^-1)
show dr
undefined_unless empty dr
as dataRace
let ur =
let r1 = locSomeW & int
in
let r2 = noid(r1)
in
r2 \ (po | po^-1)
show ur
flag ~
empty ur
as unsequencedRace