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
|
open Lin
module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
module M = Internal.Make(Spec) [@alert "-internal"]
include M
(* operate over arrays to avoid needless allocation underway *)
let interp 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_parallel (seq_pref,cmds1,cmds2) =
let sut = Spec.init () in
let pref_obs = interp sut seq_pref in
let barrier = Atomic.make 2 in
let main cmds () =
Atomic.decr barrier;
while Atomic.get barrier <> 0 do Domain.cpu_relax () done;
try Ok (interp 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
Spec.cleanup sut ;
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)
(* Linearization property based on [Domain] and an Atomic flag *)
let lin_prop (seq_pref,cmds1,cmds2) =
let pref_obs,obs1,obs2 = run_parallel (seq_pref,cmds1,cmds2) in
let seq_sut = Spec.init () in
check_seq_cons pref_obs obs1 obs2 seq_sut []
|| QCheck.Test.fail_reportf " Results incompatible with sequential execution\n\n%s"
@@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
(fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
(pref_obs,obs1,obs2)
(* "Don't crash under parallel usage" property *)
let stress_prop (seq_pref,cmds1,cmds2) =
let _ = run_parallel (seq_pref,cmds1,cmds2) in
true
(* Common magic constants *)
let rep_count = 50 (* No. of repetitions of the non-deterministic property *)
let retries = 3 (* Additional factor of repetition during shrinking *)
let lin_test ~count ~name =
M.lin_test ~rep_count ~count ~retries ~name ~lin_prop
let neg_lin_test ~count ~name =
neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop
let stress_test ~count ~name = (* Note: magic constants differ for this one *)
M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:stress_prop
end
module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))
|
