Merge pull request #400 from ocaml-multicore/catch-next-state-exc

STM: Catch exceptions in next_state for nicer UX

Author: jmid

CHANGES.md

@@ -2,6 +2,7 @@
 
 ## Next
 
+- #400: Catch and delay exceptions in `STM`'s `next_state` for a nicer UX
 - #387: Reduce needless allocations in `Lin`'s sequential consistency
   search, as part of an `Out_channel` test cleanup
 - #379: Extend the set of `Util.Pp` pretty-printers and teach them to

lib/STM.ml

@@ -118,7 +118,8 @@ struct
            then return []
            else
              (arb s).gen >>= fun c ->
-             (gen_cmds arb (Spec.next_state c s) (fuel-1)) >>= fun cs ->
+             let s' = try Spec.next_state c s with _ -> s in
+             (gen_cmds arb s' (fuel-1)) >>= fun cs ->
              return (c::cs))
     (** A fueled command list generator.
         Accepts a state parameter to enable state-dependent [cmd] generation. *)
@@ -127,7 +128,7 @@ struct
       | [] -> true
       | c::cs ->
         Spec.precond c s &&
-        let s' = Spec.next_state c s in
+        let s' = try Spec.next_state c s with _ -> s in
         cmds_ok s' cs
 
     (* This is an adaption of [QCheck.Shrink.list_spine]
@@ -180,66 +181,61 @@ struct
       | c::cs ->
         let res = Spec.run c sut in
         let b   = Spec.postcond c s res in
-        let s'  = Spec.next_state c s in
         if b
         then
+          let s'  = Spec.next_state c s in
           match check_disagree s' sut cs with
           | None -> None
           | Some rest -> Some ((c,res)::rest)
         else Some [c,res]
 
-    let check_and_next (c,res) s =
-      let b  = Spec.postcond c s res in
-      let s' = Spec.next_state c s in
-      b,s'
-
     (* checks that all interleavings of a cmd triple satisfies all preconditions *)
     let rec all_interleavings_ok pref cs1 cs2 s =
       match pref with
       | c::pref' ->
         Spec.precond c s &&
-        let s' = Spec.next_state c s in
+        let s' = try Spec.next_state c s with _ -> s in
         all_interleavings_ok pref' cs1 cs2 s'
       | [] ->
         match cs1,cs2 with
         | [],[] -> true
         | [],c2::cs2' ->
           Spec.precond c2 s &&
-          let s' = Spec.next_state c2 s in
+          let s' = try Spec.next_state c2 s with _ -> s in
           all_interleavings_ok pref cs1 cs2' s'
         | c1::cs1',[] ->
           Spec.precond c1 s &&
-          let s' = Spec.next_state c1 s in
+          let s' = try Spec.next_state c1 s with _ -> s in
           all_interleavings_ok pref cs1' cs2 s'
         | c1::cs1',c2::cs2' ->
           (Spec.precond c1 s &&
-           let s' = Spec.next_state c1 s in
+           let s' = try Spec.next_state c1 s with _ -> s in
            all_interleavings_ok pref cs1' cs2 s')
           &&
           (Spec.precond c2 s &&
-           let s' = Spec.next_state c2 s in
+           let s' = try Spec.next_state c2 s with _ -> s in
            all_interleavings_ok pref cs1 cs2' s')
 
     let rec check_obs pref cs1 cs2 s =
       match pref with
-      | p::pref' ->
-        let b,s' = check_and_next p s in
-        b && check_obs pref' cs1 cs2 s'
+      | (c,res)::pref' ->
+        let b = Spec.postcond c s res in
+        b && check_obs pref' cs1 cs2 (Spec.next_state c s)
       | [] ->
         match cs1,cs2 with
         | [],[] -> true
-        | [],p2::cs2' ->
-          let b,s' = check_and_next p2 s in
-          b && check_obs pref cs1 cs2' s'
-        | p1::cs1',[] ->
-          let b,s' = check_and_next p1 s in
-          b && check_obs pref cs1' cs2 s'
-        | p1::cs1',p2::cs2' ->
-          (let b1,s' = check_and_next p1 s in
-           b1 && check_obs pref cs1' cs2 s')
+        | [],(c2,res2)::cs2' ->
+          let b = Spec.postcond c2 s res2 in
+          b && check_obs pref cs1 cs2' (Spec.next_state c2 s)
+        | (c1,res1)::cs1',[] ->
+          let b = Spec.postcond c1 s res1 in
+          b && check_obs pref cs1' cs2 (Spec.next_state c1 s)
+        | (c1,res1)::cs1',(c2,res2)::cs2' ->
+          (let b1 = Spec.postcond c1 s res1 in
+           b1 && check_obs pref cs1' cs2 (Spec.next_state c1 s))
           ||
-          (let b2,s' = check_and_next p2 s in
-           b2 && check_obs pref cs1 cs2' s')
+          (let b2 = Spec.postcond c2 s res2 in
+           b2 && check_obs pref cs1 cs2' (Spec.next_state c2 s))
 
     let gen_cmds_size gen s size_gen = Gen.sized_size size_gen (gen_cmds gen s)
 
@@ -312,7 +308,7 @@ struct
       let gen_triple =
         Gen.(seq_pref_gen >>= fun seq_pref ->
              int_range 2 (2*par_len) >>= fun dbl_plen ->
-             let spawn_state = List.fold_left (fun st c -> Spec.next_state c st) Spec.init_state seq_pref in
+             let spawn_state = List.fold_left (fun st c -> try Spec.next_state c st with _ -> st) Spec.init_state seq_pref in
              let par_len1 = dbl_plen/2 in
              let par_gen1 = gen_cmds_size arb1 spawn_state (return par_len1) in
              let par_gen2 = gen_cmds_size arb2 spawn_state (return (dbl_plen - par_len1)) in

lib/STM.mli

@@ -99,7 +99,7 @@ sig
   val next_state : cmd -> state -> state
   (** [next_state c s] expresses how interpreting the command [c] moves the
       model's internal state machine from the state [s] to the next state.
-      Ideally a [next_state] function is pure. *)
+      Ideally a [next_state] function is pure, as it is run more than once.  *)
 
   val init_sut : unit -> sut
   (** Initialize the system under test. *)
@@ -139,7 +139,8 @@ sig
 
     val cmds_ok : Spec.state -> Spec.cmd list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
-        Accepts the initial state and the command sequence as parameters.  *)
+        Accepts the initial state and the command sequence as parameters.
+        [cmds_ok] catches and ignores exceptions arising from {!next_state}.  *)
 
     val arb_cmds : Spec.state -> Spec.cmd list arbitrary
     (** A generator of command sequences. Accepts the initial state as parameter. *)
@@ -168,16 +169,22 @@ sig
     val gen_cmds_size : (Spec.state -> Spec.cmd arbitrary) -> Spec.state -> int Gen.t -> Spec.cmd list Gen.t
     (** [gen_cmds_size arb state gen_int] generates a program of size generated
         by [gen_int] using [arb] to generate [cmd]s according to the current
-        state. [state] is the starting state. *)
+        state. [state] is the starting state.
+        [gen_cmds_size] catches and ignores generation-time exceptions arising
+        from {!next_state}. *)
 
     val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
