From 4545c255265ecb4e6cfde843f3a89068d1af64a4 Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Thu, 25 Apr 2024 19:41:47 +0200 Subject: [PATCH 01/12] Avoid spawning domains for each parallel Lin test --- lib/dune | 2 +- lib/lin_domain.ml | 30 +++++++++++++++--------------- lib/lin_domain.mli | 26 +++++++++++++++++--------- 3 files changed, 33 insertions(+), 25 deletions(-) diff --git a/lib/dune b/lib/dune index 5d8dce98d..9ddea7a76 100644 --- a/lib/dune +++ b/lib/dune @@ -34,7 +34,7 @@ (public_name qcheck-lin.domain) (modules lin_domain) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin)) + (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin domainslib)) (library (name lin_effect) diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 57eced2b6..d53fd703d 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -10,22 +10,22 @@ 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) - let run_parallel (seq_pref,cmds1,cmds2) = + let run_parallel ~pool (seq_pref,cmds1,cmds2) = let sut = Spec.init () in let pref_obs = interp sut seq_pref in let wait = Atomic.make true in - let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp sut cmds1) with exn -> Error exn) in - let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in - let obs1 = Domain.join dom1 in - let obs2 = Domain.join dom2 in + let dom1 = Domainslib.Task.async pool (fun () -> while Atomic.get wait do () done; try Ok (interp sut cmds1) with exn -> Error exn) in + let dom2 = Domainslib.Task.async pool (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in + let obs1 = Domainslib.Task.await pool dom1 in + let obs2 = Domainslib.Task.await pool dom2 in 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 lin_prop ~pool (seq_pref,cmds1,cmds2) = + let pref_obs,obs1,obs2 = run_parallel ~pool (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" @@ -34,18 +34,18 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct (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 + let stress_prop ~pool (seq_pref,cmds1,cmds2) = + let _ = run_parallel ~pool (seq_pref,cmds1,cmds2) in true - let lin_test ~count ~name = - M.lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop + let lin_test ~pool ~count ~name = + M.lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(lin_prop ~pool) - let neg_lin_test ~count ~name = - neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop + let neg_lin_test ~pool ~count ~name = + neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(lin_prop ~pool) - let stress_test ~count ~name = - M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:stress_prop + let stress_test ~pool ~count ~name = + M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(stress_prop ~pool) end module Make (Spec : Spec) = Make_internal(MakeCmd(Spec)) diff --git a/lib/lin_domain.mli b/lib/lin_domain.mli index ef701f004..4ef5b956d 100644 --- a/lib/lin_domain.mli +++ b/lib/lin_domain.mli @@ -2,32 +2,40 @@ open Lin (** functor to build an internal module representing parallel tests *) 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 + val arb_cmds_triple + : int + -> int + -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary + + val lin_prop : pool:Domainslib.Task.pool -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + + val stress_prop : pool:Domainslib.Task.pool -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + + val lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + + val neg_lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + + val stress_test : pool:Domainslib.Task.pool -> 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"] (** functor to build a module for parallel testing *) module Make (Spec : Spec) : sig - val lin_test : count:int -> name:string -> QCheck.Test.t + val lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t (** [lin_test ~count:c ~name:n] builds a parallel test with the name [n] that iterates [c] times. The test fails if one of the generated programs is not sequentially consistent. In that case it fails, and prints a reduced counter example. *) - val neg_lin_test : count:int -> name:string -> QCheck.Test.t + val neg_lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t (** [neg_lin_test ~count:c ~name:n] builds a negative parallel test with the name [n] that iterates [c] times. The test fails if no counter example is found, and succeeds if a counter example is indeed found, and prints it afterwards. *) - val stress_test : count:int -> name:string -> QCheck.Test.t + val stress_test : pool:Domainslib.Task.pool -> 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 From 5ef08430d875638f7cd44fbbf825935d94022811 Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Thu, 25 Apr 2024 20:18:11 +0200 Subject: [PATCH 02/12] Avoid spawning domains in each STM test --- lib/STM_domain.ml | 38 +++++++++++++++++---------------- lib/STM_domain.mli | 12 +++++------ lib/dune | 2 +- src/array/dune | 2 +- src/array/lin_internal_tests.ml | 9 ++++++-- src/array/lin_tests.ml | 11 +++++++--- src/array/stm_tests.ml | 10 +++++++-- 7 files changed, 51 insertions(+), 33 deletions(-) diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index aa1408df0..d5edaafce 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -1,5 +1,7 @@ open STM +module T = Domainslib.Task + module Make (Spec: Spec) = struct open Util @@ -22,14 +24,14 @@ 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 agree_prop_par ~pool (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 - let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in - let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in - let obs1 = Domain.join dom1 in - let obs2 = Domain.join dom2 in + let dom1 = T.async pool (fun () -> while Atomic.get wait do () done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in + let dom2 = T.async pool (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in + let obs1 = T.await pool dom1 in + let obs2 = T.await pool dom2 in 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 @@ -39,20 +41,20 @@ module Make (Spec: Spec) = struct (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) (pref_obs,obs1,obs2) - let agree_prop_par_asym (seq_pref, cmds1, cmds2) = + let agree_prop_par_asym ~pool (seq_pref, cmds1, cmds2) = let sut = Spec.init_sut () in let pref_obs = interp_sut_res sut seq_pref in let wait = Atomic.make 2 in let child_dom = - Domain.spawn (fun () -> + T.async pool (fun () -> Atomic.decr wait; - while Atomic.get wait <> 0 do Domain.cpu_relax() done; + while Atomic.get wait <> 0 do () done; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in Atomic.decr wait; - while Atomic.get wait <> 0 do Domain.cpu_relax() done; + while Atomic.get wait <> 0 do () done; let parent_obs = try Ok (interp_sut_res sut cmds1) with exn -> Error exn in - let child_obs = Domain.join child_dom in + let child_obs = T.await pool child_dom in let () = Spec.cleanup sut in let parent_obs = match parent_obs with Ok v -> v | Error exn -> raise exn in let child_obs = match child_obs with Ok v -> v | Error exn -> raise exn in @@ -62,7 +64,7 @@ module Make (Spec: Spec) = struct (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) (pref_obs,parent_obs,child_obs) - let agree_test_par ~count ~name = + let agree_test_par ~pool ~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 *) @@ -70,9 +72,9 @@ module Make (Spec: Spec) = struct (arb_cmds_triple seq_len par_len) (fun triple -> assume (all_interleavings_ok triple); - repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) - let neg_agree_test_par ~count ~name = + let neg_agree_test_par ~pool ~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 *) @@ -80,9 +82,9 @@ module Make (Spec: Spec) = struct (arb_cmds_triple seq_len par_len) (fun triple -> assume (all_interleavings_ok triple); - repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) - let agree_test_par_asym ~count ~name = + let agree_test_par_asym ~pool ~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 *) @@ -90,9 +92,9 @@ module Make (Spec: Spec) = struct (arb_cmds_triple seq_len par_len) (fun triple -> assume (all_interleavings_ok triple); - repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par_asym ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) - let neg_agree_test_par_asym ~count ~name = + let neg_agree_test_par_asym ~pool ~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 *) @@ -100,5 +102,5 @@ module Make (Spec: Spec) = struct (arb_cmds_triple seq_len par_len) (fun triple -> assume (all_interleavings_ok triple); - repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par_asym ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) end diff --git a/lib/STM_domain.mli b/lib/STM_domain.mli index 7280b3546..f51a5b2fb 100644 --- a/lib/STM_domain.mli +++ b/lib/STM_domain.mli @@ -40,7 +40,7 @@ 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 agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + val agree_prop_par : pool:Domainslib.Task.pool -> 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] and then spawns two parallel, symmetric domains interpreting [tl1] and @@ -49,7 +49,7 @@ module Make : functor (Spec : STM.Spec) -> @return [true] if there exists a sequential interleaving of the results which agrees with a model interpretation. *) - val agree_prop_par_asym : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + val agree_prop_par_asym : pool:Domainslib.Task.pool -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool (** Asymmetric parallel agreement property based on {!Stdlib.Domain}. [agree_prop_par_asym (seq_pref, tl1, tl2)] first interprets [seq_pref], and then interprets [tl1] while a spawned domain interprets [tl2] @@ -58,21 +58,21 @@ module Make : functor (Spec : STM.Spec) -> @return [true] if there exists a sequential interleaving of the results which agrees with a model interpretation. *) - val agree_test_par : count:int -> name:string -> QCheck.Test.t + val agree_test_par : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t (** Parallel agreement 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. *) - val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t + val neg_agree_test_par : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t (** A negative parallel agreement test (for convenience). Accepts two labeled parameters: [count] is the number of test iterations and [name] is the printed test name. *) - val agree_test_par_asym : count:int -> name:string -> QCheck.Test.t + val agree_test_par_asym : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t (** Asymmetric parallel agreement test based on {!Stdlib.Domain} and {!agree_prop_par_asym} which combines [repeat] and [~retries]. Accepts two labeled parameters: [count] is the number of test iterations and [name] is the printed test name. *) - val neg_agree_test_par_asym : count:int -> name:string -> QCheck.Test.t + val neg_agree_test_par_asym : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t (** 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. *) diff --git a/lib/dune b/lib/dune index 9ddea7a76..7d1353299 100644 --- a/lib/dune +++ b/lib/dune @@ -15,7 +15,7 @@ (public_name qcheck-stm.domain) (modules STM_domain) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-stm.stm)) + (libraries qcheck-core qcheck-stm.stm domainslib)) (library (name STM_thread) diff --git a/src/array/dune b/src/array/dune index c69df6358..2d3b03e96 100644 --- a/src/array/dune +++ b/src/array/dune @@ -22,6 +22,6 @@ (name lin_tests) (modules lin_tests) (package multicoretests) - (libraries qcheck-lin.domain) + (libraries qcheck-lin.domain domainslib) (action (run %{test} --verbose)) ) diff --git a/src/array/lin_internal_tests.ml b/src/array/lin_internal_tests.ml index 6b992eeb2..e0662d623 100644 --- a/src/array/lin_internal_tests.ml +++ b/src/array/lin_internal_tests.ml @@ -117,6 +117,11 @@ end module AT_domain = Lin_domain.Make_internal(AConf) [@alert "-internal"] ;; +let () = + let module T = Domainslib.Task in + let pool = T.setup_pool ~num_domains:2 () in + T.run pool (fun () -> QCheck_base_runner.run_tests_main [ - AT_domain.neg_lin_test ~count:1000 ~name:"Lin.Internal Array test with Domain"; -] + AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin.Internal Array test with Domain"; +]) |> ignore; + T.teardown_pool pool diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml index e52d01d34..89a22066c 100644 --- a/src/array/lin_tests.ml +++ b/src/array/lin_tests.ml @@ -28,7 +28,12 @@ end module AT_domain = Lin_domain.Make(AConf) ;; +let () = + let module T = Domainslib.Task in + let pool = T.setup_pool ~num_domains:2 () in + T.run pool (fun () -> 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"; -] + AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin Array test with Domain"; + AT_domain.stress_test ~pool ~count:1000 ~name:"Lin Array stress test with Domain"; +]) |> ignore; + T.teardown_pool pool diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index 2e0124386..4627ec882 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -162,8 +162,14 @@ end module ArraySTM_seq = STM_sequential.Make(AConf) module ArraySTM_dom = STM_domain.Make(AConf) ;; +let () = + let module T = Domainslib.Task in + let pool = T.setup_pool ~num_domains:2 () in + T.run pool (fun () -> QCheck_base_runner.run_tests_main (let count = 1000 in [ArraySTM_seq.agree_test ~count ~name:"STM Array test sequential"; - ArraySTM_dom.neg_agree_test_par ~count ~name:"STM Array test parallel" (* this test is expected to fail *) -]) + ArraySTM_dom.neg_agree_test_par ~pool ~count ~name:"STM Array test parallel"; (* this test is expected to fail *) + (*ArraySTM_dom.stress_test_par ~pool ~count ~name:"STM Array stress test" (* Test for absence of crashes *)*) + ])) |> ignore; + T.teardown_pool pool From f1b58051699fa69f00a29758f7f7f6582e53cb1c Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Thu, 25 Apr 2024 23:52:02 +0200 Subject: [PATCH 03/12] Add Domainslib to dependencies of Lin and STM --- dune-project | 6 ++++-- qcheck-lin.opam | 1 + qcheck-stm.opam | 1 + 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/dune-project b/dune-project index e36f949f6..847cdd0fc 100644 --- a/dune-project +++ b/dune-project @@ -32,7 +32,8 @@ sequential and parallel tests against a declarative model.") (depends (ocaml (>= 4.12)) (qcheck-core (>= "0.20")) - (qcheck-multicoretests-util (= :version)))) + (qcheck-multicoretests-util (= :version)) + (domainslib (>= 0.5.1)))) (package (name qcheck-lin) @@ -47,7 +48,8 @@ and explained by some sequential interleaving.") (depends (ocaml (>= 4.12)) (qcheck-core (>= "0.20")) - (qcheck-multicoretests-util (= :version)))) + (qcheck-multicoretests-util (= :version)) + (domainslib (>= 0.5.1)))) (package (name qcheck-multicoretests-util) diff --git a/qcheck-lin.opam b/qcheck-lin.opam index 365258d85..cf77bbee4 100644 --- a/qcheck-lin.opam +++ b/qcheck-lin.opam @@ -25,6 +25,7 @@ depends: [ "ocaml" {>= "4.12"} "qcheck-core" {>= "0.20"} "qcheck-multicoretests-util" {= version} + "domainslib" {>= "0.5.1"} "odoc" {with-doc} ] depopts: ["base-domains"] diff --git a/qcheck-stm.opam b/qcheck-stm.opam index 6582bfa20..b319e7335 100644 --- a/qcheck-stm.opam +++ b/qcheck-stm.opam @@ -25,6 +25,7 @@ depends: [ "ocaml" {>= "4.12"} "qcheck-core" {>= "0.20"} "qcheck-multicoretests-util" {= version} + "domainslib" {>= "0.5.1"} "odoc" {with-doc} ] depopts: ["base-domains"] From 1d756ba05927084975cb761f74ac9c930b102134 Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Sat, 27 Apr 2024 21:56:07 +0200 Subject: [PATCH 04/12] Use a domain pair rather than a domain pool (faster?) --- lib/STM_domain.ml | 16 ++++----- lib/STM_domain.mli | 12 +++---- lib/dune | 6 ++-- lib/lin_domain.ml | 11 +++--- lib/lin_domain.mli | 16 ++++----- lib/util.ml | 63 +++++++++++++++++++++++++++++++++ lib/util.mli | 11 ++++++ src/array/lin_internal_tests.ml | 7 ++-- src/array/lin_tests.ml | 7 ++-- src/array/stm_tests.ml | 7 ++-- 10 files changed, 110 insertions(+), 46 deletions(-) diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index d5edaafce..ea8f058ef 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -1,7 +1,5 @@ open STM -module T = Domainslib.Task - module Make (Spec: Spec) = struct open Util @@ -28,10 +26,10 @@ module Make (Spec: Spec) = struct let sut = Spec.init_sut () in let pref_obs = interp_sut_res sut seq_pref in let wait = Atomic.make true in - let dom1 = T.async pool (fun () -> while Atomic.get wait do () done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in - let dom2 = T.async pool (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in - let obs1 = T.await pool dom1 in - let obs2 = T.await pool dom2 in + let prom1 = Domain_pair.async_d1 pool (fun () -> while Atomic.get wait do Domain.cpu_relax () done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in + let prom2 = Domain_pair.async_d2 pool (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in + let obs1 = Domain_pair.await prom1 in + let obs2 = Domain_pair.await prom2 in 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 @@ -45,8 +43,8 @@ module Make (Spec: Spec) = struct let sut = Spec.init_sut () in let pref_obs = interp_sut_res sut seq_pref in let wait = Atomic.make 2 in - let child_dom = - T.async pool (fun () -> + let prom = + Domain_pair.async_d1 pool (fun () -> Atomic.decr wait; while Atomic.get wait <> 0 do () done; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) @@ -54,7 +52,7 @@ module Make (Spec: Spec) = struct Atomic.decr wait; while Atomic.get wait <> 0 do () done; let parent_obs = try Ok (interp_sut_res sut cmds1) with exn -> Error exn in - let child_obs = T.await pool child_dom in + let child_obs = Domain_pair.await prom in let () = Spec.cleanup sut in let parent_obs = match parent_obs with Ok v -> v | Error exn -> raise exn in let child_obs = match child_obs with Ok v -> v | Error exn -> raise exn in diff --git a/lib/STM_domain.mli b/lib/STM_domain.mli index f51a5b2fb..ced5a8150 100644 --- a/lib/STM_domain.mli +++ b/lib/STM_domain.mli @@ -40,7 +40,7 @@ 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 agree_prop_par : pool:Domainslib.Task.pool -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + val agree_prop_par : pool:Util.Domain_pair.t -> 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] and then spawns two parallel, symmetric domains interpreting [tl1] and @@ -49,7 +49,7 @@ module Make : functor (Spec : STM.Spec) -> @return [true] if there exists a sequential interleaving of the results which agrees with a model interpretation. *) - val agree_prop_par_asym : pool:Domainslib.Task.pool -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + val agree_prop_par_asym : pool:Util.Domain_pair.t -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool (** Asymmetric parallel agreement property based on {!Stdlib.Domain}. [agree_prop_par_asym (seq_pref, tl1, tl2)] first interprets [seq_pref], and then interprets [tl1] while a spawned domain interprets [tl2] @@ -58,21 +58,21 @@ module Make : functor (Spec : STM.Spec) -> @return [true] if there exists a sequential interleaving of the results which agrees with a model interpretation. *) - val agree_test_par : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val agree_test_par : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t (** Parallel agreement 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. *) - val neg_agree_test_par : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val neg_agree_test_par : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t (** A negative parallel agreement test (for convenience). Accepts two labeled parameters: [count] is the number of test iterations and [name] is the printed test name. *) - val agree_test_par_asym : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val agree_test_par_asym : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t (** Asymmetric parallel agreement test based on {!Stdlib.Domain} and {!agree_prop_par_asym} which combines [repeat] and [~retries]. Accepts two labeled parameters: [count] is the number of test iterations and [name] is the printed test name. *) - val neg_agree_test_par_asym : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val neg_agree_test_par_asym : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t (** 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. *) diff --git a/lib/dune b/lib/dune index 7d1353299..af63ad9d3 100644 --- a/lib/dune +++ b/lib/dune @@ -15,7 +15,7 @@ (public_name qcheck-stm.domain) (modules STM_domain) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-stm.stm domainslib)) + (libraries qcheck-core qcheck-stm.stm)) (library (name STM_thread) @@ -34,7 +34,7 @@ (public_name qcheck-lin.domain) (modules lin_domain) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin domainslib)) + (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin)) (library (name lin_effect) @@ -53,4 +53,4 @@ (name util) (public_name qcheck-multicoretests-util) (modules util) - (libraries qcheck-core.runner unix)) + (libraries qcheck-core.runner unix domainslib)) diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index d53fd703d..4e5e74e71 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -1,4 +1,5 @@ open Lin +open Util module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct module M = Internal.Make(Spec) [@alert "-internal"] @@ -7,17 +8,17 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct (* operate over arrays to avoid needless allocation underway *) let interp sut cs = let cs_arr = Array.of_list cs in - let res_arr = Array.map (fun c -> Domain.cpu_relax(); Spec.run c sut) cs_arr in + let res_arr = Array.map (fun c -> Spec.run c sut) cs_arr in List.combine cs (Array.to_list res_arr) let run_parallel ~pool (seq_pref,cmds1,cmds2) = let sut = Spec.init () in let pref_obs = interp sut seq_pref in let wait = Atomic.make true in - let dom1 = Domainslib.Task.async pool (fun () -> while Atomic.get wait do () done; try Ok (interp sut cmds1) with exn -> Error exn) in - let dom2 = Domainslib.Task.async pool (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in - let obs1 = Domainslib.Task.await pool dom1 in - let obs2 = Domainslib.Task.await pool dom2 in + let prom1 = Domain_pair.async_d1 pool (fun () -> while Atomic.get wait do Domain.cpu_relax () done; try Ok (interp sut cmds1) with exn -> Error exn) in + let prom2 = Domain_pair.async_d2 pool (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in + let obs1 = Domain_pair.await prom1 in + let obs2 = Domain_pair.await prom2 in 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 diff --git a/lib/lin_domain.mli b/lib/lin_domain.mli index 4ef5b956d..eb9701519 100644 --- a/lib/lin_domain.mli +++ b/lib/lin_domain.mli @@ -7,35 +7,35 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary - val lin_prop : pool:Domainslib.Task.pool -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + val lin_prop : pool:Util.Domain_pair.t -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool - val stress_prop : pool:Domainslib.Task.pool -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + val stress_prop : pool:Util.Domain_pair.t -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool - val lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t - val neg_lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val neg_lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t - val stress_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val stress_test : pool:Util.Domain_pair.t -> 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"] (** functor to build a module for parallel testing *) module Make (Spec : Spec) : sig - val lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t (** [lin_test ~count:c ~name:n] builds a parallel test with the name [n] that iterates [c] times. The test fails if one of the generated programs is not sequentially consistent. In that case it fails, and prints a reduced counter example. *) - val neg_lin_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val neg_lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t (** [neg_lin_test ~count:c ~name:n] builds a negative parallel test with the name [n] that iterates [c] times. The test fails if no counter example is found, and succeeds if a counter example is indeed found, and prints it afterwards. *) - val stress_test : pool:Domainslib.Task.pool -> count:int -> name:string -> QCheck.Test.t + val stress_test : pool:Util.Domain_pair.t -> 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 diff --git a/lib/util.ml b/lib/util.ml index 098d5432e..288349ad6 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -321,3 +321,66 @@ module Equal = struct | _ -> false let equal_array eq x y = equal_seq eq (Array.to_seq x) (Array.to_seq y) end + +module Chan = Domainslib.Chan + +module Domain_pair = struct + type 'a promise = 'a Chan.t + + type command = Command : (unit -> 'a) * 'a Chan.t -> command + + type t = + { d1 : unit Domain.t; + d2 : unit Domain.t; + d1_commands : command Chan.t; + d2_commands : command Chan.t; + d1_continue : bool Atomic.t; + d2_continue : bool Atomic.t; + } + + let async commands_chan f = + let res_chan = Chan.make_bounded 0 in + assert (Chan.send_poll commands_chan (Command (f, res_chan))); + res_chan + + let async_d1 pair f = + async pair.d1_commands f + + let async_d2 pair f = + async pair.d2_commands f + + let await = Chan.recv + + let domain_fun continue commands_chan = + while Atomic.get continue do + match Chan.recv commands_chan with + | Command (f, res_chan) -> + Chan.send res_chan (f ()); + () + done + + let init () = + let d1_continue = Atomic.make true in + let d2_continue = Atomic.make true in + let d1_commands = Chan.make_bounded 1 in + let d2_commands = Chan.make_bounded 1 in + { d1 = Domain.spawn (fun () -> domain_fun d1_continue d1_commands); + d2 = Domain.spawn (fun () -> domain_fun d2_continue d2_commands); + d1_commands; + d2_commands; + d1_continue; + d2_continue; + } + + let takedown pair = + Atomic.set pair.d1_continue false; + Atomic.set pair.d2_continue false; + Domain.join pair.d1; + Domain.join pair.d2 + + let run f = + let pair = init () in + let res = f pair in + takedown pair; + res +end diff --git a/lib/util.mli b/lib/util.mli index 5dee04219..1993e197f 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -250,3 +250,14 @@ module Equal : sig val equal_seq : 'a t -> 'a Seq.t t val equal_array : 'a t -> 'a array t end + +module Domain_pair : sig + type t + type 'a promise + val async_d1 : t -> (unit -> 'a) -> 'a promise + val async_d2 : t -> (unit -> 'a) -> 'a promise + val await : 'a promise -> 'a + val init : unit -> t + val takedown : t -> unit + val run : (t -> 'a) -> 'a +end diff --git a/src/array/lin_internal_tests.ml b/src/array/lin_internal_tests.ml index e0662d623..f9bca21dc 100644 --- a/src/array/lin_internal_tests.ml +++ b/src/array/lin_internal_tests.ml @@ -118,10 +118,7 @@ end module AT_domain = Lin_domain.Make_internal(AConf) [@alert "-internal"] ;; let () = - let module T = Domainslib.Task in - let pool = T.setup_pool ~num_domains:2 () in - T.run pool (fun () -> + Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main [ AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin.Internal Array test with Domain"; -]) |> ignore; - T.teardown_pool pool +]) diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml index 89a22066c..589b070c2 100644 --- a/src/array/lin_tests.ml +++ b/src/array/lin_tests.ml @@ -29,11 +29,8 @@ end module AT_domain = Lin_domain.Make(AConf) ;; let () = - let module T = Domainslib.Task in - let pool = T.setup_pool ~num_domains:2 () in - T.run pool (fun () -> + Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main [ AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin Array test with Domain"; AT_domain.stress_test ~pool ~count:1000 ~name:"Lin Array stress test with Domain"; -]) |> ignore; - T.teardown_pool pool +]) diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index 4627ec882..bab9680d7 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -163,13 +163,10 @@ module ArraySTM_seq = STM_sequential.Make(AConf) module ArraySTM_dom = STM_domain.Make(AConf) ;; let () = - let module T = Domainslib.Task in - let pool = T.setup_pool ~num_domains:2 () in - T.run pool (fun () -> + Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main (let count = 1000 in [ArraySTM_seq.agree_test ~count ~name:"STM Array test sequential"; ArraySTM_dom.neg_agree_test_par ~pool ~count ~name:"STM Array test parallel"; (* this test is expected to fail *) (*ArraySTM_dom.stress_test_par ~pool ~count ~name:"STM Array stress test" (* Test for absence of crashes *)*) - ])) |> ignore; - T.teardown_pool pool + ])) From a28370a38060e3d7e7bb8ac312037200e9ab09e0 Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Tue, 30 Apr 2024 23:30:41 +0200 Subject: [PATCH 05/12] Use Stdlib mutexes rather than depend on Domainslib Co-authored-by: Fabrice Buoro --- lib/util.ml | 109 +++++++++++++++++++++---------- src/atomic/lin_internal_tests.ml | 8 ++- 2 files changed, 80 insertions(+), 37 deletions(-) diff --git a/lib/util.ml b/lib/util.ml index 288349ad6..b1d89a437 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -325,56 +325,97 @@ end module Chan = Domainslib.Chan module Domain_pair = struct - type 'a promise = 'a Chan.t + type 'a promise = + { mutable result : 'a option; + mutex : Mutex.t; + fulfilled : Condition.t; + } + + type command = Task : (unit -> 'a) * 'a promise -> command - type command = Command : (unit -> 'a) * 'a Chan.t -> command + type task_mvar = + { mutable task : command option; + task_mutex : Mutex.t; + new_task : Condition.t; + promise_mutex : Mutex.t; + promise_fulfilled : Condition.t; + } type t = - { d1 : unit Domain.t; + { task1 : task_mvar; + task2 : task_mvar; + d1 : unit Domain.t; d2 : unit Domain.t; - d1_commands : command Chan.t; - d2_commands : command Chan.t; - d1_continue : bool Atomic.t; - d2_continue : bool Atomic.t; + done_ : bool Atomic.t; } - let async commands_chan f = - let res_chan = Chan.make_bounded 0 in - assert (Chan.send_poll commands_chan (Command (f, res_chan))); - res_chan + let async runner f = + let promise = + { result = None; mutex = runner.promise_mutex; fulfilled = runner.promise_fulfilled } + in + Mutex.lock runner.task_mutex; + runner.task <- (Some (Task (f, promise))); + Condition.signal runner.new_task; + Mutex.unlock runner.task_mutex; + promise let async_d1 pair f = - async pair.d1_commands f + async pair.task1 f let async_d2 pair f = - async pair.d2_commands f - - let await = Chan.recv - - let domain_fun continue commands_chan = - while Atomic.get continue do - match Chan.recv commands_chan with - | Command (f, res_chan) -> - Chan.send res_chan (f ()); - () + async pair.task2 f + + let await promise = + Mutex.lock promise.mutex; + while Option.is_none promise.result do + Condition.wait promise.fulfilled promise.mutex + done; + let result = Option.get promise.result in + promise.result <- None; + Mutex.unlock promise.mutex; + result + + let domain_fun done_ runner = + while not (Atomic.get done_) do + Mutex.lock runner.task_mutex; + while Option.is_none runner.task do + Condition.wait runner.new_task runner.task_mutex + done; + let Task (f, promise) = Option.get runner.task in + runner.task <- None; + Mutex.unlock runner.task_mutex; + Mutex.lock promise.mutex; + promise.result <- Some (f ()); + Condition.signal promise.fulfilled; + Mutex.unlock promise.mutex; done let init () = - let d1_continue = Atomic.make true in - let d2_continue = Atomic.make true in - let d1_commands = Chan.make_bounded 1 in - let d2_commands = Chan.make_bounded 1 in - { d1 = Domain.spawn (fun () -> domain_fun d1_continue d1_commands); - d2 = Domain.spawn (fun () -> domain_fun d2_continue d2_commands); - d1_commands; - d2_commands; - d1_continue; - d2_continue; + let done_ = Atomic.make false in + let task1 = + { task = None; + task_mutex = Mutex.create (); + new_task = Condition.create (); + promise_mutex = Mutex.create (); + promise_fulfilled = Condition.create (); + } + and task2 = + { task = None; + task_mutex = Mutex.create (); + new_task = Condition.create (); + promise_mutex = Mutex.create (); + promise_fulfilled = Condition.create (); + } + in + { task1; + task2; + done_; + d1 = Domain.spawn (fun () -> domain_fun done_ task1); + d2 = Domain.spawn (fun () -> domain_fun done_ task2); } let takedown pair = - Atomic.set pair.d1_continue false; - Atomic.set pair.d2_continue false; + Atomic.set pair.done_ true; Domain.join pair.d1; Domain.join pair.d2 diff --git a/src/atomic/lin_internal_tests.ml b/src/atomic/lin_internal_tests.ml index 6fa6aa81e..b71bf5e90 100644 --- a/src/atomic/lin_internal_tests.ml +++ b/src/atomic/lin_internal_tests.ml @@ -189,7 +189,9 @@ end module A3T_domain = Lin_domain.Make_internal(A3Conf) [@alert "-internal"] ;; +let () = + Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main [ - AT_domain.lin_test ~count:1000 ~name:"Lin.Internal Atomic test with Domain"; - A3T_domain.lin_test ~count:1000 ~name:"Lin.Internal Atomic3 test with Domain"; -] + AT_domain.lin_test ~pool ~count:1000 ~name:"Lin.Internal Atomic test with Domain"; + A3T_domain.lin_test ~pool ~count:1000 ~name:"Lin.Internal Atomic3 test with Domain"; +]) From 6a8302115e502ce4bf16b4ba17926044e3b699a9 Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Thu, 2 May 2024 00:27:40 +0200 Subject: [PATCH 06/12] Reuse domains only for intra-test repetitions --- lib/STM_domain.ml | 20 ++++++++++++-------- lib/STM_domain.mli | 8 ++++---- lib/lin.ml | 15 +++++++++++++++ lib/lin.mli | 2 ++ lib/lin_domain.ml | 12 ++++++------ lib/lin_domain.mli | 12 ++++++------ lib/util.ml | 24 ++++++++++++++++-------- src/array/dune | 2 +- src/array/lin_internal_tests.ml | 6 ++---- src/array/lin_tests.ml | 8 +++----- src/array/stm_tests.ml | 7 ++----- src/atomic/lin_internal_tests.ml | 8 +++----- src/domain/stm_tests_dls.ml | 3 ++- 13 files changed, 74 insertions(+), 53 deletions(-) diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index ea8f058ef..9b622679e 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -62,43 +62,47 @@ module Make (Spec: Spec) = struct (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) (pref_obs,parent_obs,child_obs) - let agree_test_par ~pool ~count ~name = + let agree_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 -> + Util.Domain_pair.run (fun pool -> assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) - let neg_agree_test_par ~pool ~count ~name = + let neg_agree_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_neg ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> + Util.Domain_pair.run (fun pool -> assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) - let agree_test_par_asym ~pool ~count ~name = + let agree_test_par_asym ~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 -> + Util.Domain_pair.run (fun pool -> assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par_asym ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) - let neg_agree_test_par_asym ~pool ~count ~name = + let neg_agree_test_par_asym ~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_neg ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> + Util.Domain_pair.run (fun pool -> assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par_asym ~pool) triple) (* 25 times each, then 25 * 10 times when shrinking *) + repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) end diff --git a/lib/STM_domain.mli b/lib/STM_domain.mli index ced5a8150..68924e4aa 100644 --- a/lib/STM_domain.mli +++ b/lib/STM_domain.mli @@ -58,21 +58,21 @@ module Make : functor (Spec : STM.Spec) -> @return [true] if there exists a sequential interleaving of the results which agrees with a model interpretation. *) - val agree_test_par : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val agree_test_par : count:int -> name:string -> QCheck.Test.t (** Parallel agreement 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. *) - val neg_agree_test_par : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t (** A negative parallel agreement test (for convenience). Accepts two labeled parameters: [count] is the number of test iterations and [name] is the printed test name. *) - val agree_test_par_asym : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val agree_test_par_asym : count:int -> name:string -> QCheck.Test.t (** Asymmetric parallel agreement test based on {!Stdlib.Domain} and {!agree_prop_par_asym} which combines [repeat] and [~retries]. Accepts two labeled parameters: [count] is the number of test iterations and [name] is the printed test name. *) - val neg_agree_test_par_asym : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val neg_agree_test_par_asym : count:int -> name:string -> QCheck.Test.t (** 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. *) diff --git a/lib/lin.ml b/lib/lin.ml index 8751100fe..16b9c8b1a 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -127,11 +127,26 @@ struct Test.make ~count ~retries ~name arb_cmd_triple (repeat rep_count lin_prop) + (* Linearization test *) + let lin_test_with_special_fun ~rep_count ~retries ~count ~name ~lin_prop ~run_fn = + let arb_cmd_triple = arb_cmds_triple 20 12 in + Test.make ~count ~retries ~name + arb_cmd_triple + (fun input -> + run_fn (fun v -> repeat rep_count (lin_prop v) input)) + (* Negative linearization test *) let neg_lin_test ~rep_count ~retries ~count ~name ~lin_prop = let arb_cmd_triple = arb_cmds_triple 20 12 in Test.make_neg ~count ~retries ~name arb_cmd_triple (repeat rep_count lin_prop) + + let neg_lin_test_with_special_fun ~rep_count ~retries ~count ~name ~lin_prop ~run_fn = + let arb_cmd_triple = arb_cmds_triple 20 12 in + Test.make_neg ~count ~retries ~name + arb_cmd_triple + (fun input -> + run_fn (fun v -> repeat rep_count (lin_prop v) input)) end end diff --git a/lib/lin.mli b/lib/lin.mli index a22288116..20f0bcf55 100644 --- a/lib/lin.mli +++ b/lib/lin.mli @@ -50,6 +50,8 @@ module Internal : sig val interp_plain : Spec.t -> Spec.cmd list -> (Spec.cmd * Spec.res) list val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t + val lin_test_with_special_fun : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:('a -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> run_fn:(('a -> bool) -> bool) -> QCheck.Test.t + val neg_lin_test_with_special_fun : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:('a -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> run_fn:(('a -> bool) -> bool) -> QCheck.Test.t end end [@@alert internal "This module is exposed for internal uses only, its API may change at any time"] diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 4e5e74e71..402d8285c 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -39,14 +39,14 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct let _ = run_parallel ~pool (seq_pref,cmds1,cmds2) in true - let lin_test ~pool ~count ~name = - M.lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(lin_prop ~pool) + let lin_test ~count ~name = + M.lin_test_with_special_fun ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(fun pool -> lin_prop ~pool) ~run_fn:Util.Domain_pair.run - let neg_lin_test ~pool ~count ~name = - neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(lin_prop ~pool) + let neg_lin_test ~count ~name = + M.neg_lin_test_with_special_fun ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(fun pool -> lin_prop ~pool) ~run_fn:Util.Domain_pair.run - let stress_test ~pool ~count ~name = - M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(stress_prop ~pool) + let stress_test ~count ~name = + M.lin_test_with_special_fun ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(fun pool -> stress_prop ~pool) ~run_fn:Util.Domain_pair.run end module Make (Spec : Spec) = Make_internal(MakeCmd(Spec)) diff --git a/lib/lin_domain.mli b/lib/lin_domain.mli index eb9701519..f08da4cad 100644 --- a/lib/lin_domain.mli +++ b/lib/lin_domain.mli @@ -11,31 +11,31 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig val stress_prop : pool:Util.Domain_pair.t -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool - val lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val lin_test : count:int -> name:string -> QCheck.Test.t - val neg_lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val neg_lin_test : count:int -> name:string -> QCheck.Test.t - val stress_test : pool:Util.Domain_pair.t -> 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"] (** functor to build a module for parallel testing *) module Make (Spec : Spec) : sig - val lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val lin_test : count:int -> name:string -> QCheck.Test.t (** [lin_test ~count:c ~name:n] builds a parallel test with the name [n] that iterates [c] times. The test fails if one of the generated programs is not sequentially consistent. In that case it fails, and prints a reduced counter example. *) - val neg_lin_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + val neg_lin_test : count:int -> name:string -> QCheck.Test.t (** [neg_lin_test ~count:c ~name:n] builds a negative parallel test with the name [n] that iterates [c] times. The test fails if no counter example is found, and succeeds if a counter example is indeed found, and prints it afterwards. *) - val stress_test : pool:Util.Domain_pair.t -> count:int -> name:string -> QCheck.Test.t + 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 diff --git a/lib/util.ml b/lib/util.ml index b1d89a437..59e40d724 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -378,16 +378,18 @@ module Domain_pair = struct let domain_fun done_ runner = while not (Atomic.get done_) do Mutex.lock runner.task_mutex; - while Option.is_none runner.task do + while Option.is_none runner.task && not (Atomic.get done_) do Condition.wait runner.new_task runner.task_mutex done; - let Task (f, promise) = Option.get runner.task in - runner.task <- None; - Mutex.unlock runner.task_mutex; - Mutex.lock promise.mutex; - promise.result <- Some (f ()); - Condition.signal promise.fulfilled; - Mutex.unlock promise.mutex; + if not (Atomic.get done_) then ( + let Task (f, promise) = Option.get runner.task in + runner.task <- None; + Mutex.unlock runner.task_mutex; + Mutex.lock promise.mutex; + promise.result <- Some (f ()); + Condition.signal promise.fulfilled; + Mutex.unlock promise.mutex; + ) done let init () = @@ -416,6 +418,12 @@ module Domain_pair = struct let takedown pair = Atomic.set pair.done_ true; + Mutex.lock pair.task1.task_mutex; + Condition.signal pair.task1.new_task; + Mutex.unlock pair.task1.task_mutex; + Mutex.lock pair.task2.task_mutex; + Condition.signal pair.task2.new_task; + Mutex.unlock pair.task2.task_mutex; Domain.join pair.d1; Domain.join pair.d2 diff --git a/src/array/dune b/src/array/dune index 2d3b03e96..c69df6358 100644 --- a/src/array/dune +++ b/src/array/dune @@ -22,6 +22,6 @@ (name lin_tests) (modules lin_tests) (package multicoretests) - (libraries qcheck-lin.domain domainslib) + (libraries qcheck-lin.domain) (action (run %{test} --verbose)) ) diff --git a/src/array/lin_internal_tests.ml b/src/array/lin_internal_tests.ml index f9bca21dc..6b992eeb2 100644 --- a/src/array/lin_internal_tests.ml +++ b/src/array/lin_internal_tests.ml @@ -117,8 +117,6 @@ end module AT_domain = Lin_domain.Make_internal(AConf) [@alert "-internal"] ;; -let () = - Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main [ - AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin.Internal Array test with Domain"; -]) + AT_domain.neg_lin_test ~count:1000 ~name:"Lin.Internal Array test with Domain"; +] diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml index 589b070c2..e52d01d34 100644 --- a/src/array/lin_tests.ml +++ b/src/array/lin_tests.ml @@ -28,9 +28,7 @@ end module AT_domain = Lin_domain.Make(AConf) ;; -let () = - Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main [ - AT_domain.neg_lin_test ~pool ~count:1000 ~name:"Lin Array test with Domain"; - AT_domain.stress_test ~pool ~count:1000 ~name:"Lin Array stress test with Domain"; -]) + 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/array/stm_tests.ml b/src/array/stm_tests.ml index bab9680d7..2e0124386 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -162,11 +162,8 @@ end module ArraySTM_seq = STM_sequential.Make(AConf) module ArraySTM_dom = STM_domain.Make(AConf) ;; -let () = - Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main (let count = 1000 in [ArraySTM_seq.agree_test ~count ~name:"STM Array test sequential"; - ArraySTM_dom.neg_agree_test_par ~pool ~count ~name:"STM Array test parallel"; (* this test is expected to fail *) - (*ArraySTM_dom.stress_test_par ~pool ~count ~name:"STM Array stress test" (* Test for absence of crashes *)*) - ])) + ArraySTM_dom.neg_agree_test_par ~count ~name:"STM Array test parallel" (* this test is expected to fail *) +]) diff --git a/src/atomic/lin_internal_tests.ml b/src/atomic/lin_internal_tests.ml index b71bf5e90..6fa6aa81e 100644 --- a/src/atomic/lin_internal_tests.ml +++ b/src/atomic/lin_internal_tests.ml @@ -189,9 +189,7 @@ end module A3T_domain = Lin_domain.Make_internal(A3Conf) [@alert "-internal"] ;; -let () = - Util.Domain_pair.run (fun pool -> QCheck_base_runner.run_tests_main [ - AT_domain.lin_test ~pool ~count:1000 ~name:"Lin.Internal Atomic test with Domain"; - A3T_domain.lin_test ~pool ~count:1000 ~name:"Lin.Internal Atomic3 test with Domain"; -]) + AT_domain.lin_test ~count:1000 ~name:"Lin.Internal Atomic test with Domain"; + A3T_domain.lin_test ~count:1000 ~name:"Lin.Internal Atomic3 test with Domain"; +] diff --git a/src/domain/stm_tests_dls.ml b/src/domain/stm_tests_dls.ml index 6fe5de365..b0fdfded1 100644 --- a/src/domain/stm_tests_dls.ml +++ b/src/domain/stm_tests_dls.ml @@ -73,8 +73,9 @@ let neg_agree_test_par ~count ~name = Test.make_neg ~retries:10 ~count ~name (DLS_STM_dom.arb_cmds_triple seq_len par_len) (fun triple -> + Util.Domain_pair.run (fun pool -> assume (DLS_STM_dom.all_interleavings_ok triple); - agree_prop_par triple) (* just repeat 1 * 10 times when shrinking *) + agree_prop_par ~pool triple)) (* just repeat 1 * 10 times when shrinking *) ;; QCheck_base_runner.run_tests_main [ agree_test ~count:1000 ~name:"STM Domain.DLS test sequential"; From 9b0eeb54c29dbe9c7a49b4cad82cc64f76ad82f9 Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Thu, 2 May 2024 00:33:46 +0200 Subject: [PATCH 07/12] Remove dependency to Domainslib --- dune-project | 6 ++---- lib/dune | 2 +- lib/util.ml | 2 -- qcheck-lin.opam | 1 - qcheck-stm.opam | 1 - 5 files changed, 3 insertions(+), 9 deletions(-) diff --git a/dune-project b/dune-project index 847cdd0fc..e36f949f6 100644 --- a/dune-project +++ b/dune-project @@ -32,8 +32,7 @@ sequential and parallel tests against a declarative model.") (depends (ocaml (>= 4.12)) (qcheck-core (>= "0.20")) - (qcheck-multicoretests-util (= :version)) - (domainslib (>= 0.5.1)))) + (qcheck-multicoretests-util (= :version)))) (package (name qcheck-lin) @@ -48,8 +47,7 @@ and explained by some sequential interleaving.") (depends (ocaml (>= 4.12)) (qcheck-core (>= "0.20")) - (qcheck-multicoretests-util (= :version)) - (domainslib (>= 0.5.1)))) + (qcheck-multicoretests-util (= :version)))) (package (name qcheck-multicoretests-util) diff --git a/lib/dune b/lib/dune index af63ad9d3..5d8dce98d 100644 --- a/lib/dune +++ b/lib/dune @@ -53,4 +53,4 @@ (name util) (public_name qcheck-multicoretests-util) (modules util) - (libraries qcheck-core.runner unix domainslib)) + (libraries qcheck-core.runner unix)) diff --git a/lib/util.ml b/lib/util.ml index 59e40d724..43e321de6 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -322,8 +322,6 @@ module Equal = struct let equal_array eq x y = equal_seq eq (Array.to_seq x) (Array.to_seq y) end -module Chan = Domainslib.Chan - module Domain_pair = struct type 'a promise = { mutable result : 'a option; diff --git a/qcheck-lin.opam b/qcheck-lin.opam index cf77bbee4..365258d85 100644 --- a/qcheck-lin.opam +++ b/qcheck-lin.opam @@ -25,7 +25,6 @@ depends: [ "ocaml" {>= "4.12"} "qcheck-core" {>= "0.20"} "qcheck-multicoretests-util" {= version} - "domainslib" {>= "0.5.1"} "odoc" {with-doc} ] depopts: ["base-domains"] diff --git a/qcheck-stm.opam b/qcheck-stm.opam index b319e7335..6582bfa20 100644 --- a/qcheck-stm.opam +++ b/qcheck-stm.opam @@ -25,7 +25,6 @@ depends: [ "ocaml" {>= "4.12"} "qcheck-core" {>= "0.20"} "qcheck-multicoretests-util" {= version} - "domainslib" {>= "0.5.1"} "odoc" {with-doc} ] depopts: ["base-domains"] From 30e65c2160d715bfe5c6fdb5f4aeb29fc36edf1d Mon Sep 17 00:00:00 2001 From: Olivier Nicole Date: Thu, 2 May 2024 01:00:40 +0200 Subject: [PATCH 08/12] Fix internal tests --- test/cleanup_lin.ml | 2 +- test/cleanup_stm.ml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/test/cleanup_lin.ml b/test/cleanup_lin.ml index 4d425aaf7..457eba44e 100644 --- a/test/cleanup_lin.ml +++ b/test/cleanup_lin.ml @@ -76,7 +76,7 @@ Test.check_exn (RT.arb_cmds_triple seq_len par_len) (fun input -> try - ignore (RT.lin_prop input); + ignore (Util.Domain_pair.run (fun pool -> RT.lin_prop ~pool input)); Atomic.get cleanup_counter = 0 with | RConf.Already_cleaned -> failwith "Already cleaned" diff --git a/test/cleanup_stm.ml b/test/cleanup_stm.ml index 81ef76a83..a7ef3cf30 100644 --- a/test/cleanup_stm.ml +++ b/test/cleanup_stm.ml @@ -89,7 +89,8 @@ for _i=1 to 100 do try Test.check_exn ~rand (Test.make ~count:1000 ~name:"STM ensure cleanup test parallel" - (RT_dom.arb_cmds_triple 20 12) RT_dom.agree_prop_par) (* without retries *) + (RT_dom.arb_cmds_triple 20 12) + (fun triple -> Util.Domain_pair.run (fun pool -> RT_dom.agree_prop_par ~pool triple))) (* without retries *) with _e -> incr i; assert (!status = Some Cleaned); done; assert (!i = 100); From f8956b7d2e354043766fff43618fe86ef4e6f18b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 3 May 2024 13:39:22 +0200 Subject: [PATCH 09/12] Inline Util.Domain_pair.run in STM and catch exception in property --- lib/STM_domain.ml | 24 ++++++++++++++++-------- lib/util.ml | 6 ------ lib/util.mli | 1 - src/domain/stm_tests_dls.ml | 6 ++++-- 4 files changed, 20 insertions(+), 17 deletions(-) diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index 9b622679e..6ebcfdab9 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -69,9 +69,11 @@ module Make (Spec: Spec) = struct Test.make ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - Util.Domain_pair.run (fun pool -> + let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) + Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) let neg_agree_test_par ~count ~name = let rep_count = 25 in @@ -80,9 +82,11 @@ module Make (Spec: Spec) = struct Test.make_neg ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - Util.Domain_pair.run (fun pool -> + let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) + Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) let agree_test_par_asym ~count ~name = let rep_count = 25 in @@ -91,9 +95,11 @@ module Make (Spec: Spec) = struct Test.make ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - Util.Domain_pair.run (fun pool -> + let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) + Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) let neg_agree_test_par_asym ~count ~name = let rep_count = 25 in @@ -102,7 +108,9 @@ module Make (Spec: Spec) = struct Test.make_neg ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - Util.Domain_pair.run (fun pool -> + let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) + Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) end diff --git a/lib/util.ml b/lib/util.ml index 43e321de6..c95c69233 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -424,10 +424,4 @@ module Domain_pair = struct Mutex.unlock pair.task2.task_mutex; Domain.join pair.d1; Domain.join pair.d2 - - let run f = - let pair = init () in - let res = f pair in - takedown pair; - res end diff --git a/lib/util.mli b/lib/util.mli index 1993e197f..a2a70a1c1 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -259,5 +259,4 @@ module Domain_pair : sig val await : 'a promise -> 'a val init : unit -> t val takedown : t -> unit - val run : (t -> 'a) -> 'a end diff --git a/src/domain/stm_tests_dls.ml b/src/domain/stm_tests_dls.ml index b0fdfded1..18a97080e 100644 --- a/src/domain/stm_tests_dls.ml +++ b/src/domain/stm_tests_dls.ml @@ -73,9 +73,11 @@ let neg_agree_test_par ~count ~name = Test.make_neg ~retries:10 ~count ~name (DLS_STM_dom.arb_cmds_triple seq_len par_len) (fun triple -> - Util.Domain_pair.run (fun pool -> + let pool = Util.Domain_pair.init () in assume (DLS_STM_dom.all_interleavings_ok triple); - agree_prop_par ~pool triple)) (* just repeat 1 * 10 times when shrinking *) + Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> agree_prop_par ~pool triple)) (* just repeat 1 * 10 times when shrinking *) ;; QCheck_base_runner.run_tests_main [ agree_test ~count:1000 ~name:"STM Domain.DLS test sequential"; From 19d8644a7f636ab7a49c8e82ab735fdf01772f48 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 3 May 2024 17:02:28 +0200 Subject: [PATCH 10/12] Inline Util.Domain_pair.run in Lin and catch exception in property --- lib/lin.ml | 15 --------------- lib/lin.mli | 2 -- lib/lin_domain.ml | 30 +++++++++++++++++++++++++++--- 3 files changed, 27 insertions(+), 20 deletions(-) diff --git a/lib/lin.ml b/lib/lin.ml index 16b9c8b1a..8751100fe 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -127,26 +127,11 @@ struct Test.make ~count ~retries ~name arb_cmd_triple (repeat rep_count lin_prop) - (* Linearization test *) - let lin_test_with_special_fun ~rep_count ~retries ~count ~name ~lin_prop ~run_fn = - let arb_cmd_triple = arb_cmds_triple 20 12 in - Test.make ~count ~retries ~name - arb_cmd_triple - (fun input -> - run_fn (fun v -> repeat rep_count (lin_prop v) input)) - (* Negative linearization test *) let neg_lin_test ~rep_count ~retries ~count ~name ~lin_prop = let arb_cmd_triple = arb_cmds_triple 20 12 in Test.make_neg ~count ~retries ~name arb_cmd_triple (repeat rep_count lin_prop) - - let neg_lin_test_with_special_fun ~rep_count ~retries ~count ~name ~lin_prop ~run_fn = - let arb_cmd_triple = arb_cmds_triple 20 12 in - Test.make_neg ~count ~retries ~name - arb_cmd_triple - (fun input -> - run_fn (fun v -> repeat rep_count (lin_prop v) input)) end end diff --git a/lib/lin.mli b/lib/lin.mli index 20f0bcf55..a22288116 100644 --- a/lib/lin.mli +++ b/lib/lin.mli @@ -50,8 +50,6 @@ module Internal : sig val interp_plain : Spec.t -> Spec.cmd list -> (Spec.cmd * Spec.res) list val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t - val lin_test_with_special_fun : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:('a -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> run_fn:(('a -> bool) -> bool) -> QCheck.Test.t - val neg_lin_test_with_special_fun : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:('a -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> run_fn:(('a -> bool) -> bool) -> QCheck.Test.t end end [@@alert internal "This module is exposed for internal uses only, its API may change at any time"] diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 402d8285c..6d3a0cf03 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -40,13 +40,37 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct true let lin_test ~count ~name = - M.lin_test_with_special_fun ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(fun pool -> lin_prop ~pool) ~run_fn:Util.Domain_pair.run + let rep_count, retries = 50,3 in + let arb_cmd_triple = arb_cmds_triple 20 12 in + QCheck.Test.make ~count ~retries ~name + arb_cmd_triple + (fun triple -> + let pool = Util.Domain_pair.init () in + Stdlib.Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (lin_prop ~pool) triple)) let neg_lin_test ~count ~name = - M.neg_lin_test_with_special_fun ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:(fun pool -> lin_prop ~pool) ~run_fn:Util.Domain_pair.run + let rep_count, retries = 50,3 in + let arb_cmd_triple = arb_cmds_triple 20 12 in + QCheck.Test.make_neg ~count ~retries ~name + arb_cmd_triple + (fun triple -> + let pool = Util.Domain_pair.init () in + Stdlib.Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (lin_prop ~pool) triple)) let stress_test ~count ~name = - M.lin_test_with_special_fun ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(fun pool -> stress_prop ~pool) ~run_fn:Util.Domain_pair.run + let rep_count, retries = 25,5 in + let arb_cmd_triple = arb_cmds_triple 20 12 in + QCheck.Test.make ~count ~retries ~name + arb_cmd_triple + (fun triple -> + let pool = Util.Domain_pair.init () in + Stdlib.Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> repeat rep_count (stress_prop ~pool) triple)) end module Make (Spec : Spec) = Make_internal(MakeCmd(Spec)) From f49e8137961ee26cae1d1d44b73e01445ccc7b47 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 3 May 2024 17:13:17 +0200 Subject: [PATCH 11/12] update test/cleanup_lin.ml and test/cleanup_stm.ml too --- test/cleanup_lin.ml | 8 +++++--- test/cleanup_stm.ml | 6 +++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/test/cleanup_lin.ml b/test/cleanup_lin.ml index 457eba44e..4e5bc7d56 100644 --- a/test/cleanup_lin.ml +++ b/test/cleanup_lin.ml @@ -75,10 +75,12 @@ Test.check_exn Test.make ~count:1000 ~name:("exactly one-cleanup test") (RT.arb_cmds_triple seq_len par_len) (fun input -> + let pool = Util.Domain_pair.init () in try - ignore (Util.Domain_pair.run (fun pool -> RT.lin_prop ~pool input)); + ignore (RT.lin_prop ~pool input); + Util.Domain_pair.takedown pool; Atomic.get cleanup_counter = 0 with - | RConf.Already_cleaned -> failwith "Already cleaned" - | _ -> Atomic.get cleanup_counter = 0 + | RConf.Already_cleaned -> (Util.Domain_pair.takedown pool; failwith "Already cleaned") + | _ -> (Util.Domain_pair.takedown pool; Atomic.get cleanup_counter = 0) )) diff --git a/test/cleanup_stm.ml b/test/cleanup_stm.ml index a7ef3cf30..3232e1c58 100644 --- a/test/cleanup_stm.ml +++ b/test/cleanup_stm.ml @@ -90,7 +90,11 @@ for _i=1 to 100 do Test.check_exn ~rand (Test.make ~count:1000 ~name:"STM ensure cleanup test parallel" (RT_dom.arb_cmds_triple 20 12) - (fun triple -> Util.Domain_pair.run (fun pool -> RT_dom.agree_prop_par ~pool triple))) (* without retries *) + (fun triple -> + let pool = Util.Domain_pair.init () in + Fun.protect + ~finally:(fun () -> Util.Domain_pair.takedown pool) + (fun () -> RT_dom.agree_prop_par ~pool triple))) (* without retries *) with _e -> incr i; assert (!status = Some Cleaned); done; assert (!i = 100); From 599c67d204fd0576f8eb0dbf487be221a7d85eb1 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 15 May 2024 16:43:22 +0200 Subject: [PATCH 12/12] Check precondition before allocating pool to ensure init-takedown --- lib/STM_domain.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index 6ebcfdab9..d2e258e3d 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -69,8 +69,8 @@ module Make (Spec: Spec) = struct Test.make ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); + let pool = Util.Domain_pair.init () in Fun.protect ~finally:(fun () -> Util.Domain_pair.takedown pool) (fun () -> repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) @@ -82,8 +82,8 @@ module Make (Spec: Spec) = struct Test.make_neg ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); + let pool = Util.Domain_pair.init () in Fun.protect ~finally:(fun () -> Util.Domain_pair.takedown pool) (fun () -> repeat rep_count (agree_prop_par ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) @@ -95,8 +95,8 @@ module Make (Spec: Spec) = struct Test.make ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); + let pool = Util.Domain_pair.init () in Fun.protect ~finally:(fun () -> Util.Domain_pair.takedown pool) (fun () -> repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *) @@ -108,8 +108,8 @@ module Make (Spec: Spec) = struct Test.make_neg ~retries:10 ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> - let pool = Util.Domain_pair.init () in assume (all_interleavings_ok triple); + let pool = Util.Domain_pair.init () in Fun.protect ~finally:(fun () -> Util.Domain_pair.takedown pool) (fun () -> repeat rep_count (agree_prop_par_asym ~pool) triple)) (* 25 times each, then 25 * 10 times when shrinking *)