Source file lin_effect.ml

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))