Merge pull request #462 from OlivierNicole/stm-stress-test

Add STM_domain.stress_test_par test

CHANGES.md

@@ -6,6 +6,8 @@
   a test failure on a slow machine
 - #443: Add `Lin_domain.stress_test` as a lighter stress test, not
   requiring an interleaving search.
+- #462: Add `STM_domain.stress_test_par`, similar to `Lin_domain.stress_test`
+  for STM models.
 
 ## 0.3
 

lib/STM_domain.ml

@@ -22,7 +22,7 @@ module Make (Spec: Spec) = struct
     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)
 
-  let agree_prop_par (seq_pref,cmds1,cmds2) =
+  let run_par seq_pref cmds1 cmds2 =
     let sut = Spec.init_sut () in
     let pref_obs = interp_sut_res sut seq_pref in
     let wait = Atomic.make true in
@@ -33,12 +33,20 @@ module Make (Spec: Spec) = struct
     let ()   = Spec.cleanup sut in
     let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
     let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
+    pref_obs, obs1, obs2
+
+  let agree_prop_par (seq_pref,cmds1,cmds2) =
+    let pref_obs, obs1, obs2 = run_par seq_pref cmds1 cmds2 in
     check_obs pref_obs obs1 obs2 Spec.init_state
       || Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
            (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 _ = run_par seq_pref cmds1 cmds2 in
+    true
+
   let agree_prop_par_asym (seq_pref, cmds1, cmds2) =
     let sut = Spec.init_sut () in
     let pref_obs = interp_sut_res sut seq_pref in
@@ -72,6 +80,16 @@ module Make (Spec: Spec) = struct
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
+  let stress_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 ->
+         assume (all_interleavings_ok triple);
+         repeat rep_count stress_test_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
+
   let neg_agree_test_par ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in

lib/STM_domain.mli

@@ -76,4 +76,14 @@ module Make : functor (Spec : STM.Spec) ->
     (** 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. *)
+
+    val stress_test_par : count:int -> name:string -> QCheck.Test.t
+    (** Parallel stress 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.
+        The test fails if an unexpected exception is raised underway. It is
+        intended as a stress test to run operations at a high frequency and
+        detect unexpected exceptions or crashes. It does not perform an
+        interleaving search like {!agree_test_par} and {!neg_agree_test_par}. *)
+
  end

lib/lin_domain.mli

@@ -30,6 +30,7 @@ module Make (Spec : Spec) : sig
   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
-      interleaving search like {!lin_test} and {!neg_lin_test}. *)
+      raised underway. It is intended as a stress test to run operations at a
+      high frequency and detect unexpected exceptions or crashes. It does not
+      perform an interleaving search like {!lin_test} and {!neg_lin_test}. *)
 end