1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
open STM
module MakeExt (Spec: SpecExt) = struct
open Util
open QCheck
open Internal.Make(Spec)
[@alert "-internal"]
let check_obs = check_obs
let all_interleavings_ok (seq_pref,cmds1,cmds2) =
all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state
let arb_cmds_triple = arb_cmds_triple
let arb_triple = arb_triple
let arb_triple_asym seq_len par_len arb0 arb1 arb2 =
let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in
set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple
(* operate over arrays to avoid needless allocation underway *)
let interp_sut_res sut cs =
let cs_arr = Array.of_list cs in
let res_arr = Array.map (fun c -> Domain.cpu_relax(); Spec.run c sut) cs_arr in
List.combine cs (Array.to_list res_arr)
let run_par seq_pref cmds1 cmds2 =
let sut = Spec.init_sut () in
let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
let barrier = Atomic.make 2 in
let main cmds () =
Spec.wrap_cmd_seq @@ fun () ->
Atomic.decr barrier;
while Atomic.get barrier <> 0 do Domain.cpu_relax() done;
try Ok (interp_sut_res sut cmds) with exn -> Error exn
in
let dom1 = Domain.spawn (main cmds1) in
let dom2 = Domain.spawn (main cmds2) in
let obs1 = Domain.join dom1 in
let obs2 = Domain.join dom2 in
let () = Spec.cleanup sut in
let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
pref_obs, obs1, obs2
let agree_prop_par (seq_pref,cmds1,cmds2) =
let pref_obs, obs1, obs2 = run_par seq_pref cmds1 cmds2 in
check_obs pref_obs obs1 obs2 Spec.init_state
|| Test.fail_reportf " Results incompatible with linearized model\n\n%s"
@@ print_triple_vertical ~fig_indent:5 ~res_width:35
(fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
(pref_obs,obs1,obs2)
let stress_prop_par (seq_pref,cmds1,cmds2) =
let _ = run_par seq_pref cmds1 cmds2 in
true
let agree_prop_par_asym (seq_pref, cmds1, cmds2) =
let sut = Spec.init_sut () in
let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
let wait = Atomic.make 2 in
let child_dom =
Domain.spawn (fun () ->
Spec.wrap_cmd_seq @@ fun () ->
Atomic.decr wait;
while Atomic.get wait <> 0 do Domain.cpu_relax() done;
try Ok (interp_sut_res sut cmds2) with exn -> Error exn)
in
let parent_obs =
Spec.wrap_cmd_seq @@ fun () ->
Atomic.decr wait;
while Atomic.get wait <> 0 do Domain.cpu_relax() done;
try Ok (interp_sut_res sut cmds1) with exn -> Error exn in
let child_obs = Domain.join child_dom in
let () = Spec.cleanup sut in
let parent_obs = match parent_obs with Ok v -> v | Error exn -> raise exn in
let child_obs = match child_obs with Ok v -> v | Error exn -> raise exn in
check_obs pref_obs parent_obs child_obs Spec.init_state
|| Test.fail_reportf " Results incompatible with linearized model:\n\n%s"
@@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false
(fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
(pref_obs,parent_obs,child_obs)
(* Common magic constants *)
let rep_count = 25 (* No. of repetitions of the non-deterministic property *)
let retries = 10 (* Additional factor of repetition during shrinking *)
let seq_len = 20 (* max length of the sequential prefix *)
let par_len = 12 (* max length of the parallel cmd lists *)
let agree_test_par ~count ~name =
let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
Test.make ~retries ~max_gen ~count ~name
(arb_cmds_triple seq_len par_len)
(fun triple ->
assume (all_interleavings_ok triple);
repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
let stress_test_par ~count ~name =
let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
Test.make ~retries ~max_gen ~count ~name
(arb_cmds_triple seq_len par_len)
(fun triple ->
assume (all_interleavings_ok triple);
repeat rep_count stress_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
let neg_agree_test_par ~count ~name =
let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
Test.make_neg ~retries ~max_gen ~count ~name
(arb_cmds_triple seq_len par_len)
(fun triple ->
assume (all_interleavings_ok triple);
repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
let agree_test_par_asym ~count ~name =
let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
Test.make ~retries ~max_gen ~count ~name
(arb_cmds_triple seq_len par_len)
(fun triple ->
assume (all_interleavings_ok triple);
repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)
let neg_agree_test_par_asym ~count ~name =
let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
Test.make_neg ~retries ~max_gen ~count ~name
(arb_cmds_triple seq_len par_len)
(fun triple ->
assume (all_interleavings_ok triple);
repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)
end
module Make (Spec: Spec) =
MakeExt (struct
include SpecDefaults
include Spec
end)
|
