Add STM_domain_eio and Lin_domain_eio libraries to run multicore tests with Eio

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)
@@ -35,6 +37,21 @@ sequential and parallel tests against a declarative model.")
   (qcheck-core           (>= "0.90"))
   (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")
@@ -50,6 +67,23 @@ and explained by some sequential interleaving.")
   (qcheck-core           (>= "0.90"))
   (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")

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

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)

lib/STM_domain_eio.ml

@@ -0,0 +1,28 @@
+open STM
+
+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 MakeExt (Spec : SpecExt) = struct
+  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)
+  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) =
+  MakeExt (struct
+    include SpecDefaults
+    include Spec
+  end)