Increase reproducability of Lin Thread tests

lib/lin.ml

@@ -40,13 +40,17 @@ module Make(Spec : CmdSpec) (*: StmTest *)
     let res_arr = Array.map (fun c -> Domain.cpu_relax(); Spec.run c sut) cs_arr in
     List.combine cs (Array.to_list res_arr)
 
-  (* use a ref to a list given by the parent thread to put the results in as a thread does not
-   return a value *)
-  let interp_thread res sut cs =
-    let cs_arr  = Array.of_list cs in
-    let res_arr = Array.map (fun c -> Thread.yield (); Spec.run c sut) cs_arr in
-    res := List.combine cs (Array.to_list res_arr)
-
+  (* Note: On purpose we use
+     - a non-tail-recursive function and
+     - an (explicit) allocation in the loop body
+     since both trigger statistically significant more thread issues/interleaving *)
+  let rec interp_thread sut cs = match cs with
+    | [] -> []
+    | c::cs ->
+        Thread.yield ();
+        let res = Spec.run c sut in
+        (c,res)::interp_thread sut cs
+
   let rec gen_cmds fuel =
     Gen.(if fuel = 0
          then return []
@@ -128,26 +132,35 @@ module Make(Spec : CmdSpec) (*: StmTest *)
   let lin_prop_thread =
     (fun (seq_pref, cmds1, cmds2) ->
       let sut = Spec.init () in
-      let pref_obs, obs1, obs2 = ref [], ref [], ref [] in
-      interp_thread pref_obs sut seq_pref;
-      let th1 = Thread.create (Thread.yield (); interp_thread obs1 sut) cmds1 in
-      let th2 = Thread.create (interp_thread obs2 sut) cmds2 in
-      Thread.join th1; Thread.join th2; Spec.cleanup sut;
+      let obs1, obs2 = ref [], ref [] in
+      let pref_obs = interp sut seq_pref in
+      let wait = ref true in
+      let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := interp_thread sut cmds1) () in
+      let th2 = Thread.create (fun () -> wait := false; obs2 := interp_thread sut cmds2) () in
+      Thread.join th1;
+      Thread.join th2;
+      Spec.cleanup sut;
       let seq_sut = Spec.init () in
-      (* we should be able to reuse [check_seq_cons] *)
-      let b = check_seq_cons !pref_obs !obs1 !obs2 seq_sut [] in
+      (* we reuse [check_seq_cons] to linearize and interpret sequentially *)
+      let b = check_seq_cons pref_obs !obs1 !obs2 seq_sut [] in
       Spec.cleanup seq_sut;
       b
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
               (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-              (!pref_obs,!obs1,!obs2))
-  
+              (pref_obs,!obs1,!obs2))
+
   (* Linearizability test based on [Domain] *)
   let lin_test ~count ~name (lib : [ `Domain | `Thread ]) =
-    let rep_count = 50 in
     let seq_len,par_len = 20,15 in
-    let lin_prop = match lib with `Domain -> lin_prop_domain | ` Thread -> lin_prop_thread in
-    Test.make ~count ~retries:3 ~name:("Linearizable " ^ name)
-      (arb_cmds_par seq_len par_len) (repeat rep_count lin_prop)
+    let arb_cmd_triple = arb_cmds_par seq_len par_len in
+    match lib with
+    | `Domain ->
+        let rep_count = 50 in
+        Test.make ~count ~retries:3 ~name:("Linearizable " ^ name ^ " with Domain")
+          arb_cmd_triple (repeat rep_count lin_prop_domain)
+    | `Thread ->
+        let rep_count = 100 in
+        Test.make ~count ~retries:10 ~name:("Linearizable " ^ name ^ " with Thread")
+          arb_cmd_triple (repeat rep_count lin_prop_thread)
 end

src/neg_tests/domain_lin_tests.ml

@@ -0,0 +1,13 @@
+open Lin_tests_common
+
+(** This is a driver of the negative tests over the Domain module *)
+
+;;
+Util.set_ci_printing ()
+;;
+QCheck_runner.run_tests_main
+  (let count = 1000 in
+   [RT_int.lin_test    `Domain ~count ~name:"ref int test";
+    RT_int64.lin_test  `Domain ~count ~name:"ref int64 test";
+    CLT_int.lin_test   `Domain ~count ~name:"CList int test";
+    CLT_int64.lin_test `Domain ~count ~name:"CList int64 test"])

