Source file STM_thread.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
open STM

module MakeExt (Spec: SpecExt) = struct

  open Util
  open QCheck
  open Internal.Make(Spec)
    [@alert "-internal"]

  exception ThreadNotFinished

  let arb_cmds_triple = arb_cmds_triple

  let alloc_callback _src =
    Thread.yield ();
    None

  let yield_tracker =
    Gc.Memprof.{ null_tracker with alloc_minor = alloc_callback;
                                   alloc_major = alloc_callback; }

  (* [interp_sut_res] specialized for [Threads] *)
  let rec interp_sut_res sut cs = match cs with
    | [] -> []
    | c::cs ->
       Thread.yield ();
       let res = Spec.run c sut in
       (c,res)::interp_sut_res sut cs

  (* Concurrent agreement property based on [Threads] *)
  let agree_prop_conc (seq_pref,cmds1,cmds2) =
    let sut = Spec.init_sut () in
    let obs1,obs2 = ref (Error ThreadNotFinished), ref (Error ThreadNotFinished) 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 = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
    let wait = ref true in
    let th1 = Thread.create (fun () -> Spec.wrap_cmd_seq @@ fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_sut_res sut cmds1) with exn -> Error exn) () in
    let th2 = Thread.create (fun () -> Spec.wrap_cmd_seq @@ fun () -> wait := false; obs2 := try Ok (interp_sut_res 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 -> v | Error exn -> raise exn in
    let obs2 = match !obs2 with Ok v -> v | Error exn -> raise exn 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)

  (* 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 seq_len = 20  (* max length of the sequential prefix *)
  let par_len = 12  (* max length of the parallel cmd lists *)

  let agree_test_conc ~count ~name =
    (* a bigger [rep_count] for [Threads] as it is more difficult to trigger a problem *)
    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 ((seq_pref,cmds1,cmds2) as triple) ->
         assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
         repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *)

  let neg_agree_test_conc ~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 ((seq_pref,cmds1,cmds2) as triple) ->
         assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
         repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *)
end

module Make (Spec: Spec) =
  MakeExt (struct
    include SpecDefaults
    include Spec
  end)