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
|
open Lin
module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
module M = Internal.Make(Spec) [@alert "-internal"]
include M
let alloc_callback _src =
Thread.yield ();
None
let yield_tracker =
Gc.Memprof.{ null_tracker with alloc_minor = alloc_callback;
alloc_major = alloc_callback; }
(* Note: On purpose we use
- a non-tail-recursive function and
- an (explicit) allocation in the loop body
since both trigger statistically significant more thread issues/interleaving *)
let rec interp_thread sut cs = match cs with
| [] -> []
| c::cs ->
Thread.yield ();
let res = Spec.run c sut in
(c,res)::interp_thread sut cs
let arb_cmds_triple = arb_cmds_triple
(* Linearization property based on [Thread] *)
let lin_prop (seq_pref, cmds1, cmds2) =
let sut = Spec.init () in
let obs1, obs2 = ref (Ok []), ref (Ok []) in
(* Gc.Memprof.{start,stop} raises Failure on OCaml 5.0 and 5.1 *)
(try ignore (Gc.Memprof.start ~sampling_rate:1e-1 ~callstack_size:0 yield_tracker) with Failure _ -> ());
let pref_obs = interp_plain sut seq_pref in
let wait = ref true in
let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_thread sut cmds1) with exn -> Error exn) () in
let th2 = Thread.create (fun () -> wait := false; obs2 := try Ok (interp_thread sut cmds2) with exn -> Error exn) () in
Thread.join th1;
Thread.join th2;
(try Gc.Memprof.stop () with Failure _ -> ());
Spec.cleanup sut;
let obs1 = match !obs1 with Ok v -> ref v | Error exn -> raise exn in
let obs2 = match !obs2 with Ok v -> ref v | Error exn -> raise exn in
let seq_sut = Spec.init () in
(* we reuse [check_seq_cons] to linearize and interpret sequentially *)
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)
(* Common magic constants *)
let rep_count = 3 (* No. of repetitions of the non-deterministic property *)
let retries = 25 (* Additional factor of repetition during shrinking *)
let lin_test ~count ~name =
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
end
module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))
|
