diff --git a/lib/lin.ml b/lib/lin.ml index c61a5ea91..9d03fba98 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -40,13 +40,17 @@ module Make(Spec : CmdSpec) (*: StmTest *) 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) - (* use a ref to a list given by the parent thread to put the results in as a thread does not - return a value *) - let interp_thread res sut cs = - let cs_arr = Array.of_list cs in - let res_arr = Array.map (fun c -> Thread.yield (); Spec.run c sut) cs_arr in - res := List.combine cs (Array.to_list res_arr) - + (* Note: On purpose we use + - a non-tail-recursive function and + - an (explicit) allocation in the loop body + since both trigger statistically significant more thread issues/interleaving *) + let rec interp_thread sut cs = match cs with + | [] -> [] + | c::cs -> + Thread.yield (); + let res = Spec.run c sut in + (c,res)::interp_thread sut cs + let rec gen_cmds fuel = Gen.(if fuel = 0 then return [] @@ -128,26 +132,35 @@ module Make(Spec : CmdSpec) (*: StmTest *) let lin_prop_thread = (fun (seq_pref, cmds1, cmds2) -> let sut = Spec.init () in - let pref_obs, obs1, obs2 = ref [], ref [], ref [] in - interp_thread pref_obs sut seq_pref; - let th1 = Thread.create (Thread.yield (); interp_thread obs1 sut) cmds1 in - let th2 = Thread.create (interp_thread obs2 sut) cmds2 in - Thread.join th1; Thread.join th2; Spec.cleanup sut; + let obs1, obs2 = ref [], ref [] in + let pref_obs = interp sut seq_pref in + let wait = ref true in + let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := interp_thread sut cmds1) () in + let th2 = Thread.create (fun () -> wait := false; obs2 := interp_thread sut cmds2) () in + Thread.join th1; + Thread.join th2; + Spec.cleanup sut; let seq_sut = Spec.init () in - (* we should be able to reuse [check_seq_cons] *) - let b = check_seq_cons !pref_obs !obs1 !obs2 seq_sut [] in + (* we reuse [check_seq_cons] to linearize and interpret sequentially *) + let b = check_seq_cons pref_obs !obs1 !obs2 seq_sut [] in Spec.cleanup seq_sut; b || Test.fail_reportf " Results incompatible with sequential execution\n\n%s" @@ 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)) - + (pref_obs,!obs1,!obs2)) + (* Linearizability test based on [Domain] *) let lin_test ~count ~name (lib : [ `Domain | `Thread ]) = - let rep_count = 50 in let seq_len,par_len = 20,15 in - let lin_prop = match lib with `Domain -> lin_prop_domain | ` Thread -> lin_prop_thread in - Test.make ~count ~retries:3 ~name:("Linearizable " ^ name) - (arb_cmds_par seq_len par_len) (repeat rep_count lin_prop) + let arb_cmd_triple = arb_cmds_par seq_len par_len in + match lib with + | `Domain -> + let rep_count = 50 in + Test.make ~count ~retries:3 ~name:("Linearizable " ^ name ^ " with Domain") + arb_cmd_triple (repeat rep_count lin_prop_domain) + | `Thread -> + let rep_count = 100 in + Test.make ~count ~retries:10 ~name:("Linearizable " ^ name ^ " with Thread") + arb_cmd_triple (repeat rep_count lin_prop_thread) end diff --git a/src/neg_tests/domain_lin_tests.ml b/src/neg_tests/domain_lin_tests.ml new file mode 100644 index 000000000..16c24af54 --- /dev/null +++ b/src/neg_tests/domain_lin_tests.ml @@ -0,0 +1,13 @@ +open Lin_tests_common + +(** This is a driver of the negative tests over the Domain module *) + +;; +Util.set_ci_printing () +;; +QCheck_runner.run_tests_main + (let count = 1000 in + [RT_int.lin_test `Domain ~count ~name:"ref int test"; + RT_int64.lin_test `Domain ~count ~name:"ref int64 test"; + CLT_int.lin_test `Domain ~count ~name:"CList int test"; + CLT_int64.lin_test `Domain ~count ~name:"CList int64 test"]) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index e5a02aee0..bb89d1744 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -4,7 +4,7 @@ (alias (name default) (package multicoretests) - (deps ref_test.exe conclist_test.exe lin_tests.exe)) + (deps ref_test.exe conclist_test.exe domain_lin_tests.exe thread_lin_tests.exe)) (executable (name ref_test) @@ -50,19 +50,34 @@ ;; Linearizability tests of ref and Clist -(executable - (name lin_tests) - (modules lin_tests) - (flags (:standard -w -27)) +(library + (name lin_tests_common) + (modules lin_tests_common) (libraries qcheck lin CList) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show))) +(executables + (names domain_lin_tests thread_lin_tests) + (modules domain_lin_tests thread_lin_tests) + (flags (:standard -w -27)) + (libraries lin_tests_common)) + +(rule + (alias runtest) + (package multicoretests) + (action + (progn + (with-accepted-exit-codes 1 + (with-stdout-to "domain_lin-output.txt" (run ./domain_lin_tests.exe --no-colors --verbose))) + (cat domain_lin-output.txt) + (run %{bin:check_error_count} "domain_lin_tests" 4 domain_lin-output.txt)))) + (rule (alias runtest) (package multicoretests) (action (progn (with-accepted-exit-codes 1 - (with-stdout-to "lin-output.txt" (run ./lin_tests.exe --no-colors --verbose))) - (cat lin-output.txt) - (run %{bin:check_error_count} "lin_tests" 5 lin-output.txt)))) + (with-stdout-to "thread_lin-output.txt" (run ./thread_lin_tests.exe --no-colors --verbose))) + (cat thread_lin-output.txt) + (run %{bin:check_error_count} "thread_lin_tests" 1 thread_lin-output.txt)))) diff --git a/src/neg_tests/lin_tests.ml b/src/neg_tests/lin_tests_common.ml similarity index 81% rename from src/neg_tests/lin_tests.ml rename to src/neg_tests/lin_tests_common.ml index 048f1a380..8f6602433 100644 --- a/src/neg_tests/lin_tests.ml +++ b/src/neg_tests/lin_tests_common.ml @@ -58,7 +58,7 @@ module RConf_int64 = struct | Add of int' | Incr | Decr [@@deriving qcheck, show { with_path = false }] - and int' = int64 [@gen Gen.ui64] + and int' = int64 [@gen Gen.(map Int64.of_int nat)] type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }] @@ -110,17 +110,3 @@ end module CLT_int = Lin.Make(CLConf (Int)) module CLT_int64 = Lin.Make(CLConf (Int64)) - -;; -Util.set_ci_printing () -;; -QCheck_runner.run_tests_main - (let count = 1000 in - [RT_int.lin_test `Domain ~count ~name:"ref int test with Domains"; - RT_int.lin_test `Thread ~count ~name:"ref int test with Threads"; - RT_int64.lin_test `Domain ~count ~name:"ref int64 test with Domains"; - RT_int64.lin_test `Thread ~count ~name:"ref int64 test with Threads"; - CLT_int.lin_test `Domain ~count ~name:"CList int test with Domains"; - CLT_int.lin_test `Thread ~count ~name:"CList int test with Threads"; - CLT_int64.lin_test `Domain ~count ~name:"CList test64 with Domains"; - CLT_int64.lin_test `Thread ~count ~name:"CList test64 with Threads"]) diff --git a/src/neg_tests/thread_lin_tests.ml b/src/neg_tests/thread_lin_tests.ml new file mode 100644 index 000000000..78232fafd --- /dev/null +++ b/src/neg_tests/thread_lin_tests.ml @@ -0,0 +1,13 @@ +open Lin_tests_common + +(** This is a driver of the negative tests over the Thread module *) + +;; +Util.set_ci_printing () +;; +QCheck_runner.run_tests_main + (let count = 1000 in + [RT_int.lin_test `Thread ~count ~name:"ref int test"; + RT_int64.lin_test `Thread ~count ~name:"ref int64 test"; + CLT_int.lin_test `Thread ~count ~name:"CList int test"; + CLT_int64.lin_test `Thread ~count ~name:"CList int64 test"])