Merge pull request #464 from ocaml-multicore/stm-stress-test-utilize

Utilize STM stress test

lib/STM_domain.ml

@@ -43,7 +43,7 @@ module Make (Spec: Spec) = struct
            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,obs1,obs2)
 
-  let stress_test_prop_par (seq_pref,cmds1,cmds2) =
+  let stress_prop_par (seq_pref,cmds1,cmds2) =
     let _ = run_par seq_pref cmds1 cmds2 in
     true
 
@@ -88,7 +88,7 @@ module Make (Spec: Spec) = struct
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
-         repeat rep_count stress_test_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
+         repeat rep_count stress_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
   let neg_agree_test_par ~count ~name =
     let rep_count = 25 in

lib/STM_domain.mli

@@ -40,6 +40,15 @@ module Make : functor (Spec : STM.Spec) ->
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system {!Spec.sut}
         and returns the list of corresponding {!Spec.cmd} and result pairs. *)
 
+    val stress_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+    (** Parallel stress testing property based on {!Stdlib.Domain}.
+        [stress_prop_par (seq_pref, tl1, tl2)] first interprets [seq_pref]
+        and then spawns two parallel, symmetric domains interpreting [tl1] and
+        [tl2] simultaneously. In contrast to {!agree_prop_par}, [stress_prop_par]
+        does not perform an interleaving search.
+
+        @return [true] if no unexpected exceptions or crashes are encountered. *)
+
     val agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
     (** Parallel agreement property based on {!Stdlib.Domain}.
         [agree_prop_par (seq_pref, tl1, tl2)] first interprets [seq_pref]

src/buffer/stm_tests.ml

@@ -147,4 +147,5 @@ module BufferSTM_dom = STM_domain.Make(BConf)
 QCheck_base_runner.run_tests_main
   (let count = 1000 in
    [BufferSTM_seq.agree_test         ~count ~name:"STM Buffer test sequential";
-    BufferSTM_dom.neg_agree_test_par ~count ~name:"STM Buffer test parallel"])
+    BufferSTM_dom.neg_agree_test_par ~count ~name:"STM Buffer test parallel";
+    BufferSTM_dom.stress_test_par    ~count ~name:"STM Buffer stress test parallel"])

src/domain/stm_tests_dls.ml

@@ -65,6 +65,9 @@ let agree_prop cs = Domain.spawn (fun () -> DLS_STM_seq.agree_prop cs) |> Domain
 (* Run domain property in a child domain to have a clean DLS for each iteration *)
 let agree_prop_par t = Domain.spawn (fun () -> DLS_STM_dom.agree_prop_par t) |> Domain.join
 
+(* Run stress property in a child domain to have a clean DLS for each iteration *)
+let stress_prop_par t = Domain.spawn (fun () -> DLS_STM_dom.stress_prop_par t) |> Domain.join
+
 let agree_test ~count ~name =
   Test.make ~name ~count (DLS_STM_seq.arb_cmds DLSConf.init_state) agree_prop
 
@@ -75,8 +78,18 @@ let neg_agree_test_par ~count ~name =
     (fun triple ->
        assume (DLS_STM_dom.all_interleavings_ok triple);
        agree_prop_par triple) (* just repeat 1 * 10 times when shrinking *)
+
+let stress_test_par ~count ~name =
+  let seq_len,par_len = 20,12 in
+  Test.make ~retries:10 ~count ~name
+    (DLS_STM_dom.arb_cmds_triple seq_len par_len)
+    (fun triple ->
+       assume (DLS_STM_dom.all_interleavings_ok triple);
+       stress_prop_par triple) (* just repeat 1 * 10 times when shrinking *)
+;;
 ;;
 QCheck_base_runner.run_tests_main [
   agree_test         ~count:1000 ~name:"STM Domain.DLS test sequential";
   neg_agree_test_par ~count:1000 ~name:"STM Domain.DLS test parallel";
+  stress_test_par    ~count:1000 ~name:"STM Domain.DLS stress test parallel";
 ]

src/sys/stm_tests.ml

@@ -330,5 +330,6 @@ QCheck_base_runner.run_tests_main [
     Sys_seq.agree_test              ~count:1000 ~name:"STM Sys test sequential";
     if Sys.unix && uname_os () = Some "Linux"
     then Sys_dom.agree_test_par     ~count:200  ~name:"STM Sys test parallel"
-    else Sys_dom.neg_agree_test_par ~count:2500 ~name:"STM Sys test parallel"
+    else Sys_dom.neg_agree_test_par ~count:2500 ~name:"STM Sys test parallel";
+    Sys_dom.stress_test_par         ~count:1000 ~name:"STM Sys stress test parallel";
   ]

src/weak/stm_tests.ml

@@ -126,9 +126,13 @@ let run_tests l =
     ~long:cli_args.cli_long_tests ~out:stdout ~rand:cli_args.cli_rand
 let status_seq =
   run_tests
-    [ WeakSTM_seq.agree_test                ~count:1000 ~name:"STM Weak test sequential"; ]
+    [ WeakSTM_seq.agree_test         ~count:1000 ~name:"STM Weak test sequential"; ]
 let () = Gc.full_major ()
 let status_par =
   run_tests
-    [ WeakSTM_dom.neg_agree_test_par        ~count:5000 ~name:"STM Weak test parallel"; ]
-let _ = exit (if status_seq=0 && status_par=0 then 0 else 1)
+    [ WeakSTM_dom.neg_agree_test_par ~count:5000 ~name:"STM Weak test parallel"; ]
+let () = Gc.full_major ()
+let status_stress =
+  run_tests
+    [ WeakSTM_dom.stress_test_par    ~count:1000 ~name:"STM Weak stress test parallel"; ]
+let _ = exit (if status_seq=0 && status_par=0 && status_stress=0 then 0 else 1)

src/weak/stm_tests_hashset.ml

@@ -186,4 +186,8 @@ let () = Gc.full_major ()
 let status_par =
   run_tests
     [ WeakHashsetSTM_dom.neg_agree_test_par ~count:5000 ~name:"STM Weak HashSet test parallel" ]
-let _ = exit (if status_seq=0 && status_par=0 then 0 else 1)
+let () = Gc.full_major ()
+let status_stress =
+  run_tests
+    [ WeakHashsetSTM_dom.stress_test_par    ~count:1000 ~name:"STM Weak HashSet stress test parallel"; ]
+let _ = exit (if status_seq=0 && status_par=0 && status_stress=0 then 0 else 1)