Skip to content

Commit b7a78e9

Browse files
lyrmlyrm
committed
Add multicoretest tests for current data structures.
1 parent 9abc664 commit b7a78e9

File tree

11 files changed

+380
-47
lines changed

11 files changed

+380
-47
lines changed

‎CHANGES.md‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,14 @@
22

33
All notable changes to this project will be documented in this file.
44

5-
## 0.3.1
5+
## Not released
6+
7+
* Add STM tests for current data structures (@lyrm, @jmid)
8+
9+
## 0.3.1
610

711
* Rework dscheck integration to work with utop (@lyrm)
8-
* Add OCaml 4 compatability (@sudha247)
12+
* Add OCaml 4 compatability (@sudha247)
913
* Add STM ws_deque tests (@jmid, @lyrm)
1014

1115
## 0.3.0

‎lockfree.opam‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ depends: [
1717
"qcheck-alcotest" {with-test & >= "0.18.1"}
1818
"alcotest" {with-test & >= "1.6.0"}
1919
"yojson" {>= "2.0.2"}
20-
"dscheck" {with-test & >= "0.0.1"}
20+
"dscheck" {with-test & >= "0.1.0"}
2121
]
2222
depopts: []
2323
build: ["dune" "build" "-p" name "-j" jobs]

‎test/michael_scott_queue/dune‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,10 @@
1313
(name qcheck_michael_scott_queue)
1414
(libraries lockfree qcheck qcheck-alcotest)
1515
(modules qcheck_michael_scott_queue))
16+
17+
(test
18+
(name stm_michael_scott_queue)
19+
(modules stm_michael_scott_queue)
20+
(libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
21+
(action
22+
(run %{test} --verbose)))

‎test/michael_scott_queue/stm_michael_scott_queue.ml‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
(** Sequential and Parallel model-based tests of michael_scott_queue *)
2+
3+
open QCheck
4+
open STM
5+
module Ms_queue = Lockfree.Michael_scott_queue
6+
7+
module MSQConf = struct
8+
type cmd = Push of int | Pop | Is_empty
9+
10+
let show_cmd c =
11+
match c with
12+
| Push i -> "Push " ^ string_of_int i
13+
| Pop -> "Pop"
14+
| Is_empty -> "Is_empty"
15+
16+
type state = int list
17+
type sut = int Ms_queue.t
18+
19+
let arb_cmd _s =
20+
let int_gen = Gen.nat in
21+
QCheck.make ~print:show_cmd
22+
(Gen.oneof
23+
[
24+
Gen.map (fun i -> Push i) int_gen;
25+
Gen.return Pop;
26+
Gen.return Is_empty;
27+
])
28+
29+
let init_state = []
30+
let init_sut () = Ms_queue.create ()
31+
let cleanup _ = ()
32+
33+
let next_state c s =
34+
match c with
35+
| Push i -> i :: s
36+
| Pop -> ( match List.rev s with [] -> s | _ :: s' -> List.rev s')
37+
| Is_empty -> s
38+
39+
let precond _ _ = true
40+
41+
let run c d =
42+
match c with
43+
| Push i -> Res (unit, Ms_queue.push d i)
44+
| Pop -> Res (option int, Ms_queue.pop d)
45+
| Is_empty -> Res (bool, Ms_queue.is_empty d)
46+
47+
let postcond c (s : state) res =
48+
match (c, res) with
49+
| Push _, Res ((Unit, _), _) -> true
50+
| Pop, Res ((Option Int, _), res) -> (
51+
match List.rev s with [] -> res = None | j :: _ -> res = Some j)
52+
| Is_empty, Res ((Bool, _), res) -> res = (s = [])
53+
| _, _ -> false
54+
end
55+
56+
module MSQ_seq = STM_sequential.Make (MSQConf)
57+
module MSQ_dom = STM_domain.Make (MSQConf)
58+
59+
let () =
60+
let count = 500 in
61+
QCheck_base_runner.run_tests_main
62+
[
63+
MSQ_seq.agree_test ~count
64+
~name:"STM Lockfree.Michael_scott_queue test sequential";
65+
MSQ_dom.agree_test_par ~count
66+
~name:"STM Lockfree.Michael_scott_queue test parallel";
67+
]

‎test/mpsc_queue/dune‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,10 @@
1010
(name qcheck_mpsc_queue)
1111
(libraries lockfree qcheck qcheck-alcotest)
1212
(modules qcheck_mpsc_queue))
13+
14+
(test
15+
(name stm_mpsc_queue)
16+
(modules stm_mpsc_queue)
17+
(libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
18+
(action
19+
(run %{test} --verbose)))

‎test/mpsc_queue/stm_mpsc_queue.ml‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
(** Sequential and Parallel model-based tests of mpsc_queue *)
2+
3+
open QCheck
4+
open STM
5+
open Util
6+
module Mpsc_queue = Lockfree.Mpsc_queue
7+
8+
module MPSCConf = struct
9+
type cmd = Push of int | Pop | Push_head of int | Is_empty | Close
10+
11+
let show_cmd c =
12+
match c with
13+
| Push i -> "Push " ^ string_of_int i
14+
| Pop -> "Pop"
15+
| Push_head i -> "Push_head" ^ string_of_int i
16+
| Is_empty -> "Is_empty"
17+
| Close -> "Close"
18+
19+
type state = bool * int list
20+
type sut = int Mpsc_queue.t
21+
22+
let producer_cmd _s =
23+
let int_gen = Gen.nat in
24+
QCheck.make ~print:show_cmd
25+
(Gen.oneof
26+
[
27+
Gen.map (fun i -> Push i) int_gen;
28+
Gen.return Is_empty;
29+
Gen.return Close;
30+
])
31+
32+
let arb_cmd _s =
33+
let int_gen = Gen.nat in
34+
QCheck.make ~print:show_cmd
35+
(Gen.oneof
36+
[
37+
Gen.return Pop;
38+
Gen.map (fun i -> Push_head i) int_gen;
39+
Gen.return Is_empty;
40+
Gen.return Close;
41+
])
42+
43+
let init_state = (false, [])
44+
let init_sut () = Mpsc_queue.create ()
45+
let cleanup _ = ()
46+
47+
let next_state c (is_closed, s) =
48+
match c with
49+
| Push i ->
50+
(is_closed, if not is_closed then i :: List.rev s |> List.rev else s)
51+
| Push_head i -> (is_closed, if not (is_closed && s = []) then i :: s else s)
52+
| Is_empty -> (is_closed, s)
53+
| Pop -> ( (is_closed, match s with [] -> s | _ :: s' -> s'))
54+
| Close -> (true, s)
55+
56+
let precond _ _ = true
57+
58+
let run c d =
59+
match c with
60+
| Push i -> Res (result unit exn, protect (fun d -> Mpsc_queue.push d i) d)
61+
| Pop -> Res (result (option int) exn, protect Mpsc_queue.pop d)
62+
| Push_head i ->
63+
Res (result unit exn, protect (fun d -> Mpsc_queue.push_head d i) d)
64+
| Is_empty -> Res (result bool exn, protect Mpsc_queue.is_empty d)
65+
| Close -> Res (result unit exn, protect Mpsc_queue.close d)
66+
67+
let postcond c ((is_closed, s) : state) res =
68+
match (c, res) with
69+
| Push _, Res ((Result (Unit, Exn), _), res) ->
70+
if is_closed then res = Error Mpsc_queue.Closed else res = Ok ()
71+
| Push_head _, Res ((Result (Unit, Exn), _), res) ->
72+
if is_closed && s = [] then res = Error Mpsc_queue.Closed
73+
else res = Ok ()
74+
| Pop, Res ((Result (Option Int, Exn), _), res) -> (
75+
match s with
76+
| [] ->
77+
if is_closed then res = Error Mpsc_queue.Closed else res = Ok None
78+
| x :: _ -> res = Ok (Some x))
79+
| Is_empty, Res ((Result (Bool, Exn), _), res) ->
80+
if is_closed && s = [] then res = Error Mpsc_queue.Closed
81+
else res = Ok (s = [])
82+
| Close, Res ((Result (Unit, Exn), _), res) ->
83+
if is_closed then res = Error Mpsc_queue.Closed else res = Ok ()
84+
| _, _ -> false
85+
end
86+
87+
module MPSC_seq = STM_sequential.Make (MPSCConf)
88+
module MPSC_dom = STM_domain.Make (MPSCConf)
89+
90+
(* [arb_cmds_par] differs in what each triple component generates:
91+
"Consumer domain" cmds can't be [Push] (but can be [Pop], [Is_empty], [Close] or [Push_head]),
92+
"producer domain" cmds can't be [Push_head] or [Pop] (but can be [Push], [Is_empty] or [Close]). *)
93+
let arb_cmds_par =
94+
MPSC_dom.arb_triple 20 12 MPSCConf.arb_cmd MPSCConf.arb_cmd
95+
MPSCConf.producer_cmd
96+
97+
(* A parallel agreement test - w/repeat and retries combined *)
98+
let agree_test_par_asym ~count ~name =
99+
let rep_count = 50 in
100+
Test.make ~retries:10 ~count ~name arb_cmds_par (fun triple ->
101+
assume (MPSC_dom.all_interleavings_ok triple);
102+
repeat rep_count MPSC_dom.agree_prop_par_asym triple)
103+
104+
let () =
105+
let count = 1000 in
106+
QCheck_base_runner.run_tests_main
107+
[
108+
MPSC_seq.agree_test ~count ~name:"STM Lockfree.Mpsc_queue test sequential";
109+
agree_test_par_asym ~count ~name:"STM Lockfree.Mpsc_queue test parallel";
110+
MPSC_dom.neg_agree_test_par ~count
111+
~name:"STM Lockfree.Mpsc_queue test parallel, negative";
112+
]

‎test/spsc_queue/dune‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,3 +15,10 @@
1515
(name qcheck_spsc_queue)
1616
(libraries lockfree qcheck "qcheck-alcotest")
1717
(modules qcheck_spsc_queue))
18+
19+
(test
20+
(name stm_spsc_queue)
21+
(modules stm_spsc_queue)
22+
(libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
23+
(action
24+
(run %{test} --verbose)))

‎test/spsc_queue/stm_spsc_queue.ml‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
(** Sequential and Parallel model-based tests of spsc_queue *)
2+
3+
open QCheck
4+
open STM
5+
open Util
6+
module Spsc_queue = Lockfree.Spsc_queue
7+
8+
module SPSCConf = struct
9+
type cmd = Push of int | Pop
10+
11+
let show_cmd c =
12+
match c with Push i -> "Push " ^ string_of_int i | Pop -> "Pop"
13+
14+
type state = int * int list
15+
type sut = int Spsc_queue.t
16+
17+
let producer_cmd _s =
18+
let int_gen = Gen.nat in
19+
QCheck.make ~print:show_cmd (Gen.map (fun i -> Push i) int_gen)
20+
21+
let consumer_cmd _s = QCheck.make ~print:show_cmd (Gen.return Pop)
22+
23+
let arb_cmd _s =
24+
let int_gen = Gen.nat in
25+
QCheck.make ~print:show_cmd
26+
(Gen.oneof [ Gen.return Pop; Gen.map (fun i -> Push i) int_gen ])
27+
28+
let size_exponent = 4
29+
let max_size = Int.shift_left 1 size_exponent
30+
let init_state = (0, [])
31+
let init_sut () = Spsc_queue.create ~size_exponent
32+
let cleanup _ = ()
33+
34+
let next_state c (n, s) =
35+
match c with
36+
| Push i -> if n = max_size then (n, s) else (n + 1, i :: s)
37+
| Pop -> (
38+
match List.rev s with [] -> (0, s) | _ :: s' -> (n - 1, List.rev s'))
39+
40+
let precond _ _ = true
41+
42+
let run c d =
43+
match c with
44+
| Push i -> Res (result unit exn, protect (fun d -> Spsc_queue.push d i) d)
45+
| Pop -> Res (result (option int) exn, protect Spsc_queue.pop d)
46+
47+
let postcond c ((n, s) : state) res =
48+
match (c, res) with
49+
| Push _, Res ((Result (Unit, Exn), _), res) -> (
50+
match res with
51+
| Error Spsc_queue.Full -> n = max_size
52+
| Ok () -> n < max_size
53+
| _ -> false)
54+
| Pop, Res ((Result (Option Int, Exn), _), res) -> (
55+
match (res, List.rev s) with
56+
| Ok None, [] -> true
57+
| Ok (Some j), x :: _ -> x = j
58+
| _ -> false)
59+
| _, _ -> false
60+
end
61+
62+
module SPSC_seq = STM_sequential.Make (SPSCConf)
63+
module SPSC_dom = STM_domain.Make (SPSCConf)
64+
65+
(* [arb_cmds_par] differs in what each triple component generates:
66+
"Producer domain" cmds can't be [Pop], "consumer domain" cmds can only be [Pop]. *)
67+
let arb_cmds_par =
68+
SPSC_dom.arb_triple 20 12 SPSCConf.producer_cmd SPSCConf.producer_cmd
69+
SPSCConf.consumer_cmd
70+
71+
(* A parallel agreement test - w/repeat and retries combined *)
72+
let agree_test_par_asym ~count ~name =
73+
let rep_count = 20 in
74+
Test.make ~retries:10 ~count ~name arb_cmds_par (fun triple ->
75+
assume (SPSC_dom.all_interleavings_ok triple);
76+
repeat rep_count SPSC_dom.agree_prop_par_asym triple)
77+
78+
let () =
79+
let count = 1000 in
80+
QCheck_base_runner.run_tests_main
81+
[
82+
SPSC_seq.agree_test ~count ~name:"STM Lockfree.Spsc_queue test sequential";
83+
agree_test_par_asym ~count ~name:"STM Lockfree.Spsc_queue test parallel";
84+
(* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *)
85+
SPSC_dom.neg_agree_test_par ~count
86+
~name:"STM Lockfree.Spsc_queue test parallel, negative";
87+
]

‎test/treiber_stack/dune‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,10 @@
1313
(name qcheck_treiber_stack)
1414
(libraries lockfree qcheck qcheck-alcotest)
1515
(modules qcheck_treiber_stack))
16+
17+
(test
18+
(name stm_treiber_stack)
19+
(modules stm_treiber_stack)
20+
(libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
21+
(action
22+
(run %{test} --verbose)))

0 commit comments

Comments
 (0)