Add Lin Domain.DLS test

src/domain/dune

@@ -17,3 +17,20 @@
  (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))
+ (action (echo "Skipping src/domain/%{test} from the test suite\n\n"))
+)
+
+(test
+ (name stm_tests_dsl_dls)
+ (modules stm_tests_dsl_dls)
+ (package multicoretests)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
+ (action (run %{test} --verbose))
+)

src/domain/lin_tests_dsl_dls.ml

@@ -0,0 +1,34 @@
+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)
+;;
+(*
+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";
+]
+

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";
+]