The Ballad of Dependencies - cat files, kinds and litmus tests

catalogue/dependencies/cats/aarch64.cat

@@ -0,0 +1,123 @@
+AArch64 "ARMv8 AArch64"
+catdep (* This option tells that the cat file computes dependencies *)
+
+(*
+ * Include the cos.cat file shipped with herd.
+ * This builds the co relation as a total order over writes to the same
+ * location and then consequently defines the fr relation using co and
+ * rf.
+ *)
+include "cos.cat"
+
+(*
+ * Include aarch64fences.cat to define barriers.
+ *)
+include "aarch64fences.cat"
+
+(*
+ * Include aarch64deps.cat to define dependencies.
+ *)
+include "aarch64deps-pick.cat"
+
+(* Show relations in generated diagrams *)
+include "aarch64show.cat"
+
+(*
+ * As a restriction of the model, all observers are limited to the same
+ * inner-shareable domain. Consequently, the ISH, OSH and SY barrier
+ * options are all equivalent to each other.
+ *)
+let dsb.full = DSB.ISH | DSB.OSH | DSB.SY
+let dsb.ld = DSB.ISHLD | DSB.OSHLD | DSB.LD
+let dsb.st = DSB.ISHST | DSB.OSHST | DSB.ST
+
+(*
+ * A further restriction is that standard litmus tests are unable to
+ * distinguish between DMB and DSB instructions, so the model treats
+ * them as equivalent to each other.
+ *)
+let dmb.full = DMB.ISH | DMB.OSH | DMB.SY | dsb.full
+let dmb.ld = DMB.ISHLD | DMB.OSHLD | DMB.LD | dsb.ld
+let dmb.st = DMB.ISHST | DMB.OSHST | DMB.ST | dsb.st
+
+(* Flag any use of shareability options, due to the restrictions above. *)
+flag ~empty (dmb.full | dmb.ld | dmb.st) \
+	    (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST)
+	    as Assuming-common-inner-shareable-domain
+
+(* Intrinsic order *)
+let intrinsic = (iico_data|iico_ctrl)+
+
+(* Coherence-after *)
+let ca = fr | co
+
+(* Local read successor *)
+let lrs = [W]; (po-loc \ (po-loc;[W];po-loc)) ; [R]
+
+(* Local write successor *)
+let lws = po-loc; [W]
+
+(* Observed-by *)
+let obs = rfe | fre | coe
+
+(* Read-modify-write *)
+let rmw = lxsx | amo
+
+(* Dependency-ordered-before *)
+let dob = addr | data | ctrl; [W]
+	| (ctrl | (addr; po)); [ISB]; po; [M]
+	| addr; po; [W]
+	| (addr | data); lrs
+show ctrl;[M] as ctrl
+
+(* Pick-ordered-before *)
+let pob = pick-dep; [W]
+        | (pick-ctrl-dep | pick-addr-dep; po); [ISB]; po; [M]
+        | pick-addr-dep; [M]; po; [W]
+
+(* Atomic-ordered-before *)
+let aob = rmw
+	| rmw; lrs; [A | Q]
+
+(* Barrier-ordered-before *)
+let bob = po; [dmb.full]; po
+        | po; ([A];amo;[L]); po
+	| [L]; po; [A]
+	| [R\NoRet]; po; [dmb.ld]; po
+	| [A | Q]; po
+	| [W]; po; [dmb.st]; po; [W]
+	| po; [L]
+
+(* Tag-ordered-before *)
+let tob = [R & T]; iico_data; [BR]; iico_ctrl; [M \ T]
+
+(* Locally-ordered-before *)
+let rec lob = lws; si
+            | dob
+            | pob
+            | aob
+            | bob
+            | tob
+            | lob; lob
+let pick-lob = pick-basic-dep; lob; [W]
+
+(* Ordered-before *)
+let rec ob = obs; si
+        | lob
+        | pick-lob
+	| ob; ob
+
+(* Tag-location-ordered *)
+let tlo = [R & T]; tob; loc; tob^-1; [R & T]
+
+(* Internal visibility requirement *)
+let po-loc =
+  let Exp = M\domain(tob) in
+  (po-loc & Exp*Exp) | (po & tlo)
+acyclic po-loc | ca | rf as internal
+
+(* External visibility requirement *)
+irreflexive ob as external
+
+(* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *)
+empty rmw & (fre; coe) as atomic

catalogue/dependencies/cats/aarch64deps-down-one-leg.cat

