[herd] New "topological order" solver

This PR also introduced two new variants:
  - `-variant oldsolver` use the previous, iterative, solver.
  - `-variant oota`, do not reject circular dependencies. Those
     execution candidates will be rejected by mots models in a
     subsequent phase.

herd/AArch64Sem.ml

@@ -771,7 +771,7 @@ module Make
         >>= fun v -> write_reg_op op sz rd v ii
         >>= fun () -> B.nextT
 
-      let do_read_mem sz  = do_read_mem_op (M.op1 (Op.Mask sz)) sz
+      let do_read_mem sz  = do_read_mem_op (uxt_op sz) sz
 
       let read_mem_acquire sz = do_read_mem sz Annot.A
       let read_mem_acquire_pc sz = do_read_mem sz Annot.Q

herd/Pretty.ml

@@ -395,7 +395,8 @@ module Make (S:SemExtra.S) : S with module S = S  = struct
         (fun ess iico ->
           let r = S.unions (iico::order_one_proc ess)
           and es = E.EventSet.unions ess in
-          E.EventRel.topo es r)
+          try E.EventRel.topo es r
+          with E.EventRel.Cyclic -> assert false)
         by_proc_and_poi iicos in
     let max =
       List.fold_left

herd/eventsMonad.ml

@@ -45,6 +45,7 @@ and type evt_struct = E.event_structure) =
           let hexa = C.hexa
           let debug = C.debug
           let keep_failed_as_undetermined = C.variant Variant.ASL_AArch64
+          let old_solver = C.variant Variant.OldSolver
         end)
         (A)
 

herd/mem.ml

@@ -164,6 +164,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
     let kvm = C.variant Variant.VMSA
     let self = C.variant Variant.Ifetch
     let asl = C.variant Variant.ASL
+    let oota = C.variant Variant.OOTA
     let unroll =
       match C.unroll with
       | None -> Opts.unroll_default A.arch
@@ -835,6 +836,8 @@ let match_reg_events es =
                   (A.V.pp_v v_stored) ;
                 assert false)
           rfm csn in
+      if  C.debug.Debug_herd.solver then
+        prerr_endline "++ Solve  registers" ;
       match VC.solve csn with
       | VC.NoSolns ->
          if C.debug.Debug_herd.solver then
@@ -1077,6 +1080,8 @@ let match_reg_events es =
                 loads stores cns in
             if dbg then eprintf "\n%!" ;
             (* And solve *)
+            if C.debug.Debug_herd.solver then
+              prerr_endline "++ Solve memory" ;
             match VC.solve cns with
             | VC.NoSolns ->
                if C.debug.Debug_herd.solver then begin
@@ -1119,7 +1124,6 @@ let match_reg_events es =
           let module PP = Pretty.Make(S) in
           prerr_endline "Unsolvable system" ;
           PP.show_es_rfm test es rfm ;
-          prerr_endline "Unsolvable system"
         end ;
       assert (true || rfmap_is_cyclic es rfm);
       res
@@ -2068,7 +2072,8 @@ Please use `-variant self` as an argument to herd7 to enable it."
               match cs with
               | _::_
                    when
-                     (not C.initwrites || not do_deps)
+                     (not oota)
+                     && (not C.initwrites || not do_deps)
                      && not asl
                      && Misc.is_none ofail
                 ->

herd/partition.ml

@@ -21,7 +21,7 @@ module Make (O:Set.OrderedType) : sig
 
 (* All creation steps must preceed union/find operations *)
   val create : unit -> t
-  val add : t -> O.t -> t
+  val add : O.t -> t -> t
 
 (* Union/Find *)
   val find : t -> O.t -> O.t
@@ -44,7 +44,7 @@ end = struct
 (* Creation *)
   let create () = M.empty
 
-  let add m x =
+  let add x m =
     let rec c = { value=x; rank=0; parent=c; } in
     M.add x c m
 

herd/partition.mli

@@ -21,7 +21,7 @@ module Make (O:Set.OrderedType) : sig
 
 (* All creation steps must precede union/find operations *)
   val create : unit -> t
-  val add : t -> O.t -> t
+  val add : O.t -> t -> t
 
 (* Union/Find *)
   val find : t -> O.t -> O.t

herd/tests/instructions/C/C13.litmus

@@ -0,0 +1,22 @@
+C C13
+(* Forbidden by rc11, allowed by most C11 models that tolerate oota *)
+{
+x = 0;
+y = 0;
+}
+
+P0(atomic_int *x, atomic_int *y) {
+  int r1 = atomic_load_explicit(y, memory_order_relaxed);
+  atomic_store_explicit(x, r1, memory_order_relaxed);
+  int r2 = (r1^r1)+r1;
+}
+
+P1(atomic_int *x, atomic_int *y) {
+  int r4 = atomic_load_explicit(x, memory_order_relaxed);
+  atomic_store_explicit(y, r4, memory_order_relaxed);
+}
+
+locations [0:r2; 1:r4;]
+exists 0:r1 != 0
+
+

herd/tests/instructions/C/C13.litmus.expected

@@ -0,0 +1,10 @@
+Test C13 Allowed
+States 1
+0:r1=0x0; 0:r2=0x0; 1:r4=0x0;
+No
+Witnesses
+Positive: 0 Negative: 3
+Condition exists (not (0:r1=0x0))
+Observation C13 Never 0 3
+Hash=45b06aedc4caf5ef4fdf494a986f8199
+