diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index 61acba21..8c148a25 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -79,51 +79,47 @@ module MakeExt (Spec: SpecExt) = struct (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 rep_count = 25 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries:10 ~max_gen ~count ~name + 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 rep_count = 25 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries:10 ~max_gen ~count ~name + 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 rep_count = 25 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries:10 ~max_gen ~count ~name + 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 rep_count = 25 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries:10 ~max_gen ~count ~name + 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 *) let neg_agree_test_par_asym ~count ~name = - let rep_count = 25 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries:10 ~max_gen ~count ~name + Test.make_neg ~retries ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun triple -> assume (all_interleavings_ok triple); diff --git a/lib/STM_thread.ml b/lib/STM_thread.ml index 0dbdbca7..8301a701 100644 --- a/lib/STM_thread.ml +++ b/lib/STM_thread.ml @@ -49,22 +49,24 @@ module MakeExt (Spec: SpecExt) = struct (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) (pref_obs,obs1,obs2) + (* Common magic constants *) + let rep_count = 3 (* No. of repetitions of the non-deterministic property *) + let retries = 25 (* 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_conc ~count ~name = (* a bigger [rep_count] for [Threads] as it is more difficult to trigger a problem *) - let rep_count = 3 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries:25 ~max_gen ~count ~name + Test.make ~retries ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun ((seq_pref,cmds1,cmds2) as triple) -> assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *) let neg_agree_test_conc ~count ~name = - let rep_count = 3 in - let seq_len,par_len = 20,12 in let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries:25 ~max_gen ~count ~name + Test.make_neg ~retries ~max_gen ~count ~name (arb_cmds_triple seq_len par_len) (fun ((seq_pref,cmds1,cmds2) as triple) -> assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); diff --git a/lib/lin.ml b/lib/lin.ml index aa68e58c..d80fce64 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -121,15 +121,19 @@ struct then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace) else (Spec.cleanup seq_sut'; false)) + (* Common magic constants *) + let seq_len = 20 (* max length of the sequential prefix *) + let par_len = 12 (* max length of the parallel cmd lists *) + (* Linearization test *) let lin_test ~rep_count ~retries ~count ~name ~lin_prop = - let arb_cmd_triple = arb_cmds_triple 20 12 in + let arb_cmd_triple = arb_cmds_triple seq_len par_len in Test.make ~count ~retries ~name arb_cmd_triple (repeat rep_count lin_prop) (* Negative linearization test *) let neg_lin_test ~rep_count ~retries ~count ~name ~lin_prop = - let arb_cmd_triple = arb_cmds_triple 20 12 in + let arb_cmd_triple = arb_cmds_triple seq_len par_len in Test.make_neg ~count ~retries ~name arb_cmd_triple (repeat rep_count lin_prop) end diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 1feafd82..03cf33a5 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -43,13 +43,17 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct 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:50 ~count ~retries:3 ~name ~lin_prop:lin_prop + M.lin_test ~rep_count ~count ~retries ~name ~lin_prop let neg_lin_test ~count ~name = - neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop + neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop - let stress_test ~count ~name = + 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 end diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml index 1da365de..40c75680 100644 --- a/lib/lin_effect.ml +++ b/lib/lin_effect.ml @@ -112,17 +112,18 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r)) (pref_obs,!obs1,!obs2) + (* Common magic constants *) + 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 lin_test ~count ~name = - let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in - let rep_count = 1 in - QCheck.Test.make ~count ~retries:10 ~name - arb_cmd_triple (Util.repeat rep_count lin_prop) + let arb_cmd_triple = EffTest.arb_cmds_triple seq_len par_len in + QCheck.Test.make ~count ~retries ~name arb_cmd_triple lin_prop let neg_lin_test ~count ~name = - let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in - let rep_count = 1 in - QCheck.Test.make_neg ~count ~retries:10 ~name - arb_cmd_triple (Util.repeat rep_count lin_prop) + let arb_cmd_triple = EffTest.arb_cmds_triple seq_len par_len in + QCheck.Test.make_neg ~count ~retries ~name arb_cmd_triple lin_prop end module Make (Spec : Spec) = Make_internal(MakeCmd(Spec)) diff --git a/lib/lin_thread.ml b/lib/lin_thread.ml index 90c3194d..aefdf66b 100644 --- a/lib/lin_thread.ml +++ b/lib/lin_thread.ml @@ -49,11 +49,15 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r)) (pref_obs,!obs1,!obs2) + (* Common magic constants *) + let rep_count = 3 (* No. of repetitions of the non-deterministic property *) + let retries = 25 (* Additional factor of repetition during shrinking *) + let lin_test ~count ~name = - lin_test ~rep_count:3 ~count ~retries:25 ~name ~lin_prop:lin_prop + lin_test ~rep_count ~count ~retries ~name ~lin_prop let neg_lin_test ~count ~name = - neg_lin_test ~rep_count:3 ~count ~retries:25 ~name ~lin_prop:lin_prop + neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop end module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))