Reuse domains only for intra-test repetitions

Author: OlivierNicole

lib/STM_domain.ml

@@ -62,43 +62,47 @@ module Make (Spec: Spec) = struct
            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,parent_obs,child_obs)
 
-  let agree_test_par ~pool ~count ~name =
+  let agree_test_par ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
     Test.make ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
+        Util.Domain_pair.run (fun pool ->
          assume (all_interleavings_ok triple);
-         repeat rep_count (agree_prop_par ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *)
+         repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *)
 
-  let neg_agree_test_par ~pool ~count ~name =
+  let neg_agree_test_par ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
     Test.make_neg ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
+        Util.Domain_pair.run (fun pool ->
          assume (all_interleavings_ok triple);
-         repeat rep_count (agree_prop_par ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *)
+         repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *)
 
-  let agree_test_par_asym ~pool ~count ~name =
+  let agree_test_par_asym ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
     Test.make ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
+        Util.Domain_pair.run (fun pool ->
          assume (all_interleavings_ok triple);
-         repeat rep_count (agree_prop_par_asym ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *)
+         repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *)
 
-  let neg_agree_test_par_asym ~pool ~count ~name =
+  let neg_agree_test_par_asym ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
     Test.make_neg ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
+        Util.Domain_pair.run (fun pool ->
          assume (all_interleavings_ok triple);
-         repeat rep_count (agree_prop_par_asym ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *)
+         repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *)
 end

lib/STM_domain.mli

@@ -58,21 +58,21 @@ module Make : functor (Spec : STM.Spec) ->
         @return [true] if there exists a sequential interleaving of the results
         which agrees with a model interpretation. *)
 
-    val agree_test_par : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+    val agree_test_par : count:int -> name:string -> QCheck.Test.t
     (** Parallel agreement test based on {!Stdlib.Domain} which combines [repeat] and [~retries].
         Accepts two labeled parameters:
         [count] is the number of test iterations and [name] is the printed test name. *)
 
-    val neg_agree_test_par : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+    val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t
     (** A negative parallel agreement test (for convenience). Accepts two labeled parameters:
         [count] is the number of test iterations and [name] is the printed test name. *)
 
-    val agree_test_par_asym : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+    val agree_test_par_asym : count:int -> name:string -> QCheck.Test.t
     (** Asymmetric parallel agreement test based on {!Stdlib.Domain} and {!agree_prop_par_asym}
         which combines [repeat] and [~retries]. Accepts two labeled parameters:
         [count] is the number of test iterations and [name] is the printed test name. *)
 
-    val neg_agree_test_par_asym : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+    val neg_agree_test_par_asym : count:int -> name:string -> QCheck.Test.t
     (** A negative asymmetric parallel agreement test (for convenience).
         Accepts two labeled parameters:
         [count] is the number of test iterations and [name] is the printed test name. *)

lib/lin.ml

@@ -127,11 +127,26 @@ struct
       Test.make ~count ~retries ~name
         arb_cmd_triple (repeat rep_count lin_prop)
 
+    (* Linearization test *)
+    let lin_test_with_special_fun ~rep_count ~retries ~count ~name ~lin_prop ~run_fn =
+      let arb_cmd_triple = arb_cmds_triple 20 12 in
+      Test.make ~count ~retries ~name
+        arb_cmd_triple
+          (fun input ->
+            run_fn (fun v -> repeat rep_count (lin_prop v) input))
+
     (* Negative linearization test *)
     let neg_lin_test ~rep_count ~retries ~count ~name ~lin_prop =
       let arb_cmd_triple = arb_cmds_triple 20 12 in
       Test.make_neg ~count ~retries ~name
         arb_cmd_triple (repeat rep_count lin_prop)
+
+    let neg_lin_test_with_special_fun ~rep_count ~retries ~count ~name ~lin_prop ~run_fn =
+      let arb_cmd_triple = arb_cmds_triple 20 12 in
+      Test.make_neg ~count ~retries ~name
+        arb_cmd_triple
+          (fun input ->
+            run_fn (fun v -> repeat rep_count (lin_prop v) input))
   end
 end
 

lib/lin.mli

@@ -50,6 +50,8 @@ module Internal : sig
     val interp_plain : Spec.t -> Spec.cmd list -> (Spec.cmd * Spec.res) list
     val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
     val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
+    val lin_test_with_special_fun : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:('a -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> run_fn:(('a -> bool) -> bool) -> QCheck.Test.t
+    val neg_lin_test_with_special_fun : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:('a -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> run_fn:(('a -> bool) -> bool) -> QCheck.Test.t
   end
 end
   [@@alert internal "This module is exposed for internal uses only, its API may change at any time"]

lib/lin_domain.ml

@@ -39,14 +39,14 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     let _ = run_parallel ~pool (seq_pref,cmds1,cmds2) in
     true
 
-  let lin_test ~pool ~count ~name =
-    M.lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(lin_prop ~pool)
+  let lin_test ~count ~name =
+    M.lin_test_with_special_fun ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(fun pool -> lin_prop ~pool) ~run_fn:Util.Domain_pair.run
 
