[herd] Optimised evaluation by implicit transitive relations.

Add implicitly transitive relations to the cat interpreter.

Implicitly transitive relations are
subject to two main optimisations :
  + When the acyclic test argument is a disjunction
   `(..|r|..)` and that argument `r` is
   a relation in implicit transitive form, there is
   no need to apply transitive closure. Namely
   `acyclic (..|r|..)` and `acyclic (..|r+|..)` are
   equivalent.
  + Intersection with a standard relation provides
    a support for repetitively testing connectivity,
    without effectively computing transitive closures.

The implicitly transitive relations are implemented
as an ordinary relation `r`. Their value is `r+`

Context where transitive closure need not be performed
(such as a disjunction argument in an acyclicity clause)
is implemented as a new boolean parameter to the
evaluation function.

Co-authored-by: Hadrien Renaud <[email protected]>

herd/libdir/asl.cat

@@ -33,14 +33,14 @@ let asl_iico_data = iico_data
 let asl_rf_reg = rf-reg
 let asl_rf = rf
 (* Warning, partial_po is _implicitely_ transitive *)
-let asl_po = partial_po
+let asl_po = as_transitive (partial_po)
 
 (* Working relations *)
 
 let aarch64 = NASLLocal * NASLLocal
 
-let asl_fr_reg = inter_transitive (asl_po,[Rreg];loc;[Wreg]) (* loc extended to registers *)
-let asl_fr = inter_transitive (asl_po,[R] ; loc ; [W])
+let asl_fr_reg = asl_po & ([Rreg];loc;[Wreg]) (* loc extended to registers *)
+let asl_fr = asl_po & ([R] ; loc ; [W])
 
 let asl_data = asl_iico_data | asl_rf_reg
 let asl_deps = asl_data (* | asl_iico_ctrl *)

herd/mem.ml

@@ -1794,7 +1794,7 @@ let match_reg_events es =
       (* We can build those now *)
       let evts = es.E.events in
       let po_iico = U.po_iico es in
-      let partial_po = E.EventTransRel.to_transitive_rel es.E.partial_po in
+      let partial_po = E.EventTransRel.to_implicitely_transitive_rel es.E.partial_po in
       let ppoloc = make_ppoloc po_iico evts in
       let store_load_vbf = store_load rfm
       and init_load_vbf = init_load es rfm in

lib/BellInterpreter.ml

@@ -74,6 +74,7 @@ module Make (C: Config) = struct
         module EventSet = MySet.Make(Ordered)
         module EventRel = InnerRel.Make(Ordered)
         module EventMap = MyMap.Make(Ordered)
+        module EventTransRel = InnerTransRel.Make(Ordered)
       end
 
       type test = unit

lib/InnerTransRel.ml

@@ -17,8 +17,8 @@ module type S = sig
   val union5 : t -> t -> t -> t -> t -> t
   val union6 : t -> t -> t -> t -> t -> t -> t
   val unions : t list -> t
-  val to_transitive_rel : t -> Rel.t
   val to_implicitely_transitive_rel : t -> Rel.t
+
 end
 
 module Make (O : MySet.OrderedType) :
@@ -106,7 +106,6 @@ module Make (O : MySet.OrderedType) :
     | [ h ] -> h
     | li -> unions2 [] li |> unions
 
-  let to_transitive_rel t = Rel.transitive_closure t.rel
-
   let to_implicitely_transitive_rel t = t.rel
+
 end

lib/InnerTransRel.mli

@@ -1,4 +1,4 @@
-(** Implements a transitive relation. *)
+(** Implements an acyclic transitive relation. *)
 
 module type S = sig
   (** Output module. *)
@@ -10,9 +10,21 @@ module type S = sig
   module Rel : InnerRel.S with type elt0 = elt and module Elts = Set
 
   type t = { input : Set.t; rel : Rel.t; output : Set.t }
-  (** Represents a transitive relation.
+  (** Represents an (acyclic) transitive relation from input to output:
+        + input is the set of minimal events (no relation to them);
+        + output is the set of maximal events (no relation from them);
+        + rel is a relation of which transitive closure is the relation
+          represented.
 
-      Note that users should not use this representation to build their
+      The input and output field are here for the efficiency, except
+      for the case  of an empty relation where they are equal and describe
+      the relation support.
+
+      In the following we identify the rel components and the values of
+      type t. Notice that, if r is this component, the value of type t
+      represents r+.
+
+      Users should not use this representation to build their
       relation, but they should rely on the constructor [from_nodes] and the
       [union] and [seq] operations.
   *)
@@ -30,22 +42,28 @@ module type S = sig
   (** maps on nodes, does not affect edges. *)
 
   val seq : t -> t -> t
-  (** Sequential operation: every element of t1 is before every element of t2. *)
+  (** Sequential composition.
+      [seq r1 r2] return a relation r, s. t. (a,b) is in r+, iff there
+      exists  c and d, s.t, (a,c) is in r1+ and (d,b) is in r2+. *)
 
   val union : t -> t -> t
-  (** Parallel composition, union of graphs. *)
+  (** Parallel composition, union of graphs.
+      [union r1 r2] returns a relation r, s.t. r+ is (r1|r2)+. *)
+
 
   val union3 : t -> t -> t -> t
   val union4 : t -> t -> t -> t -> t
   val union5 : t -> t -> t -> t -> t -> t
   val union6 : t -> t -> t -> t -> t -> t -> t
   val unions : t list -> t
 
-  val to_transitive_rel : t -> Rel.t
-  (** [to_transitive_rel t] is the InnerRel representation of t. *)
-
   val to_implicitely_transitive_rel : t -> Rel.t
-  (** [to_implicitely_transitive_rel t] is a non-transitive representation of t. *)
+  (** [to_implicitely_transitive_rel t] is a non-transitive
+      representation of t, _i.e._ the function returns r
+      such that [t] represent r+.
+      In practice, r is the internal representation of [t].
+  *)
+
 end
 
 module Make : functor (O : MySet.OrderedType) ->

lib/innerRel.ml

@@ -70,6 +70,7 @@ module type S =  sig
   val up_from_set : Elts.t -> t -> Elts.t
 
 (* Does not detect cycles either *)
+  val transitive_to_map : t -> Elts.t M.ME.t
   val transitive_closure : t -> t
 
 (* Direct cycles *)
@@ -450,7 +451,9 @@ and module Elts = MySet.Make(O) =
 
     end
 
-    let transitive_closure r = M.of_map (M.tr (M.to_map r))
+    let transitive_to_map r = M.to_map r |> M.tr
+
+    let transitive_closure r = transitive_to_map r |> M.of_map
 
 (* Acyclicity check *)
 

lib/innerRel.mli

@@ -71,7 +71,8 @@ module type S =  sig
   val up :  elt0 -> t -> Elts.t
   val up_from_set : Elts.t -> t -> Elts.t
 
-(* Does not detect cycles either *)
+  (* Transitive closure, the fist function returns Map form *)
+  val transitive_to_map : t -> Elts.t M.ME.t
   val transitive_closure : t -> t
 
 (* Direct cycles *)