Add thread for STM

doc/example/dune

@@ -11,5 +11,5 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))

doc/example/stm_tests.ml

@@ -1,5 +1,5 @@
 open QCheck
-open STM
+open STM_base
 
 (** parallel STM tests of Hashtbl *)
 
@@ -57,9 +57,10 @@ struct
     | _ -> false
 end
 
-module HTest = STM.Make(HashtblModel)
+module HT_seq = STM_sequential.Make(HashtblModel)
+module HT_dom = STM_domain.Make(HashtblModel)
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 200 in
-   [HTest.agree_test     ~count ~name:"Hashtbl test";
-    HTest.agree_test_par ~count ~name:"Hashtbl test"; ])
+   [HT_seq.agree_test     ~count ~name:"Hashtbl test";
+    HT_dom.agree_test_par ~count ~name:"Hashtbl test"; ])

doc/paper-examples/dune

@@ -11,5 +11,5 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))

doc/paper-examples/stm_tests.ml

@@ -1,5 +1,5 @@
 open QCheck
-open STM
+open STM_base
 
 (** parallel STM tests of Hashtbl *)
 
@@ -68,10 +68,11 @@ struct
     | _ -> false
 end
 
-module HTest = STM.Make(HashtblModel)
+module HT_seq = STM_sequential.Make(HashtblModel)
+module HT_dom = STM_domain.Make(HashtblModel)
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 200 in
-   [HTest.agree_test       ~count ~name:"Hashtbl test";
-    HTest.agree_test_par   ~count ~name:"Hashtbl test";
+   [HT_seq.agree_test       ~count ~name:"Hashtbl test";
+    HT_dom.agree_test_par   ~count ~name:"Hashtbl test";
    ])

lib/STM_base.ml

@@ -0,0 +1,6 @@
+(** Base module for specifying STM tests *)
+
+module STM_internal = STM_internal
+module STM_spec = STM_spec
+include STM_spec
+include Util

lib/STM_domain.ml

@@ -0,0 +1,53 @@
+open STM_base
+
+module Make (Spec: STM_spec.Spec) = struct
+
+  open Util
+  open QCheck
+  open STM_internal.Make(Spec)
+
+  let check_obs = check_obs
+  let arb_cmds_par = arb_cmds_par
+  let arb_triple = arb_triple
+  let shrink_triple = shrink_triple
+
+  (* operate over arrays to avoid needless allocation underway *)
+  let interp_sut_res sut cs =
+    let cs_arr = Array.of_list cs in
+    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)
+
+  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
+    let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in
+    let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in
+    let obs1 = Domain.join dom1 in
+    let obs2 = Domain.join dom2 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) (STM_spec.show_res r))
+           (pref_obs,obs1,obs2)
+
+  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:15 ~max_gen ~count ~name
+      (arb_cmds_par seq_len par_len)
+      (repeat rep_count agree_prop_par) (* 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:15 ~max_gen ~count ~name
+      (arb_cmds_par seq_len par_len)
+      (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *)
+  end

lib/STM_domain.mli

@@ -0,0 +1,32 @@
+(** Module for building parallel STM tests over [Domain]s *)
+
+module Make : functor (Spec : STM_base.Spec) ->
+  sig
+    val check_obs : (Spec.cmd * STM_base.res) list -> (Spec.cmd * STM_base.res) list -> (Spec.cmd * STM_base.res) list -> Spec.state -> bool
+    (** [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 arb_triple : 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 seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
+        sequential commands and at most [par_len] parallel commands each.
+        The three [cmd] components are generated with [arb0], [arb1], and [arb2], respectively.
+        Each of these take the model state as a parameter. *)
+
+    val shrink_triple : (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.Shrink.t
+    (** [shrink_triple arb0 arb1 arb2] is a [Shrinker.t] for programs (triple of list of [cmd]s) that is specialized for each part of the program. *)
+
+    val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM_base.res) list
+    (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut]
+        and returns the list of corresponding [cmd] and result pairs. *)
+
+    val agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+    (** Parallel agreement property based on [Domain] *)
+
+    val agree_test_par : count:int -> name:string -> QCheck.Test.t
+    (** Parallel agreement test based on [Domain] which combines [repeat] and [~retries] *)
+
+    val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t
+    (** An negative agreement test (for convenience). Accepts two labeled parameters:
+        [count] is the test count and [name] is the printed test name. *)
+
+ end