riscv-tso-defs.cat

(*************)
(* Utilities *)
(*************)

let fence.r.r = [R];fencerel(Fence.r.r);[R]
let fence.r.w = [R];fencerel(Fence.r.w);[W]
let fence.r.rw = [R];fencerel(Fence.r.rw);[M]
let fence.w.r = [W];fencerel(Fence.w.r);[R]
let fence.w.w = [W];fencerel(Fence.w.w);[W]
let fence.w.rw = [W];fencerel(Fence.w.rw);[M]
let fence.rw.r = [M];fencerel(Fence.rw.r);[R]
let fence.rw.w = [M];fencerel(Fence.rw.w);[W]
let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M]
let fence.tso =
  let f = fencerel(Fence.tso) in
  ([W];f;[W]) | ([R];f;[M])

let fence = 
  fence.r.r | fence.r.w | fence.r.rw |
  fence.w.r | fence.w.w | fence.w.rw |
  fence.rw.r | fence.rw.w | fence.rw.rw |
  fence.tso


let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc)
let rsw = rf^-1;rf
let AcqRel = AcqRel|Sc (* Compat *)
let AQ = (Acq|AcqRel)
and RL = (Rel|AcqRel)
let AMO = try AMO with (R & W) (* Compat *)
(* All AMO ops have RCsc annotations *)
let RCsc = (Acq|Rel|AcqRel|AMO) & (AMO|X)
(*************)
(* ppo rules *)
(*************)

let r1 = [M];po-loc;[W]
and r2 = ([R];po-loc-no-w;[R]) \ rsw
and r3 = [AMO|X];rfi;[R]
(* Explicit Synchronization *)
and r4 = fence
and r5 = [AQ];po;[M]
and r6 = [M];po;[RL]
and r7 = [RCsc];po;[RCsc]
and r8 = rmw
(* Syntactic Dependencies *)
and r9 = [M];addr;[M]
and r10 = [M];data;[W]
and r11 = [M];ctrl;[W]
(* Pipeline Dependencies *)
and r12 = [M];(addr|data);[W];rfi;[R]
and r13 = [M];addr;[M];po;[W]
(* All loads have RCpc Acquire *)
and r14 = [R];po;[M]
(* All stores have RCpc Release *)
and r15 = [M];po;[W]

let ppo =
  r1
| r2
| r3
| r4
| r5
| r6
| r7
| r8
| r9
| r10
| r11
| r12
| r13
| r14
| r15