From 9af871f38576274a0942086cda9967fb8e44c8de Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Mon, 10 Nov 2025 15:29:59 +0100 Subject: [PATCH 1/6] Create qcheck-stm.domain_eio. --- lib/STM_domain_eio.ml | 134 +++++++++++++++++++++++++++++++++++++++++ lib/STM_domain_eio.mli | 100 ++++++++++++++++++++++++++++++ lib/dune | 36 +++++++++-- 3 files changed, 264 insertions(+), 6 deletions(-) create mode 100644 lib/STM_domain_eio.ml create mode 100644 lib/STM_domain_eio.mli diff --git a/lib/STM_domain_eio.ml b/lib/STM_domain_eio.ml new file mode 100644 index 000000000..4220f0d8d --- /dev/null +++ b/lib/STM_domain_eio.ml @@ -0,0 +1,134 @@ +open STM + +module MakeExt (Spec: SpecExt) = struct + + open Util + open QCheck + open Internal.Make(Spec) + [@alert "-internal"] + + let check_obs = check_obs + let all_interleavings_ok (seq_pref,cmds1,cmds2) = + all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state + let arb_cmds_triple = arb_cmds_triple + let arb_triple = arb_triple + let arb_triple_asym seq_len par_len arb0 arb1 arb2 = + let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in + set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple + + (* operate over arrays to avoid needless allocation underway *) + let interp_sut_res 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 + List.combine cs (Array.to_list res_arr) + + let run_par ~domain_mgr seq_pref cmds1 cmds2 = + let sut = Spec.init_sut () in + let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in + let barrier = Atomic.make 2 in + let main cmds () = + Eio.Domain_manager.run domain_mgr @@ fun () -> + (Spec.wrap_cmd_seq @@ fun () -> + Atomic.decr barrier; + while Atomic.get barrier <> 0 do () done; + try Ok (interp_sut_res sut cmds) with exn -> Error exn) + in + let obs1, obs2 = + Eio.Fiber.pair (main cmds1) + (main cmds2) 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 + pref_obs, obs1, obs2 + + let agree_prop_par ~domain_mgr (seq_pref,cmds1,cmds2) = + let pref_obs, obs1, obs2 = run_par ~domain_mgr seq_pref cmds1 cmds2 in + check_obs pref_obs obs1 obs2 Spec.init_state + || Test.fail_reportf " Results incompatible with linearized model\n\n%s" + @@ print_triple_vertical ~fig_indent:5 ~res_width:35 + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) + (pref_obs,obs1,obs2) + + let stress_prop_par ~domain_mgr (seq_pref,cmds1,cmds2) = + let _ = run_par ~domain_mgr seq_pref cmds1 cmds2 in + true + + let agree_prop_par_asym ~domain_mgr (seq_pref, cmds1, cmds2) = + let sut = Spec.init_sut () in + let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in + let wait = Atomic.make 2 in + let child_work () = + Eio.Domain_manager.run domain_mgr (fun () -> + Spec.wrap_cmd_seq @@ fun () -> + Atomic.decr wait; + while Atomic.get wait <> 0 do Domain.cpu_relax() done; + try Ok (interp_sut_res sut cmds2) with exn -> Error exn) + in + let parent_work () = + Eio.Domain_manager.run domain_mgr (fun () -> + Spec.wrap_cmd_seq @@ fun () -> + Atomic.decr wait; + while Atomic.get wait <> 0 do Domain.cpu_relax() done; + try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in + let parent_obs, child_obs = Eio.Fiber.pair parent_work child_work 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 + check_obs pref_obs parent_obs child_obs Spec.init_state + || Test.fail_reportf " Results incompatible with linearized model:\n\n%s" + @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) + (pref_obs,parent_obs,child_obs) + + (* Common magic constants *) + let rep_count = 25 (* No. of repetitions of the non-deterministic property *) + let retries = 10 (* Additional factor of repetition during shrinking *) + let seq_len = 20 (* max length of the sequential prefix *) + let par_len = 12 (* max length of the parallel cmd lists *) + + let agree_test_par ~domain_mgr ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let stress_test_par ~domain_mgr ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (stress_prop_par ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let neg_agree_test_par ~domain_mgr ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make_neg ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let agree_test_par_asym ~domain_mgr ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par_asym ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let neg_agree_test_par_asym ~domain_mgr ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make_neg ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par_asym ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) +end + +module Make (Spec: Spec) = + MakeExt (struct + include SpecDefaults + include Spec + end) diff --git a/lib/STM_domain_eio.mli b/lib/STM_domain_eio.mli new file mode 100644 index 000000000..16725d26c --- /dev/null +++ b/lib/STM_domain_eio.mli @@ -0,0 +1,100 @@ + +module Make : functor (Spec : STM.Spec) -> + sig + val check_obs : (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> Spec.state -> bool + (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref] + and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *) + + val all_interleavings_ok : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + (** [all_interleavings_ok (seq,spawn0,spawn1)] checks that + preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the + possible interleavings and starting with {!Spec.init_state}. + [all_interleavings_ok] catches and ignores exceptions arising from + {!next_state}. *) + + val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary + (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len] + sequential commands and at most [par_len] parallel commands each. + All [cmds] are generated with {!Spec.arb_cmd}. + [arb_cmds_triple] catches and ignores generation-time exceptions arising + from {!Spec.next_state}. *) + + val arb_triple : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary + (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len] + sequential commands and at most [par_len] parallel commands each. + The three {!Spec.cmd} components are generated with [arb0], [arb1], and [arb2], respectively. + Each of these take the model state as a parameter. + [arb_triple] catches and ignores generation-time exceptions arising + from {!Spec.next_state}. *) + + val arb_triple_asym : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary + (** [arb_triple_asym seq_len par_len arb0 arb1 arb2] creates a triple [cmd] + generator like {!arb_triple}. It differs in that the resulting printer + is asymmetric, printing [arb1]'s result below [arb0]'s result and + printing [arb2]'s result to the right of [arb1]'s result. + [arb_triple_asym] catches and ignores generation-time exceptions arising + from {!Spec.next_state}. *) + + val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list + (** [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 stress_prop_par : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + (** Parallel stress testing property based on {!Stdlib.Domain}. + [stress_prop_par (seq_pref, tl1, tl2)] first interprets [seq_pref] + and then spawns two parallel, symmetric domains interpreting [tl1] and + [tl2] simultaneously. In contrast to {!agree_prop_par}, [stress_prop_par] + does not perform an interleaving search. + + @return [true] if no unexpected exceptions or crashes are encountered. *) + + val agree_prop_par : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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 + [tl2] simultaneously. + + @return [true] if there exists a sequential interleaving of the results + which agrees with a model interpretation. *) + + val agree_prop_par_asym : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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] + in parallel with the parent domain. + + @return [true] if there exists a sequential interleaving of the results + which agrees with a model interpretation. *) + + val agree_test_par : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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 : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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 : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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 : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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. *) + + val stress_test_par : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> count:int -> name:string -> QCheck.Test.t + (** Parallel stress test based on {!Stdlib.Domain} which combines [repeat] and [~retries]. + Accepts two labeled parameters: + [count] is the number of test iterations and [name] is the printed test name. + The test fails if an unexpected exception is raised underway. It is + intended as a stress test to run operations at a high frequency and + detect unexpected exceptions or crashes. It does not perform an + interleaving search like {!agree_test_par} and {!neg_agree_test_par}. *) + + end + +module MakeExt : functor (Spec : STM.SpecExt) -> + module type of Make (Spec) diff --git a/lib/dune b/lib/dune index 5d8dce98d..227e27e81 100644 --- a/lib/dune +++ b/lib/dune @@ -14,9 +14,18 @@ (name STM_domain) (public_name qcheck-stm.domain) (modules STM_domain) - (enabled_if (>= %{ocaml_version} 5)) + (enabled_if + (>= %{ocaml_version} 5)) (libraries qcheck-core qcheck-stm.stm)) +(library + (name STM_domain_eio) + (public_name qcheck-stm.domain_eio) + (modules STM_domain_eio) + (enabled_if + (>= %{ocaml_version} 5)) + (libraries qcheck-core qcheck-stm.stm eio)) + (library (name STM_thread) (public_name qcheck-stm.thread) @@ -33,21 +42,36 @@ (name lin_domain) (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)) + (enabled_if + (>= %{ocaml_version} 5)) + (libraries + qcheck-core + qcheck-core.runner + qcheck-multicoretests-util + qcheck-lin.lin)) (library (name lin_effect) (public_name qcheck-lin.effect) (modules lin_effect) - (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin)) + (enabled_if + (>= %{ocaml_version} 5)) + (libraries + qcheck-core + qcheck-core.runner + qcheck-multicoretests-util + qcheck-lin.lin)) (library (name lin_thread) (public_name qcheck-lin.thread) (modules lin_thread) - (libraries threads qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin)) + (libraries + threads + qcheck-core + qcheck-core.runner + qcheck-multicoretests-util + qcheck-lin.lin)) (library (name util) From 6dc52b7b51215888f57147e7954cc90736ca4f3b Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 6 Jan 2026 21:34:20 +0100 Subject: [PATCH 2/6] Add missing deps. --- dune-project | 98 ++++++++++++++++++++++++++++++++++--------------- qcheck-stm.opam | 1 + 2 files changed, 70 insertions(+), 29 deletions(-) diff --git a/dune-project b/dune-project index 7643327b0..140e12ad0 100644 --- a/dune-project +++ b/dune-project @@ -1,61 +1,101 @@ (lang dune 3.18) + (name multicoretests) + (generate_opam_files true) -(source (github ocaml-multicore/multicoretests)) +(source + (github ocaml-multicore/multicoretests)) + (authors "Jan Midtgaard" "Olivier Nicole" "Nicolas Osborne" "Samuel Hym") + (maintainers "Jan Midtgaard ") + (license BSD-2-clause) + (version "0.11") + (maintenance_intent "(latest)") (package (name multicoretests) (synopsis "Experimental multicore test suite of OCaml 5.0") (authors "Multiple contributors") - (description "This package contains a collection of randomized QCheck tests to exercise -the multicore run-time of OCaml 5.0.") - (tags ("test" "test suite" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) + (description + "This package contains a collection of randomized QCheck tests to exercise\nthe multicore run-time of OCaml 5.0.") + (tags + ("test" + "test suite" + "property" + "qcheck" + "quickcheck" + "multicore" + "non-determinism")) (depends base-domains - (qcheck-core (>= "0.90")) - (qcheck-lin (= :version)) - (qcheck-stm (= :version)))) + (qcheck-core + (>= "0.90")) + (qcheck-lin + (= :version)) + (qcheck-stm + (= :version)))) (package (name qcheck-stm) - (synopsis "State-machine testing library for sequential and parallel model-based tests") - (description "A state-machine testing library based on QCheck that can generate both -sequential and parallel tests against a declarative model.") - (tags ("test" "property" "qcheck" "quickcheck" "state-machine testing" - "model-based testing" "parallel testing")) + (synopsis + "State-machine testing library for sequential and parallel model-based tests") + (description + "A state-machine testing library based on QCheck that can generate both\nsequential and parallel tests against a declarative model.") + (tags + ("test" + "property" + "qcheck" + "quickcheck" + "state-machine testing" + "model-based testing" + "parallel testing")) (depopts base-domains) (depends - (ocaml (>= 4.12)) - (qcheck-core (>= "0.90")) - (qcheck-multicoretests-util (= :version)))) + (ocaml + (>= 4.12)) + (qcheck-core + (>= "0.90")) + (eio + (>= "1.0")) + (qcheck-multicoretests-util + (= :version)))) (package (name qcheck-lin) (synopsis "A multicore testing library for OCaml") (description - "A testing library based on QCheck to test interface behaviour under parallel -usage. Lin will generate and run random parallel tests and check the observed -behaviour for sequential consistency, that is, whether they can be linearized -and explained by some sequential interleaving.") - (tags ("test" "property" "qcheck" "quickcheck" "parallelism" "sequential consistency")) + "A testing library based on QCheck to test interface behaviour under parallel\nusage. Lin will generate and run random parallel tests and check the observed\nbehaviour for sequential consistency, that is, whether they can be linearized\nand explained by some sequential interleaving.") + (tags + ("test" + "property" + "qcheck" + "quickcheck" + "parallelism" + "sequential consistency")) (depopts base-domains) (depends - (ocaml (>= 4.12)) - (qcheck-core (>= "0.90")) - (qcheck-multicoretests-util (= :version)))) + (ocaml + (>= 4.12)) + (qcheck-core + (>= "0.90")) + (qcheck-multicoretests-util + (= :version)))) (package (name qcheck-multicoretests-util) - (synopsis "Various utility functions for property-based testing of multicore programs") - (description "A small library of utility functions for QCheck-based testing of -multicore programs.") - (tags ("test" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) + (synopsis + "Various utility functions for property-based testing of multicore programs") + (description + "A small library of utility functions for QCheck-based testing of\nmulticore programs.") + (tags + ("test" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) (depends - (ocaml (>= 4.12)) - (qcheck-core (>= "0.90")))) + (ocaml + (>= 4.12)) + (qcheck-core + (>= "0.90")))) diff --git a/qcheck-stm.opam b/qcheck-stm.opam index ffbff6ae0..18d87d68a 100644 --- a/qcheck-stm.opam +++ b/qcheck-stm.opam @@ -24,6 +24,7 @@ depends: [ "dune" {>= "3.18"} "ocaml" {>= "4.12"} "qcheck-core" {>= "0.90"} + "eio" {>= "1.0"} "qcheck-multicoretests-util" {= version} "odoc" {with-doc} ] From 4be7b25ccad939b7eadef5c90a638eab8cea34af Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 19 Feb 2026 18:46:20 +0100 Subject: [PATCH 3/6] Factorize code between STM_domain and STM_domain_eio to minimize code duplication. --- lib/STM_domain.ml | 143 ++++++-------------------------------- lib/STM_domain_common.ml | 129 +++++++++++++++++++++++++++++++++++ lib/STM_domain_eio.ml | 144 ++++++--------------------------------- lib/STM_domain_eio.mli | 2 + lib/dune | 12 +++- 5 files changed, 179 insertions(+), 251 deletions(-) create mode 100644 lib/STM_domain_common.ml diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index 8c148a259..ca16517af 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -1,132 +1,27 @@ open STM -module MakeExt (Spec: SpecExt) = struct - - open Util - open QCheck - open Internal.Make(Spec) - [@alert "-internal"] - - let check_obs = check_obs - let all_interleavings_ok (seq_pref,cmds1,cmds2) = - all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state - let arb_cmds_triple = arb_cmds_triple - let arb_triple = arb_triple - let arb_triple_asym seq_len par_len arb0 arb1 arb2 = - let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in - set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple - - (* operate over arrays to avoid needless allocation underway *) - let interp_sut_res 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 - List.combine cs (Array.to_list res_arr) - - let run_par seq_pref cmds1 cmds2 = - let sut = Spec.init_sut () in - let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in - let barrier = Atomic.make 2 in - let main cmds () = - Spec.wrap_cmd_seq @@ fun () -> - Atomic.decr barrier; - while Atomic.get barrier <> 0 do Domain.cpu_relax() done; - try Ok (interp_sut_res sut cmds) with exn -> Error exn - in - let dom1 = Domain.spawn (main cmds1) in - let dom2 = Domain.spawn (main cmds2) in - let obs1 = Domain.join dom1 in - let obs2 = Domain.join 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 - pref_obs, obs1, obs2 - - let agree_prop_par (seq_pref,cmds1,cmds2) = - let pref_obs, obs1, obs2 = run_par seq_pref cmds1 cmds2 in - check_obs pref_obs obs1 obs2 Spec.init_state - || Test.fail_reportf " Results incompatible with linearized model\n\n%s" - @@ print_triple_vertical ~fig_indent:5 ~res_width:35 - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) - (pref_obs,obs1,obs2) - - let stress_prop_par (seq_pref,cmds1,cmds2) = - let _ = run_par seq_pref cmds1 cmds2 in - true - - let agree_prop_par_asym (seq_pref, cmds1, cmds2) = - let sut = Spec.init_sut () in - let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in - let wait = Atomic.make 2 in - let child_dom = - Domain.spawn (fun () -> - Spec.wrap_cmd_seq @@ fun () -> - Atomic.decr wait; - while Atomic.get wait <> 0 do Domain.cpu_relax() done; - try Ok (interp_sut_res sut cmds2) with exn -> Error exn) - in - let parent_obs = - Spec.wrap_cmd_seq @@ fun () -> - Atomic.decr wait; - while Atomic.get wait <> 0 do Domain.cpu_relax() done; - try Ok (interp_sut_res sut cmds1) with exn -> Error exn in - let child_obs = Domain.join 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 - check_obs pref_obs parent_obs child_obs Spec.init_state - || Test.fail_reportf " Results incompatible with linearized model:\n\n%s" - @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) - (pref_obs,parent_obs,child_obs) - - (* Common magic constants *) - let rep_count = 25 (* No. of repetitions of the non-deterministic property *) - let retries = 10 (* Additional factor of repetition during shrinking *) - let seq_len = 20 (* max length of the sequential prefix *) - let par_len = 12 (* max length of the parallel cmd lists *) - - let agree_test_par ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries ~max_gen ~count ~name - (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 *) - - let stress_test_par ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries ~max_gen ~count ~name - (arb_cmds_triple seq_len par_len) - (fun triple -> - assume (all_interleavings_ok triple); - repeat rep_count stress_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *) - - let neg_agree_test_par ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries ~max_gen ~count ~name - (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 *) - - let agree_test_par_asym ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries ~max_gen ~count ~name - (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 *) +module Domain_backend = struct + type context = unit + let spawn_pair () f g = + let d1 = Domain.spawn f in + let d2 = Domain.spawn g in + (Domain.join d1, Domain.join d2) +end - let neg_agree_test_par_asym ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries ~max_gen ~count ~name - (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 *) +module MakeExt (Spec : SpecExt) = struct + module Common = STM_domain_common.MakeExt(Spec)(Domain_backend) + include Common + let agree_prop_par = Common.agree_prop_par ~ctx:() + let stress_prop_par = Common.stress_prop_par ~ctx:() + let agree_prop_par_asym = Common.agree_prop_par_asym ~ctx:() + let agree_test_par = Common.agree_test_par ~ctx:() + let stress_test_par = Common.stress_test_par ~ctx:() + let neg_agree_test_par = Common.neg_agree_test_par ~ctx:() + let agree_test_par_asym = Common.agree_test_par_asym ~ctx:() + let neg_agree_test_par_asym = Common.neg_agree_test_par_asym ~ctx:() end -module Make (Spec: Spec) = +module Make (Spec : Spec) = MakeExt (struct include SpecDefaults include Spec diff --git a/lib/STM_domain_common.ml b/lib/STM_domain_common.ml new file mode 100644 index 000000000..8b482424f --- /dev/null +++ b/lib/STM_domain_common.ml @@ -0,0 +1,129 @@ +open STM + +module type Backend = sig + type context + val spawn_pair : context -> (unit -> 'a) -> (unit -> 'b) -> 'a * 'b +end + +module MakeExt (Spec: SpecExt) (B : Backend) = struct + + open Util + open QCheck + open Internal.Make(Spec) + [@alert "-internal"] + + let check_obs = check_obs + let all_interleavings_ok (seq_pref,cmds1,cmds2) = + all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state + let arb_cmds_triple = arb_cmds_triple + let arb_triple = arb_triple + let arb_triple_asym seq_len par_len arb0 arb1 arb2 = + let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in + set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple + + (* operate over arrays to avoid needless allocation underway *) + let interp_sut_res 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 + List.combine cs (Array.to_list res_arr) + + let run_par ~ctx seq_pref cmds1 cmds2 = + let sut = Spec.init_sut () in + let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in + let barrier = Atomic.make 2 in + let main cmds () = + Spec.wrap_cmd_seq @@ fun () -> + Atomic.decr barrier; + while Atomic.get barrier <> 0 do Domain.cpu_relax() done; + try Ok (interp_sut_res sut cmds) with exn -> Error exn + in + let obs1, obs2 = B.spawn_pair ctx (main cmds1) (main cmds2) 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 + pref_obs, obs1, obs2 + + let agree_prop_par ~ctx (seq_pref,cmds1,cmds2) = + let pref_obs, obs1, obs2 = run_par ~ctx seq_pref cmds1 cmds2 in + check_obs pref_obs obs1 obs2 Spec.init_state + || Test.fail_reportf " Results incompatible with linearized model\n\n%s" + @@ print_triple_vertical ~fig_indent:5 ~res_width:35 + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) + (pref_obs,obs1,obs2) + + let stress_prop_par ~ctx (seq_pref,cmds1,cmds2) = + let _ = run_par ~ctx seq_pref cmds1 cmds2 in + true + + let agree_prop_par_asym ~ctx (seq_pref, cmds1, cmds2) = + let sut = Spec.init_sut () in + let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in + let wait = Atomic.make 2 in + let work cmds () = + Spec.wrap_cmd_seq @@ fun () -> + Atomic.decr wait; + while Atomic.get wait <> 0 do Domain.cpu_relax() done; + try Ok (interp_sut_res sut cmds) with exn -> Error exn + in + let parent_obs, child_obs = B.spawn_pair ctx (work cmds1) (work cmds2) 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 + check_obs pref_obs parent_obs child_obs Spec.init_state + || Test.fail_reportf " Results incompatible with linearized model:\n\n%s" + @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) + (pref_obs,parent_obs,child_obs) + + (* Common magic constants *) + let rep_count = 25 (* No. of repetitions of the non-deterministic property *) + let retries = 10 (* Additional factor of repetition during shrinking *) + let seq_len = 20 (* max length of the sequential prefix *) + let par_len = 12 (* max length of the parallel cmd lists *) + + let agree_test_par ~ctx ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par ~ctx) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let stress_test_par ~ctx ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (stress_prop_par ~ctx) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let neg_agree_test_par ~ctx ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make_neg ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par ~ctx) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let agree_test_par_asym ~ctx ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par_asym ~ctx) triple) (* 25 times each, then 25 * 10 times when shrinking *) + + let neg_agree_test_par_asym ~ctx ~count ~name = + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make_neg ~retries ~max_gen ~count ~name + (arb_cmds_triple seq_len par_len) + (fun triple -> + assume (all_interleavings_ok triple); + repeat rep_count (agree_prop_par_asym ~ctx) triple) (* 25 times each, then 25 * 10 times when shrinking *) +end + +module Make (Spec: Spec) (B : Backend) = + MakeExt (struct + include SpecDefaults + include Spec + end) (B) diff --git a/lib/STM_domain_eio.ml b/lib/STM_domain_eio.ml index 4220f0d8d..d1451b85e 100644 --- a/lib/STM_domain_eio.ml +++ b/lib/STM_domain_eio.ml @@ -1,133 +1,27 @@ open STM -module MakeExt (Spec: SpecExt) = struct - - open Util - open QCheck - open Internal.Make(Spec) - [@alert "-internal"] - - let check_obs = check_obs - let all_interleavings_ok (seq_pref,cmds1,cmds2) = - all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state - let arb_cmds_triple = arb_cmds_triple - let arb_triple = arb_triple - let arb_triple_asym seq_len par_len arb0 arb1 arb2 = - let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in - set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple - - (* operate over arrays to avoid needless allocation underway *) - let interp_sut_res 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 - List.combine cs (Array.to_list res_arr) - - let run_par ~domain_mgr seq_pref cmds1 cmds2 = - let sut = Spec.init_sut () in - let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in - let barrier = Atomic.make 2 in - let main cmds () = - Eio.Domain_manager.run domain_mgr @@ fun () -> - (Spec.wrap_cmd_seq @@ fun () -> - Atomic.decr barrier; - while Atomic.get barrier <> 0 do () done; - try Ok (interp_sut_res sut cmds) with exn -> Error exn) - in - let obs1, obs2 = - Eio.Fiber.pair (main cmds1) - (main cmds2) 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 - pref_obs, obs1, obs2 - - let agree_prop_par ~domain_mgr (seq_pref,cmds1,cmds2) = - let pref_obs, obs1, obs2 = run_par ~domain_mgr seq_pref cmds1 cmds2 in - check_obs pref_obs obs1 obs2 Spec.init_state - || Test.fail_reportf " Results incompatible with linearized model\n\n%s" - @@ print_triple_vertical ~fig_indent:5 ~res_width:35 - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) - (pref_obs,obs1,obs2) - - let stress_prop_par ~domain_mgr (seq_pref,cmds1,cmds2) = - let _ = run_par ~domain_mgr seq_pref cmds1 cmds2 in - true - - let agree_prop_par_asym ~domain_mgr (seq_pref, cmds1, cmds2) = - let sut = Spec.init_sut () in - let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in - let wait = Atomic.make 2 in - let child_work () = - Eio.Domain_manager.run domain_mgr (fun () -> - Spec.wrap_cmd_seq @@ fun () -> - Atomic.decr wait; - while Atomic.get wait <> 0 do Domain.cpu_relax() done; - try Ok (interp_sut_res sut cmds2) with exn -> Error exn) - in - let parent_work () = - Eio.Domain_manager.run domain_mgr (fun () -> - Spec.wrap_cmd_seq @@ fun () -> - Atomic.decr wait; - while Atomic.get wait <> 0 do Domain.cpu_relax() done; - try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in - let parent_obs, child_obs = Eio.Fiber.pair parent_work child_work 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 - check_obs pref_obs parent_obs child_obs Spec.init_state - || Test.fail_reportf " Results incompatible with linearized model:\n\n%s" - @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) - (pref_obs,parent_obs,child_obs) - - (* Common magic constants *) - let rep_count = 25 (* No. of repetitions of the non-deterministic property *) - let retries = 10 (* Additional factor of repetition during shrinking *) - let seq_len = 20 (* max length of the sequential prefix *) - let par_len = 12 (* max length of the parallel cmd lists *) - - let agree_test_par ~domain_mgr ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries ~max_gen ~count ~name - (arb_cmds_triple seq_len par_len) - (fun triple -> - assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) - - let stress_test_par ~domain_mgr ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries ~max_gen ~count ~name - (arb_cmds_triple seq_len par_len) - (fun triple -> - assume (all_interleavings_ok triple); - repeat rep_count (stress_prop_par ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) - - let neg_agree_test_par ~domain_mgr ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries ~max_gen ~count ~name - (arb_cmds_triple seq_len par_len) - (fun triple -> - assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) - - let agree_test_par_asym ~domain_mgr ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries ~max_gen ~count ~name - (arb_cmds_triple seq_len par_len) - (fun triple -> - assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par_asym ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) +module Eio_backend = struct + type context = Dm : [> Eio.Domain_manager.ty ] Eio.Resource.t -> context + let spawn_pair (Dm dm) f g = + Eio.Fiber.pair + (fun () -> Eio.Domain_manager.run dm f) + (fun () -> Eio.Domain_manager.run dm g) +end - let neg_agree_test_par_asym ~domain_mgr ~count ~name = - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries ~max_gen ~count ~name - (arb_cmds_triple seq_len par_len) - (fun triple -> - assume (all_interleavings_ok triple); - repeat rep_count (agree_prop_par_asym ~domain_mgr) triple) (* 25 times each, then 25 * 10 times when shrinking *) +module MakeExt (Spec : SpecExt) = struct + module Common = STM_domain_common.MakeExt(Spec)(Eio_backend) + include Common + let agree_prop_par ~domain_mgr = Common.agree_prop_par ~ctx:(Eio_backend.Dm domain_mgr) + let stress_prop_par ~domain_mgr = Common.stress_prop_par ~ctx:(Eio_backend.Dm domain_mgr) + let agree_prop_par_asym ~domain_mgr = Common.agree_prop_par_asym ~ctx:(Eio_backend.Dm domain_mgr) + let agree_test_par ~domain_mgr = Common.agree_test_par ~ctx:(Eio_backend.Dm domain_mgr) + let stress_test_par ~domain_mgr = Common.stress_test_par ~ctx:(Eio_backend.Dm domain_mgr) + let neg_agree_test_par ~domain_mgr = Common.neg_agree_test_par ~ctx:(Eio_backend.Dm domain_mgr) + let agree_test_par_asym ~domain_mgr = Common.agree_test_par_asym ~ctx:(Eio_backend.Dm domain_mgr) + let neg_agree_test_par_asym ~domain_mgr = Common.neg_agree_test_par_asym ~ctx:(Eio_backend.Dm domain_mgr) end -module Make (Spec: Spec) = +module Make (Spec : Spec) = MakeExt (struct include SpecDefaults include Spec diff --git a/lib/STM_domain_eio.mli b/lib/STM_domain_eio.mli index 16725d26c..fc369e528 100644 --- a/lib/STM_domain_eio.mli +++ b/lib/STM_domain_eio.mli @@ -1,4 +1,6 @@ +(** Module for building parallel STM tests over {!Eio.Domain_manager}s *) + module Make : functor (Spec : STM.Spec) -> sig val check_obs : (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> Spec.state -> bool diff --git a/lib/dune b/lib/dune index 227e27e81..f27d05def 100644 --- a/lib/dune +++ b/lib/dune @@ -10,13 +10,21 @@ (modules STM_sequential) (libraries qcheck-core qcheck-stm.stm)) +(library + (name STM_domain_common) + (public_name qcheck-stm.domain_common) + (modules STM_domain_common) + (enabled_if + (>= %{ocaml_version} 5)) + (libraries qcheck-core qcheck-stm.stm)) + (library (name STM_domain) (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 qcheck-stm.domain_common)) (library (name STM_domain_eio) @@ -24,7 +32,7 @@ (modules STM_domain_eio) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-stm.stm eio)) + (libraries qcheck-core qcheck-stm.stm qcheck-stm.domain_common eio)) (library (name STM_thread) From 2a861de6d416bd6190a530614d6410e6cad926dc Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 19 Feb 2026 18:48:48 +0100 Subject: [PATCH 4/6] Add Lin_domain_eio. --- lib/dune | 29 ++++++++++++++++- lib/lin_domain.ml | 69 +++++++++------------------------------- lib/lin_domain_common.ml | 62 ++++++++++++++++++++++++++++++++++++ lib/lin_domain_eio.ml | 21 ++++++++++++ lib/lin_domain_eio.mli | 36 +++++++++++++++++++++ 5 files changed, 162 insertions(+), 55 deletions(-) create mode 100644 lib/lin_domain_common.ml create mode 100644 lib/lin_domain_eio.ml create mode 100644 lib/lin_domain_eio.mli diff --git a/lib/dune b/lib/dune index f27d05def..f43bbf007 100644 --- a/lib/dune +++ b/lib/dune @@ -46,6 +46,18 @@ (modules lin) (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util)) +(library + (name lin_domain_common) + (public_name qcheck-lin.domain_common) + (modules lin_domain_common) + (enabled_if + (>= %{ocaml_version} 5)) + (libraries + qcheck-core + qcheck-core.runner + qcheck-multicoretests-util + qcheck-lin.lin)) + (library (name lin_domain) (public_name qcheck-lin.domain) @@ -56,7 +68,22 @@ qcheck-core qcheck-core.runner qcheck-multicoretests-util - qcheck-lin.lin)) + qcheck-lin.lin + qcheck-lin.domain_common)) + +(library + (name lin_domain_eio) + (public_name qcheck-lin.domain_eio) + (modules lin_domain_eio) + (enabled_if + (>= %{ocaml_version} 5)) + (libraries + qcheck-core + qcheck-core.runner + qcheck-multicoretests-util + qcheck-lin.lin + qcheck-lin.domain_common + eio)) (library (name lin_effect) diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 03cf33a55..492ebe40e 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -1,60 +1,21 @@ open Lin -module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct - module M = Internal.Make(Spec) [@alert "-internal"] - include M - - (* 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 - List.combine cs (Array.to_list res_arr) - - let run_parallel (seq_pref,cmds1,cmds2) = - let sut = Spec.init () in - let pref_obs = interp sut seq_pref in - let barrier = Atomic.make 2 in - let main cmds () = - Atomic.decr barrier; - while Atomic.get barrier <> 0 do Domain.cpu_relax () done; - try Ok (interp sut cmds) with exn -> Error exn - in - let dom1 = Domain.spawn (main cmds1) in - let dom2 = Domain.spawn (main cmds2) in - let obs1 = Domain.join dom1 in - let obs2 = Domain.join 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 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 - - (* Common magic constants *) - let rep_count = 50 (* No. of repetitions of the non-deterministic property *) - let retries = 3 (* Additional factor of repetition during shrinking *) - - let lin_test ~count ~name = - M.lin_test ~rep_count ~count ~retries ~name ~lin_prop - - let neg_lin_test ~count ~name = - neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop +module Domain_backend = struct + type context = unit + let spawn_pair () f g = + let d1 = Domain.spawn f in + let d2 = Domain.spawn g in + (Domain.join d1, Domain.join d2) +end - let stress_test ~count ~name = (* Note: magic constants differ for this one *) - M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:stress_prop +module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct + module Common = Lin_domain_common.Make_internal(Spec)(Domain_backend) + include Common + let lin_prop = Common.lin_prop ~ctx:() + let stress_prop = Common.stress_prop ~ctx:() + let lin_test = Common.lin_test ~ctx:() + let neg_lin_test = Common.neg_lin_test ~ctx:() + let stress_test = Common.stress_test ~ctx:() end module Make (Spec : Spec) = Make_internal(MakeCmd(Spec)) diff --git a/lib/lin_domain_common.ml b/lib/lin_domain_common.ml new file mode 100644 index 000000000..8afe685c1 --- /dev/null +++ b/lib/lin_domain_common.ml @@ -0,0 +1,62 @@ +open Lin + +module type Backend = sig + type context + val spawn_pair : context -> (unit -> 'a) -> (unit -> 'b) -> 'a * 'b +end + +module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) (B : Backend) = struct + module M = Internal.Make(Spec) [@alert "-internal"] + include M + + (* 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 + List.combine cs (Array.to_list res_arr) + + let run_parallel ~ctx (seq_pref,cmds1,cmds2) = + let sut = Spec.init () in + let pref_obs = interp sut seq_pref in + let barrier = Atomic.make 2 in + let main cmds () = + Atomic.decr barrier; + while Atomic.get barrier <> 0 do Domain.cpu_relax () done; + try Ok (interp sut cmds) with exn -> Error exn + in + let obs1, obs2 = B.spawn_pair ctx (main cmds1) (main cmds2) 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 an Atomic flag *) + let lin_prop ~ctx (seq_pref,cmds1,cmds2) = + let pref_obs,obs1,obs2 = run_parallel ~ctx (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 ~ctx (seq_pref,cmds1,cmds2) = + let _ = run_parallel ~ctx (seq_pref,cmds1,cmds2) in + true + + (* Common magic constants *) + let rep_count = 50 (* No. of repetitions of the non-deterministic property *) + let retries = 3 (* Additional factor of repetition during shrinking *) + + let lin_test ~ctx ~count ~name = + M.lin_test ~rep_count ~count ~retries ~name ~lin_prop:(lin_prop ~ctx) + + let neg_lin_test ~ctx ~count ~name = + neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop:(lin_prop ~ctx) + + let stress_test ~ctx ~count ~name = (* Note: magic constants differ for this one *) + M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:(stress_prop ~ctx) +end + +module Make (Spec : Spec) (B : Backend) = Make_internal(MakeCmd(Spec))(B) diff --git a/lib/lin_domain_eio.ml b/lib/lin_domain_eio.ml new file mode 100644 index 000000000..a1245e530 --- /dev/null +++ b/lib/lin_domain_eio.ml @@ -0,0 +1,21 @@ +open Lin + +module Eio_backend = struct + type context = Dm : [> Eio.Domain_manager.ty ] Eio.Resource.t -> context + let spawn_pair (Dm dm) f g = + Eio.Fiber.pair + (fun () -> Eio.Domain_manager.run dm f) + (fun () -> Eio.Domain_manager.run dm g) +end + +module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct + module Common = Lin_domain_common.Make_internal(Spec)(Eio_backend) + include Common + let lin_prop ~domain_mgr = Common.lin_prop ~ctx:(Eio_backend.Dm domain_mgr) + let stress_prop ~domain_mgr = Common.stress_prop ~ctx:(Eio_backend.Dm domain_mgr) + let lin_test ~domain_mgr = Common.lin_test ~ctx:(Eio_backend.Dm domain_mgr) + let neg_lin_test ~domain_mgr = Common.neg_lin_test ~ctx:(Eio_backend.Dm domain_mgr) + let stress_test ~domain_mgr = Common.stress_test ~ctx:(Eio_backend.Dm domain_mgr) +end + +module Make (Spec : Spec) = Make_internal(MakeCmd(Spec)) diff --git a/lib/lin_domain_eio.mli b/lib/lin_domain_eio.mli new file mode 100644 index 000000000..4df37bc9c --- /dev/null +++ b/lib/lin_domain_eio.mli @@ -0,0 +1,36 @@ +open Lin + +(** Functor to build an internal module representing parallel tests over {!Eio.Domain_manager}s *) +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 : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + val stress_prop : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool + val lin_test : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> count:int -> name:string -> QCheck.Test.t + val neg_lin_test : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> count:int -> name:string -> QCheck.Test.t + val stress_test : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.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 over {!Eio.Domain_manager}s *) +module Make (Spec : Spec) : sig + val lin_test : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> count:int -> name:string -> QCheck.Test.t + (** [lin_test ~domain_mgr ~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 : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> count:int -> name:string -> QCheck.Test.t + (** [neg_lin_test ~domain_mgr ~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 : domain_mgr:[> Eio.Domain_manager.ty ] Eio.Resource.t -> count:int -> name:string -> QCheck.Test.t + (** [stress_test ~domain_mgr ~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 to run operations at a + high frequency and detect unexpected exceptions or crashes. It does not + perform an interleaving search like {!lin_test} and {!neg_lin_test}. *) +end [@@warning "-unused-functor-parameter"] From 252f6d5aefc08cdc7b6131d67ed8166f9e4921f3 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 19 Feb 2026 18:58:40 +0100 Subject: [PATCH 5/6] Replace creating _common libraries by cp the shared files. --- dune-project | 100 +++++++++++++----------------------------- lib/STM_domain_eio.ml | 2 +- lib/dune | 40 ++++++----------- lib/lin_domain_eio.ml | 2 +- qcheck-stm.opam | 2 +- 5 files changed, 47 insertions(+), 99 deletions(-) diff --git a/dune-project b/dune-project index 140e12ad0..4c7818e4c 100644 --- a/dune-project +++ b/dune-project @@ -1,101 +1,63 @@ (lang dune 3.18) - (name multicoretests) - (generate_opam_files true) -(source - (github ocaml-multicore/multicoretests)) - +(source (github ocaml-multicore/multicoretests)) (authors "Jan Midtgaard" "Olivier Nicole" "Nicolas Osborne" "Samuel Hym") - (maintainers "Jan Midtgaard ") - (license BSD-2-clause) - (version "0.11") - (maintenance_intent "(latest)") (package (name multicoretests) (synopsis "Experimental multicore test suite of OCaml 5.0") (authors "Multiple contributors") - (description - "This package contains a collection of randomized QCheck tests to exercise\nthe multicore run-time of OCaml 5.0.") - (tags - ("test" - "test suite" - "property" - "qcheck" - "quickcheck" - "multicore" - "non-determinism")) + (description "This package contains a collection of randomized QCheck tests to exercise +the multicore run-time of OCaml 5.0.") + (tags ("test" "test suite" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) (depends base-domains - (qcheck-core - (>= "0.90")) - (qcheck-lin - (= :version)) - (qcheck-stm - (= :version)))) + (qcheck-core (>= "0.90")) + (qcheck-lin (= :version)) + (qcheck-stm (= :version)))) (package (name qcheck-stm) - (synopsis - "State-machine testing library for sequential and parallel model-based tests") - (description - "A state-machine testing library based on QCheck that can generate both\nsequential and parallel tests against a declarative model.") - (tags - ("test" - "property" - "qcheck" - "quickcheck" - "state-machine testing" - "model-based testing" - "parallel testing")) + (synopsis "State-machine testing library for sequential and parallel model-based tests") + (description "A state-machine testing library based on QCheck that can generate both +sequential and parallel tests against a declarative model.") + (tags ("test" "property" "qcheck" "quickcheck" "state-machine testing" + "model-based testing" "parallel testing")) (depopts base-domains) (depends - (ocaml - (>= 4.12)) - (qcheck-core - (>= "0.90")) - (eio - (>= "1.0")) - (qcheck-multicoretests-util - (= :version)))) + (ocaml (>= 4.12)) + (qcheck-core (>= "0.90")) + (eio (>= "1.0")) + (qcheck-multicoretests-util (= :version)))) (package (name qcheck-lin) (synopsis "A multicore testing library for OCaml") (description - "A testing library based on QCheck to test interface behaviour under parallel\nusage. Lin will generate and run random parallel tests and check the observed\nbehaviour for sequential consistency, that is, whether they can be linearized\nand explained by some sequential interleaving.") - (tags - ("test" - "property" - "qcheck" - "quickcheck" - "parallelism" - "sequential consistency")) + "A testing library based on QCheck to test interface behaviour under parallel +usage. Lin will generate and run random parallel tests and check the observed +behaviour for sequential consistency, that is, whether they can be linearized +and explained by some sequential interleaving.") + (tags ("test" "property" "qcheck" "quickcheck" "parallelism" "sequential consistency")) (depopts base-domains) (depends - (ocaml - (>= 4.12)) - (qcheck-core - (>= "0.90")) - (qcheck-multicoretests-util - (= :version)))) + (ocaml (>= 4.12)) + (qcheck-core (>= "0.90")) + (eio (>= "1.0")) + (qcheck-multicoretests-util (= :version)))) (package (name qcheck-multicoretests-util) - (synopsis - "Various utility functions for property-based testing of multicore programs") - (description - "A small library of utility functions for QCheck-based testing of\nmulticore programs.") - (tags - ("test" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) + (synopsis "Various utility functions for property-based testing of multicore programs") + (description "A small library of utility functions for QCheck-based testing of +multicore programs.") + (tags ("test" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) (depends - (ocaml - (>= 4.12)) - (qcheck-core - (>= "0.90")))) + (ocaml (>= 4.12)) + (qcheck-core (>= "0.90")))) diff --git a/lib/STM_domain_eio.ml b/lib/STM_domain_eio.ml index d1451b85e..2fe177897 100644 --- a/lib/STM_domain_eio.ml +++ b/lib/STM_domain_eio.ml @@ -9,7 +9,7 @@ module Eio_backend = struct end module MakeExt (Spec : SpecExt) = struct - module Common = STM_domain_common.MakeExt(Spec)(Eio_backend) + module Common = STM_domain_common_eio.MakeExt(Spec)(Eio_backend) include Common let agree_prop_par ~domain_mgr = Common.agree_prop_par ~ctx:(Eio_backend.Dm domain_mgr) let stress_prop_par ~domain_mgr = Common.stress_prop_par ~ctx:(Eio_backend.Dm domain_mgr) diff --git a/lib/dune b/lib/dune index f43bbf007..372f853fe 100644 --- a/lib/dune +++ b/lib/dune @@ -10,29 +10,25 @@ (modules STM_sequential) (libraries qcheck-core qcheck-stm.stm)) -(library - (name STM_domain_common) - (public_name qcheck-stm.domain_common) - (modules STM_domain_common) - (enabled_if - (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-stm.stm)) +(rule + (action + (copy STM_domain_common.ml STM_domain_common_eio.ml))) (library (name STM_domain) (public_name qcheck-stm.domain) - (modules STM_domain) + (modules STM_domain STM_domain_common) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-stm.stm qcheck-stm.domain_common)) + (libraries qcheck-core qcheck-stm.stm)) (library (name STM_domain_eio) (public_name qcheck-stm.domain_eio) - (modules STM_domain_eio) + (modules STM_domain_eio STM_domain_common_eio) (enabled_if (>= %{ocaml_version} 5)) - (libraries qcheck-core qcheck-stm.stm qcheck-stm.domain_common eio)) + (libraries qcheck-core qcheck-stm.stm eio)) (library (name STM_thread) @@ -46,35 +42,26 @@ (modules lin) (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util)) -(library - (name lin_domain_common) - (public_name qcheck-lin.domain_common) - (modules lin_domain_common) - (enabled_if - (>= %{ocaml_version} 5)) - (libraries - qcheck-core - qcheck-core.runner - qcheck-multicoretests-util - qcheck-lin.lin)) +(rule + (action + (copy lin_domain_common.ml lin_domain_common_eio.ml))) (library (name lin_domain) (public_name qcheck-lin.domain) - (modules lin_domain) + (modules lin_domain lin_domain_common) (enabled_if (>= %{ocaml_version} 5)) (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util - qcheck-lin.lin - qcheck-lin.domain_common)) + qcheck-lin.lin)) (library (name lin_domain_eio) (public_name qcheck-lin.domain_eio) - (modules lin_domain_eio) + (modules lin_domain_eio lin_domain_common_eio) (enabled_if (>= %{ocaml_version} 5)) (libraries @@ -82,7 +69,6 @@ qcheck-core.runner qcheck-multicoretests-util qcheck-lin.lin - qcheck-lin.domain_common eio)) (library diff --git a/lib/lin_domain_eio.ml b/lib/lin_domain_eio.ml index a1245e530..2f376367d 100644 --- a/lib/lin_domain_eio.ml +++ b/lib/lin_domain_eio.ml @@ -9,7 +9,7 @@ module Eio_backend = struct end module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct - module Common = Lin_domain_common.Make_internal(Spec)(Eio_backend) + module Common = Lin_domain_common_eio.Make_internal(Spec)(Eio_backend) include Common let lin_prop ~domain_mgr = Common.lin_prop ~ctx:(Eio_backend.Dm domain_mgr) let stress_prop ~domain_mgr = Common.stress_prop ~ctx:(Eio_backend.Dm domain_mgr) diff --git a/qcheck-stm.opam b/qcheck-stm.opam index 18d87d68a..f3f40b0c5 100644 --- a/qcheck-stm.opam +++ b/qcheck-stm.opam @@ -24,7 +24,7 @@ depends: [ "dune" {>= "3.18"} "ocaml" {>= "4.12"} "qcheck-core" {>= "0.90"} - "eio" {>= "1.0"} + "eio" {>= "1.0"} "qcheck-multicoretests-util" {= version} "odoc" {with-doc} ] From 4a7ca3b28aa1337e7b9ba06111e118e3305f9664 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 19 Feb 2026 19:35:56 +0100 Subject: [PATCH 6/6] Remove eio from qcheck-lin and qcheck-stm packages and add new packages for eio-specific libraries instead. --- dune-project | 38 ++++++++++++++++++++++++++++++++--- lib/dune | 4 ++-- qcheck-lin-eio.opam | 48 +++++++++++++++++++++++++++++++++++++++++++++ qcheck-stm-eio.opam | 48 +++++++++++++++++++++++++++++++++++++++++++++ qcheck-stm.opam | 1 - 5 files changed, 133 insertions(+), 6 deletions(-) create mode 100644 qcheck-lin-eio.opam create mode 100644 qcheck-stm-eio.opam diff --git a/dune-project b/dune-project index 4c7818e4c..0eb22ee2e 100644 --- a/dune-project +++ b/dune-project @@ -20,7 +20,9 @@ the multicore run-time of OCaml 5.0.") base-domains (qcheck-core (>= "0.90")) (qcheck-lin (= :version)) - (qcheck-stm (= :version)))) + (qcheck-stm (= :version)) + (qcheck-stm-eio (= :version)) + (qcheck-lin-eio (= :version)))) (package (name qcheck-stm) @@ -33,9 +35,23 @@ sequential and parallel tests against a declarative model.") (depends (ocaml (>= 4.12)) (qcheck-core (>= "0.90")) - (eio (>= "1.0")) (qcheck-multicoretests-util (= :version)))) +(package + (name qcheck-stm-eio) + (synopsis "State-machine testing library for sequential and parallel model-based tests") + (description "A state-machine testing library based on QCheck that can generate both +sequential and parallel tests against a declarative model.") + (tags ("test" "property" "qcheck" "quickcheck" "state-machine testing" + "model-based testing" "parallel testing")) + (depopts base-domains) + (depends + (ocaml (>= 4.12)) + (qcheck-core (>= "0.90")) + (eio (>= "1.0")) + (qcheck-multicoretests-util (= :version)) + (qcheck-stm (= :version)))) + (package (name qcheck-lin) (synopsis "A multicore testing library for OCaml") @@ -49,9 +65,25 @@ and explained by some sequential interleaving.") (depends (ocaml (>= 4.12)) (qcheck-core (>= "0.90")) - (eio (>= "1.0")) (qcheck-multicoretests-util (= :version)))) +(package + (name qcheck-lin-eio) + (synopsis "A multicore testing library for OCaml") + (description + "A testing library based on QCheck to test interface behaviour under parallel +usage. Lin will generate and run random parallel tests and check the observed +behaviour for sequential consistency, that is, whether they can be linearized +and explained by some sequential interleaving.") + (tags ("test" "property" "qcheck" "quickcheck" "parallelism" "sequential consistency")) + (depopts base-domains) + (depends + (ocaml (>= 4.12)) + (qcheck-core (>= "0.90")) + (eio (>= "1.0")) + (qcheck-multicoretests-util (= :version)) + (qcheck-lin (= :version)))) + (package (name qcheck-multicoretests-util) (synopsis "Various utility functions for property-based testing of multicore programs") diff --git a/lib/dune b/lib/dune index 372f853fe..affc917ec 100644 --- a/lib/dune +++ b/lib/dune @@ -24,7 +24,7 @@ (library (name STM_domain_eio) - (public_name qcheck-stm.domain_eio) + (public_name qcheck-stm-eio.domain) (modules STM_domain_eio STM_domain_common_eio) (enabled_if (>= %{ocaml_version} 5)) @@ -60,7 +60,7 @@ (library (name lin_domain_eio) - (public_name qcheck-lin.domain_eio) + (public_name qcheck-lin-eio.domain) (modules lin_domain_eio lin_domain_common_eio) (enabled_if (>= %{ocaml_version} 5)) diff --git a/qcheck-lin-eio.opam b/qcheck-lin-eio.opam new file mode 100644 index 000000000..04da3b7d3 --- /dev/null +++ b/qcheck-lin-eio.opam @@ -0,0 +1,48 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.11" +synopsis: "A multicore testing library for OCaml" +description: """ +A testing library based on QCheck to test interface behaviour under parallel +usage. Lin will generate and run random parallel tests and check the observed +behaviour for sequential consistency, that is, whether they can be linearized +and explained by some sequential interleaving.""" +maintainer: ["Jan Midtgaard "] +authors: ["Jan Midtgaard" "Olivier Nicole" "Nicolas Osborne" "Samuel Hym"] +license: "BSD-2-clause" +tags: [ + "test" + "property" + "qcheck" + "quickcheck" + "parallelism" + "sequential consistency" +] +homepage: "https://github.com/ocaml-multicore/multicoretests" +bug-reports: "https://github.com/ocaml-multicore/multicoretests/issues" +depends: [ + "dune" {>= "3.18"} + "ocaml" {>= "4.12"} + "qcheck-core" {>= "0.90"} + "eio" {>= "1.0"} + "qcheck-multicoretests-util" {= version} + "qcheck-lin" {= version} + "odoc" {with-doc} +] +depopts: ["base-domains"] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/ocaml-multicore/multicoretests.git" +x-maintenance-intent: ["(latest)"] diff --git a/qcheck-stm-eio.opam b/qcheck-stm-eio.opam new file mode 100644 index 000000000..a70b6b72b --- /dev/null +++ b/qcheck-stm-eio.opam @@ -0,0 +1,48 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.11" +synopsis: + "State-machine testing library for sequential and parallel model-based tests" +description: """ +A state-machine testing library based on QCheck that can generate both +sequential and parallel tests against a declarative model.""" +maintainer: ["Jan Midtgaard "] +authors: ["Jan Midtgaard" "Olivier Nicole" "Nicolas Osborne" "Samuel Hym"] +license: "BSD-2-clause" +tags: [ + "test" + "property" + "qcheck" + "quickcheck" + "state-machine testing" + "model-based testing" + "parallel testing" +] +homepage: "https://github.com/ocaml-multicore/multicoretests" +bug-reports: "https://github.com/ocaml-multicore/multicoretests/issues" +depends: [ + "dune" {>= "3.18"} + "ocaml" {>= "4.12"} + "qcheck-core" {>= "0.90"} + "eio" {>= "1.0"} + "qcheck-multicoretests-util" {= version} + "qcheck-stm" {= version} + "odoc" {with-doc} +] +depopts: ["base-domains"] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/ocaml-multicore/multicoretests.git" +x-maintenance-intent: ["(latest)"] diff --git a/qcheck-stm.opam b/qcheck-stm.opam index f3f40b0c5..ffbff6ae0 100644 --- a/qcheck-stm.opam +++ b/qcheck-stm.opam @@ -24,7 +24,6 @@ depends: [ "dune" {>= "3.18"} "ocaml" {>= "4.12"} "qcheck-core" {>= "0.90"} - "eio" {>= "1.0"} "qcheck-multicoretests-util" {= version} "odoc" {with-doc} ]