diff --git a/dune-project b/dune-project
index 7643327b..0eb22ee2 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)
@@ -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")
diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml
index 8c148a25..ca16517a 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 00000000..8b482424
--- /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
new file mode 100644
index 00000000..2fe17789
--- /dev/null
+++ 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)
diff --git a/lib/STM_domain_eio.mli b/lib/STM_domain_eio.mli
new file mode 100644
index 00000000..fc369e52
--- /dev/null
+++ b/lib/STM_domain_eio.mli
@@ -0,0 +1,102 @@
+
+(** 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
+    (** [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 5d8dce98..affc917e 100644
--- a/lib/dune
+++ b/lib/dune
@@ -10,13 +10,26 @@
  (modules STM_sequential)
  (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)
- (enabled_if (>= %{ocaml_version} 5))
+ (modules STM_domain STM_domain_common)
+ (enabled_if
+  (>= %{ocaml_version} 5))
  (libraries qcheck-core qcheck-stm.stm))
 
+(library
+ (name STM_domain_eio)
+ (public_name qcheck-stm-eio.domain)
+ (modules STM_domain_eio STM_domain_common_eio)
+ (enabled_if
+  (>= %{ocaml_version} 5))
+ (libraries qcheck-core qcheck-stm.stm eio))
+
 (library
  (name STM_thread)
  (public_name qcheck-stm.thread)
@@ -29,25 +42,57 @@
  (modules lin)
  (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util))
 
+(rule
+ (action
+  (copy lin_domain_common.ml lin_domain_common_eio.ml)))
+
 (library
  (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))
+ (modules lin_domain lin_domain_common)
+ (enabled_if
+  (>= %{ocaml_version} 5))
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-multicoretests-util
+  qcheck-lin.lin))
+
+(library
+ (name lin_domain_eio)
+ (public_name qcheck-lin-eio.domain)
+ (modules lin_domain_eio lin_domain_common_eio)
+ (enabled_if
+  (>= %{ocaml_version} 5))
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-multicoretests-util
+  qcheck-lin.lin
+  eio))
 
 (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)
diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml
index 03cf33a5..492ebe40 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 00000000..8afe685c
--- /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 00000000..2f376367
--- /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_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)
+  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 00000000..4df37bc9
--- /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"]
diff --git a/qcheck-lin-eio.opam b/qcheck-lin-eio.opam
new file mode 100644
index 00000000..04da3b7d
--- /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 <mail@janmidtgaard.dk>"]
+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 00000000..a70b6b72
--- /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 <mail@janmidtgaard.dk>"]
+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)"]