Source file STM_domain.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
130
131
132
133
open STM

module MakeExt (Spec: SpecExt) = struct

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

  let check_obs = check_obs
  let all_interleavings_ok (seq_pref,cmds1,cmds2) =
    all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state
  let arb_cmds_triple = arb_cmds_triple
  let arb_triple = arb_triple
  let arb_triple_asym seq_len par_len arb0 arb1 arb2 =
    let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in
    set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple

  (* operate over arrays to avoid needless allocation underway *)
  let interp_sut_res 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_par seq_pref cmds1 cmds2 =
    let sut = Spec.init_sut () in
    let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
    let barrier = Atomic.make 2 in
    let main cmds () =
      Spec.wrap_cmd_seq @@ fun () ->
      Atomic.decr barrier;
      while Atomic.get barrier <> 0 do Domain.cpu_relax() done;
      try Ok (interp_sut_res 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
    let ()   = Spec.cleanup sut in
    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

  let agree_prop_par (seq_pref,cmds1,cmds2) =
    let pref_obs, obs1, obs2 = run_par seq_pref cmds1 cmds2 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)

  let stress_prop_par (seq_pref,cmds1,cmds2) =
    let _ = run_par seq_pref cmds1 cmds2 in
    true

  let agree_prop_par_asym (seq_pref, cmds1, cmds2) =
    let sut = Spec.init_sut () in
    let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
    let wait = Atomic.make 2 in
    let child_dom =
      Domain.spawn (fun () ->
          Spec.wrap_cmd_seq @@ fun () ->
          Atomic.decr wait;
          while Atomic.get wait <> 0 do Domain.cpu_relax() done;
          try Ok (interp_sut_res sut cmds2) with exn -> Error exn)
    in
    let parent_obs =
      Spec.wrap_cmd_seq @@ fun () ->
      Atomic.decr wait;
      while Atomic.get wait <> 0 do Domain.cpu_relax() done;
      try Ok (interp_sut_res sut cmds1) with exn -> Error exn in
    let child_obs = Domain.join child_dom in
    let () = Spec.cleanup sut in
    let parent_obs = match parent_obs with Ok v -> v | Error exn -> raise exn in
    let child_obs = match child_obs with Ok v -> v | Error exn -> raise exn in
    check_obs pref_obs parent_obs child_obs Spec.init_state
      || Test.fail_reportf "  Results incompatible with linearized model:\n\n%s"
         @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false
           (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
           (pref_obs,parent_obs,child_obs)

  (* Common magic constants *)
  let rep_count = 25 (* No. of repetitions of the non-deterministic property *)
  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 agree_test_par ~count ~name =
    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 triple ->
         assume (all_interleavings_ok triple);
         repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)

  let stress_test_par ~count ~name =
    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 triple ->
         assume (all_interleavings_ok triple);
         repeat rep_count stress_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)

  let neg_agree_test_par ~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 triple ->
         assume (all_interleavings_ok triple);
         repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)

  let agree_test_par_asym ~count ~name =
    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 triple ->
         assume (all_interleavings_ok triple);
         repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)

  let neg_agree_test_par_asym ~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 triple ->
         assume (all_interleavings_ok triple);
         repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)
end

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