@@ -0,0 +1,43 @@
+(* Intrinsic dependencies *)
+let intrinsic = (iico_data|iico_ctrl)+
+
+(* Dependency through register *)
+let generated-by-stxr = udr(same-instr;[range(lxsx)])
+let rf-reg-no-stxr =
+  let NW = ~generated-by-stxr in
+  [NW];rf-reg
+let dd = (rf-reg-no-stxr | intrinsic)+
+
+(* The relation to-PoD is a dependency through register
+   to a point of divergence*)
+let to-PoD = [R]; dd; [PoD]
+
+(** Data and Address dependencies *)
+let data = [R]; dd; [DATA]; intrinsic; [W]
+let addrW = [R]; dd; [NDATA]; intrinsic; [W]
+let addrR =
+ let dd-no-interv-PoD = dd \ (to-PoD;dd) in
+ [R]; dd-no-interv-PoD; [NDATA]; intrinsic; [R]
+let addr = addrW | addrR
+
+(** Control dependency *)
+(* Pre-control dependency *)
+let pre-ctrl = to-PoD; po
+
+(* Equivalent writes *)
+let antecedent =
+  let immediate-lws = singlestep([W];po-loc;[W]) in
+  (intrinsic|rf-reg|lrs|immediate-lws)^-1
+
+let pre-equiv-evts =
+  let rdw-ext =
+    let wwloc = ((W * W) & loc) \ id in
+    ((rfe^-1;wwloc;rf)|(rf^-1;wwloc;rfe))
+  in same-static\rdw-ext
+show pre-equiv-evts \ id as pre-equiv-evts
+
+let equivalent-writes = (W*W) & bisimulation(antecedent,pre-equiv-evts)
+show equivalent-writes \ id as equivalent-writes
+
+(* Control dependency *)
+let ctrl = pre-ctrl \ (always-executed(to-PoD,equivalent-writes))

catalogue/dependencies/cats/aarch64deps-down-two-legs.cat

@@ -0,0 +1,25 @@
+(* Intrinsic dependencies *)
+let intrinsic = (iico_data|iico_ctrl)+
+
+(* Dependency through register *)
+let rf-reg-no-stxr =
+  rf-reg \ ([W & range(lxsx)];rf-reg)
+
+let dd =
+  let r = (rf-reg-no-stxr | intrinsic)* in
+  r;rf-reg-no-stxr;r
+
+(* The relation to-BR is a dependency through register
+   to a Branching effect *)
+let to-BR = [R]; dd; [BR]
+
+(** Data and Address dependencies *)
+let data = ([R]; dd; [DATA]; intrinsic; [W]) \ same-instance
+let addrW = [R]; dd; [NDATA]; intrinsic; [W]
+let addrR =
+ let dd-no-interv-BR = dd \ (to-BR;dd) in
+ [R]; dd-no-interv-BR; [NDATA]; intrinsic; [R]
+let addr = (addrW | addrR) \ same-instance
+
+(** Control dependencies *)
+let ctrl = to-BR; po

catalogue/dependencies/cats/aarch64deps-pick.cat

@@ -0,0 +1,32 @@
+(* Dependency through registers and memory *)
+let rec dtrm = 
+  rf-reg \ ([W & range(lxsx)];rf-reg)
+  | rfi
+  | iico_data 
+  | dtrm; dtrm
+
+let Reg=~M | ~BR
+(** Data, Address and Control dependencies *)
+let ADDR=NDATA
+let basic-dep =
+   [R|Rreg]; dtrm?
+let data = basic-dep; [DATA]; iico_data; [W]
+let addr = basic-dep; [ADDR]; iico_data; [M]
+let ctrl = basic-dep; [BR]; po
+
+(** Pick dependencies *)
+let pick-basic-dep =
+   [R|Rreg]; dtrm?; [Reg]; iico_ctrl; [Reg]; dtrm? 
+let pick-addr-dep =
+   pick-basic-dep; [ADDR]; iico_data; [M]
+let pick-data-dep =
+   pick-basic-dep; [DATA]; iico_data; [W]
+let pick-ctrl-dep =
+   pick-basic-dep; [BR]; po
+let pick-dep =
+( 
+   pick-basic-dep | 
+   pick-addr-dep  | 
+   pick-data-dep  |
+   pick-ctrl-dep  
+)

catalogue/dependencies/cats/always-executed-writes.cat

