BPF
"BPF Memory model based on LKMM"
let RMW = [R & W] & [SC]
let SRMW = (SC * SC) & amo
let po_amo_fetch = ([M];po;RMW) | (RMW;po;[M]) | ([M];po;[domain(SRMW)]) | ([range(SRMW)];po;[M])
show po_amo_fetch
as atomicfetch
let load_acquire = ([AQ];po;[M])
let store_release = ([M];po;[RL])
let rcpc = load_acquire | store_release
let addr_dep = [R];addr;[M]
let data_dep = [R];data;[W]
let ctrl_dep = [R];ctrl;[W]
show addr_dep
as addr
show data_dep
as data
show ctrl_dep
as ctrl
include "cos-opt.cat"
let com = co | rf | fr
let ppo =
po_amo_fetch | rcpc
| addr_dep
| data_dep
| ctrl_dep
| [M];(addr|data);[W];rfi;[R]
| [M];addr;[M];po;[W]
| (coi | fri)
let A-cumul = rfe? ; (po_amo_fetch | store_release)
let amo-sequence = (rf ; ([R & W] | amo))*
let prop = (coe | fre)? ; (A-cumul ; amo-sequence)* ; rfe?
acyclic com | po-loc
as Coherence
let hb = ppo | rfe | ((prop \ id) & int)
acyclic hb
as Happens-before
let pb = prop ; po_amo_fetch ; hb*
acyclic pb
as Propagation
empty rmw & (fre;coe)
as Atomic