From da5fc7ecbcf3b66ae64fac07cd0f31dac15a9f19 Mon Sep 17 00:00:00 2001 From: n-osborne Date: Tue, 28 Jun 2022 11:58:12 +0200 Subject: [PATCH] tweek `STM_Thread` tests to trigger bugs and add dune rule for tests --- lib/STM_Thread.ml | 23 ++++++++++++++++------- src/atomic/dune | 2 +- src/domainslib/dune | 4 ++-- src/neg_tests/dune | 24 +++++++++++++++++++++--- 4 files changed, 40 insertions(+), 13 deletions(-) diff --git a/lib/STM_Thread.ml b/lib/STM_Thread.ml index e0f293ba..2dcce65b 100644 --- a/lib/STM_Thread.ml +++ b/lib/STM_Thread.ml @@ -8,7 +8,15 @@ module Make (Spec: Spec) = struct exception ThreadNotFinished - (* Parallel agreement property based on [Threads] *) + (* overwrite [STM_Core.interp_sut_res] for [Threads] *) + let rec interp_sut_res sut cs = match cs with + | [] -> [] + | c::cs -> + Thread.yield (); + let res = Spec.run c sut in + (c,res)::interp_sut_res sut cs + + (* Concurrent agreement property based on [Threads] *) let agree_prop_conc (seq_pref,cmds1,cmds2) = assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); let sut = Spec.init_sut () in @@ -17,11 +25,11 @@ module Make (Spec: Spec) = struct let wait = ref true in let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_sut_res sut cmds1) with exn -> Error exn) () in let th2 = Thread.create (fun () -> wait := false; obs2 := try Ok (interp_sut_res sut cmds2) with exn -> Error exn) () in - let () = Thread.join th1 in - let () = Thread.join th2 in + let () = Thread.join th1 in + let () = Thread.join th2 in + let () = Spec.cleanup sut in let obs1 = match !obs1 with Ok v -> v | Error exn -> raise exn in let obs2 = match !obs2 with Ok v -> v | Error exn -> raise exn in - let () = Spec.cleanup sut in check_obs pref_obs obs1 obs2 Spec.init_state || Test.fail_reportf " Results incompatible with linearized model\n\n%s" @@ print_triple_vertical ~fig_indent:5 ~res_width:35 @@ -29,11 +37,12 @@ module Make (Spec: Spec) = struct (pref_obs,obs1,obs2) let agree_test_conc ~count ~name = - let rep_count = 25 in + (* a bigger [rep_count] for [Threads] as it is more difficult to trigger a problem *) + let rep_count = 100 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:15 ~max_gen ~count ~name:("parallel " ^ name) + Test.make ~retries:15 ~max_gen ~count ~name:("concurrent " ^ name) (arb_cmds_par seq_len par_len) - (repeat rep_count agree_prop_conc) (* 25 times each, then 25 * 15 times when shrinking *) + (repeat rep_count agree_prop_conc) (* 100 times each, then 100 * 15 times when shrinking *) end diff --git a/src/atomic/dune b/src/atomic/dune index 6364eb2a..1b86aa13 100644 --- a/src/atomic/dune +++ b/src/atomic/dune @@ -7,7 +7,7 @@ (deps stm_tests.exe lin_tests.exe)) -;; STM_Seq STM_Domain STM_Thread test of Atomic +;; STM_Seq STM_Domain test of Atomic (executable (name stm_tests) diff --git a/src/domainslib/dune b/src/domainslib/dune index 4f4e4df0..d7cca569 100644 --- a/src/domainslib/dune +++ b/src/domainslib/dune @@ -10,7 +10,7 @@ task_more_deps.exe task_parallel.exe)) -;; tests of Domainslib.Task's async functionality (non-STM_Seq STM_Domain STM_Thread) +;; tests of Domainslib.Task's async functionality (non-STM) (executable (name task_one_dep) @@ -51,7 +51,7 @@ (action (run ./%{deps} --no-colors --verbose))) -;; STM_Seq STM_Domain STM_Thread test of Domainslib.Chan +;; STM_Seq STM_Domain test of Domainslib.Chan (executable (name chan_stm_tests) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index 076bde10..87fd8499 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -42,11 +42,29 @@ (rule (alias runtest) (package multicoretests) - (deps ref_stm_tests.exe) + (deps ref_stm_seq_tests.exe) (action (progn - (bash "(./ref_stm_tests.exe --no-colors --verbose || echo 'test run triggered an error') | tee ref-output.txt") - (run %{bin:check_error_count} "neg_tests/ref_stm_tests" 4 ref-output.txt)))) + (bash "(./ref_stm_seq_tests.exe --no-colors --verbose || echo 'test run triggered an error') | tee ref-seq-output.txt") + (run %{bin:check_error_count} "neg_tests/ref_stm_seq_tests" 0 ref-seq-output.txt)))) + +(rule + (alias runtest) + (package multicoretests) + (deps ref_stm_dom_tests.exe) + (action + (progn + (bash "(./ref_stm_dom_tests.exe --no-colors --verbose || echo 'test run triggered an error') | tee ref-dom-output.txt") + (run %{bin:check_error_count} "neg_tests/ref_stm_dom_tests" 4 ref-dom-output.txt)))) + +(rule + (alias runtest) + (package multicoretests) + (deps ref_stm_thread_tests.exe) + (action + (progn + (bash "(./ref_stm_thread_tests.exe --no-colors --verbose || echo 'test run triggered an error') | tee ref-thread-output.txt") + (run %{bin:check_error_count} "neg_tests/ref_stm_thread_tests" 4 ref-thread-output.txt)))) (library (name CList)