diff --git a/doc/example/dune b/doc/example/dune index 761d9b86d..09899b094 100644 --- a/doc/example/dune +++ b/doc/example/dune @@ -11,5 +11,5 @@ (executable (name stm_tests) (modules stm_tests) - (libraries qcheck-stm) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) diff --git a/doc/example/stm_tests.ml b/doc/example/stm_tests.ml index 30cef071c..064967d7c 100644 --- a/doc/example/stm_tests.ml +++ b/doc/example/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** parallel STM tests of Hashtbl *) @@ -57,9 +57,10 @@ struct | _ -> false end -module HTest = STM.Make(HashtblModel) +module HT_seq = STM_sequential.Make(HashtblModel) +module HT_dom = STM_domain.Make(HashtblModel) ;; QCheck_base_runner.run_tests_main (let count = 200 in - [HTest.agree_test ~count ~name:"Hashtbl test"; - HTest.agree_test_par ~count ~name:"Hashtbl test"; ]) + [HT_seq.agree_test ~count ~name:"Hashtbl test"; + HT_dom.agree_test_par ~count ~name:"Hashtbl test"; ]) diff --git a/doc/paper-examples/dune b/doc/paper-examples/dune index 761d9b86d..09899b094 100644 --- a/doc/paper-examples/dune +++ b/doc/paper-examples/dune @@ -11,5 +11,5 @@ (executable (name stm_tests) (modules stm_tests) - (libraries qcheck-stm) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) diff --git a/doc/paper-examples/stm_tests.ml b/doc/paper-examples/stm_tests.ml index ce9866892..2a5d123d9 100644 --- a/doc/paper-examples/stm_tests.ml +++ b/doc/paper-examples/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** parallel STM tests of Hashtbl *) @@ -68,10 +68,11 @@ struct | _ -> false end -module HTest = STM.Make(HashtblModel) +module HT_seq = STM_sequential.Make(HashtblModel) +module HT_dom = STM_domain.Make(HashtblModel) ;; QCheck_base_runner.run_tests_main (let count = 200 in - [HTest.agree_test ~count ~name:"Hashtbl test"; - HTest.agree_test_par ~count ~name:"Hashtbl test"; + [HT_seq.agree_test ~count ~name:"Hashtbl test"; + HT_dom.agree_test_par ~count ~name:"Hashtbl test"; ]) diff --git a/lib/STM.mli b/lib/STM.mli deleted file mode 100644 index 03fecad1c..000000000 --- a/lib/STM.mli +++ /dev/null @@ -1,186 +0,0 @@ -(** A state machine framework supporting both sequential and parallel model-based testing. *) - - -include module type of Util -(** Sub-module of various utility functions *) - -(** Extensible type to represent result values *) -type 'a ty = .. - -(** A range of constructors to represent built-in types *) -type _ ty += - | Unit : unit ty - | Bool : bool ty - | Char : char ty - | Int : int ty - | Int32 : int32 ty - | Int64 : int64 ty - | Float : float ty - | String : string ty - | Bytes : bytes ty - | Exn : exn ty - | Option : 'a ty -> 'a option ty - | Result : 'a ty * 'b ty -> ('a, 'b) result ty - | List : 'a ty -> 'a list ty - | Array : 'a ty -> 'a array ty - | Seq : 'a ty -> 'a Seq.t ty - -type 'a ty_show = 'a ty * ('a -> string) -(** Combinator type to represent an OCaml type along with an associated [to_string] function *) - -val unit : unit ty_show -(** Combinator to represent the [unit] type *) - -val bool : bool ty_show -(** Combinator to represent the [bool] type *) - -val char : char ty_show -(** Combinator to represent the [char] type *) - -val int : int ty_show -(** Combinator to represent the [int] type *) - -val int32 : int32 ty_show -(** Combinator to represent the [int32] type *) - -val int64 : int64 ty_show -(** Combinator to represent the [int64] type *) - -val float : float ty_show -(** Combinator to represent the [float] type *) - -val string : string ty_show -(** Combinator to represent the [string] type *) - -val bytes : bytes ty_show -(** Combinator to represent the [bytes] type *) - -val option : 'a ty_show -> 'a option ty_show -(** [option t] builds a [t option] type representation *) - -val exn : exn ty_show -(** Combinator to represent the [exception] type *) - -val result : 'a ty_show -> 'b ty_show -> ('a,'b) Result.t ty_show -(** [result a b] builds an [(a,b) Result.t] type representation *) - -val list : 'a ty_show -> 'a list ty_show -(** [list t] builds a [t list] type representation *) - -val array : 'a ty_show -> 'a array ty_show -(** [array t] builds a [t array] type representation *) - -val seq : 'a ty_show -> 'a Seq.t ty_show -(** [seq t] builds a [t Seq.t] type representation *) - -type res = - Res : 'a ty_show * 'a -> res - -val show_res : res -> string - -(** The specification of a state machine. *) -module type StmSpec = -sig - type cmd - (** The type of commands *) - - type state - (** The type of the model's state *) - - type sut - (** The type of the system under test *) - - val arb_cmd : state -> cmd QCheck.arbitrary - (** A command generator. Accepts a state parameter to enable state-dependent [cmd] generation. *) - - val show_cmd : cmd -> string - (** [show_cmd c] returns a string representing the command [c]. *) - - val init_state : state - (** The model's initial state. *) - - val next_state : cmd -> state -> state - (** Move the internal state machine to the next state. *) - - val init_sut : unit -> sut - (** Initialize the system under test. *) - - val cleanup : sut -> unit - (** Utility function to clean up the [sut] after each test instance, - e.g., for closing sockets, files, or resetting global parameters*) - - val precond : cmd -> state -> bool - (** [precond c s] expresses preconditions for command [c]. - This is useful, e.g., to prevent the shrinker from breaking invariants when minimizing - counterexamples. *) - - val run : cmd -> sut -> res - (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *) - - val postcond : cmd -> state -> res -> bool - (** [postcond c s res] checks whether [res] arising from interpreting the - command [c] over the system under test with [run] agrees with the - model's result. - Note: [s] is in this case the model's state prior to command execution. *) -end - -(** A functor to build model-based tests from a state-machine specification module *) -module Make(Spec : StmSpec) - : 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. *) - - val arb_cmds : Spec.state -> Spec.cmd list QCheck.arbitrary - (** A generator of command sequences. Accepts the initial state as parameter. *) - - val consistency_test : count:int -> name:string -> QCheck.Test.t - (** A consistency test that generates a number of [cmd] sequences and - checks that all contained [cmd]s satisfy the precondition [precond]. - Accepts two labeled parameters: - [count] is the test count and [name] is the printed test name. *) - - val interp_agree : Spec.state -> Spec.sut -> Spec.cmd list -> bool - (** Checks agreement between the model and the system under test - (stops early, thanks to short-circuit Boolean evaluation). *) - - val agree_prop : Spec.cmd list -> bool - (** The agreement property: the command sequence [cs] yields the same observations - when interpreted from the model's initial state and the [sut]'s initial state. - Cleans up after itself by calling [Spec.cleanup] *) - - val agree_test : count:int -> name:string -> QCheck.Test.t - (** An actual agreement test (for convenience). Accepts two labeled parameters: - [count] is the test count and [name] is the printed test name. *) - - val neg_agree_test : count:int -> name:string -> QCheck.Test.t - (** An negative agreement test (for convenience). Accepts two labeled parameters: - [count] is the test count and [name] is the printed test name. *) - - val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * res) list - (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut] - and returns the list of corresponding [cmd] and result pairs. *) - - val check_obs : (Spec.cmd * res) list -> (Spec.cmd * res) list -> (Spec.cmd * res) list -> Spec.state -> bool - (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref] - and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *) - - 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_cmds_par 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. *) - - val arb_cmds_par : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary - (** [arb_cmds_par seq_len par_len] generates a [cmd] triple with at most [seq_len] - sequential commands and at most [par_len] parallel commands each. *) - - val agree_prop_par : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool - (** Parallel agreement property based on [Domain] *) - - val agree_test_par : count:int -> name:string -> QCheck.Test.t - (** Parallel agreement test based on [Domain] which combines [repeat] and [~retries] *) - - val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t - (** Negative parallel agreement test based on [Domain] which combines [repeat] and [~retries] *) -end diff --git a/lib/STM_base.ml b/lib/STM_base.ml new file mode 100644 index 000000000..e9370ade3 --- /dev/null +++ b/lib/STM_base.ml @@ -0,0 +1,6 @@ +(** Base module for specifying STM tests *) + +module STM_internal = STM_internal +module STM_spec = STM_spec +include STM_spec +include Util diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml new file mode 100644 index 000000000..868b3d83d --- /dev/null +++ b/lib/STM_domain.ml @@ -0,0 +1,53 @@ +open STM_base + +module Make (Spec: STM_spec.Spec) = struct + + open Util + open QCheck + open STM_internal.Make(Spec) + + let check_obs = check_obs + let arb_cmds_par = arb_cmds_par + let arb_triple = arb_triple + let shrink_triple = shrink_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 agree_prop_par (seq_pref,cmds1,cmds2) = + assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); + let sut = Spec.init_sut () in + let pref_obs = interp_sut_res sut seq_pref in + let wait = Atomic.make true in + let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in + 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 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 + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (STM_spec.show_res r)) + (pref_obs,obs1,obs2) + + let agree_test_par ~count ~name = + let rep_count = 25 in + let seq_len,par_len = 20,12 in + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries:15 ~max_gen ~count ~name + (arb_cmds_par seq_len par_len) + (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *) + + let neg_agree_test_par ~count ~name = + let rep_count = 25 in + let seq_len,par_len = 20,12 in + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make_neg ~retries:15 ~max_gen ~count ~name + (arb_cmds_par seq_len par_len) + (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *) + end diff --git a/lib/STM_domain.mli b/lib/STM_domain.mli new file mode 100644 index 000000000..6cbf68a8d --- /dev/null +++ b/lib/STM_domain.mli @@ -0,0 +1,32 @@ +(** Module for building parallel STM tests over [Domain]s *) + +module Make : functor (Spec : STM_base.Spec) -> + sig + val check_obs : (Spec.cmd * STM_base.res) list -> (Spec.cmd * STM_base.res) list -> (Spec.cmd * STM_base.res) list -> Spec.state -> bool + (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref] + and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *) + + 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 [cmd] components are generated with [arb0], [arb1], and [arb2], respectively. + Each of these take the model state as a parameter. *) + + val shrink_triple : (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.Shrink.t + (** [shrink_triple arb0 arb1 arb2] is a [Shrinker.t] for programs (triple of list of [cmd]s) that is specialized for each part of the program. *) + + val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM_base.res) list + (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut] + and returns the list of corresponding [cmd] and result pairs. *) + + val agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + (** Parallel agreement property based on [Domain] *) + + val agree_test_par : count:int -> name:string -> QCheck.Test.t + (** Parallel agreement test based on [Domain] which combines [repeat] and [~retries] *) + + val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t + (** An negative agreement test (for convenience). Accepts two labeled parameters: + [count] is the test count and [name] is the printed test name. *) + + end diff --git a/lib/STM.ml b/lib/STM_internal.ml similarity index 51% rename from lib/STM.ml rename to lib/STM_internal.ml index 81ac76c3d..cd2e7cb74 100644 --- a/lib/STM.ml +++ b/lib/STM_internal.ml @@ -1,93 +1,6 @@ open QCheck -include Util -type 'a ty = .. - -type _ ty += - | Unit : unit ty - | Bool : bool ty - | Char : char ty - | Int : int ty - | Int32 : int32 ty - | Int64 : int64 ty - | Float : float ty - | String : string ty - | Bytes : bytes ty - | Exn : exn ty - | Option : 'a ty -> 'a option ty - | Result : 'a ty * 'b ty -> ('a, 'b) result ty - | List : 'a ty -> 'a list ty - | Array : 'a ty -> 'a array ty - | Seq : 'a ty -> 'a Seq.t ty - -type 'a ty_show = 'a ty * ('a -> string) - -let unit = (Unit, fun () -> "()") -let bool = (Bool, string_of_bool) -let char = (Char, fun c -> Printf.sprintf "%C" c) -let int = (Int, string_of_int) -let int32 = (Int32, Int32.to_string) -let int64 = (Int64, Int64.to_string) -let float = (Float, Float.to_string) -let string = (String, fun s -> Printf.sprintf "%S" s) -let bytes = (Bytes, fun b -> Printf.sprintf "%S" (Bytes.to_string b)) -let option spec = - let (ty,show) = spec in - (Option ty, QCheck.Print.option show) -let exn = (Exn, Printexc.to_string) - -let show_result show_ok show_err = function - | Ok x -> Printf.sprintf "Ok (%s)" (show_ok x) - | Error y -> Printf.sprintf "Error (%s)" (show_err y) - -let result spec_ok spec_err = - let (ty_ok, show_ok) = spec_ok in - let (ty_err, show_err) = spec_err in - (Result (ty_ok, ty_err), show_result show_ok show_err) - -let list spec = - let (ty,show) = spec in - (List ty, QCheck.Print.list show) - -let array spec = - let (ty,show) = spec in - (Array ty, QCheck.Print.array show) - -let seq spec = - let (ty,show) = spec in - (Seq ty, fun s -> QCheck.Print.list show (List.of_seq s)) - -type res = - Res : 'a ty_show * 'a -> res - -let show_res (Res ((_,show), v)) = show v - -(** The specification of a state machine. *) -module type StmSpec = -sig - type cmd - type state - type sut - - val arb_cmd : state -> cmd arbitrary - val show_cmd : cmd -> string - - val init_state : state - val next_state : cmd -> state -> state - - val init_sut : unit -> sut - val cleanup : sut -> unit - - val precond : cmd -> state -> bool - val run : cmd -> sut -> res - val postcond : cmd -> state -> res -> bool -end - - -(** Derives a test framework from a state machine specification. *) -module Make(Spec : StmSpec) = -struct - (** {3 The resulting test framework derived from a state machine specification} *) +module Make(Spec : STM_spec.Spec) = struct let rec gen_cmds arb s fuel = Gen.(if fuel = 0 @@ -140,40 +53,11 @@ struct | Some rest -> Some ((c,res)::rest) else Some [c,res] - let print_seq_trace trace = - List.fold_left - (fun acc (c,r) -> Printf.sprintf "%s\n %s : %s" acc (Spec.show_cmd c) (show_res r)) - "" trace - - let agree_prop = - (fun 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 () = Spec.cleanup sut in - match res with - | None -> true - | Some trace -> - Test.fail_reportf " Results incompatible with model\n%s" - @@ print_seq_trace trace) - - let agree_test ~count ~name = - Test.make ~name ~count (arb_cmds Spec.init_state) agree_prop - - let neg_agree_test ~count ~name = - Test.make_neg ~name ~count (arb_cmds Spec.init_state) agree_prop - 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' - (* 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) - (* checks that all interleavings of a cmd triple satisfies all preconditions *) let rec all_interleavings_ok pref cs1 cs2 s = match pref with @@ -298,93 +182,7 @@ struct 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 triple (return seq_pref) par_gen1 par_gen2) in - make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple + make ~print:(Util.print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple let arb_cmds_par seq_len par_len = arb_triple seq_len par_len Spec.arb_cmd Spec.arb_cmd Spec.arb_cmd - - let agree_prop_par (seq_pref,cmds1,cmds2) = - assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); - let sut = Spec.init_sut () in - let pref_obs = interp_sut_res sut seq_pref in - let wait = Atomic.make true in - let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in - 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 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 - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r)) - (pref_obs,obs1,obs2) - - let agree_test_par ~count ~name = - let rep_count = 25 in - let seq_len,par_len = 20,12 in - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make ~retries:15 ~max_gen ~count ~name - (arb_cmds_par seq_len par_len) - (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *) - - let neg_agree_test_par ~count ~name = - let rep_count = 25 in - let seq_len,par_len = 20,12 in - let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) - Test.make_neg ~retries:15 ~max_gen ~count ~name - (arb_cmds_par seq_len par_len) - (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *) -end - -(** ********************************************************************** *) - -module AddGC(Spec : StmSpec) : StmSpec -= -struct - type cmd = - | GC_minor - | UserCmd of Spec.cmd - - type state = Spec.state - type sut = Spec.sut - - let init_state = Spec.init_state - let init_sut () = Spec.init_sut () - let cleanup sut = Spec.cleanup sut - - let show_cmd c = match c with - | GC_minor -> "" - | UserCmd c -> Spec.show_cmd c - - let gen_cmd s = - (Gen.frequency - [(1,Gen.return GC_minor); - (5,Gen.map (fun c -> UserCmd c) (Spec.arb_cmd s).gen)]) - - let shrink_cmd s c = match c with - | GC_minor -> Iter.empty - | UserCmd c -> - match (Spec.arb_cmd s).shrink with - | None -> Iter.empty (* no shrinker provided *) - | Some shk -> Iter.map (fun c' -> UserCmd c') (shk c) - - let arb_cmd s = make ~print:show_cmd ~shrink:(shrink_cmd s) (gen_cmd s) - - let next_state c s = match c with - | GC_minor -> s - | UserCmd c -> Spec.next_state c s - - let precond c s = match c with - | GC_minor -> true - | UserCmd c -> Spec.precond c s - - let run c s = match c with - | GC_minor -> (Gc.minor (); Res (unit, ())) - | UserCmd c -> Spec.run c s - - let postcond c s r = match c,r with - | GC_minor, Res ((Unit,_),_) -> true - | UserCmd c, r -> Spec.postcond c s r - | _,_ -> false end diff --git a/lib/STM_internal.mli b/lib/STM_internal.mli new file mode 100644 index 000000000..075c4c7db --- /dev/null +++ b/lib/STM_internal.mli @@ -0,0 +1,63 @@ +open QCheck +open STM_spec +(** A revised state machine framework with parallel testing. + This version does not come with built-in GC commands. *) + + +(** Derives a test framework from a state machine specification. *) +module Make : functor (Spec : Spec) -> + sig + (** {3 The resulting test framework derived from a state machine specification} *) + + 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. *) + + val arb_cmds : Spec.state -> Spec.cmd list arbitrary + (** A generator of command sequences. Accepts the initial state as parameter. *) + + val consistency_test : count:int -> name:string -> QCheck.Test.t + (** A consistency test that generates a number of [cmd] sequences and + checks that all contained [cmd]s satisfy the precondition [precond]. + Accepts two labeled parameters: + [count] is the test count and [name] is the printed test name. *) + + val interp_agree : Spec.state -> Spec.sut -> Spec.cmd list -> bool + (** Checks agreement between the model and the system under test + (stops early, thanks to short-circuit Boolean evaluation). *) + + val check_disagree : Spec.state -> Spec.sut -> Spec.cmd list -> (Spec.cmd * res) list option + (** [check_disagree state sut pg] checks that none of the commands present + in [pg] violated the declared postconditions when [pg] is run in [state]. + Return [None] if none of the commands violate its postcondition, and + [Some] list corresponding to the prefix of [pg] ending with the [cmd] + violating its postcondition. *) + + val check_obs : (Spec.cmd * res) list -> (Spec.cmd * res) list -> (Spec.cmd * res) list -> Spec.state -> bool + (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref] + and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *) + + 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. *) + + val arb_cmds_par : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary + (** [arb_cmds_par seq_len par_len] generates a [cmd] triple with at most [seq_len] + sequential commands and at most [par_len] parallel commands each. *) + + 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] *) + + 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 [Shrinker.t] for programs (triple of list of [cmd]s) that is specialized for each part of the program. *) + + val arb_triple : int -> int -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) 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 [cmd] components are generated with [arb0], [arb1], and [arb2], respectively. + Each of these take the model state as a parameter. *) + + end diff --git a/lib/STM_sequential.ml b/lib/STM_sequential.ml new file mode 100644 index 000000000..827329b79 --- /dev/null +++ b/lib/STM_sequential.ml @@ -0,0 +1,35 @@ +open STM_base + +module Make (Spec: STM_spec.Spec) = struct + + open QCheck + open STM_internal.Make(Spec) + + (* re-export some functions *) + let cmds_ok = cmds_ok + let gen_cmds_size = gen_cmds_size + + let print_seq_trace trace = + List.fold_left + (fun acc (c,r) -> Printf.sprintf "%s\n %s : %s" acc (Spec.show_cmd c) (show_res r)) + "" trace + + let agree_prop = + (fun 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 () = Spec.cleanup sut in + match res with + | None -> true + | Some trace -> + Test.fail_reportf " Results incompatible with model\n%s" + @@ print_seq_trace trace) + + let agree_test ~count ~name = + Test.make ~name ~count (arb_cmds Spec.init_state) agree_prop + + let neg_agree_test ~count ~name = + Test.make_neg ~name ~count (arb_cmds Spec.init_state) agree_prop + + end diff --git a/lib/STM_sequential.mli b/lib/STM_sequential.mli new file mode 100644 index 000000000..8384b6eba --- /dev/null +++ b/lib/STM_sequential.mli @@ -0,0 +1,26 @@ +(** Module for building sequential STM tests *) + +module Make : functor (Spec : STM_base.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. *) + + val gen_cmds_size : (Spec.state -> Spec.cmd QCheck.arbitrary) -> Spec.state -> int QCheck.Gen.t -> Spec.cmd list QCheck.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. *) + + val agree_prop : Spec.cmd list -> bool + (** The agreement property: the command sequence [cs] yields the same observations + when interpreted from the model's initial state and the [sut]'s initial state. + Cleans up after itself by calling [Spec.cleanup] *) + + val agree_test : count:int -> name:string -> QCheck.Test.t + (** An actual agreement test (for convenience). Accepts two labeled parameters: + [count] is the test count and [name] is the printed test name. *) + + val neg_agree_test : count:int -> name:string -> QCheck.Test.t + (** An negative agreement test (for convenience). Accepts two labeled parameters: + [count] is the test count and [name] is the printed test name. *) + end diff --git a/lib/STM_spec.ml b/lib/STM_spec.ml new file mode 100644 index 000000000..c9fe841b1 --- /dev/null +++ b/lib/STM_spec.ml @@ -0,0 +1,155 @@ +open QCheck + +type 'a ty = .. + +type _ ty += + | Unit : unit ty + | Bool : bool ty + | Char : char ty + | Int : int ty + | Int32 : int32 ty + | Int64 : int64 ty + | Float : float ty + | String : string ty + | Bytes : bytes ty + | Exn : exn ty + | Option : 'a ty -> 'a option ty + | Result : 'a ty * 'b ty -> ('a, 'b) result ty + | List : 'a ty -> 'a list ty + | Array : 'a ty -> 'a array ty + | Seq : 'a ty -> 'a Seq.t ty + +type 'a ty_show = 'a ty * ('a -> string) + +let unit = (Unit, fun () -> "()") +let bool = (Bool, string_of_bool) +let char = (Char, fun c -> Printf.sprintf "%C" c) +let int = (Int, string_of_int) +let int32 = (Int32, Int32.to_string) +let int64 = (Int64, Int64.to_string) +let float = (Float, Float.to_string) +let string = (String, QCheck.Print.string) +let bytes = (Bytes, fun b -> QCheck.Print.string (Bytes.to_string b)) +let option spec = + let (ty,show) = spec in + (Option ty, QCheck.Print.option show) +let exn = (Exn, Printexc.to_string) + +let show_result show_ok show_err = function + | Ok x -> Printf.sprintf "Ok (%s)" (show_ok x) + | Error y -> Printf.sprintf "Error (%s)" (show_err y) + +let result spec_ok spec_err = + let (ty_ok, show_ok) = spec_ok in + let (ty_err, show_err) = spec_err in + (Result (ty_ok, ty_err), show_result show_ok show_err) +let list spec = + let (ty,show) = spec in + (List ty, QCheck.Print.list show) +let array spec = + let (ty,show) = spec in + (Array ty, QCheck.Print.array show) +let seq spec = + let (ty,show) = spec in + (Seq ty, fun s -> QCheck.Print.list show (List.of_seq s)) + + + +type res = + Res : 'a ty_show * 'a -> res + +let show_res (Res ((_,show), v)) = show v + +(** The specification of a state machine. *) +module type Spec = +sig + type cmd + (** The type of commands *) + + type state + (** The type of the model's state *) + + type sut + (** The type of the system under test *) + + val arb_cmd : state -> cmd arbitrary + (** A command generator. Accepts a state parameter to enable state-dependent [cmd] generation. *) + + val init_state : state + (** The model's initial state. *) + + val show_cmd : cmd -> string + (** [show_cmd c] returns a string representing the command [c]. *) + + val next_state : cmd -> state -> state + (** Move the internal state machine to the next state. *) + + val init_sut : unit -> sut + (** Initialize the system under test. *) + + val cleanup : sut -> unit + (** Utility function to clean up the [sut] after each test instance, + e.g., for closing sockets, files, or resetting global parameters*) + + val precond : cmd -> state -> bool + (** [precond c s] expresses preconditions for command [c]. + This is useful, e.g., to prevent the shrinker from breaking invariants when minimizing + counterexamples. *) + + val run : cmd -> sut -> res + (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *) + + val postcond : cmd -> state -> res -> bool + (** [postcond c s res] checks whether [res] arising from interpreting the + command [c] over the system under test with [run] agrees with the + model's result. + Note: [s] is in this case the model's state prior to command execution. *) +end + +module AddGC(Spec : Spec) : Spec = struct + type cmd = + | GC_minor + | UserCmd of Spec.cmd + + type state = Spec.state + type sut = Spec.sut + + let init_state = Spec.init_state + let init_sut () = Spec.init_sut () + let cleanup sut = Spec.cleanup sut + + let show_cmd c = match c with + | GC_minor -> "" + | UserCmd c -> Spec.show_cmd c + + let gen_cmd s = + (Gen.frequency + [(1,Gen.return GC_minor); + (5,Gen.map (fun c -> UserCmd c) (Spec.arb_cmd s).gen)]) + + let shrink_cmd s c = match c with + | GC_minor -> Iter.empty + | UserCmd c -> + match (Spec.arb_cmd s).shrink with + | None -> Iter.empty (* no shrinker provided *) + | Some shk -> Iter.map (fun c' -> UserCmd c') (shk c) + + let arb_cmd s = make ~print:show_cmd ~shrink:(shrink_cmd s) (gen_cmd s) + + let next_state c s = match c with + | GC_minor -> s + | UserCmd c -> Spec.next_state c s + + let precond c s = match c with + | GC_minor -> true + | UserCmd c -> Spec.precond c s + + let run c s = match c with + | GC_minor -> (Gc.minor (); Res (unit, ())) + | UserCmd c -> Spec.run c s + + let postcond c s r = match c,r with + | GC_minor, Res ((Unit,_),_) -> true + | UserCmd c, r -> Spec.postcond c s r + | _,_ -> false +end diff --git a/lib/STM_spec.mli b/lib/STM_spec.mli new file mode 100644 index 000000000..ed2ec326a --- /dev/null +++ b/lib/STM_spec.mli @@ -0,0 +1,121 @@ +(** Extensible type to represent result values *) +type 'a ty = .. + +(** A range of constructors to represent built-in types *) +type _ ty += + | Unit : unit ty + | Bool : bool ty + | Char : char ty + | Int : int ty + | Int32 : int32 ty + | Int64 : int64 ty + | Float : float ty + | String : string ty + | Bytes : bytes ty + | Exn : exn ty + | Option : 'a ty -> 'a option ty + | Result : 'a ty * 'b ty -> ('a, 'b) result ty + | List : 'a ty -> 'a list ty + | Array : 'a ty -> 'a array ty + | Seq : 'a ty -> 'a Seq.t ty + +type 'a ty_show = 'a ty * ('a -> string) +(** Combinator type to represent an OCaml type along with an associated [to_string] function *) + +val unit : unit ty_show +(** Combinator to represent the [unit] type *) + +val bool : bool ty_show +(** Combinator to represent the [bool] type *) + +val char : char ty_show +(** Combinator to represent the [char] type *) + +val int : int ty_show +(** Combinator to represent the [int] type *) + +val int32 : int32 ty_show +(** Combinator to represent the [int32] type *) + +val int64 : int64 ty_show +(** Combinator to represent the [int64] type *) + +val float : float ty_show +(** Combinator to represent the [float] type *) + +val string : string ty_show +(** Combinator to represent the [string] type *) + +val bytes : bytes ty_show +(** Combinator to represent the [bytes] type *) + +val option : 'a ty_show -> 'a option ty_show +(** [option t] builds a [t option] type representation *) + +val exn : exn ty_show +(** Combinator to represent the [exception] type *) + +val result : 'a ty_show -> 'b ty_show -> ('a,'b) Result.t ty_show +(** [result a b] builds an [(a,b) Result.t] type representation *) + +val list : 'a ty_show -> 'a list ty_show +(** [list t] builds a [t list] type representation *) + +val array : 'a ty_show -> 'a array ty_show +(** [array t] builds a [t array] type representation *) + +val seq : 'a ty_show -> 'a Seq.t ty_show +(** [seq t] builds a [t Seq.t] type representation *) + +type res = + Res : 'a ty_show * 'a -> res + +val show_res : res -> string + +(** The specification of a state machine. *) +module type Spec = +sig + type cmd + (** The type of commands *) + + type state + (** The type of the model's state *) + + type sut + (** The type of the system under test *) + + val arb_cmd : state -> cmd QCheck.arbitrary + (** A command generator. Accepts a state parameter to enable state-dependent [cmd] generation. *) + + val init_state : state + (** The model's initial state. *) + + val show_cmd : cmd -> string + (** [show_cmd c] returns a string representing the command [c]. *) + + val next_state : cmd -> state -> state + (** Move the internal state machine to the next state. *) + + val init_sut : unit -> sut + (** Initialize the system under test. *) + + val cleanup : sut -> unit + (** Utility function to clean up the [sut] after each test instance, + e.g., for closing sockets, files, or resetting global parameters*) + + val precond : cmd -> state -> bool + (** [precond c s] expresses preconditions for command [c]. + This is useful, e.g., to prevent the shrinker from breaking invariants when minimizing + counterexamples. *) + + val run : cmd -> sut -> res + (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *) + + val postcond : cmd -> state -> res -> bool + (** [postcond c s res] checks whether [res] arising from interpreting the + command [c] over the system under test with [run] agrees with the + model's result. + Note: [s] is in this case the model's state prior to command execution. *) +end + +module AddGC : functor (Spec : Spec) -> Spec diff --git a/lib/STM_thread.ml b/lib/STM_thread.ml new file mode 100644 index 000000000..561f4aacb --- /dev/null +++ b/lib/STM_thread.ml @@ -0,0 +1,55 @@ +open STM_base + +module Make (Spec: STM_spec.Spec) = struct + + open Util + open QCheck + open STM_internal.Make(Spec) + + exception ThreadNotFinished + + (* [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) = + assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); + let sut = Spec.init_sut () in + let obs1,obs2 = ref (Error ThreadNotFinished), ref (Error ThreadNotFinished) in + let pref_obs = interp_sut_res sut seq_pref in + let wait = ref true in + let th1 = Thread.create (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 () -> wait := false; obs2 := try Ok (interp_sut_res sut cmds2) with exn -> Error exn) () in + let () = Thread.join th1 in + let () = Thread.join th2 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 + 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) (STM_spec.show_res r)) + (pref_obs,obs1,obs2) + + let agree_test_conc ~count ~name = + (* a bigger [rep_count] for [Threads] as it is more difficult to trigger a problem *) + let rep_count = 100 in + let seq_len,par_len = 20,12 in + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make ~retries:15 ~max_gen ~count ~name + (arb_cmds_par seq_len par_len) + (repeat rep_count agree_prop_conc) (* 100 times each, then 100 * 15 times when shrinking *) + + let neg_agree_test_conc ~count ~name = + let rep_count = 25 in + let seq_len,par_len = 20,12 in + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) + Test.make_neg ~retries:15 ~max_gen ~count ~name + (arb_cmds_par seq_len par_len) + (repeat rep_count agree_prop_conc) (* 25 times each, then 25 * 15 times when shrinking *) + end diff --git a/lib/STM_thread.mli b/lib/STM_thread.mli new file mode 100644 index 000000000..ea1a0ebe8 --- /dev/null +++ b/lib/STM_thread.mli @@ -0,0 +1,21 @@ +(** Module for building concurrent STM tests over [Thread]s *) + +module Make : functor (Spec : STM_base.Spec) -> + sig + exception ThreadNotFinished + + val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM_base.res) list + (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut] + and returns the list of corresponding [cmd] and result pairs. *) + + val agree_prop_conc : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool + (** Concurrent agreement property based on [Thread] *) + + val agree_test_conc : count:int -> name:string -> QCheck.Test.t + (** Concurrent agreement test based on [Thread] which combines [repeat] and [~retries] *) + + val neg_agree_test_conc : count:int -> name:string -> QCheck.Test.t + (** An negative agreement test (for convenience). Accepts two labeled parameters: + [count] is the test count and [name] is the printed test name. *) + + end diff --git a/lib/dune b/lib/dune index 31d992e60..5940f1bb5 100644 --- a/lib/dune +++ b/lib/dune @@ -1,8 +1,26 @@ (library - (name STM) - (public_name qcheck-stm) - (modules STM) - (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util)) + (name STM_base) + (public_name qcheck-stm.base) + (modules STM_base STM_internal STM_spec) + (libraries qcheck-core qcheck-multicoretests-util)) + +(library + (name STM_sequential) + (public_name qcheck-stm.sequential) + (modules STM_sequential) + (libraries qcheck-core STM_base)) + +(library + (name STM_domain) + (public_name qcheck-stm.domain) + (modules STM_domain) + (libraries qcheck-core STM_base)) + +(library + (name STM_thread) + (public_name qcheck-stm.thread) + (modules STM_thread) + (libraries threads qcheck-core STM_base)) (library (name lin) diff --git a/src/array/dune b/src/array/dune index f05e0ae7e..b09719a4d 100644 --- a/src/array/dune +++ b/src/array/dune @@ -12,7 +12,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index 142e3fc7d..ef62d5e9d 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -1,6 +1,5 @@ open QCheck -open STM -open Util +open STM_base (** parallel STM tests of Array *) @@ -104,13 +103,14 @@ struct | _, _ -> false end -module ArraySTM = STM.Make(AConf) +module ArraySTM_seq = STM_sequential.Make(AConf) +module ArraySTM_dom = STM_domain.Make(AConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [ArraySTM.agree_test ~count ~name:"STM Array test sequential"; - ArraySTM.neg_agree_test_par ~count ~name:"STM Array test parallel" (* this test is expected to fail *) + [ArraySTM_seq.agree_test ~count ~name:"STM Array test sequential"; + ArraySTM_dom.neg_agree_test_par ~count ~name:"STM Array test parallel" (* this test is expected to fail *) ]) diff --git a/src/atomic/dune b/src/atomic/dune index 65566c1c2..c138a7a73 100644 --- a/src/atomic/dune +++ b/src/atomic/dune @@ -7,12 +7,12 @@ (deps stm_tests.exe lin_tests.exe lin_tests_dsl.exe)) -;; STM test of Atomic +;; STM_sequential and STM_domain test of Atomic (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/atomic/stm_tests.ml b/src/atomic/stm_tests.ml index e2d602303..c72c055a4 100644 --- a/src/atomic/stm_tests.ml +++ b/src/atomic/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** This is a parallel test of the Atomic module *) @@ -66,11 +66,12 @@ struct | _,_ -> false end -module AT = STM.Make(CConf) +module AT_seq = STM_sequential.Make(CConf) +module AT_dom = STM_domain.Make(CConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 250 in - [AT.agree_test ~count ~name:"STM Atomic test sequential"; - AT.agree_test_par ~count ~name:"STM Atomic test parallel";]) + [AT_seq.agree_test ~count ~name:"STM Atomic test sequential"; + AT_dom.agree_test_par ~count ~name:"STM Atomic test parallel";]) diff --git a/src/bigarray/dune b/src/bigarray/dune index c3a381ff5..71abeab67 100644 --- a/src/bigarray/dune +++ b/src/bigarray/dune @@ -15,7 +15,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) diff --git a/src/bigarray/stm_tests.ml b/src/bigarray/stm_tests.ml index 91d665eeb..23df25d3e 100644 --- a/src/bigarray/stm_tests.ml +++ b/src/bigarray/stm_tests.ml @@ -1,13 +1,11 @@ open QCheck -open STM -open Util +open STM_base open Bigarray (** parallel STM tests of Big Array *) module BAConf = struct - type cmd = | Size_in_bytes @@ -45,7 +43,7 @@ struct (* | Sub (_,_) -> s *) | Fill n -> List.map (fun _ -> n) s - let init_sut () = + let init_sut () = let ba = Array1.create int C_layout barray_size in Array1.fill ba 0 ; ba @@ -56,8 +54,8 @@ struct | _ -> true let run n ba = match n with - | Size_in_bytes -> Res (STM.int, Array1.size_in_bytes ba) - | Get i -> Res (result STM.int exn, protect (Array1.get ba) i) + | Size_in_bytes -> Res (STM_base.int, Array1.size_in_bytes ba) + | Get i -> Res (result STM_base.int exn, protect (Array1.get ba) i) | Set (i,n) -> Res (result unit exn, protect (Array1.set ba i) n) (* STM don't support bigarray type for the moment*) (* | Sub (i,l) -> Res (result (array char) exn, protect (Array.sub a i) l) *) @@ -82,13 +80,14 @@ struct | _, _ -> false end -module BigArraySTM = STM.Make(BAConf) +module BigArraySTM_seq = STM_sequential.Make(BAConf) +module BigArraySTM_dom = STM_domain.Make(BAConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [BigArraySTM.agree_test ~count ~name:"STM BigArray test sequential"; - BigArraySTM.neg_agree_test_par ~count ~name:"STM BigArray test parallel" + [BigArraySTM_seq.agree_test ~count ~name:"STM BigArray test sequential"; + BigArraySTM_dom.neg_agree_test_par ~count ~name:"STM BigArray test parallel" ]) diff --git a/src/buffer/dune b/src/buffer/dune index 2f06232dc..f0fb4a262 100644 --- a/src/buffer/dune +++ b/src/buffer/dune @@ -10,7 +10,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/buffer/stm_tests.ml b/src/buffer/stm_tests.ml index b5903bacd..080f1e2d3 100644 --- a/src/buffer/stm_tests.ml +++ b/src/buffer/stm_tests.ml @@ -1,6 +1,5 @@ open QCheck -open STM -open Util +open STM_base (** parallel STM tests of Buffer *) @@ -125,12 +124,13 @@ struct | _, _ -> false end -module BufferSTM = STM.Make(BConf) +module BufferSTM_seq = STM_sequential.Make(BConf) +module BufferSTM_dom = STM_domain.Make(BConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [BufferSTM.agree_test ~count ~name:"STM Buffer test sequential"; - BufferSTM.neg_agree_test_par ~count ~name:"STM Buffer test parallel" (* this test is expected to fail *)]) + [BufferSTM_seq.agree_test ~count ~name:"STM Buffer test sequential"; + BufferSTM_dom.neg_agree_test_par ~count ~name:"STM Buffer test parallel"]) diff --git a/src/bytes/dune b/src/bytes/dune index 201dc0fe2..72e00a280 100644 --- a/src/bytes/dune +++ b/src/bytes/dune @@ -17,7 +17,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) diff --git a/src/bytes/stm_tests.ml b/src/bytes/stm_tests.ml index 297f8a110..6c1127d28 100644 --- a/src/bytes/stm_tests.ml +++ b/src/bytes/stm_tests.ml @@ -1,6 +1,5 @@ open QCheck -open STM -open Util +open STM_base (** parallel STM tests of Bytes *) @@ -70,7 +69,7 @@ struct if i < 0 || i >= List.length s then r = Error (Invalid_argument "index out of bounds") else r = Ok (List.nth s i) - | Set (i,_), Res ((Result (Unit,Exn),_), r) -> + | Set (i,_), Res ((Result (Unit,Exn),_), r) -> if i < 0 || i >= List.length s then r = Error (Invalid_argument "index out of bounds") else r = Ok () @@ -87,13 +86,14 @@ struct | _, _ -> false end -module BytesSTM = STM.Make(ByConf) +module BytesSTM_seq = STM_sequential.Make(ByConf) +module BytesSTM_dom = STM_domain.Make(ByConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [BytesSTM.agree_test ~count ~name:"STM Bytes test sequential"; - BytesSTM.neg_agree_test_par ~count ~name:"STM Bytes test parallel" + [BytesSTM_seq.agree_test ~count ~name:"STM Bytes test sequential"; + BytesSTM_dom.neg_agree_test_par ~count ~name:"STM Bytes test parallel" ]) diff --git a/src/domainslib/chan_stm_tests.ml b/src/domainslib/chan_stm_tests.ml index 37a39e064..95e576357 100644 --- a/src/domainslib/chan_stm_tests.ml +++ b/src/domainslib/chan_stm_tests.ml @@ -1,6 +1,6 @@ open QCheck -open STM open Domainslib +open STM_base (** This is a parallel test of Domainslib.Chan *) @@ -69,12 +69,13 @@ struct end -module ChT = STM.Make(ChConf) +module ChT_seq = STM_sequential.Make(ChConf) +module ChT_dom = STM_domain.Make(ChConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count,name = 500,"global Domainslib.Chan test" in [ - ChT.agree_test ~count ~name; - ChT.agree_test_par ~count ~name; + ChT_seq.agree_test ~count ~name; + ChT_dom.agree_test_par ~count ~name; ]) diff --git a/src/domainslib/dune b/src/domainslib/dune index 53fa141e0..6de896e3a 100644 --- a/src/domainslib/dune +++ b/src/domainslib/dune @@ -48,12 +48,12 @@ (action (run ./%{deps} --verbose))) -;; STM test of Domainslib.Chan +;; STM_seq and STM_domain test of Domainslib.Chan (executable (name chan_stm_tests) (modules chan_stm_tests) - (libraries util STM domainslib) + (libraries qcheck-stm.sequential qcheck-stm.domain domainslib) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/dune b/src/dune index 8e9f2a1af..e5142aa4c 100644 --- a/src/dune +++ b/src/dune @@ -6,10 +6,12 @@ ;; stdlib, in alphabetic order (alias array/default) (alias atomic/default) + (alias bigarray/default) (alias buffer/default) (alias bytes/default) (alias domain/default) (alias ephemeron/default) + (alias floatarray/default) (alias hashtbl/default) (alias lazy/default) (alias queue/default) diff --git a/src/ephemeron/dune b/src/ephemeron/dune index 756c2cec6..ff834a65d 100644 --- a/src/ephemeron/dune +++ b/src/ephemeron/dune @@ -8,7 +8,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/ephemeron/stm_tests.ml b/src/ephemeron/stm_tests.ml index 95d322b19..196c0ef98 100644 --- a/src/ephemeron/stm_tests.ml +++ b/src/ephemeron/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** parallel STM tests of Ephemeron *) @@ -133,13 +133,13 @@ module EphemeronModel = | _ -> false end -module ETest = STM.Make(EphemeronModel) +module ETest_seq = STM_sequential.Make(EphemeronModel) +module ETest_dom = STM_domain.Make(EphemeronModel) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [ ETest.agree_test ~count ~name:"STM Ephemeron test sequential"; (* succeed *) - ETest.neg_agree_test_par ~count ~name:"STM Ephemeron test parallel"; (* fail *) + [ ETest_seq.agree_test ~count ~name:"STM Ephemeron test sequential"; (* succeed *) + ETest_dom.neg_agree_test_par ~count ~name:"STM Ephemeron test parallel"; (* fail *) ]) - diff --git a/src/floatarray/dune b/src/floatarray/dune index fee77e79f..e1b3ff75c 100644 --- a/src/floatarray/dune +++ b/src/floatarray/dune @@ -10,7 +10,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) diff --git a/src/floatarray/stm_tests.ml b/src/floatarray/stm_tests.ml index ef9eea5e6..60245877e 100644 --- a/src/floatarray/stm_tests.ml +++ b/src/floatarray/stm_tests.ml @@ -1,6 +1,5 @@ open QCheck -open STM -open Util +open STM_base (** parallel STM tests of Float.Array *) @@ -119,13 +118,14 @@ struct | _, _ -> false end -module FloatArraySTM = STM.Make(FAConf) +module FloatArraySTM_seq = STM_sequential.Make(FAConf) +module FloatArraySTM_dom = STM_domain.Make(FAConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [FloatArraySTM.agree_test ~count ~name:"STM Float Array test sequential"; - FloatArraySTM.neg_agree_test_par ~count ~name:"STM Float Array test parallel" + [FloatArraySTM_seq.agree_test ~count ~name:"STM Float Array test sequential"; + FloatArraySTM_dom.neg_agree_test_par ~count ~name:"STM Float Array test parallel" ]) diff --git a/src/hashtbl/dune b/src/hashtbl/dune index 27d9d13ba..02fe30d02 100644 --- a/src/hashtbl/dune +++ b/src/hashtbl/dune @@ -12,7 +12,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/hashtbl/stm_tests.ml b/src/hashtbl/stm_tests.ml index 114bf289c..cbfba5160 100644 --- a/src/hashtbl/stm_tests.ml +++ b/src/hashtbl/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** parallel STM tests of Hashtbl *) @@ -117,12 +117,13 @@ struct end -module HTest = STM.Make(HConf) +module HTest_seq = STM_sequential.Make(HConf) +module HTest_dom = STM_domain.Make(HConf) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 200 in - [HTest.agree_test ~count ~name:"STM Hashtbl test sequential"; - HTest.neg_agree_test_par ~count ~name:"STM Hashtbl test parallel"; + [HTest_seq.agree_test ~count ~name:"STM Hashtbl test sequential"; + HTest_dom.neg_agree_test_par ~count ~name:"STM Hashtbl test parallel"; ]) diff --git a/src/lazy/dune b/src/lazy/dune index d209cb158..9825ecbfc 100644 --- a/src/lazy/dune +++ b/src/lazy/dune @@ -1,4 +1,4 @@ -;; Parallel STM and Lin tests of the stdlib Lazy module +;; Parallel STM_seq STM_domain and Lin tests of the stdlib Lazy module ;; this prevents the tests from running on a default build (alias @@ -9,7 +9,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/lazy/stm_tests.ml b/src/lazy/stm_tests.ml index e7cc08f90..0ad6fe33c 100644 --- a/src/lazy/stm_tests.ml +++ b/src/lazy/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** parallel STM tests of Lazy *) @@ -76,8 +76,8 @@ struct let run c l = match c with - | Force -> Res (result int exn, Util.protect Lazy.force l) - | Force_val -> Res (result int exn, Util.protect Lazy.force_val l) + | Force -> Res (result int exn, protect Lazy.force l) + | Force_val -> Res (result int exn, protect Lazy.force_val l) | Is_val -> Res (bool, Lazy.is_val l) | Map (Fun (_,f)) -> Res (result int exn, try Ok (Lazy.force (Lazy.map f l)) @@ -96,18 +96,33 @@ struct | _,_ -> false end +module LTlazy_seq = STM_sequential.Make(struct + include LConfbase + let init_state = (7 * 100, false) + let init_sut () = lazy (work ()) + end) +module LTfromval_seq = STM_sequential.Make(struct + include LConfbase + let init_state = (42, true) + let init_sut () = Lazy.from_val 42 + end) +module LTfromfun_seq = STM_sequential.Make(struct + include LConfbase + let init_state = (7 * 100, false) + let init_sut () = Lazy.from_fun work + end) -module LTlazy = STM.Make(struct +module LTlazy_dom = STM_domain.Make(struct include LConfbase let init_state = (7 * 100, false) let init_sut () = lazy (work ()) end) -module LTfromval = STM.Make(struct +module LTfromval_dom = STM_domain.Make(struct include LConfbase let init_state = (42, true) let init_sut () = Lazy.from_val 42 end) -module LTfromfun = STM.Make(struct +module LTfromfun_dom = STM_domain.Make(struct include LConfbase let init_state = (7 * 100, false) let init_sut () = Lazy.from_fun work @@ -117,10 +132,10 @@ Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 200 in - [LTlazy.agree_test ~count ~name:"STM Lazy test sequential"; - LTfromval.agree_test ~count ~name:"STM Lazy test sequential from_val"; - LTfromfun.agree_test ~count ~name:"STM Lazy test sequential from_fun"; - LTlazy.neg_agree_test_par ~count ~name:"STM Lazy test parallel"; - LTfromval.agree_test_par ~count ~name:"STM Lazy test parallel from_val"; - LTfromfun.neg_agree_test_par ~count ~name:"STM Lazy test parallel from_fun"; + [LTlazy_seq.agree_test ~count ~name:"STM Lazy test sequential"; + LTfromval_seq.agree_test ~count ~name:"STM Lazy test sequential from_val"; + LTfromfun_seq.agree_test ~count ~name:"STM Lazy test sequential from_fun"; + LTlazy_dom.neg_agree_test_par ~count ~name:"STM Lazy test parallel"; + LTfromval_dom.agree_test_par ~count ~name:"STM Lazy test parallel from_val"; + LTfromfun_dom.neg_agree_test_par ~count ~name:"STM Lazy test parallel from_fun"; ]) diff --git a/src/lockfree/dune b/src/lockfree/dune index 81c776989..342982c68 100644 --- a/src/lockfree/dune +++ b/src/lockfree/dune @@ -11,7 +11,7 @@ (executable (name ws_deque_test) (modules ws_deque_test) - (libraries STM lockfree) + (libraries qcheck-stm.sequential qcheck-stm.domain lockfree) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/lockfree/ws_deque_test.ml b/src/lockfree/ws_deque_test.ml index 1f2b48404..e839fab0d 100644 --- a/src/lockfree/ws_deque_test.ml +++ b/src/lockfree/ws_deque_test.ml @@ -1,8 +1,8 @@ (** Sequential tests of ws_deque *) open QCheck -open STM - +open STM_base +open Util module Ws_deque = Lockfree.Ws_deque module WSDConf = @@ -58,7 +58,8 @@ struct | _,_ -> false end -module WSDT = STM.Make(WSDConf) +module WSDT_seq = STM_sequential.Make(WSDConf) +module WSDT_dom = STM_domain.Make(WSDConf) (* The following definitions differ slightly from those in STM.ml. This has to do with how work-stealing deques are supposed to be used according to spec: @@ -66,44 +67,43 @@ module WSDT = STM.Make(WSDConf) in parallel with the original "owner domain" (it also uses [Semaphore.Binary]) *) let agree_prop_par = (fun (seq_pref,owner,stealer) -> - assume (WSDT.cmds_ok WSDConf.init_state (seq_pref@owner)); - assume (WSDT.cmds_ok WSDConf.init_state (seq_pref@stealer)); + assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref@owner)); + assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref@stealer)); let sut = WSDConf.init_sut () in - let pref_obs = WSDT.interp_sut_res sut seq_pref in + let pref_obs = WSDT_dom.interp_sut_res sut seq_pref in let sema = Semaphore.Binary.make false in - let stealer_dom = Domain.spawn (fun () -> Semaphore.Binary.release sema; WSDT.interp_sut_res sut stealer) in + let stealer_dom = Domain.spawn (fun () -> Semaphore.Binary.release sema; WSDT_dom.interp_sut_res sut stealer) in while not (Semaphore.Binary.try_acquire sema) do Domain.cpu_relax() done; - let own_obs = WSDT.interp_sut_res sut owner in + let own_obs = WSDT_dom.interp_sut_res sut owner in let stealer_obs = Domain.join stealer_dom in - let res = WSDT.check_obs pref_obs own_obs stealer_obs WSDConf.init_state in + let res = WSDT_dom.check_obs pref_obs own_obs stealer_obs WSDConf.init_state in let () = WSDConf.cleanup sut in res || Test.fail_reportf " Results incompatible with linearized model:\n\n%s" - @@ Util.print_triple_vertical ~center_prefix:false show_res + @@ Util.print_triple_vertical ~center_prefix:false STM_base.show_res (List.map snd pref_obs, List.map snd own_obs, List.map snd stealer_obs)) (* [arb_cmds_par] differs in what each triple component generates: "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *) -let arb_cmds_par = WSDT.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd +let arb_cmds_par = WSDT_dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd (* A parallel agreement test - w/repeat and retries combined *) let agree_test_par ~count ~name = let rep_count = 50 in Test.make ~retries:10 ~count ~name - arb_cmds_par (STM.repeat rep_count agree_prop_par) (* 50 times each, then 50 * 10 times when shrinking *) + arb_cmds_par (repeat rep_count agree_prop_par) (* 50 times each, then 50 * 10 times when shrinking *) -(* Note: since this can generate, e.g., [Pop] commands/actions in the "stealer domain", - we are violating the spec. - and the deque will not behave as expected, hence a negative test *) -let agree_test_par_negative ~count ~name = WSDT.neg_agree_test_par ~count ~name +(* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *) +let agree_test_par_negative ~count ~name = WSDT_dom.neg_agree_test_par ~count ~name ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in [ - WSDT.agree_test ~count ~name:"ws_deque test"; + WSDT_seq.agree_test ~count ~name:"sequential ws_deque test"; agree_test_par ~count ~name:"parallel ws_deque test"; - agree_test_par_negative ~count ~name:"ws_deque test, negative"; + agree_test_par_negative ~count ~name:"parallel ws_deque test, negative"; ]) diff --git a/src/neg_tests/conclist_stm_tests.ml b/src/neg_tests/conclist_stm_tests.ml index cd1f16a4a..2dffed938 100644 --- a/src/neg_tests/conclist_stm_tests.ml +++ b/src/neg_tests/conclist_stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** This is a parallel test of the buggy concurrent list CList *) @@ -49,14 +49,16 @@ module Int = struct let of_int (i:int) : t = i end -module CLT_int = STM.Make(CLConf(Int)) -module CLT_int64 = STM.Make(CLConf(Int64)) +module CLT_int_seq = STM_sequential.Make(CLConf(Int)) +module CLT_int_dom = STM_domain.Make(CLConf(Int)) +module CLT_int64_seq = STM_sequential.Make(CLConf(Int64)) +module CLT_int64_dom = STM_domain.Make(CLConf(Int64)) ;; Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [CLT_int.agree_test ~count ~name:"STM int CList test sequential"; - CLT_int64.agree_test ~count ~name:"STM int64 CList test sequential"; - CLT_int.neg_agree_test_par ~count ~name:"STM int CList test parallel"; - CLT_int64.neg_agree_test_par ~count ~name:"STM int64 CList test parallel"]) + [CLT_int_seq.agree_test ~count ~name:"STM int CList test sequential"; + CLT_int64_seq.agree_test ~count ~name:"STM int64 CList test sequential"; + CLT_int_dom.neg_agree_test_par ~count ~name:"STM int CList test parallel"; + CLT_int64_dom.neg_agree_test_par ~count ~name:"STM int64 CList test parallel"]) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index fd805dec9..12f68f65c 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -5,22 +5,51 @@ (name default) (package multicoretests) (deps - ref_stm_tests.exe + ref_stm_seq_tests.exe + ref_stm_dom_tests.exe + ref_stm_thread_tests.exe conclist_stm_tests.exe domain_lin_tests_dsl.exe thread_lin_tests.exe effect_lin_tests_dsl.exe)) +(library + (name ref_stm_spec) + (modules ref_stm_spec) + (libraries qcheck qcheck-stm.base) + (preprocess (pps ppx_deriving.show ppx_deriving.eq))) + (executable - (name ref_stm_tests) - (modules ref_stm_tests) - (libraries STM) - (preprocess (pps ppx_deriving.show))) + (name ref_stm_seq_tests) + (modules ref_stm_seq_tests) + (libraries ref_stm_spec qcheck-stm.sequential)) + +(executable + (name ref_stm_dom_tests) + (modules ref_stm_dom_tests) + (libraries ref_stm_spec qcheck-stm.domain)) + +(executable + (name ref_stm_thread_tests) + (modules ref_stm_thread_tests) + (libraries ref_stm_spec qcheck-stm.thread)) + +(rule + (alias runtest) + (package multicoretests) + (deps ref_stm_seq_tests.exe) + (action (run ./%{deps} --verbose))) + +(rule + (alias runtest) + (package multicoretests) + (deps ref_stm_dom_tests.exe) + (action (run ./%{deps} --verbose))) (rule (alias runtest) (package multicoretests) - (deps ref_stm_tests.exe) + (deps ref_stm_thread_tests.exe) (action (run ./%{deps} --verbose))) (library @@ -30,7 +59,7 @@ (executable (name conclist_stm_tests) (modules conclist_stm_tests) - (libraries CList STM) + (libraries CList qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/neg_tests/ref_stm_dom_tests.ml b/src/neg_tests/ref_stm_dom_tests.ml new file mode 100644 index 000000000..359cf3228 --- /dev/null +++ b/src/neg_tests/ref_stm_dom_tests.ml @@ -0,0 +1,20 @@ +open Ref_stm_spec + +module RT_int = STM_domain.Make(RConf_int) +module RT_int64 = STM_domain.Make(RConf_int64) + +(*module RConf_int_GC = STM_base.AddGC(RConf_int)*) +(*module RConf_int64_GC = STM_base.AddGC(RConf_int64)*) + +(*module RT_int_GC = STM_domain.Make(RConf_int_GC)*) +(*module RT_int64_GC = STM_domain.Make(RConf_int64_GC)*) +;; +Util.set_ci_printing () +;; +QCheck_runner.run_tests_main + (let count = 1000 in + [RT_int.neg_agree_test_par ~count ~name:"STM int ref test parallel"; + (*RT_int_GC.neg_agree_test_par ~count ~name:"STM int ref test parallel (w/AddGC functor)";*) + RT_int64.neg_agree_test_par ~count ~name:"STM int64 ref test parallel"; + (*RT_int64_GC.neg_agree_test_par ~count ~name:"STM int64 ref test parallel (w/AddGC functor)";*) + ]) diff --git a/src/neg_tests/ref_stm_seq_tests.ml b/src/neg_tests/ref_stm_seq_tests.ml new file mode 100644 index 000000000..00a223b1a --- /dev/null +++ b/src/neg_tests/ref_stm_seq_tests.ml @@ -0,0 +1,12 @@ +open Ref_stm_spec + +module RT_int_seq = STM_sequential.Make(RConf_int) +module RT_int64_seq = STM_sequential.Make(RConf_int64) +;; +Util.set_ci_printing () +;; +QCheck_runner.run_tests_main + (let count = 1000 in + [RT_int_seq.agree_test ~count ~name:"STM int ref test sequential"; + RT_int64_seq.agree_test ~count ~name:"STM int64 ref test sequential"; + ]) diff --git a/src/neg_tests/ref_stm_tests.ml b/src/neg_tests/ref_stm_spec.ml similarity index 79% rename from src/neg_tests/ref_stm_tests.ml rename to src/neg_tests/ref_stm_spec.ml index acb4f391a..c91e63ac1 100644 --- a/src/neg_tests/ref_stm_tests.ml +++ b/src/neg_tests/ref_stm_spec.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** This is a parallel test of refs *) @@ -132,25 +132,3 @@ struct | Decr, Res ((Unit,_),_) -> true | _,_ -> false end - - -module RT_int = STM.Make(RConf_int) -module RT_int64 = STM.Make(RConf_int64) - -(* module RConf_int_GC = STM.AddGC(RConf_int) *) -(* module RConf_int64_GC = STM.AddGC(RConf_int64) *) - -(* module RT_int_GC = STM.Make(RConf_int_GC) *) -(* module RT_int64_GC = STM.Make(RConf_int64_GC) *) -;; -Util.set_ci_printing () -;; -QCheck_base_runner.run_tests_main - (let count = 1000 in - [RT_int.agree_test ~count ~name:"STM int ref test sequential"; - RT_int.neg_agree_test_par ~count ~name:"STM int ref test parallel"; - (*RT_int_GC.neg_agree_test_par ~count ~name:"STM int ref test parallel (w/AddGC functor)";*) - RT_int64.agree_test ~count ~name:"STM int64 ref test sequential"; - RT_int64.neg_agree_test_par ~count ~name:"STM int64 ref test parallel"; - (*RT_int_GC.neg_agree_test_par ~count ~name:"STM int64 ref test parallel (w/AddGC functor)";*) - ]) diff --git a/src/neg_tests/ref_stm_thread_tests.ml b/src/neg_tests/ref_stm_thread_tests.ml new file mode 100644 index 000000000..7d13dc1cd --- /dev/null +++ b/src/neg_tests/ref_stm_thread_tests.ml @@ -0,0 +1,20 @@ +open Ref_stm_spec + +module RT_int = STM_thread.Make(RConf_int) +module RT_int64 = STM_thread.Make(RConf_int64) + +(*module RConf_int_GC = STM_base.AddGC(RConf_int)*) +(*module RConf_int64_GC = STM_base.AddGC(RConf_int64)*) + +(*module RT_int_GC = STM_thread.Make(RConf_int_GC)*) +(*module RT_int64_GC = STM_thread.Make(RConf_int64_GC)*) +;; +Util.set_ci_printing () +;; +QCheck_runner.run_tests_main + (let count = 1000 in + [RT_int.agree_test_conc ~count ~name:"STM int ref test with Thread"; + (*RT_int_GC.agree_test_conc ~count ~name:"STM int ref test with Thread (w/AddGC functor)";*) + RT_int64.neg_agree_test_conc ~count ~name:"STM int64 ref test with Thread"; + (*RT_int64_GC.agree_test_conc ~count ~name:"STM int64 ref test with Thread (w/AddGC functor)";*) + ]) diff --git a/src/semaphore/dune b/src/semaphore/dune index 046ec0c91..8c1394c67 100644 --- a/src/semaphore/dune +++ b/src/semaphore/dune @@ -9,7 +9,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) (rule diff --git a/src/semaphore/stm_tests.ml b/src/semaphore/stm_tests.ml index 0453231e4..732c12665 100644 --- a/src/semaphore/stm_tests.ml +++ b/src/semaphore/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM +open STM_base (** parallel STM tests of Semaphore.Counting *) @@ -62,12 +62,13 @@ module SCConf = | _ -> false end -module SCTest = STM.Make(SCConf) +module SCTest_seq = STM_sequential.Make(SCConf) +module SCTest_dom = STM_domain.Make(SCConf) let _ = Util.set_ci_printing () ; QCheck_base_runner.run_tests_main (let count = 200 in - [SCTest.agree_test ~count ~name:"STM Semaphore.Counting test sequential"; - SCTest.agree_test_par ~count ~name:"STM Semaphore.Counting test parallel"; + [SCTest_seq.agree_test ~count ~name:"STM Semaphore.Counting test sequential"; + SCTest_dom.agree_test_par ~count ~name:"STM Semaphore.Counting test parallel"; ])