src/neg_tests/dune

@@ -4,7 +4,7 @@
 (alias
  (name default)
  (package multicoretests)
- (deps ref_test.exe conclist_test.exe lin_tests.exe))
+ (deps ref_test.exe conclist_test.exe domain_lin_tests.exe thread_lin_tests.exe))
 
 (executable
  (name ref_test)
@@ -50,19 +50,34 @@
 
 ;; Linearizability tests of ref and Clist
 
-(executable
- (name lin_tests)
- (modules lin_tests)
- (flags (:standard -w -27))
+(library
+ (name lin_tests_common)
+ (modules lin_tests_common)
  (libraries qcheck lin CList)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
+(executables
+ (names domain_lin_tests thread_lin_tests)
+ (modules domain_lin_tests thread_lin_tests)
+ (flags (:standard -w -27))
+ (libraries lin_tests_common))
+
+(rule
+ (alias runtest)
+ (package multicoretests)
+ (action
+   (progn
+    (with-accepted-exit-codes 1
+      (with-stdout-to "domain_lin-output.txt" (run ./domain_lin_tests.exe --no-colors --verbose)))
+    (cat domain_lin-output.txt)
+    (run %{bin:check_error_count} "domain_lin_tests" 4 domain_lin-output.txt))))
+
 (rule
  (alias runtest)
  (package multicoretests)
  (action
    (progn
     (with-accepted-exit-codes 1
-      (with-stdout-to "lin-output.txt" (run ./lin_tests.exe --no-colors --verbose)))
-    (cat lin-output.txt)
-    (run %{bin:check_error_count} "lin_tests" 5 lin-output.txt))))
+      (with-stdout-to "thread_lin-output.txt" (run ./thread_lin_tests.exe --no-colors --verbose)))
+    (cat thread_lin-output.txt)
+    (run %{bin:check_error_count} "thread_lin_tests" 1 thread_lin-output.txt))))

src/neg_tests/lin_tests.ml → src/neg_tests/lin_tests_common.ml

@@ -58,7 +58,7 @@ module RConf_int64 = struct
     | Add of int'
     | Incr
     | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int64 [@gen Gen.ui64]
+  and int' = int64 [@gen Gen.(map Int64.of_int nat)]
 
   type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }]
 
@@ -110,17 +110,3 @@ end
 
 module CLT_int = Lin.Make(CLConf (Int))
 module CLT_int64 = Lin.Make(CLConf (Int64))
-
-;;
-Util.set_ci_printing ()
-;;
-QCheck_runner.run_tests_main
-  (let count = 1000 in
-   [RT_int.lin_test    `Domain ~count ~name:"ref int test with Domains";
-    RT_int.lin_test    `Thread ~count ~name:"ref int test with Threads";
-    RT_int64.lin_test  `Domain ~count ~name:"ref int64 test with Domains";
-    RT_int64.lin_test  `Thread ~count ~name:"ref int64 test with Threads";
-    CLT_int.lin_test   `Domain ~count ~name:"CList int test with Domains";
-    CLT_int.lin_test   `Thread ~count ~name:"CList int test with Threads";
-    CLT_int64.lin_test `Domain ~count ~name:"CList test64 with Domains";
-    CLT_int64.lin_test `Thread ~count ~name:"CList test64 with Threads"])

src/neg_tests/thread_lin_tests.ml

@@ -0,0 +1,13 @@
+open Lin_tests_common
+
+(** This is a driver of the negative tests over the Thread module *)
+
+;;
+Util.set_ci_printing ()
+;;
+QCheck_runner.run_tests_main
+  (let count = 1000 in
+   [RT_int.lin_test    `Thread ~count ~name:"ref int test";
+    RT_int64.lin_test  `Thread ~count ~name:"ref int64 test";
+    CLT_int.lin_test   `Thread ~count ~name:"CList int test";
+    CLT_int64.lin_test `Thread ~count ~name:"CList int64 test"])