diff --git a/src/domain/dune b/src/domain/dune index 945e18c72..6461e0f07 100644 --- a/src/domain/dune +++ b/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)) +) diff --git a/src/domain/lin_tests_dsl_dls.ml b/src/domain/lin_tests_dsl_dls.ml new file mode 100644 index 000000000..97d4b68f3 --- /dev/null +++ b/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"; +] + 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"; +]