Merge pull request #295 from ocaml-multicore/try-to-cleanup

Run cleanup in the presence of exceptions

Author: jmid

CHANGES.md

@@ -1,5 +1,11 @@
 # Changes
 
+## Next version
+
+- ensure `cleanup` is run in the presence of exceptions in
+  - `STM_sequential.agree_prop` and `STM_domain.agree_prop_par`
+  - `Lin_thread.lin_prop` and `Lin_effect.lin_prop`
+
 ## 0.1.1
 
 - #263: Cleanup resources after each domain-based `Lin` test

lib/STM_domain.ml

@@ -26,9 +26,9 @@ module Make (Spec: Spec) = struct
     let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) 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
-    let ()   = Spec.cleanup sut 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

lib/STM_sequential.ml

@@ -18,8 +18,9 @@ module Make (Spec: Spec) = struct
   let agree_prop cs =
     assume (cmds_ok Spec.init_state cs);
     let sut = Spec.init_sut () in (* reset system's state *)
-    let res = check_disagree Spec.init_state sut cs in
+    let res = try Ok (check_disagree Spec.init_state sut cs) with exn -> Error exn in
     let ()  = Spec.cleanup sut in
+    let res = match res with Ok res -> res | Error exn -> raise exn in
     match res with
     | None -> true
     | Some trace ->

lib/lin_effect.ml

@@ -96,12 +96,14 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     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 [], ref [] in
+    let obs1,obs2 = ref (Ok []), ref (Ok []) in
     let main () =
-      fork (fun () -> let tmp1 = interp sut cmds1 in obs1 := tmp1);
-      fork (fun () -> let tmp2 = interp sut cmds2 in obs2 := tmp2); in
+      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 []

lib/lin_thread.ml

@@ -20,14 +20,16 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
   (* Linearization property based on [Thread] *)
   let lin_prop (seq_pref, cmds1, cmds2) =
     let sut = Spec.init () in
-    let obs1, obs2 = ref [], ref [] in
+    let obs1, obs2 = ref (Ok []), ref (Ok []) in
     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 := interp_thread sut cmds1) () in
-    let th2 = Thread.create (fun () -> wait := false; obs2 := interp_thread sut cmds2) () 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;
     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 []

test/cleanup.ml renamed to test/cleanup_lin.ml

@@ -0,0 +1,90 @@
+open QCheck
+open STM
+
+exception Cleanup_without_init
+exception Already_cleaned
+exception Random_postcond_failure
+
+type status = Inited | Cleaned
+
+let status = ref None (* global ref to keep track of cleanup/init status *)
+
+(** This is a variant of refs to test for missing and double cleanup *)
+
+module RConf =
+struct
+
+  type cmd =
+    | Get
+    | Set of int
+    | Add of int [@@deriving show { with_path = false }]
+
+  let gen_cmd =
+    let int_gen = Gen.nat in
+      (Gen.oneof
+         [Gen.return Get;
+	  Gen.map (fun i -> Set i) int_gen;
+	  Gen.map (fun i -> Add i) int_gen;
+         ])
+  let arb_cmd _ = make ~print:show_cmd gen_cmd
+
+  type state = int
+
+  let init_state = 0
+
+  let next_state c s = match c with
+    | Get -> s
+    | Set i -> i
+    | Add i -> s+i
+
+  type sut = int ref
+
+  let init_sut () =
+    assert (!status = None || !status = Some Cleaned);
+    status := Some Inited;
+    ref 0
+
+  let cleanup _ = match !status with
+    | None -> raise Cleanup_without_init
+    | Some Cleaned -> raise Already_cleaned
+    | Some Inited -> status := Some Cleaned
+
+  let run c r = match c with
+    | Get   -> Res (int, !r)
+    | Set i -> Res (unit, (r:=i))
+    | Add i -> Res (unit, let old = !r in r := i + old) (* buggy: not atomic *)
+
+  let precond _ _ = true
+
+  let postcond c (s:state) res = match c,res with
+    | Get,   Res ((Int,_),r) -> if r>70 then raise Random_postcond_failure; r = s
+    | Set _, Res ((Unit,_),_)
+    | Add _, Res ((Unit,_),_) -> true
+    | _,_ -> false
+end
+
+module RT_seq = STM_sequential.Make(RConf)
+module RT_dom = STM_domain.Make(RConf)
+
+let rand = Random.State.make_self_init ()
+let i = ref 0
+;;
+for _i=1 to 250 do
+  try
+    Test.check_exn ~rand (RT_seq.agree_test ~count:1000 ~name:"STM ensure cleanup test sequential")
+  with _e -> incr i; assert (!status = Some Cleaned);
+done;
+assert (!i = 250);
+Printf.printf "STM ensure cleanup: sequential test OK\n%!";
+(* reset things *)
+i := 0;
+status := None;
+for _i=1 to 100 do
+  try
+    Test.check_exn ~rand
+      (Test.make ~count:1000 ~name:"STM ensure cleanup test parallel"
+         (RT_dom.arb_cmds_triple 20 12) RT_dom.agree_prop_par) (* without retries *)
+  with _e -> incr i; assert (!status = Some Cleaned);
+done;
+assert (!i = 100);
+Printf.printf "STM ensure cleanup: parallel test OK\n%!";

test/cleanup_stm.ml

@@ -8,13 +8,21 @@
 
 
 (test
- (name cleanup)
- (modules cleanup)
+ (name cleanup_lin)
+ (modules cleanup_lin)
  (package qcheck-lin)
  (libraries qcheck-lin.domain)
  (preprocess (pps ppx_deriving.show ppx_deriving.eq))
  (action (run ./%{test} --verbose)))
 
+(test
+ (name cleanup_stm)
+ (modules cleanup_stm)
+ (package qcheck-stm)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq))
+ (action (run ./%{test} --verbose)))
+
 (rule
  (enabled_if (= %{arch_sixtyfour} true))
  (action (copy mutable_set_v5.expected.64 mutable_set_v5.expected)))