Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

STM: Catch exceptions in next_state for nicer UX #400

Merged
merged 10 commits into from
Oct 11, 2023
1 change: 1 addition & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
52 changes: 24 additions & 28 deletions lib/STM.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand All @@ -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]
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand Down
21 changes: 15 additions & 6 deletions lib/STM.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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. *)
Expand Down Expand Up @@ -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. *)
Expand All @@ -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"]

Expand Down
16 changes: 12 additions & 4 deletions lib/STM_domain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
7 changes: 5 additions & 2 deletions lib/STM_sequential.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion lib/STM_thread.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
7 changes: 7 additions & 0 deletions test/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
83 changes: 83 additions & 0 deletions test/stm_next_state_exc.ml
Original file line number Diff line number Diff line change
@@ -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