Add a QCheck-STM test for Stack

Author: polytypic

dune-project

@@ -82,6 +82,14 @@
    (and
     (>= 1.7.0)
     :with-test))
+  (qcheck-core
+   (and
+    (>= 0.21.2)
+    :with-test))
+  (qcheck-stm
+   (and
+    (>= 0.3)
+    :with-test))
   (mdx
    (and
     (>= 2.3.0)

kcas_data.opam

@@ -20,6 +20,8 @@ depends: [
   "domain_shims" {>= "0.1.0" & with-test}
   "mtime" {>= "2.0.0" & with-test}
   "alcotest" {>= "1.7.0" & with-test}
+  "qcheck-core" {>= "0.21.2" & with-test}
+  "qcheck-stm" {>= "0.3" & with-test}
   "mdx" {>= "2.3.0" & with-test}
   "yojson" {>= "2.1.0" & with-test}
   "odoc" {>= "2.2.0" & with-doc}

test/kcas_data/dune

@@ -1,3 +1,14 @@
+(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
   dllist_test
@@ -6,6 +17,21 @@
   mvar_test
   queue_test
   stack_test
+  stack_test_stm
   xt_test)
- (libraries alcotest kcas kcas_data domain_shims)
+ (libraries
+  alcotest
+  kcas
+  kcas_data
+  domain_shims
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-stm.thread
+  (select
+   empty.ml
+   from
+   (qcheck-stm.domain -> empty.ocaml5.ml)
+   (-> empty.ocaml4.ml)))
  (package kcas_data))

test/kcas_data/empty.ocaml4.ml

@@ -0,0 +1,59 @@
+open Kcas_data
+
+module Spec = struct
+  type cmd = Push of int | Pop_opt | Top_opt | Length
+
+  let show_cmd = function
+    | Push x -> "Push " ^ string_of_int x
+    | Pop_opt -> "Pop_opt"
+    | Top_opt -> "Top_opt"
+    | Length -> "Length"
+
+  type state = int list
+  type sut = int Stack.t
+
+  let arb_cmd _s =
+    QCheck.(
+      [
+        Gen.int |> Gen.map (fun x -> Push x);
+        Gen.return Pop_opt;
+        Gen.return Top_opt;
+        Gen.return Length;
+      ]
+      |> Gen.oneof |> make ~print:show_cmd)
+
+  let init_state = []
+  let init_sut () = Stack.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Push x -> x :: s
+    | Pop_opt -> ( match s with [] -> [] | _ :: s -> s)
+    | Top_opt -> s
+    | Length -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    let open STM in
+    match c with
+    | Push x -> Res (unit, Stack.push x d)
+    | Pop_opt -> Res (option int, Stack.pop_opt d)
+    | Top_opt -> Res (option int, Stack.top_opt d)
+    | Length -> Res (int, Stack.length d)
+
+  let postcond c (s : state) res =
+    let open STM in
+    match (c, res) with
+    | Push _x, Res ((Unit, _), ()) -> true
+    | Pop_opt, Res ((Option Int, _), res) -> (
+        res = match s with [] -> None | x :: _ -> Some x)
+    | Top_opt, Res ((Option Int, _), res) -> (
+        res = match s with [] -> None | x :: _ -> Some x)
+    | Length, Res ((Int, _), res) -> res = List.length s
+    | _, _ -> false
+end
+
+let () =
+  Stm_run.run ~count:1000 ~verbose:true ~name:"Stack" (module Spec) |> exit

test/kcas_data/empty.ocaml5.ml

@@ -0,0 +1,8 @@
+let run ~verbose ~count ~name (module Spec : STM.Spec) =
+  let module Seq = STM_sequential.Make (Spec) in
+  let module Con = STM_thread.Make (Spec) [@alert "-experimental"] in
+  QCheck_base_runner.run_tests ~verbose
+    [
+      Seq.agree_test ~count ~name:(name ^ " sequential");
+      Con.agree_test_conc ~count ~name:(name ^ " concurrent");
+    ]

test/kcas_data/stack_test_stm.ml

@@ -0,0 +1,8 @@
+let run ~verbose ~count ~name (module Spec : STM.Spec) =
+  let module Seq = STM_sequential.Make (Spec) in
+  let module Dom = STM_domain.Make (Spec) in
+  QCheck_base_runner.run_tests ~verbose
+    [
+      Seq.agree_test ~count ~name:(name ^ " sequential");
+      Dom.agree_test_par ~count ~name:(name ^ " parallel");
+    ]