tweek STM_Thread tests to trigger bugs and add dune rule for tests

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,23 +25,24 @@ 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
            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (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

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)

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)

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)