-  let neg_lin_test ~pool ~count ~name =
-    neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(lin_prop ~pool)
+  let neg_lin_test ~count ~name =
+    M.neg_lin_test_with_special_fun ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(fun pool -> lin_prop ~pool) ~run_fn:Util.Domain_pair.run
 
-  let stress_test ~pool ~count ~name =
-    M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(stress_prop ~pool)
+  let stress_test ~count ~name =
+    M.lin_test_with_special_fun ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(fun pool -> stress_prop ~pool) ~run_fn:Util.Domain_pair.run
 end
 
 module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))

lib/lin_domain.mli

@@ -11,31 +11,31 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
 
   val stress_prop : pool:Util.Domain_pair.t -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
 
-  val lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+  val lin_test : count:int -> name:string -> QCheck.Test.t
 
-  val neg_lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+  val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 
-  val stress_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+  val stress_test : count:int -> name:string -> QCheck.Test.t
 end
   [@@alert internal "This module is exposed for internal uses only, its API may change at any time"]
 
 (** functor to build a module for parallel testing *)
 module Make (Spec : Spec) : sig
-  val lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+  val lin_test : count:int -> name:string -> QCheck.Test.t
   (** [lin_test ~count:c ~name:n] builds a parallel test with the name [n] that
       iterates [c] times. The test fails if one of the generated programs is not
       sequentially consistent. In that case it fails, and prints a reduced
       counter example.
   *)
 
-  val neg_lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+  val neg_lin_test : count:int -> name:string -> QCheck.Test.t
   (** [neg_lin_test ~count:c ~name:n] builds a negative parallel test with the
       name [n] that iterates [c] times. The test fails if no counter example is
       found, and succeeds if a counter example is indeed found, and prints it
       afterwards.
   *)
 
-  val stress_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t
+  val stress_test : count:int -> name:string -> QCheck.Test.t
   (** [stress_test ~count:c ~name:n] builds a parallel test with the name
       [n] that iterates [c] times. The test fails if an unexpected exception is
       raised underway. It is intended as a stress test and does not perform an

lib/util.ml

@@ -378,16 +378,18 @@ module Domain_pair = struct
   let domain_fun done_ runner =
     while not (Atomic.get done_) do
       Mutex.lock runner.task_mutex;
-      while Option.is_none runner.task do
+      while Option.is_none runner.task && not (Atomic.get done_) do
         Condition.wait runner.new_task runner.task_mutex
       done;
-      let Task (f, promise) = Option.get runner.task in
-      runner.task <- None;
-      Mutex.unlock runner.task_mutex;
-      Mutex.lock promise.mutex;
-      promise.result <- Some (f ());
-      Condition.signal promise.fulfilled;
-      Mutex.unlock promise.mutex;
+      if not (Atomic.get done_) then (
+        let Task (f, promise) = Option.get runner.task in
+        runner.task <- None;
+        Mutex.unlock runner.task_mutex;
+        Mutex.lock promise.mutex;
+        promise.result <- Some (f ());
+        Condition.signal promise.fulfilled;
+        Mutex.unlock promise.mutex;
+      )
     done
 
   let init () =
@@ -416,6 +418,12 @@ module Domain_pair = struct
 
   let takedown pair =
     Atomic.set pair.done_ true;
+    Mutex.lock pair.task1.task_mutex;
+    Condition.signal pair.task1.new_task;
+    Mutex.unlock pair.task1.task_mutex;
+    Mutex.lock pair.task2.task_mutex;
+    Condition.signal pair.task2.new_task;
+    Mutex.unlock pair.task2.task_mutex;
     Domain.join pair.d1;
     Domain.join pair.d2
 

src/array/dune

@@ -22,6 +22,6 @@
  (name lin_tests)
  (modules lin_tests)
  (package multicoretests)
- (libraries qcheck-lin.domain domainslib)
+ (libraries qcheck-lin.domain)
  (action (run %{test} --verbose))
 )

src/array/lin_internal_tests.ml

@@ -117,8 +117,6 @@ end
 
 module AT_domain = Lin_domain.Make_internal(AConf) [@alert "-internal"]
 ;;
-let () =
-  Util.Domain_pair.run (fun pool ->
 QCheck_base_runner.run_tests_main [
-  AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin.Internal Array test with Domain";
-])
+  AT_domain.neg_lin_test ~count:1000 ~name:"Lin.Internal Array test with Domain";
+]

src/array/lin_tests.ml

@@ -28,9 +28,7 @@ end
 
 module AT_domain = Lin_domain.Make(AConf)
 ;;
-let () =
-  Util.Domain_pair.run (fun pool ->
 QCheck_base_runner.run_tests_main [
-  AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin Array test with Domain";
-  AT_domain.stress_test  ~pool ~count:1000 ~name:"Lin Array stress test with Domain";
-])
+  AT_domain.neg_lin_test ~count:1000 ~name:"Lin Array test with Domain";
+  AT_domain.stress_test  ~count:1000 ~name:"Lin Array stress test with Domain";
+]