Merge pull request #318 from ocaml-multicore/avoid-repetitive-interleaving-search

Avoid repetitive interleaving search in STM_domain

Author: jmid

CHANGES.md

@@ -2,10 +2,11 @@
 
 ## Next version
 
-- ensure `cleanup` is run in the presence of exceptions in
+- #318: avoid repetitive interleaving searches in `STM_domain` and `STM_thread`
+- #312: Escape and quote `bytes` printed with `STM`'s `bytes` combinator
+- #295: ensure `cleanup` is run in the presence of exceptions in
   - `STM_sequential.agree_prop` and `STM_domain.agree_prop_par`
   - `Lin_thread.lin_prop` and `Lin_effect.lin_prop`
-- #312: Escape and quote `bytes` printed with `STM`'s `bytes` combinator
 
 ## 0.1.1
 

lib/STM_domain.ml

@@ -18,7 +18,6 @@ module Make (Spec: Spec) = struct
     List.combine cs (Array.to_list res_arr)
 
   let agree_prop_par (seq_pref,cmds1,cmds2) =
-    assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
     let sut = Spec.init_sut () in
     let pref_obs = interp_sut_res sut seq_pref in
     let wait = Atomic.make true in
@@ -41,13 +40,17 @@ module Make (Spec: Spec) = struct
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
     Test.make ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
-      (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *)
+      (fun ((seq_pref,cmds1,cmds2) as triple) ->
+         assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
+         repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 15 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
       (arb_cmds_triple seq_len par_len)
-      (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *)
+      (fun ((seq_pref,cmds1,cmds2) as triple) ->
+         assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
+         repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 15 times when shrinking *)
   end

lib/STM_thread.ml

@@ -21,7 +21,6 @@ module Make (Spec: Spec) = struct
 
   (* 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
     let obs1,obs2 = ref (Error ThreadNotFinished), ref (Error ThreadNotFinished) in
     let pref_obs = interp_sut_res sut seq_pref in
@@ -46,13 +45,17 @@ module Make (Spec: Spec) = struct
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
     Test.make ~retries:15 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
-      (repeat rep_count agree_prop_conc) (* 100 times each, then 100 * 15 times when shrinking *)
+      (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 = 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:15 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
-      (repeat rep_count agree_prop_conc) (* 25 times each, then 25 * 15 times when shrinking *)
+      (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 *)
   end