From 092cfe76cefec664cb813ed1c665ab70da589b75 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 7 Sep 2023 12:27:55 +0200
Subject: [PATCH 1/4] Add initial Domain.DLS test

---
 src/domain/dune                 |  8 ++++++++
 src/domain/lin_tests_dsl_dls.ml | 25 +++++++++++++++++++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 src/domain/lin_tests_dsl_dls.ml

diff --git a/src/domain/dune b/src/domain/dune
index 945e18c72..820f3dcec 100644
--- a/src/domain/dune
+++ b/src/domain/dune
@@ -17,3 +17,11 @@
  (libraries util qcheck-core qcheck-core.runner)
  (action (run %{test} --verbose))
 )
+
+(test
+ (name lin_tests_dsl_dls)
+ (modules lin_tests_dsl_dls)
+ (package multicoretests)
+ (libraries qcheck-lin.domain)
+ (action (run %{test} --verbose))
+)
diff --git a/src/domain/lin_tests_dsl_dls.ml b/src/domain/lin_tests_dsl_dls.ml
new file mode 100644
index 000000000..97a56b408
--- /dev/null
+++ b/src/domain/lin_tests_dsl_dls.ml
@@ -0,0 +1,25 @@
+open Domain
+open Lin
+
+module DLSConf = struct
+  type t = int DLS.key
+  let init () = DLS.new_key (fun () -> 0) (* without split from parent *)
+  let cleanup _ = ()
+  let int = int_small
+  let api = [
+    val_ "DLS.get" DLS.get (t @-> returning int) ;
+    val_ "DLS.set" DLS.set (t @-> int @-> returning unit) ;
+  ]
+end
+
+module DLSN = Lin_domain.Make (DLSConf)
+module DLST = Lin_domain.Make (struct
+    include DLSConf
+    let init () = (* get and set will see the parent's key *)
+      DLS.new_key ~split_from_parent:(fun i -> i) (fun () -> 0)
+  end)
+;;
+QCheck_base_runner.run_tests_main [
+  DLSN.neg_lin_test ~count:100 ~name:"Lin DSL Domain.DLS negative test with Domain";
+  DLST.lin_test     ~count:75  ~name:"Lin DSL Domain.DLS test with Domain";
+]

From 7eb9b7877e2cac0081eccdb23ef863b3b4b7fe89 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 8 Sep 2023 11:36:30 +0200
Subject: [PATCH 2/4] Experiment with running test in a child Domain

---
 src/domain/lin_tests_dsl_dls.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/domain/lin_tests_dsl_dls.ml b/src/domain/lin_tests_dsl_dls.ml
index 97a56b408..97d4b68f3 100644
--- a/src/domain/lin_tests_dsl_dls.ml
+++ b/src/domain/lin_tests_dsl_dls.ml
@@ -19,7 +19,16 @@ module DLST = Lin_domain.Make (struct
       DLS.new_key ~split_from_parent:(fun i -> i) (fun () -> 0)
   end)
 ;;
+(*
+let _ =
+  Domain.join (Domain.spawn (fun () -> QCheck_base_runner.run_tests ~verbose:true
+                                [DLSN.neg_lin_test ~count:100 ~name:"Lin DSL Domain.DLS negative test with Domain"]))
+let _ =
+  Domain.join (Domain.spawn (fun () -> QCheck_base_runner.run_tests ~verbose:true
+                                [DLST.lin_test     ~count:75  ~name:"Lin DSL Domain.DLS test with Domain"]))
+*)
 QCheck_base_runner.run_tests_main [
   DLSN.neg_lin_test ~count:100 ~name:"Lin DSL Domain.DLS negative test with Domain";
   DLST.lin_test     ~count:75  ~name:"Lin DSL Domain.DLS test with Domain";
 ]
+

From ef4b42d58bcd2ae776fe2107dd2163f90549f9ea Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 11 Sep 2023 09:44:18 +0200
Subject: [PATCH 3/4] Add an STM test of Domain.DLS

---
 src/domain/dune                 |  8 ++++
 src/domain/stm_tests_dsl_dls.ml | 82 +++++++++++++++++++++++++++++++++
 2 files changed, 90 insertions(+)
 create mode 100644 src/domain/stm_tests_dsl_dls.ml

diff --git a/src/domain/dune b/src/domain/dune
index 820f3dcec..84a9d7ca0 100644
--- a/src/domain/dune
+++ b/src/domain/dune
@@ -25,3 +25,11 @@
  (libraries qcheck-lin.domain)
  (action (run %{test} --verbose))
 )
