Merge pull request #770 from herd/herd-topo-solver

[herd] New solver

The new solver substitutes variables in equations following dependencies. It should be functionally equivalent to the previous solver.

his PR introduces an enhanced equation solver (step 2. below), which should run slightly  faster than the previous one and also follows equation structure more closely.

Equations produced by "semantic" modules are solved by a two step process:

1. Identify class of equivalent variables.  Variables in a class are replaced by a class representative.
As a result, sets of mutually dependent "variable = variable" equations are discarded during that step. Nevertheless the representative variable may be present in other, dependent, equations and in the final execution candidate.

2. Solve equations by substitution and computation. Previous step 2. proceeds by iteration until stabilisation. The new step 2. orders equations according to their dependencies and then substitutes variables into equations, computes results and checks equations by following this dependency order.

Mutually dependent sets of equations yield strongly connected components of the dependency graph and are handled as such as follows: the execution is normally discarded, except if the variant `-variant oota` is active where circular equations are  kept unsolved.

In such a case the resulting execution will have unsolved variables, and, if the model accepts such "oota"-like execution, it will make its way to final outcome.

As the old solver, the new solver will accept the simplest out-of-thin-air equations, that is, cyclic variable definitions. Small unrelated additions to the test still most often lead to rejection. Typically, the following tests yields some OOTA result
```
C oota-test
{
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 != 0);
}

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:r1; 1:r4;]
```
In effect some unsolved variable appear in the list of outcomes:
```
% herd7 -c11 oota-test.litmus
Test oota-test Allowed
States 2
0:r1=S8; 1:r4=S8;
0:r1=0; 1:r4=0;
Ok
Witnesses
Positive: 1 Negative: 3
Condition exists (not (0:r1=0))
Observation oota-test Sometimes 1 3
Time oota-test 0.01
```

Uncommenting the definition of 0:r2 at the end of `P0` yields the rejection of the "OOTA" execution, although the C11 model allows it. In effect, the said execution does not get through the solver. However, with the new variant `-variant oota` the "OOTA" behaviour will be accepted.

The PR introduces another new variant `-variant oldsolver`  that disables the topological solver, resorting to the old, iterative, solver.

Finally, all those subtleties are of no importance for models that reject cyclic dependencies, such as all hardware models and the revised C11 model.

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
+