Merge pull request #443 from ocaml-multicore/lin-stress-mode

Add Lin_domain.stress_test

Author: jmid

CHANGES.md

@@ -4,6 +4,8 @@
 
 - #415: Remove `--verbose` in internal `mutable_set_v5` expect test to avoid
   a test failure on a slow machine
+- #443: Add `Lin_domain.stress_test` as a lighter stress test, not
+  requiring an interleaving search.
 
 ## 0.3
 

lib/lin_domain.ml

@@ -10,8 +10,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = 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)
 
-  (* Linearization property based on [Domain] and an Atomic flag *)
-  let lin_prop (seq_pref,cmds1,cmds2) =
+  let run_parallel (seq_pref,cmds1,cmds2) =
     let sut = Spec.init () in
     let pref_obs = interp sut seq_pref in
     let wait = Atomic.make true in
@@ -22,18 +21,31 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     Spec.cleanup sut ;
     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)
+
+  (* Linearization property based on [Domain] and an Atomic flag *)
+  let lin_prop (seq_pref,cmds1,cmds2) =
+    let pref_obs,obs1,obs2 = run_parallel (seq_pref,cmds1,cmds2) in
     let seq_sut = Spec.init () in
     check_seq_cons pref_obs obs1 obs2 seq_sut []
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ Util.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)
 
+  (* "Don't crash under parallel usage" property *)
+  let stress_prop (seq_pref,cmds1,cmds2) =
+    let _ = run_parallel (seq_pref,cmds1,cmds2) in
+    true
+
   let lin_test ~count ~name =
-    lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
+    M.lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
 
   let neg_lin_test ~count ~name =
     neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
+
+  let stress_test ~count ~name =
+    M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:stress_prop
 end
 
 module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))

lib/lin_domain.mli

@@ -4,8 +4,10 @@ open Lin
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
   val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+  val stress_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : 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"]
 
@@ -24,4 +26,10 @@ module Make (Spec : Spec) : sig
       found, and succeeds if a counter example is indeed found, and prints it
       afterwards.
   *)
+
+  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}. *)
 end

src/README.md

@@ -45,7 +45,7 @@ Tests utilizing the parallel STM.ml capability:
 
 
 
-Tests utilizing the linearization tests of Lin.ml:
+Tests utilizing `Lin`:
 
  - [array/lin_internal_tests.ml](array/lin_internal_tests.ml) and [array/lin_tests.ml](array/lin_tests.ml)
    contain experimental `Lin.Internal` and `Lin`-tests of `Array`
@@ -61,6 +61,8 @@ Tests utilizing the linearization tests of Lin.ml:
 
  - [dynlink/lin_tests.ml](dynlink/lin_tests.ml) contains experimental `Lin`-tests of `Dynlink`
 
+ - [ephemeron/lin_tests.ml](ephemeron/lin_tests.ml) contains experimental `Lin`-stress tests of `Ephemeron`
+
  - [floatarray/lin_tests.ml](floatarray/lin_tests.ml) contains experimental `Lin`-tests of `Float.Array`
 
  - [hashtbl/lin_internal_tests.ml](hashtbl/lin_internal_tests.ml) and [hashtbl/lin_tests.ml](hashtbl/lin_tests.ml)
@@ -80,6 +82,10 @@ Tests utilizing the linearization tests of Lin.ml:
  - [stack/lin_internal_tests.ml](stack/lin_internal_tests.ml) and [stack/lin_tests.ml](stack/lin_tests.ml)
    contain experimental `Lin.Internal` and `Lin`-tests of `Stack`
 
+ - [weak/lin_tests.ml](weak/lin_tests.ml) and
+   [weak/lin_tests_hashset.ml](weak/lin_tests_hashset.ml) contains experimental
+   `Lin`-stress tests of the `Weak` module
+
 
 
 Tests of the underlying spawn/async functionality of `Domain` and

src/array/lin_tests.ml

@@ -30,4 +30,5 @@ module AT_domain = Lin_domain.Make(AConf)
 ;;
 QCheck_base_runner.run_tests_main [
   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";
 ]

