Polish #88

lib/STM_domain.mli

@@ -15,10 +15,10 @@ module Make : functor (Spec : STM_spec.Spec) ->
     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 -> QCheck2.Test.t
+    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 -> QCheck2.Test.t
+    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. *)
 

lib/STM_sequential.mli

@@ -27,7 +27,7 @@ module Make : functor (Spec : STM_spec.Spec) ->
         when interpreted from the model's initial state and the [sut]'s initial state.
         Cleans up after itself by calling [Spec.cleanup] *)
 
-    val agree_test : count:int -> name:string -> QCheck2.Test.t
+    val agree_test : count:int -> name:string -> QCheck.Test.t
     (** An actual agreement test (for convenience). Accepts two labeled parameters:
         [count] is the test count and [name] is the printed test name. *)
 

lib/STM_thread.mli

@@ -11,10 +11,10 @@ module Make : functor (Spec : STM_spec.Spec) ->
     val agree_prop_conc : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
     (** Concurrent agreement property based on [Thread] *)
 
-    val agree_test_conc : count:int -> name:string -> QCheck2.Test.t
+    val agree_test_conc : count:int -> name:string -> QCheck.Test.t
     (** Concurrent agreement test based on [Thread] which combines [repeat] and [~retries] *)
 
-    val neg_agree_test_conc : count:int -> name:string -> QCheck2.Test.t
+    val neg_agree_test_conc : 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. *)
 

src/array/dune

@@ -12,7 +12,7 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/array/stm_tests.ml

@@ -103,14 +103,14 @@ struct
     | _, _ -> false
 end
 
-module ArraySTM_Seq = STM_sequential.Make(AConf)
-module ArraySTM_Dom = STM_domain.Make(AConf)
+module ArraySTM_seq = STM_sequential.Make(AConf)
+module ArraySTM_dom = STM_domain.Make(AConf)
 
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 1000 in
-   [ArraySTM_Seq.agree_test         ~count ~name:"STM Array test sequential";
-    ArraySTM_Dom.neg_agree_test_par ~count ~name:"STM Array test parallel" (* this test is expected to fail *)
+   [ArraySTM_seq.agree_test         ~count ~name:"STM Array test sequential";
+    ArraySTM_dom.neg_agree_test_par ~count ~name:"STM Array test parallel" (* this test is expected to fail *)
 ])

src/atomic/dune

@@ -12,7 +12,7 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/atomic/stm_tests.ml

@@ -66,12 +66,12 @@ struct
     | _,_ -> false
 end
 
-module AT_Seq = STM_sequential.Make(CConf)
-module AT_Dom = STM_domain.Make(CConf)
+module AT_seq = STM_sequential.Make(CConf)
+module AT_dom = STM_domain.Make(CConf)
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
-  (let count = 1000 in
-   [AT_Seq.agree_test     ~count ~name:"STM Atomic test sequential";
-    AT_Dom.agree_test_par ~count ~name:"STM Atmoic test parallel";])
+  (let count = 250 in
+   [AT_seq.agree_test     ~count ~name:"STM Atomic test sequential";
+    AT_dom.agree_test_par ~count ~name:"STM Atmoic test parallel";])

src/bigarray/dune

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

src/buffer/dune

@@ -9,7 +9,7 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/buffer/stm_tests.ml

@@ -125,13 +125,13 @@ struct
     | _, _ -> false
 end
 
-module BufferSTM_Seq = STM_sequential.Make(BConf)
-module BufferSTM_Dom = STM_domain.Make(BConf)
+module BufferSTM_seq = STM_sequential.Make(BConf)
+module BufferSTM_dom = STM_domain.Make(BConf)
 
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
-  (let count = 100 in
-   [BufferSTM_Seq.agree_test         ~count ~name:"STM Buffer test sequential";
-    BufferSTM_Dom.neg_agree_test_par ~count ~name:"STM Buffer test parallel"])
+  (let count = 1000 in
+   [BufferSTM_seq.agree_test         ~count ~name:"STM Buffer test sequential";
+    BufferSTM_dom.neg_agree_test_par ~count ~name:"STM Buffer test parallel"])

src/bytes/dune

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

src/bytes/stm_tests.ml

@@ -87,14 +87,14 @@ struct
     | _, _ -> false
 end
 
-module BytesSTM_Seq = STM_sequential.Make(ByConf)
-module BytesSTM_Dom = STM_domain.Make(ByConf)
+module BytesSTM_seq = STM_sequential.Make(ByConf)
+module BytesSTM_dom = STM_domain.Make(ByConf)
 
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 1000 in
-   [BytesSTM_Seq.agree_test     ~count ~name:"STM Bytes test sequential";
-    BytesSTM_Dom.neg_agree_test_par ~count ~name:"STM Bytes test parallel"
+   [BytesSTM_seq.agree_test     ~count ~name:"STM Bytes test sequential";
+    BytesSTM_dom.neg_agree_test_par ~count ~name:"STM Bytes test parallel"
 ])

src/domainslib/chan_stm_tests.ml

@@ -69,13 +69,13 @@ struct
 end
 
 
