Add agree_prop_par_asym to STM_domain

lib/STM_domain.ml

@@ -8,8 +8,13 @@ module Make (Spec: Spec) = struct
     [@alert "-internal"]
 
   let check_obs = check_obs
+  let all_interleavings_ok (seq_pref,cmds1,cmds2) =
+    all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state
   let arb_cmds_triple = arb_cmds_triple
   let arb_triple = arb_triple
+  let arb_triple_asym seq_len par_len arb0 arb1 arb2 =
+    let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in
+    set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple
 
   (* operate over arrays to avoid needless allocation underway *)
   let interp_sut_res sut cs =
@@ -34,23 +39,66 @@ module Make (Spec: Spec) = struct
            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,obs1,obs2)
 
+  let agree_prop_par_asym (seq_pref, cmds1, cmds2) =
+    let sut = Spec.init_sut () in
+    let pref_obs = interp_sut_res sut seq_pref in
+    let sema = Semaphore.Binary.make false in
+    let child_dom =
+      Domain.spawn (fun () ->
+          Semaphore.Binary.release sema;
+          try Ok (interp_sut_res sut cmds2) with exn -> Error exn)
+    in
+    while not (Semaphore.Binary.try_acquire sema) do
+      Domain.cpu_relax ()
+    done;
+    let parent_obs = try Ok (interp_sut_res sut cmds1) with exn -> Error exn in
+    let child_obs = Domain.join child_dom in
+    let () = Spec.cleanup sut in
+    let parent_obs = match parent_obs with Ok v -> v | Error exn -> raise exn in
+    let child_obs = match child_obs with Ok v -> v | Error exn -> raise exn in
+    check_obs pref_obs parent_obs child_obs Spec.init_state
+      || Test.fail_reportf "  Results incompatible with linearized model:\n\n%s"
+         @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false
+           (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
+           (pref_obs,parent_obs,child_obs)
+
   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
       (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_par triple) (* 25 times each, then 25 * 15 times when shrinking *)
+      (fun triple ->
+         assume (all_interleavings_ok triple);
+         repeat rep_count agree_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
       (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_par triple) (* 25 times each, then 25 * 15 times when shrinking *)
-  end
+      (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
+      (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
+      (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 *)
+end

lib/STM_domain.mli

@@ -6,6 +6,11 @@ module Make : functor (Spec : STM.Spec) ->
     (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref]
         and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *)
 
+    val all_interleavings_ok : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+    (** [all_interleavings_ok (seq,spawn0,spawn1)] checks that
+        preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
+        possible interleavings and starting with {!Spec.init_state}. *)
+
     val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
@@ -17,18 +22,50 @@ module Make : functor (Spec : STM.Spec) ->
         The three {!Spec.cmd} components are generated with [arb0], [arb1], and [arb2], respectively.
         Each of these take the model state as a parameter. *)
 
+    val arb_triple_asym : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
+    (** [arb_triple_asym seq_len par_len arb0 arb1 arb2] creates a triple [cmd]
+        generator like {!arb_triple}. It differs in that the resulting printer
+        is asymmetric, printing [arb1]'s result below [arb0]'s result and
+        printing [arb2]'s result to the right of [arb1]'s result. *)
+
     val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system {!Spec.sut}
         and returns the list of corresponding {!Spec.cmd} and result pairs. *)
 
     val agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
-    (** Parallel agreement property based on {!Stdlib.Domain} *)
+    (** Parallel agreement property based on {!Stdlib.Domain}.
+        [agree_prop_par (seq_pref, tl1, tl2)] first interprets [seq_pref]
+        and then spawns two parallel, symmetric domains interpreting [tl1] and
+        [tl2] simultaneously.
+
+        @return [true] if there exists a sequential interleaving of the results
+        which agrees with a model interpretation. *)
+
+    val agree_prop_par_asym : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+    (** Asymmetric parallel agreement property based on {!Stdlib.Domain}.
+        [agree_prop_par_asym (seq_pref, tl1, tl2)] first interprets [seq_pref],
+        and then interprets [tl1] while a spawned domain interprets [tl2]
+        in parallel with the parent domain.
+
+        @return [true] if there exists a sequential interleaving of the results
+        which agrees with a model interpretation. *)
 
     val agree_test_par : count:int -> name:string -> QCheck.Test.t
-    (** Parallel agreement test based on {!Stdlib.Domain} which combines [repeat] and [~retries] *)
+    (** Parallel agreement test based on {!Stdlib.Domain} which combines [repeat] and [~retries].
+        Accepts two labeled parameters:
+        [count] is the number of test iterations and [name] is the printed test name. *)
 
     val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t
-    (** A negative agreement test (for convenience). Accepts two labeled parameters:
-        [count] is the test count and [name] is the printed test name. *)
+    (** A negative parallel agreement test (for convenience). Accepts two labeled parameters:
+        [count] is the number of test iterations and [name] is the printed test name. *)
+
+    val agree_test_par_asym : count:int -> name:string -> QCheck.Test.t
+    (** Asymmetric parallel agreement test based on {!Stdlib.Domain} and {!agree_prop_par_asym}
+        which combines [repeat] and [~retries]. Accepts two labeled parameters:
+        [count] is the number of test iterations and [name] is the printed test name. *)
 
+    val neg_agree_test_par_asym : count:int -> name:string -> QCheck.Test.t
+    (** A negative asymmetric parallel agreement test (for convenience).
+        Accepts two labeled parameters:
+        [count] is the number of test iterations and [name] is the printed test name. *)
  end

src/neg_tests/stm_tests_domain_ref.ml

@@ -5,6 +5,8 @@ module RT_int64 = STM_domain.Make(RConf_int64)
 ;;
 QCheck_runner.run_tests_main
   (let count = 1000 in
-   [RT_int.neg_agree_test_par      ~count ~name:"STM int ref test parallel";
-    RT_int64.neg_agree_test_par    ~count ~name:"STM int64 ref test parallel";
+   [RT_int.neg_agree_test_par        ~count ~name:"STM int ref test parallel";
+    RT_int64.neg_agree_test_par      ~count ~name:"STM int64 ref test parallel";
+    RT_int.neg_agree_test_par_asym   ~count ~name:"STM int ref test parallel asymmetric";
+    RT_int64.neg_agree_test_par_asym ~count ~name:"STM int64 ref test parallel asymmetric";
    ])