src/bigarray/lin_tests.ml

@@ -30,4 +30,5 @@ module BA1T = Lin_domain.Make(BA1Conf)
 let _ =
   QCheck_base_runner.run_tests_main [
     BA1T.neg_lin_test ~count:5000 ~name:"Lin Bigarray.Array1 (of ints) test with Domain";
+    BA1T.stress_test  ~count:1000 ~name:"Lin Bigarray.Array1 stress test with Domain";
   ]

src/dynlink/lin_tests.ml

@@ -31,9 +31,10 @@ end
 module DynT = Lin_domain.Make(DynConf)
 
 let _ =
-  if Sys.win32 then
-    Printf.printf "negative Lin Dynlink test with Domain disabled under Windows\n\n%!"
-  else
-    QCheck_base_runner.run_tests_main [
-      DynT.neg_lin_test ~count:100 ~name:"negative Lin Dynlink test with Domain";
-    ]
+  let ts = [DynT.stress_test ~count:1000 ~name:"Lin Dynlink stress test with Domain"] in
+  let ts =
+    if Sys.win32 then
+      (Printf.printf "negative Lin Dynlink test with Domain disabled under Windows\n\n%!"; ts)
+    else
+      (DynT.neg_lin_test ~count:100 ~name:"negative Lin Dynlink test with Domain")::ts in
+  QCheck_base_runner.run_tests_main ts

src/ephemeron/dune

@@ -7,3 +7,11 @@
  (libraries qcheck-stm.sequential qcheck-stm.domain)
  (action (run %{test} --verbose))
 )
+
+(test
+ (name lin_tests)
+ (modules lin_tests)
+ (package multicoretests)
+ (libraries qcheck-lin.domain)
+ (action (run %{test} --verbose))
+)

src/ephemeron/lin_tests.ml

@@ -0,0 +1,37 @@
+(* ************************************************************ *)
+(*                   Lin tests of [Ephemeron]                   *)
+(* ************************************************************ *)
+
+module EConf =
+  struct
+     module E = Ephemeron.K1.Make(struct
+                   type t = Int.t
+                   let equal = Int.equal
+                   let hash = Fun.id
+                 end)
+
+    type t = string E.t
+    let init () = E.create 42
+    let cleanup _ = ()
+
+    open Lin
+    let int,string = nat_small, string_small_printable
+    let api =
+      [ val_ "Ephemeron.clear"    E.clear    (t @-> returning unit);
+        val_ "Ephemeron.add"      E.add      (t @-> int @-> string @-> returning unit);
+        val_ "Ephemeron.remove"   E.remove   (t @-> int @-> returning unit);
+        val_ "Ephemeron.find"     E.find     (t @-> int @-> returning_or_exc string);
+        val_ "Ephemeron.find_opt" E.find_opt (t @-> int @-> returning (option string));
+        val_ "Ephemeron.find_all" E.find_all (t @-> int @-> returning (list string));
+        val_ "Ephemeron.replace"  E.replace  (t @-> int @-> string @-> returning unit);
+        val_ "Ephemeron.mem"      E.mem      (t @-> int @-> returning bool);
+        val_ "Ephemeron.length"   E.length   (t @-> returning int);
+        val_ "Ephemeron.clean"    E.clean    (t @-> returning unit);
+      ]
+  end
+
+module ET_domain = Lin_domain.Make(EConf)
+;;
+QCheck_base_runner.run_tests_main [
+  ET_domain.stress_test ~count:1000 ~name:"Lin Ephemeron stress test with Domain";
+]

src/floatarray/lin_tests.ml

@@ -38,4 +38,5 @@ module FAT = Lin_domain.Make(FAConf)
 let _ =
   QCheck_base_runner.run_tests_main [
     FAT.neg_lin_test ~count:1000 ~name:"Lin Float.Array test with Domain";
+    FAT.stress_test  ~count:1000 ~name:"Lin Float.Array stress test with Domain";
   ]