Use stm_run private lib (from Picos) with time based deadline

Some of the tests just take too much time on some of the OCaml CI machines.

Author: polytypic

dune-project

@@ -48,6 +48,14 @@
    (and
     (>= 1.8.0)
     :with-test))
+  (qcheck-core
+   (and
+    (>= 0.21.2)
+    :with-test))
+  (qcheck-stm
+   (and
+    (>= 0.3)
+    :with-test))
   (mdx
    (and
     (>= 2.4.1)

kcas.opam

@@ -24,6 +24,8 @@ depends: [
   "multicore-magic" {>= "2.3.0"}
   "domain_shims" {>= "0.1.0" & with-test}
   "alcotest" {>= "1.8.0" & with-test}
+  "qcheck-core" {>= "0.21.2" & with-test}
+  "qcheck-stm" {>= "0.3" & with-test}
   "mdx" {>= "2.4.1" & with-test}
   "sherlodoc" {>= "0.2" & with-doc}
   "odoc" {>= "2.4.2" & with-doc}

test/kcas_data/dune

@@ -1,14 +1,3 @@
-(rule
- (enabled_if %{lib-available:qcheck-stm.domain})
- (action
-  (copy stm_run.ocaml5.ml stm_run.ml)))
-
-(rule
- (enabled_if
-  (not %{lib-available:qcheck-stm.domain}))
- (action
-  (copy stm_run.ocaml4.ml stm_run.ml)))
-
 (tests
  (names
   accumulator_test_stm
@@ -30,10 +19,8 @@
   kcas_data
   domain_shims
   qcheck-core
-  qcheck-core.runner
   qcheck-stm.stm
-  qcheck-stm.sequential
-  qcheck-stm.thread
+  stm_run
   (select
    empty.ml
    from

test/kcas_data/stm_run.ocaml4.ml

@@ -0,0 +1,25 @@
+(rule
+ (enabled_if %{lib-available:qcheck-stm.domain})
+ (action
+  (copy stm_run.ocaml5.ml stm_run.ml)))
+
+(rule
+ (enabled_if
+  (not %{lib-available:qcheck-stm.domain}))
+ (action
+  (copy stm_run.ocaml4.ml stm_run.ml)))
+
+(library
+ (name stm_run)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-stm.thread
+  unix
+  (select
+   empty.ml
+   from
+   (qcheck-stm.domain -> empty.ocaml5.ml)
+   (-> empty.ocaml4.ml))))

test/kcas_data/stm_run.ocaml5.ml

@@ -0,0 +1,45 @@
+module type STM_domain = sig
+  module Spec : STM.Spec
+
+  val check_obs :
+    (Spec.cmd * STM.res) list ->
+    (Spec.cmd * STM.res) list ->
+    (Spec.cmd * STM.res) list ->
+    Spec.state ->
+    bool
+
+  val all_interleavings_ok :
+    Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+
+  val arb_cmds_triple :
+    int ->
+    int ->
+    (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
+
+  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
+
+  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
+
+  val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
+  val agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+
+  val agree_prop_par_asym :
+    Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+
+  val agree_test_par : count:int -> name:string -> QCheck.Test.t
+  val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t
+  val agree_test_par_asym : count:int -> name:string -> QCheck.Test.t
+  val neg_agree_test_par_asym : count:int -> name:string -> QCheck.Test.t
+end

test/kcas_data/stm_run/dune

@@ -0,0 +1,19 @@
+include Intf
+
+let count =
+  let factor b = if b then 10 else 1 in
+  factor (64 <= Sys.word_size) * factor (Sys.backend_type = Native) * 10
+
+let run ?(verbose = true) ?(count = count) ?(budgetf = 60.0) ~name ?make_domain
+    (module Spec : STM.Spec) =
+  let module Seq = STM_sequential.Make (Spec) in
+  let module Con = STM_thread.Make (Spec) [@alert "-experimental"] in
+  Util.run_with_budget ~budgetf ~count @@ fun count ->
+  [
+    [ Seq.agree_test ~count ~name:(name ^ " sequential") ];
+    (match make_domain with
+    | None -> [ Con.agree_test_conc ~count ~name:(name ^ " concurrent") ]
+    | Some _ -> []);
+  ]
+  |> List.concat
+  |> QCheck_base_runner.run_tests ~verbose