STM tests

CHANGES.md

@@ -2,10 +2,14 @@
 
 All notable changes to this project will be documented in this file.
 
-## 0.3.1 
+## Not released
+
+* Add STM tests for current data structures (@lyrm, @jmid)
+
+## 0.3.1
 
 * Rework dscheck integration to work with utop (@lyrm)
-* Add OCaml 4 compatability (@sudha247) 
+* Add OCaml 4 compatability (@sudha247)
 * Add STM ws_deque tests (@jmid, @lyrm)
 
 ## 0.3.0

lockfree.opam

@@ -13,12 +13,15 @@ depends: [
   "dune" {>= "3.0"}
   "domain_shims" {>= "0.1.0"}
   "qcheck" {with-test & >= "0.18.1"}
-  "qcheck-stm" {with-test & >= "0.1"}
+  "qcheck-stm" {with-test & >= "0.1.1"}
   "qcheck-alcotest" {with-test & >= "0.18.1"}
   "alcotest" {with-test & >= "1.6.0"}
   "yojson" {>= "2.0.2"}
-  "dscheck" {with-test & >= "0.0.1"}
+  "dscheck" {with-test & >= "0.1.0"}
 ]
 available: arch != "x86_32" & arch != "arm32" & arch != "ppc64"
 depopts: []
 build: ["dune" "build" "-p" name "-j" jobs]
+pin-depends: [
+  [ "qcheck-stm.0.1.1"
+    "git+https://github.com/ocaml-multicore/multicoretests.git#4e2e1b22bffec3675a15cf6c2e05f733e9f8b66d" ] ]

test/michael_scott_queue/dune

@@ -13,3 +13,10 @@
  (name qcheck_michael_scott_queue)
  (libraries lockfree qcheck qcheck-alcotest)
  (modules qcheck_michael_scott_queue))
+
+(test
+ (name stm_michael_scott_queue)
+ (modules stm_michael_scott_queue)
+ (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))

test/michael_scott_queue/stm_michael_scott_queue.ml

@@ -0,0 +1,67 @@
+(** Sequential and Parallel model-based tests of michael_scott_queue *)
+
+open QCheck
+open STM
+module Ms_queue = Lockfree.Michael_scott_queue
+
+module MSQConf = struct
+  type cmd = Push of int | Pop | Is_empty
+
+  let show_cmd c =
+    match c with
+    | Push i -> "Push " ^ string_of_int i
+    | Pop -> "Pop"
+    | Is_empty -> "Is_empty"
+
+  type state = int list
+  type sut = int Ms_queue.t
+
+  let arb_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (Gen.oneof
+         [
+           Gen.map (fun i -> Push i) int_gen;
+           Gen.return Pop;
+           Gen.return Is_empty;
+         ])
+
+  let init_state = []
+  let init_sut () = Ms_queue.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Push i -> i :: s
+    | Pop -> ( match List.rev s with [] -> s | _ :: s' -> List.rev s')
+    | Is_empty -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Push i -> Res (unit, Ms_queue.push d i)
+    | Pop -> Res (option int, Ms_queue.pop d)
+    | Is_empty -> Res (bool, Ms_queue.is_empty d)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Push _, Res ((Unit, _), _) -> true
+    | Pop, Res ((Option Int, _), res) -> (
+        match List.rev s with [] -> res = None | j :: _ -> res = Some j)
+    | Is_empty, Res ((Bool, _), res) -> res = (s = [])
+    | _, _ -> false
+end
+
+module MSQ_seq = STM_sequential.Make (MSQConf)
+module MSQ_dom = STM_domain.Make (MSQConf)
+
+let () =
+  let count = 500 in
+  QCheck_base_runner.run_tests_main
+    [
+      MSQ_seq.agree_test ~count
+        ~name:"STM Lockfree.Michael_scott_queue test sequential";
+      MSQ_dom.agree_test_par ~count
+        ~name:"STM Lockfree.Michael_scott_queue test parallel";
+    ]

test/mpsc_queue/dune

@@ -10,3 +10,10 @@
  (name qcheck_mpsc_queue)
  (libraries lockfree qcheck qcheck-alcotest)
  (modules qcheck_mpsc_queue))
+
+(test
+ (name stm_mpsc_queue)
+ (modules stm_mpsc_queue)
+ (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))

test/mpsc_queue/stm_mpsc_queue.ml

