Add Lin_domain.stress_test

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";
   ]

src/hashtbl/lin_tests.ml

@@ -27,4 +27,5 @@ module HT_domain = Lin_domain.Make(HConf)
 ;;
 QCheck_base_runner.run_tests_main [
   HT_domain.neg_lin_test ~count:1000 ~name:"Lin Hashtbl test with Domain";
+  HT_domain.stress_test  ~count:1000 ~name:"Lin Hashtbl stress test with Domain";
 ]

src/io/lin_tests_domain.ml

@@ -6,5 +6,6 @@ module IC_domain = Lin_domain.Make(Lin_tests_spec_io.ICConf)
 
 let _ =
   QCheck_base_runner.run_tests_main [
-    IC_domain.neg_lin_test ~count:1000 ~name:"Lin In_channel test with Domain"
+    IC_domain.neg_lin_test ~count:1000 ~name:"Lin In_channel test with Domain";
+    IC_domain.stress_test  ~count:1000 ~name:"Lin In_channel stress test with Domain";
   ]

src/lazy/lin_tests.ml

@@ -68,6 +68,8 @@ module LTfromfun_domain = Lin_domain.Make(LTfromfunAPI)
 QCheck_base_runner.run_tests_main
   (let count = 100 in
    [LTlazy_domain.neg_lin_test    ~count ~name:"Lin Lazy test with Domain";
+    LTlazy_domain.stress_test     ~count ~name:"Lin Lazy stress test with Domain";
     LTfromval_domain.lin_test     ~count ~name:"Lin Lazy test with Domain from_val";
     LTfromfun_domain.neg_lin_test ~count ~name:"Lin Lazy test with Domain from_fun";
+    LTfromfun_domain.stress_test  ~count ~name:"Lin Lazy stress test with Domain from_fun";
    ])

src/queue/lin_tests.ml

@@ -23,6 +23,7 @@ module Lin_queue_thread = Lin_thread.Make(Queue_spec) [@alert "-experimental"]
 let () =
   let tests = [
     Lin_queue_domain.neg_lin_test ~count:1000 ~name:"Lin Queue test with Domain";
+    Lin_queue_domain.stress_test  ~count:1000 ~name:"Lin Queue stress test with Domain";
     Lin_queue_thread.lin_test     ~count:250  ~name:"Lin Queue test with Thread";
   ] in
   let tests =

src/stack/lin_tests.ml

@@ -23,6 +23,7 @@ module Stack_thread = Lin_thread.Make(Stack_spec) [@alert "-experimental"]
 let () =
   let tests = [
     Stack_domain.neg_lin_test ~count:1000 ~name:"Lin Stack test with Domain";
+    Stack_domain.stress_test  ~count:1000 ~name:"Lin Stack stress test with Domain";
     Stack_thread.lin_test ~count:250 ~name:"Lin Stack test with Thread";
   ] in
   let tests =

src/weak/dune

@@ -15,3 +15,19 @@
  (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))
+)
+
+(test
+ (name lin_tests_hashset)
+ (modules lin_tests_hashset)
+ (package multicoretests)
+ (libraries qcheck-lin.domain)
+ (action (run %{test} --verbose))
+)

src/weak/lin_tests.ml

@@ -0,0 +1,29 @@
+(* ********************************************************************** *)
+(*                            Lin Tests [Weak]                            *)
+(* ********************************************************************** *)
+module WConf =
+struct
+  type t = int64 Weak.t
+
+  let weak_size = 16
+  let init () = Weak.create weak_size
+  let cleanup _ = ()
+
+  open Lin
+  let int,int64 = nat_small,nat64_small
+  let api =
+    [ val_ "Weak.length"   Weak.length   (t @-> returning int);
+      val_ "Weak.set"      Weak.set      (t @-> int @-> option int64 @-> returning_or_exc unit);
+      val_ "Weak.get"      Weak.get      (t @-> int @-> returning_or_exc (option int64));
+      val_ "Weak.get_copy" Weak.get_copy (t @-> int @-> returning_or_exc (option int64));
+      val_ "Weak.check"    Weak.check    (t @-> int @-> returning_or_exc bool);
+      val_ "Weak.fill"     Weak.fill     (t @-> int @-> int @-> option int64 @-> returning_or_exc unit);
+    (*val blit : 'a t -> int -> 'a t -> int -> int -> unit *)
+    ]
+end
+
+module WT_domain = Lin_domain.Make(WConf)
+;;
+QCheck_base_runner.run_tests_main [
+  WT_domain.stress_test ~count:1000 ~name:"Lin Weak stress test with Domain";
+]

src/weak/lin_tests_hashset.ml

@@ -0,0 +1,34 @@
+(* ********************************************************************** *)
+(*                       Lin tests of [Weak Hashset]                      *)
+(* ********************************************************************** *)
+module WHSConf =
+struct
+  module WHS = Weak.Make(String)
+  type t = WHS.t
+  let weak_size = 16
+  let init () = WHS.create weak_size
+  let cleanup t = WHS.clear t
+
+  open Lin
+  let string = string_small
+  let api =
+    [ val_ "Weak.S.clear"    WHS.clear    (t @-> returning unit);
+      val_ "Weak.S.merge"    WHS.merge    (t @-> string @-> returning_or_exc string);
+      val_ "Weak.S.add"      WHS.add      (t @-> string @-> returning_or_exc unit);
+      val_ "Weak.S.remove"   WHS.remove   (t @-> string @-> returning_or_exc unit);
+      val_ "Weak.S.find"     WHS.find     (t @-> string @-> returning_or_exc string);
+      val_ "Weak.S.find_opt" WHS.find_opt (t @-> string @-> returning_or_exc (option string));
+      val_ "Weak.S.find_all" WHS.find_all (t @-> string @-> returning_or_exc (list string));
+      val_ "Weak.S.mem"      WHS.mem      (t @-> string @-> returning_or_exc bool);
+    (*val iter : (data -> unit) -> t -> unit*)
+    (*val fold : (data -> 'a -> 'a) -> t -> 'a -> 'a*)
+      val_ "Weak.S.count"    WHS.count    (t @-> returning int);
+    (*val stats : t -> int * int * int * int * int * int*)
+    ]
+end
+
+module WHST_domain = Lin_domain.Make(WHSConf)
+;;
+QCheck_base_runner.run_tests_main [
+  WHST_domain.stress_test ~count:1000 ~name:"Lin Weak HashSet stress test with Domain";
+]