-        sequential commands and at most [par_len] parallel commands each. *)
+        sequential commands and at most [par_len] parallel commands each.
+        [arb_cmds_triple] catches and ignores generation-time exceptions arising
+        from {!next_state}. *)
 
     val all_interleavings_ok : Spec.cmd list -> Spec.cmd list -> Spec.cmd list -> Spec.state -> bool
     (** [all_interleavings_ok seq spawn0 spawn1 state] checks that
         preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
-        possible interleavings and starting with [state] *)
+        possible interleavings and starting with [state].
+        [all_interleavings_ok] catches and ignores exceptions arising from
+        {!next_state}. *)
 
     val shrink_triple : (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) Shrink.t
     (** [shrink_triple arb0 arb1 arb2] is a {!QCheck.Shrink.t} for programs (triple of list of [cmd]s) that is specialized for each part of the program. *)
@@ -186,7 +193,9 @@ sig
     (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         The three [cmd] components are generated with [arb0], [arb1], and [arb2], respectively.
-        Each of these take the model state as a parameter. *)
+        Each of these take the model state as a parameter.
+        [arb_triple] catches and ignores generation-time exceptions arising
+        from {!next_state}. *)
 end
   [@@alert internal "This module is exposed for internal uses only, its API may change at any time"]
 

lib/STM_domain.mli

@@ -9,24 +9,32 @@ module Make : functor (Spec : STM.Spec) ->
     val all_interleavings_ok : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
     (** [all_interleavings_ok (seq,spawn0,spawn1)] checks that
         preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
-        possible interleavings and starting with {!Spec.init_state}. *)
+        possible interleavings and starting with {!Spec.init_state}.
+        [all_interleavings_ok] catches and ignores exceptions arising from
+        {!next_state}. *)
 
     val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
-        All [cmds] are generated with {!Spec.arb_cmd}. *)
+        All [cmds] are generated with {!Spec.arb_cmd}.
+        [arb_cmds_triple] catches and ignores generation-time exceptions arising
+        from {!Spec.next_state}. *)
 
     val arb_triple : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
     (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         The three {!Spec.cmd} components are generated with [arb0], [arb1], and [arb2], respectively.
-        Each of these take the model state as a parameter. *)
+        Each of these take the model state as a parameter.
+        [arb_triple] catches and ignores generation-time exceptions arising
+        from {!Spec.next_state}. *)
 
     val arb_triple_asym : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
     (** [arb_triple_asym seq_len par_len arb0 arb1 arb2] creates a triple [cmd]
         generator like {!arb_triple}. It differs in that the resulting printer
         is asymmetric, printing [arb1]'s result below [arb0]'s result and
-        printing [arb2]'s result to the right of [arb1]'s result. *)
+        printing [arb2]'s result to the right of [arb1]'s result.
+        [arb_triple_asym] catches and ignores generation-time exceptions arising
+        from {!Spec.next_state}. *)
 
     val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system {!Spec.sut}