+
+(test
+ (name stm_tests_dsl_dls)
+ (modules stm_tests_dsl_dls)
+ (package multicoretests)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
+ (action (run %{test} --verbose))
+)
diff --git a/src/domain/stm_tests_dsl_dls.ml b/src/domain/stm_tests_dsl_dls.ml
new file mode 100644
index 000000000..6fe5de365
--- /dev/null
+++ b/src/domain/stm_tests_dsl_dls.ml
@@ -0,0 +1,82 @@
+open Domain
+open QCheck
+open STM
+
+(** parallel STM tests of Domain.DLS *)
+
+module DLSConf =
+struct
+  let length = 4
+
+  type index = int
+  type cmd =
+    | Get of index
+    | Set of index * int
+
+  let pp_cmd par fmt x =
+    let open Util.Pp in
+    match x with
+    | Get i -> cst1 pp_int "Get" par fmt i
+    | Set (i,x) -> cst2 pp_int pp_int "Set" par fmt i x
+
+  let show_cmd = Util.Pp.to_show pp_cmd
+
+  type state = int list
+  type sut   = int Domain.DLS.key list
+
+  let arb_cmd _s =
+    let index = Gen.int_bound (length-1) in
+    let int_gen = Gen.small_nat in
+    QCheck.make ~print:show_cmd
+      Gen.(oneof
+             [ map (fun i -> Get i) index;
+               map2 (fun i x -> Set (i,x)) index int_gen;
+             ])
+
+  let init_state  = List.init length (fun i -> i)
+
+  let next_state n s = match n with
+    | Get _     -> s
+    | Set (i,n) -> List.mapi (fun j x -> if i=j then n else x) s
+
+  let init_sut () = List.init length (fun i -> DLS.new_key ~split_from_parent:(fun x -> x) (fun () -> i))
+
+  let cleanup _   = ()
+
+  let precond n _s = match n with
+    | _ -> true
+
+  let run n t = match n with
+    | Get i     -> Res (STM.int, Domain.DLS.get (List.nth t i))
+    | Set (i,x) -> Res (unit, Domain.DLS.set (List.nth t i) x)
+
+  let postcond n (s:int list) res = match n, res with
+    | Get i, Res ((Int,_), r) -> (List.nth s i) = r
+    | Set _, Res ((Unit,_), ()) -> true
+    | _, _ -> false
+end
+
+module DLS_STM_seq = STM_sequential.Make(DLSConf)
+module DLS_STM_dom = STM_domain.Make(DLSConf)
+
+(* Run seq. property in a child domain to have a clean DLS for each iteration *)
+let agree_prop cs = Domain.spawn (fun () -> DLS_STM_seq.agree_prop cs) |> Domain.join
+
+(* Run domain property in a child domain to have a clean DLS for each iteration *)
+let agree_prop_par t = Domain.spawn (fun () -> DLS_STM_dom.agree_prop_par t) |> Domain.join
+
+let agree_test ~count ~name =
+  Test.make ~name ~count (DLS_STM_seq.arb_cmds DLSConf.init_state) agree_prop
+
+let neg_agree_test_par ~count ~name =
+  let seq_len,par_len = 20,12 in
+  Test.make_neg ~retries:10 ~count ~name
+    (DLS_STM_dom.arb_cmds_triple seq_len par_len)
+    (fun triple ->
+       assume (DLS_STM_dom.all_interleavings_ok triple);
+       agree_prop_par triple) (* just repeat 1 * 10 times when shrinking *)
+;;
+QCheck_base_runner.run_tests_main [
+  agree_test         ~count:1000 ~name:"STM Domain.DLS test sequential";
+  neg_agree_test_par ~count:1000 ~name:"STM Domain.DLS test parallel";
+]

From dd95793226b2d113ef9384a45764769e2921f113 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 11 Sep 2023 15:08:17 +0200
Subject: [PATCH 4/4] Disable the initial Lin DLS test

---
 src/domain/dune | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/domain/dune b/src/domain/dune
index 84a9d7ca0..6461e0f07 100644
--- a/src/domain/dune
+++ b/src/domain/dune
@@ -23,7 +23,8 @@
  (modules lin_tests_dsl_dls)
  (package multicoretests)
  (libraries qcheck-lin.domain)
- (action (run %{test} --verbose))
+ ; (action (run %{test} --verbose))
+ (action (echo "Skipping src/domain/%{test} from the test suite\n\n"))
 )
 
 (test