diff --git a/CHANGES.md b/CHANGES.md index 04e1d45d..194dd4f8 100644 --- a/CHANGES.md +++ b/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 diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 4c525e67..57eced2b 100644 --- a/lib/lin_domain.ml +++ b/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,6 +21,11 @@ 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" @@ -29,11 +33,19 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct (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)) diff --git a/lib/lin_domain.mli b/lib/lin_domain.mli index f8306a44..ef701f00 100644 --- a/lib/lin_domain.mli +++ b/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 diff --git a/src/README.md b/src/README.md index 5970f3b5..bbd43bef 100644 --- a/src/README.md +++ b/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 diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml index 28e034fc..e52d01d3 100644 --- a/src/array/lin_tests.ml +++ b/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"; ] diff --git a/src/bigarray/lin_tests.ml b/src/bigarray/lin_tests.ml index d55b5926..f96398fe 100644 --- a/src/bigarray/lin_tests.ml +++ b/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"; ] diff --git a/src/dynlink/lin_tests.ml b/src/dynlink/lin_tests.ml index 89ca2f59..e93afd4c 100644 --- a/src/dynlink/lin_tests.ml +++ b/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 diff --git a/src/ephemeron/dune b/src/ephemeron/dune index f314661f..9afe1de4 100644 --- a/src/ephemeron/dune +++ b/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)) +) diff --git a/src/ephemeron/lin_tests.ml b/src/ephemeron/lin_tests.ml new file mode 100644 index 00000000..8b602e7d --- /dev/null +++ b/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"; +] diff --git a/src/floatarray/lin_tests.ml b/src/floatarray/lin_tests.ml index 9ee93982..20005ca7 100644 --- a/src/floatarray/lin_tests.ml +++ b/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"; ] diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml index bc58020a..55f2d8a3 100644 --- a/src/hashtbl/lin_tests.ml +++ b/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"; ] diff --git a/src/io/lin_tests_domain.ml b/src/io/lin_tests_domain.ml index b10c5775..c1c4c888 100644 --- a/src/io/lin_tests_domain.ml +++ b/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"; ] diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml index 10991eda..e03cb7b2 100644 --- a/src/lazy/lin_tests.ml +++ b/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"; ]) diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml index d5be8746..02845316 100644 --- a/src/queue/lin_tests.ml +++ b/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 = diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml index a9d4cefe..1fdef20c 100644 --- a/src/stack/lin_tests.ml +++ b/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 = diff --git a/src/weak/dune b/src/weak/dune index 0d59a61a..dc28984e 100644 --- a/src/weak/dune +++ b/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)) +) diff --git a/src/weak/lin_tests.ml b/src/weak/lin_tests.ml new file mode 100644 index 00000000..56c44db2 --- /dev/null +++ b/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"; +] diff --git a/src/weak/lin_tests_hashset.ml b/src/weak/lin_tests_hashset.ml new file mode 100644 index 00000000..8e045168 --- /dev/null +++ b/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"; +]