lib/STM_sequential.mli

@@ -4,10 +4,13 @@ module Make : functor (Spec : STM.Spec) ->
   sig
     val cmds_ok : Spec.state -> Spec.cmd list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
-        Accepts the initial state and the command sequence as parameters.  *)
+        Accepts the initial state and the command sequence as parameters.
+        [cmds_ok] catches and ignores exceptions arising from {!next_state}.  *)
 
     val arb_cmds : Spec.state -> Spec.cmd list QCheck.arbitrary
-    (** A generator of {!Spec.cmd} sequences. Accepts the initial state as a parameter. *)
+    (** A generator of {!Spec.cmd} sequences. Accepts the initial state as a parameter.
+        [arb_cmds] catches and ignores generation-time exceptions arising from
+        {!Spec.next_state}. *)
 
     val agree_prop : Spec.cmd list -> bool
     (** The agreement property: the command sequence [cs] yields the same observations

lib/STM_thread.mli

@@ -7,7 +7,9 @@ module Make : functor (Spec : STM.Spec) ->
     val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len conc_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [conc_len] concurrent commands each.
-        All [cmds] are generated with {!Spec.arb_cmd}. *)
+        All [cmds] are generated with {!Spec.arb_cmd}.
+        [arb_cmds_triple] catches and ignores generation-time exceptions arising
+        from {!Spec.next_state}. *)
 
     val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut]

test/dune

@@ -92,3 +92,10 @@
  (libraries qcheck-stm.sequential threads.posix)
  (action
   (with-accepted-exit-codes 1 (run ./%{test} --verbose --seed 229109553))))
+
+(test
+ (name stm_next_state_exc)
+ (modules stm_next_state_exc)
+ (package qcheck-stm)
+ (libraries qcheck-stm.sequential qcheck-stm.domain)
+ (enabled_if (>= %{ocaml_version} 5)))

test/stm_next_state_exc.ml

@@ -0,0 +1,83 @@
+open QCheck
+open STM
+
+exception Random_next_state_failure
+
+(** This is a variant of refs to test for exceptions in next_state *)
+
+module RConf =
+struct
+
+  type cmd = Get | Set of int | Add of int
+
+  let pp_cmd par fmt x =
+    let open Util.Pp in
+    match x with
+    | Get -> cst0 "Get" fmt
+    | Set x -> cst1 pp_int "Set" par fmt x
+    | Add x -> cst1 pp_int "Add" par fmt x
+
+  let show_cmd = Util.Pp.to_show pp_cmd
+
+  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 -> if i>70 then raise Random_next_state_failure; s+i
+
+  type sut = int ref
+
+  let init_sut () = ref 0
+
+  let cleanup _ = ()
+
+  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) -> r = s
+    | Set _, Res ((Unit,_),_)
+    | Add _, Res ((Unit,_),_) -> true
+    | _,_ -> false
+end
+
+module RT_int = STM.Internal.Make(RConf)[@alert "-internal"]
+module RT_seq = STM_sequential.Make(RConf)
+module RT_dom = STM_domain.Make(RConf)
+
+let () = QCheck_base_runner.set_seed 301717275
+let _ =
+  QCheck_base_runner.run_tests ~verbose:true
+    [RT_int.consistency_test ~count:1000 ~name:"STM test exception during next_state consistency"]
+let () = (* raises Test_error not handled by neg_agree_test so handled explicitly *)
+  let name = "STM test exception during next_state sequential" in
+  try
+    Test.check_exn (RT_seq.agree_test ~count:1000 ~name);
+    Printf.printf "%s unexpectedly succeeded\n%!" name;
+  with Test.Test_error (err_name,_,Random_next_state_failure,_) ->
+    assert (err_name = name);
+    Printf.printf "%s failed with Random_next_state_failure as expected\n%!" name
+let () = (* raises Test_error not handled by neg_agree_test so handled explicitly *)
+  let name = "STM test exception during next_state parallel" in
+  try
+    Test.check_exn (RT_dom.agree_test_par ~count:1000 ~name);
+    Printf.printf "%s unexpectedly succeeded\n%!" name;
+  with Test.Test_error (err_name,_,Random_next_state_failure,_) ->
+    assert (err_name = name);
+    Printf.printf "%s failed with Random_next_state_failure as expected\n%!" name