@@ -0,0 +1,112 @@
+(** Sequential and Parallel model-based tests of mpsc_queue *)
+
+open QCheck
+open STM
+open Util
+module Mpsc_queue = Lockfree.Mpsc_queue
+
+module MPSCConf = struct
+  type cmd = Push of int | Pop | Push_head of int | Is_empty | Close
+
+  let show_cmd c =
+    match c with
+    | Push i -> "Push " ^ string_of_int i
+    | Pop -> "Pop"
+    | Push_head i -> "Push_head" ^ string_of_int i
+    | Is_empty -> "Is_empty"
+    | Close -> "Close"
+
+  type state = bool * int list
+  type sut = int Mpsc_queue.t
+
+  let producer_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (Gen.oneof
+         [
+           Gen.map (fun i -> Push i) int_gen;
+           Gen.return Is_empty;
+           Gen.return Close;
+         ])
+
+  let arb_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (Gen.oneof
+         [
+           Gen.return Pop;
+           Gen.map (fun i -> Push_head i) int_gen;
+           Gen.return Is_empty;
+           Gen.return Close;
+         ])
+
+  let init_state = (false, [])
+  let init_sut () = Mpsc_queue.create ()
+  let cleanup _ = ()
+
+  let next_state c (is_closed, s) =
+    match c with
+    | Push i ->
+        (is_closed, if not is_closed then i :: List.rev s |> List.rev else s)
+    | Push_head i -> (is_closed, if not (is_closed && s = []) then i :: s else s)
+    | Is_empty -> (is_closed, s)
+    | Pop -> ( (is_closed, match s with [] -> s | _ :: s' -> s'))
+    | Close -> (true, s)
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Push i -> Res (result unit exn, protect (fun d -> Mpsc_queue.push d i) d)
+    | Pop -> Res (result (option int) exn, protect Mpsc_queue.pop d)
+    | Push_head i ->
+        Res (result unit exn, protect (fun d -> Mpsc_queue.push_head d i) d)
+    | Is_empty -> Res (result bool exn, protect Mpsc_queue.is_empty d)
+    | Close -> Res (result unit exn, protect Mpsc_queue.close d)
+
+  let postcond c ((is_closed, s) : state) res =
+    match (c, res) with
+    | Push _, Res ((Result (Unit, Exn), _), res) ->
+        if is_closed then res = Error Mpsc_queue.Closed else res = Ok ()
+    | Push_head _, Res ((Result (Unit, Exn), _), res) ->
+        if is_closed && s = [] then res = Error Mpsc_queue.Closed
+        else res = Ok ()
+    | Pop, Res ((Result (Option Int, Exn), _), res) -> (
+        match s with
+        | [] ->
+            if is_closed then res = Error Mpsc_queue.Closed else res = Ok None
+        | x :: _ -> res = Ok (Some x))
+    | Is_empty, Res ((Result (Bool, Exn), _), res) ->
+        if is_closed && s = [] then res = Error Mpsc_queue.Closed
+        else res = Ok (s = [])
+    | Close, Res ((Result (Unit, Exn), _), res) ->
+        if is_closed then res = Error Mpsc_queue.Closed else res = Ok ()
+    | _, _ -> false
+end
+
+module MPSC_seq = STM_sequential.Make (MPSCConf)
+module MPSC_dom = STM_domain.Make (MPSCConf)
+
+(* [arb_cmds_par] differs in what each triple component generates:
+   "Consumer domain" cmds can't be [Push] (but can be [Pop], [Is_empty], [Close] or [Push_head]),
+   "producer domain" cmds can't be [Push_head] or [Pop] (but can be [Push], [Is_empty] or [Close]). *)
+let arb_cmds_par =
+  MPSC_dom.arb_triple 20 12 MPSCConf.arb_cmd MPSCConf.arb_cmd
+    MPSCConf.producer_cmd
+
+(* A parallel agreement test - w/repeat and retries combined *)
+let agree_test_par_asym ~count ~name =
+  let rep_count = 50 in
+  Test.make ~retries:10 ~count ~name arb_cmds_par (fun triple ->
+      assume (MPSC_dom.all_interleavings_ok triple);
+      repeat rep_count MPSC_dom.agree_prop_par_asym triple)
+
+let () =
+  let count = 1000 in
+  QCheck_base_runner.run_tests_main
+    [
+      MPSC_seq.agree_test ~count ~name:"STM Lockfree.Mpsc_queue test sequential";
+      agree_test_par_asym ~count ~name:"STM Lockfree.Mpsc_queue test parallel";
+      MPSC_dom.neg_agree_test_par ~count
+        ~name:"STM Lockfree.Mpsc_queue test parallel, negative";
+    ]

test/spsc_queue/dune

@@ -15,3 +15,10 @@
  (name qcheck_spsc_queue)
  (libraries lockfree qcheck "qcheck-alcotest")
  (modules qcheck_spsc_queue))