@@ -0,0 +1,103 @@
+(* Cat file to compute always executed write effects *)
+
+(* Utilities *)
+
+let roots(r) = domain(r) \ range(r)
+let succs (e,r) = range ([e];r)
+
+let mapset2rel f =
+  let rec map_rec xs = match xs with
+  || {} -> 0
+  || x ++ xs ->
+     f x | map_rec xs
+  end in
+  map_rec
+
+let mapset2set f =
+  let rec map_rec xs = match xs with
+  || {} -> {}
+  || x ++ xs ->
+     f x | map_rec xs
+  end in
+  map_rec
+
+(* Basic definitions *)
+let poDorW = [PoD|W];po;[PoD|W]
+let nextDorW = poDorW \ (poDorW;poDorW)
+
+let sibling =
+  let inv = nextDorW^-1 in
+  fun s -> ([s];inv;nextDorW;[s])\(id|inv|nextDorW)
+
+let DpoDorW = [PoD];poDorW
+
+(* Add pair dw for w in ws
+   More precisely:
+   addD d (ws,dw) = dw U {(d,w) | w in ws}
+*)
+
+let addD d =
+  let rec do_rec ws =  match ws with
+  || {} -> fun k -> k
+  || w ++ ws ->
+       let kws = do_rec ws in
+       fun k -> (d,w) ++ kws k
+  end in do_rec
+
+(*
+  Set combination: union of equiv-related sets
+*)
+
+let addifequiv (equiv,ws0) = mapset2set (fun w -> succs (w,equiv) & ws0)
+
+let combine (equiv,ws1,ws2) =
+  addifequiv (equiv,ws1) ws2 | addifequiv (equiv,ws2) ws1
+
+(* Tree scan: returns ws,dw, where ws is the set of writes always performed at
+this level and dw is the relation from PoD to writes always performed *)
+
+let rec case_disjunction (equiv,e) = match { e } & PoD with
+|| {} ->  (* e is not a PoD, hence is a write *)
+    let (ws,dw) = write_acc (equiv, (succs (e,nextDorW))) in
+    (e ++ ws,dw)
+|| d ++ es ->   (* e is a PoD *)
+   let nexts = (succs (d,nextDorW)) in
+   match sibling(nexts) with
+   || {} -> (* Only one branch, nothing equivalent *)
+      ({},0)
+   || _e ++ _es ->
+      let (ws,dw) = keep_equiv_writes (equiv,nexts) in
+      (ws,addD d ws dw)
+   end
+end
+
+and write_acc (equiv,es) = match es with
+|| {} -> ({},0)
+|| e ++ es ->
+    let (ws_e,dw_e) = case_disjunction (equiv, e)
+    and (ws_es,dw_es) = write_acc (equiv, es) in
+    (ws_e|ws_es, dw_e|dw_es)
+end
+
+(* Warning, base case is on singleton *)
+and keep_equiv_writes (equiv,es) = match es with
+  || {} -> ({},0)  (* No successors, ie no W po-after, special case *)
+  || e ++ es ->
+        match es with
+        || {} -> case_disjunction(equiv,e) (* Singleton = base case *)
+        || f ++ fs  ->
+          let (ws_e,dw_e) = case_disjunction(equiv,e)
+          and (ws_es,dw_es) = keep_equiv_writes(equiv,es) in
+          (combine (equiv,ws_e,ws_es), dw_e|dw_es)
+        end
+end
+
+(* Final call *)
+let zyva equiv =
+  mapset2rel
+    (fun r -> let (ws,dw) = case_disjunction(equiv,r) in dw)
+
+let Dmins = roots(DpoDorW)
+let always-executed (to-PoD,equiv) =
+  let DW = zyva equiv Dmins in
+  to-PoD; DW

catalogue/dependencies/tests/desired-kinds.txt

@@ -0,0 +1,54 @@
+MP+rel+CAS-addr               Allow
+MP+rel+CSEL-addr              Allow
+MP+rel+CSEL-addr2             Allow
+LB+rel+CAS                    Forbid
+LB+CSEL-rfi-data+DMB          Forbid
+S+rel+CSEL-data               Forbid
+S+rel+CSEL-data2              Forbid
+MP+CSEL-rfi-addr-rfi-addr     Allow
+LB+CSEL-addr-po+DMB           Forbid
+LB+CSEL-data-po+DMB           Allow
+MP+rel+CSEL-rfi-data-rfi-addr Allow
+S+rel+CSEL-rfi-data-rfi-addr  Forbid
+S+rel+CSEL-rfi-ctrl           Forbid
+T3                            Forbid
+T3-bis                        Forbid
+S+DMB.ST+CSEL-ctrl            Forbid
+LB+rel+data                   Forbid
+MP+rel+CSEL                   Allow 
+MP+rel+CSEL-rf-reg            Forbid
+WILL-7                        Forbid
+WILL-7dep                     Forbid
+WILL-8                        Allow 
+WILL-8+BIS                    Forbid
+WILL-9                        Allow
+WILL-9B                       Forbid
+WILL-9C                       Allow
+WILL-10B                      Forbid
+WILL-10C                      Forbid
+WILL-11                       Allow
+WILL-12                       Allow
+WILL-12B                      Allow
+WILL-13                       Forbid 
+WILL-13B                      Allow
+WILL-13-mod2                  Allow
+WILL-13-mod3                  Forbid
+WILL-13-mod4                  Allow
+WILL-14                       Allow
+WILL-14B                      Forbid
+WILL-14B-corrected            Forbid
+WILL-14-controldep            Allow
+WILL-14B-controldep           Forbid 
+WILL-LDAR                     Allow 
+WILL-newest                   Forbid
+WILL-newest-mod               Forbid 
+WILL-99                       Forbid
+WILL-99-excls                 Forbid
+WILL-99-excls-RZR             Forbid
+WILL-99-STADD                 Forbid
+WILL-21-01-29                 Allow 
+2021-01-29-Richard            Allow 
+2021-01-29-WILL-newest        Forbid
+2021-01-29-WILL-newest-noWZR  Forbid
+WILL-15-corrected             Forbid
+WILL-15-datadep-corrected     Forbid