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
|
open Lin
(** Definitions for Effect interpretation *)
(* Scheduler adapted from https://kcsrk.info/slides/retro_effects_simcorp.pdf *)
open Effect
open Effect.Deep
type _ t += Fork : (unit -> unit) -> unit t
| Yield : unit t
let enqueue k q = Queue.push k q
let dequeue q =
if Queue.is_empty q
then () (*Finished*)
else continue (Queue.pop q) ()
let start_sched main =
(* scheduler's queue of continuations *)
let q = Queue.create () in
let rec spawn = fun (type res) (f : unit -> res) ->
match_with f ()
{ retc = (fun _v -> dequeue q); (* value case *)
exnc = (fun e -> (Stdlib.print_string (Printexc.to_string e); raise e));
effc = (fun (type a) (e : a t) -> match e with
| Yield -> Some (fun (k : (a, _) continuation) -> enqueue k q; dequeue q)
| Fork f -> Some (fun (k : (a, _) continuation) -> enqueue k q; spawn f)
| _ -> None ) }
in
spawn main
(* short hands *)
let fork f = perform (Fork f)
let yield () = perform Yield
module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
(** A refined [CmdSpec] specification with generator-controlled [Yield] effects *)
module EffSpec
= struct
open QCheck
type t = Spec.t
let init = Spec.init
let cleanup = Spec.cleanup
type cmd = SchedYield | UserCmd of Spec.cmd
let show_cmd c = match c with
| SchedYield -> "<SchedYield>"
| UserCmd c -> Spec.show_cmd c
let gen_cmd =
(Gen.frequency
[(3,Gen.return SchedYield);
(5,Gen.map (fun c -> UserCmd c) Spec.gen_cmd)])
let shrink_cmd c = match c with
| SchedYield -> Iter.empty
| UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c)
type res = SchedYieldRes | UserRes of Spec.res
let show_res r = match r with
| SchedYieldRes -> "<SchedYieldRes>"
| UserRes r -> Spec.show_res r
let equal_res r r' = match r,r' with
| SchedYieldRes, SchedYieldRes -> true
| UserRes r, UserRes r' -> Spec.equal_res r r'
| _, _ -> false
let run c sut = match c with
| SchedYield ->
(yield (); SchedYieldRes)
| UserCmd uc ->
let res = Spec.run uc sut in
UserRes res
end
module EffTest = Internal.Make(EffSpec) [@alert "-internal"]
let arb_cmds_triple = EffTest.arb_cmds_triple
let filter_res rs = List.filter (fun (c,_) -> c <> EffSpec.SchedYield) rs
let rec interp sut cs = match cs with
| [] -> []
| c::cs ->
let res = EffSpec.run c sut in
(c,res)::interp sut cs
(* Concurrent agreement property based on effect-handler scheduler *)
let lin_prop (seq_pref,cmds1,cmds2) =
let sut = Spec.init () in
(* exclude [Yield]s from sequential prefix *)
let pref_obs = EffTest.interp_plain sut (List.filter (fun c -> c <> EffSpec.SchedYield) seq_pref) in
let obs1,obs2 = ref (Ok []), ref (Ok []) in
let main () =
fork (fun () -> let tmp1 = try Ok (interp sut cmds1) with exn -> Error exn in obs1 := tmp1);
fork (fun () -> let tmp2 = try Ok (interp sut cmds2) with exn -> Error exn in obs2 := tmp2); in
let () = start_sched main in
let () = Spec.cleanup sut in
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
(* exclude [Yield]s from sequential executions when searching for an interleaving *)
EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
|| QCheck.Test.fail_reportf " Results incompatible with linearized model\n\n%s"
@@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
(fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r))
(pref_obs,!obs1,!obs2)
(* Common magic constants *)
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 lin_test ~count ~name =
let arb_cmd_triple = EffTest.arb_cmds_triple seq_len par_len in
QCheck.Test.make ~count ~retries ~name arb_cmd_triple lin_prop
let neg_lin_test ~count ~name =
let arb_cmd_triple = EffTest.arb_cmds_triple seq_len par_len in
QCheck.Test.make_neg ~count ~retries ~name arb_cmd_triple lin_prop
end
module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))
|