-module ChT_Seq = STM_sequential.Make(ChConf)
-module ChT_Dom = STM_domain.Make(ChConf)
+module ChT_seq = STM_sequential.Make(ChConf)
+module ChT_dom = STM_domain.Make(ChConf)
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count,name = 500,"global Domainslib.Chan test" in [
-      ChT_Seq.agree_test     ~count ~name;
-      ChT_Dom.agree_test_par ~count ~name;
+      ChT_seq.agree_test     ~count ~name;
+      ChT_dom.agree_test_par ~count ~name;
     ])

src/domainslib/dune

@@ -53,7 +53,7 @@
 (executable
  (name chan_stm_tests)
  (modules chan_stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain domainslib)
+ (libraries qcheck-stm.sequential qcheck-stm.domain domainslib)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/ephemeron/dune

@@ -8,7 +8,7 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/ephemeron/stm_tests.ml

@@ -134,13 +134,13 @@ module EphemeronModel =
       | _ -> false
   end
 
-module ETest_Seq = STM_sequential.Make(EphemeronModel)
-module ETest_Dom = STM_domain.Make(EphemeronModel)
+module ETest_seq = STM_sequential.Make(EphemeronModel)
+module ETest_dom = STM_domain.Make(EphemeronModel)
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 1000 in
-   [ ETest_Seq.agree_test         ~count ~name:"STM Ephemeron test sequential"; (* succeed *)
-     ETest_Dom.neg_agree_test_par ~count ~name:"STM Ephemeron test parallel";   (* fail *)
+   [ ETest_seq.agree_test         ~count ~name:"STM Ephemeron test sequential"; (* succeed *)
+     ETest_dom.neg_agree_test_par ~count ~name:"STM Ephemeron test parallel";   (* fail *)
   ])

src/floatarray/dune

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

src/floatarray/stm_tests.ml

@@ -119,14 +119,14 @@ struct
     | _, _ -> false
 end
 
-module FloatArraySTM_Seq = STM_sequential.Make(FAConf)
-module FloatArraySTM_Dom = STM_domain.Make(FAConf)
+module FloatArraySTM_seq = STM_sequential.Make(FAConf)
+module FloatArraySTM_dom = STM_domain.Make(FAConf)
 
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 1000 in
-   [FloatArraySTM_Seq.agree_test         ~count ~name:"STM Float Array test sequential";
-    FloatArraySTM_Dom.neg_agree_test_par ~count ~name:"STM Float Array test parallel"
+   [FloatArraySTM_seq.agree_test         ~count ~name:"STM Float Array test sequential";
+    FloatArraySTM_dom.neg_agree_test_par ~count ~name:"STM Float Array test parallel"
 ])

src/hashtbl/dune

@@ -12,7 +12,7 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/hashtbl/stm_tests.ml

@@ -118,13 +118,13 @@ struct
 end
 
 
-module HTest_Seq = STM_sequential.Make(HConf)
-module HTest_Dom = STM_domain.Make(HConf)
+module HTest_seq = STM_sequential.Make(HConf)
+module HTest_dom = STM_domain.Make(HConf)
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 200 in
-   [HTest_Seq.agree_test         ~count ~name:"STM Hashtbl test sequential";
-    HTest_Dom.neg_agree_test_par ~count ~name:"STM Hashtbl test parallel";
+   [HTest_seq.agree_test         ~count ~name:"STM Hashtbl test sequential";
+    HTest_dom.neg_agree_test_par ~count ~name:"STM Hashtbl test parallel";
    ])

src/lazy/dune

@@ -9,7 +9,7 @@
 (executable
  (name stm_tests)
  (modules stm_tests)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/lazy/stm_tests.ml

@@ -96,33 +96,33 @@ struct
     | _,_ -> false
 end
 
-module LTlazy_Seq    = STM_sequential.Make(struct
+module LTlazy_seq    = STM_sequential.Make(struct
     include LConfbase
     let init_state  = (7 * 100, false)
     let init_sut () = lazy (work ())
   end)
-module LTfromval_Seq = STM_sequential.Make(struct
+module LTfromval_seq = STM_sequential.Make(struct
     include LConfbase
     let init_state = (42, true)
     let init_sut () = Lazy.from_val 42
   end)
-module LTfromfun_Seq = STM_sequential.Make(struct
+module LTfromfun_seq = STM_sequential.Make(struct
     include LConfbase
     let init_state = (7 * 100, false)
     let init_sut () = Lazy.from_fun work
   end)
 
-module LTlazy_Dom    = STM_domain.Make(struct
+module LTlazy_dom    = STM_domain.Make(struct
     include LConfbase
     let init_state  = (7 * 100, false)
     let init_sut () = lazy (work ())
   end)
-module LTfromval_Dom = STM_domain.Make(struct
+module LTfromval_dom = STM_domain.Make(struct
     include LConfbase
     let init_state = (42, true)
     let init_sut () = Lazy.from_val 42
   end)
-module LTfromfun_Dom = STM_domain.Make(struct
+module LTfromfun_dom = STM_domain.Make(struct
     include LConfbase
     let init_state = (7 * 100, false)
     let init_sut () = Lazy.from_fun work
@@ -132,10 +132,10 @@ Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 200 in
-   [LTlazy_Seq.agree_test        ~count ~name:"STM Lazy test sequential";
-    LTfromval_Seq.agree_test     ~count ~name:"STM Lazy test sequential from_val";
-    LTfromfun_Seq.agree_test     ~count ~name:"STM Lazy test sequential from_fun";
-    LTlazy_Dom.neg_agree_test_par    ~count ~name:"STM Lazy test parallel";
-    LTfromval_Dom.agree_test_par     ~count ~name:"STM Lazy test parallel from_val";
-    LTfromfun_Dom.neg_agree_test_par ~count ~name:"STM Lazy test parallel from_fun";
+   [LTlazy_seq.agree_test        ~count ~name:"STM Lazy test sequential";
+    LTfromval_seq.agree_test     ~count ~name:"STM Lazy test sequential from_val";
+    LTfromfun_seq.agree_test     ~count ~name:"STM Lazy test sequential from_fun";
+    LTlazy_dom.neg_agree_test_par    ~count ~name:"STM Lazy test parallel";
+    LTfromval_dom.agree_test_par     ~count ~name:"STM Lazy test parallel from_val";
+    LTfromfun_dom.neg_agree_test_par ~count ~name:"STM Lazy test parallel from_fun";
    ])

src/lockfree/dune

@@ -11,7 +11,7 @@
 (executable
  (name ws_deque_test)
  (modules ws_deque_test)
- (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain lockfree)
+ (libraries qcheck-stm.sequential qcheck-stm.domain lockfree)
  (preprocess (pps ppx_deriving.show)))
 
 (rule

src/lockfree/ws_deque_test.ml

@@ -57,25 +57,25 @@ struct
     | _,_ -> false)
 end
 
-module WSDT_Seq = STM_sequential.Make(WSDConf)
-module WSDT_Dom = STM_domain.Make(WSDConf)
+module WSDT_seq = STM_sequential.Make(WSDConf)
+module WSDT_dom = STM_domain.Make(WSDConf)
 
 (* The following definitions differ slightly from those in STM.ml.
    This has to do with how work-stealing deques are supposed to be used according to spec:
    - [agree_prop_par] differs in that it only spawns one domain ("a stealer domain")
      in parallel with the original "owner domain" (it also uses [Semaphore.Binary]) *)
 let agree_prop_par =
   (fun (seq_pref,owner,stealer) ->
-    assume (WSDT_Seq.cmds_ok WSDConf.init_state (seq_pref@owner));
-    assume (WSDT_Seq.cmds_ok WSDConf.init_state (seq_pref@stealer));
+    assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref@owner));
+    assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref@stealer));
     let sut = WSDConf.init_sut () in
-    let pref_obs = WSDT_Seq.interp_sut_res sut seq_pref in
+    let pref_obs = WSDT_seq.interp_sut_res sut seq_pref in
     let sema = Semaphore.Binary.make false in
-    let stealer_dom = Domain.spawn (fun () -> Semaphore.Binary.release sema; WSDT_Seq.interp_sut_res sut stealer) in
+    let stealer_dom = Domain.spawn (fun () -> Semaphore.Binary.release sema; WSDT_seq.interp_sut_res sut stealer) in
     while not (Semaphore.Binary.try_acquire sema) do Domain.cpu_relax() done;
-    let own_obs = WSDT_Seq.interp_sut_res sut owner in
+    let own_obs = WSDT_seq.interp_sut_res sut owner in
     let stealer_obs = Domain.join stealer_dom in
-    let res = WSDT_Seq.check_obs pref_obs own_obs stealer_obs WSDConf.init_state in
+    let res = WSDT_seq.check_obs pref_obs own_obs stealer_obs WSDConf.init_state in
     let () = WSDConf.cleanup sut in
     res ||
       Test.fail_reportf "  Results incompatible with linearized model:\n\n%s"
@@ -86,7 +86,7 @@ let agree_prop_par =
 
 (* [arb_cmds_par] differs in what each triple component generates:
    "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *)
-let arb_cmds_par = WSDT_Dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd
+let arb_cmds_par = WSDT_dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd
 
 (* A parallel agreement test - w/repeat and retries combined *)
 let agree_test_par ~count ~name =
@@ -95,14 +95,14 @@ let agree_test_par ~count ~name =
     arb_cmds_par (repeat rep_count agree_prop_par) (* 50 times each, then 50 * 10 times when shrinking *)
 
 (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *)
-let agree_test_par_negative ~count ~name = WSDT_Dom.neg_agree_test_par ~count ~name
+let agree_test_par_negative ~count ~name = WSDT_dom.neg_agree_test_par ~count ~name
 
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 1000 in [
-    WSDT_Seq.agree_test     ~count ~name:"sequential ws_deque test";
+    WSDT_seq.agree_test     ~count ~name:"sequential ws_deque test";
     agree_test_par          ~count ~name:"parallel ws_deque test (w/repeat)";
     agree_test_par_negative ~count ~name:"parallel ws_deque test (w/non_det module)";
   ])