+
+(test
+ (name stm_spsc_queue)
+ (modules stm_spsc_queue)
+ (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))

test/spsc_queue/stm_spsc_queue.ml

@@ -0,0 +1,87 @@
+(** Sequential and Parallel model-based tests of spsc_queue *)
+
+open QCheck
+open STM
+open Util
+module Spsc_queue = Lockfree.Spsc_queue
+
+module SPSCConf = struct
+  type cmd = Push of int | Pop
+
+  let show_cmd c =
+    match c with Push i -> "Push " ^ string_of_int i | Pop -> "Pop"
+
+  type state = int * int list
+  type sut = int Spsc_queue.t
+
+  let producer_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd (Gen.map (fun i -> Push i) int_gen)
+
+  let consumer_cmd _s = QCheck.make ~print:show_cmd (Gen.return Pop)
+
+  let arb_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (Gen.oneof [ Gen.return Pop; Gen.map (fun i -> Push i) int_gen ])
+
+  let size_exponent = 4
+  let max_size = Int.shift_left 1 size_exponent
+  let init_state = (0, [])
+  let init_sut () = Spsc_queue.create ~size_exponent
+  let cleanup _ = ()
+
+  let next_state c (n, s) =
+    match c with
+    | Push i -> if n = max_size then (n, s) else (n + 1, i :: s)
+    | Pop -> (
+        match List.rev s with [] -> (0, s) | _ :: s' -> (n - 1, List.rev s'))
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Push i -> Res (result unit exn, protect (fun d -> Spsc_queue.push d i) d)
+    | Pop -> Res (result (option int) exn, protect Spsc_queue.pop d)
+
+  let postcond c ((n, s) : state) res =
+    match (c, res) with
+    | Push _, Res ((Result (Unit, Exn), _), res) -> (
+        match res with
+        | Error Spsc_queue.Full -> n = max_size
+        | Ok () -> n < max_size
+        | _ -> false)
+    | Pop, Res ((Result (Option Int, Exn), _), res) -> (
+        match (res, List.rev s) with
+        | Ok None, [] -> true
+        | Ok (Some j), x :: _ -> x = j
+        | _ -> false)
+    | _, _ -> false
+end
+
+module SPSC_seq = STM_sequential.Make (SPSCConf)
+module SPSC_dom = STM_domain.Make (SPSCConf)
+
+(* [arb_cmds_par] differs in what each triple component generates:
+   "Producer domain" cmds can't be [Pop], "consumer domain" cmds can only be [Pop]. *)
+let arb_cmds_par =
+  SPSC_dom.arb_triple 20 12 SPSCConf.producer_cmd SPSCConf.producer_cmd
+    SPSCConf.consumer_cmd
+
+(* A parallel agreement test - w/repeat and retries combined *)
+let agree_test_par_asym ~count ~name =
+  let rep_count = 20 in
+  Test.make ~retries:10 ~count ~name arb_cmds_par (fun triple ->
+      assume (SPSC_dom.all_interleavings_ok triple);
+      repeat rep_count SPSC_dom.agree_prop_par_asym triple)
+
+let () =
+  let count = 1000 in
+  QCheck_base_runner.run_tests_main
+    [
+      SPSC_seq.agree_test ~count ~name:"STM Lockfree.Spsc_queue test sequential";
+      agree_test_par_asym ~count ~name:"STM Lockfree.Spsc_queue test parallel";
+      (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *)
+      SPSC_dom.neg_agree_test_par ~count
+        ~name:"STM Lockfree.Spsc_queue test parallel, negative";
+    ]

test/treiber_stack/dune

@@ -13,3 +13,10 @@
  (name qcheck_treiber_stack)
  (libraries lockfree qcheck qcheck-alcotest)
  (modules qcheck_treiber_stack))
+
+(test
+ (name stm_treiber_stack)
+ (modules stm_treiber_stack)
+ (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))