diff --git a/doc/example/dune b/doc/example/dune index 09899b094..9084cb85e 100644 --- a/doc/example/dune +++ b/doc/example/dune @@ -3,7 +3,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries qcheck-lin)) + (libraries qcheck-lin.domain)) ;; A model-based test of the stdlib Hashtbl library diff --git a/doc/example/lin_tests_dsl.ml b/doc/example/lin_tests_dsl.ml index a52b062de..0fde16290 100644 --- a/doc/example/lin_tests_dsl.ml +++ b/doc/example/lin_tests_dsl.ml @@ -7,7 +7,7 @@ struct let init () = Hashtbl.create ~random:false 42 let cleanup _ = () - open Lin_api + open Lin_base let a,b = char_printable,nat_small let api = [ val_ "Hashtbl.add" Hashtbl.add (t @-> a @-> b @-> returning unit); @@ -17,8 +17,8 @@ struct val_ "Hashtbl.length" Hashtbl.length (t @-> returning int); ] end -module HT = Lin_api.Make(HashtblSig) +module HT = Lin_domain.Make(HashtblSig) ;; QCheck_base_runner.run_tests_main [ - HT.lin_test `Domain ~count:1000 ~name:"Hashtbl DSL test"; + HT.lin_test ~count:1000 ~name:"Hashtbl DSL test"; ] diff --git a/lib/dune b/lib/dune index 5940f1bb5..01aeeaf95 100644 --- a/lib/dune +++ b/lib/dune @@ -23,11 +23,28 @@ (libraries threads qcheck-core STM_base)) (library - (name lin) - (wrapped false) - (public_name qcheck-lin) - (modules lin lin_api) - (libraries threads qcheck-core qcheck-core.runner qcheck-multicoretests-util)) + (name lin_base) + (public_name qcheck-lin.base) + (modules lin_internal lin_common lin_base) + (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util)) + +(library + (name lin_domain) + (public_name qcheck-lin.domain) + (modules lin_domain) + (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.base)) + +(library + (name lin_effect) + (public_name qcheck-lin.effect) + (modules lin_effect) + (libraries qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.base)) + +(library + (name lin_thread) + (public_name qcheck-lin.thread) + (modules lin_thread) + (libraries threads qcheck-core qcheck-core.runner qcheck-multicoretests-util qcheck-lin.base)) (library (name util) diff --git a/lib/lin.ml b/lib/lin.ml deleted file mode 100644 index 68bdb0ff9..000000000 --- a/lib/lin.ml +++ /dev/null @@ -1,325 +0,0 @@ -open QCheck -include Util - -module type CmdSpec = sig - type t - (** The type of the system under test *) - - type cmd - (** The type of commands *) - - val show_cmd : cmd -> string - (** [show_cmd c] returns a string representing the command [c]. *) - - val gen_cmd : cmd Gen.t - (** A command generator. *) - - val shrink_cmd : cmd Shrink.t - (** A command shrinker. - To a first approximation you can use [Shrink.nil]. *) - - type res - (** The command result type *) - - val show_res : res -> string - (** [show_res r] returns a string representing the result [r]. *) - - val equal_res : res -> res -> bool - - val init : unit -> t - (** Initialize the system under test. *) - - val cleanup : t -> unit - (** Utility function to clean up [t] after each test instance, - e.g., for closing sockets, files, or resetting global parameters *) - - val run : cmd -> t -> res - (** [run c t] should interpret the command [c] over the system under test [t] (typically side-effecting). *) -end - -(** A functor to create Domain and Thread test setups. - We use it below, but it can also be used independently *) -module MakeDomThr(Spec : CmdSpec) - = struct - - (* plain interpreter of a cmd list *) - let interp_plain sut cs = List.map (fun c -> (c, Spec.run c sut)) cs - - (* operate over arrays to avoid needless allocation underway *) - let interp 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) - - (* Note: On purpose we use - - a non-tail-recursive function and - - an (explicit) allocation in the loop body - since both trigger statistically significant more thread issues/interleaving *) - let rec interp_thread sut cs = match cs with - | [] -> [] - | c::cs -> - Thread.yield (); - let res = Spec.run c sut in - (c,res)::interp_thread sut cs - - let rec gen_cmds fuel = - Gen.(if fuel = 0 - then return [] - else - Spec.gen_cmd >>= fun c -> - gen_cmds (fuel-1) >>= fun cs -> - return (c::cs)) - (** A fueled command list generator. *) - - let gen_cmds_size size_gen = Gen.sized_size size_gen gen_cmds - - let shrink_triple (seq,p1,p2) = - let open Iter in - (* Shrinking heuristic: - First reduce the cmd list sizes as much as possible, since the interleaving - is most costly over long cmd lists. *) - (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq)) - <+> - (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2)) - <+> - (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s)) - <+> - (map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1)) - <+> - (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2)) - <+> - (* Secondly reduce the cmd data of individual list elements *) - (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems Spec.shrink_cmd seq)) - <+> - (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems Spec.shrink_cmd p1)) - <+> - (map (fun p2' -> (seq,p1,p2')) (Shrink.list_elems Spec.shrink_cmd p2)) - - let arb_cmds_par seq_len par_len = - let gen_triple = - Gen.(int_range 2 (2*par_len) >>= fun dbl_plen -> - let seq_pref_gen = gen_cmds_size (int_bound seq_len) in - let par_len1 = dbl_plen/2 in - let par_gen1 = gen_cmds_size (return par_len1) in - let par_gen2 = gen_cmds_size (return (dbl_plen - par_len1)) in - triple seq_pref_gen par_gen1 par_gen2) in - make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple - - let rec check_seq_cons pref cs1 cs2 seq_sut seq_trace = match pref with - | (c,res)::pref' -> - if Spec.equal_res res (Spec.run c seq_sut) - then check_seq_cons pref' cs1 cs2 seq_sut (c::seq_trace) - else (Spec.cleanup seq_sut; false) - (* Invariant: call Spec.cleanup immediately after mismatch *) - | [] -> match cs1,cs2 with - | [],[] -> Spec.cleanup seq_sut; true - | [],(c2,res2)::cs2' -> - if Spec.equal_res res2 (Spec.run c2 seq_sut) - then check_seq_cons pref cs1 cs2' seq_sut (c2::seq_trace) - else (Spec.cleanup seq_sut; false) - | (c1,res1)::cs1',[] -> - if Spec.equal_res res1 (Spec.run c1 seq_sut) - then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace) - else (Spec.cleanup seq_sut; false) - | (c1,res1)::cs1',(c2,res2)::cs2' -> - (if Spec.equal_res res1 (Spec.run c1 seq_sut) - then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace) - else (Spec.cleanup seq_sut; false)) - || - (* rerun to get seq_sut to same cmd branching point *) - (let seq_sut' = Spec.init () in - let _ = interp_plain seq_sut' (List.rev seq_trace) in - if Spec.equal_res res2 (Spec.run c2 seq_sut') - then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace) - else (Spec.cleanup seq_sut'; false)) - - (* Linearizability property based on [Domain] and an Atomic flag *) - let lin_prop_domain (seq_pref,cmds1,cmds2) = - let sut = Spec.init () in - let pref_obs = interp 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 cmds1) with exn -> Error exn) in - let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp 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 seq_sut = Spec.init () in - check_seq_cons pref_obs obs1 obs2 seq_sut [] - || Test.fail_reportf " Results incompatible with sequential execution\n\n%s" - @@ print_triple_vertical ~fig_indent:5 ~res_width:35 - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r)) - (pref_obs,obs1,obs2) - - (* Linearizability property based on [Thread] *) - let lin_prop_thread = - (fun (seq_pref, cmds1, cmds2) -> - let sut = Spec.init () in - let obs1, obs2 = ref [], ref [] in - let pref_obs = interp_plain sut seq_pref in - let wait = ref true in - let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := interp_thread sut cmds1) () in - let th2 = Thread.create (fun () -> wait := false; obs2 := interp_thread sut cmds2) () in - Thread.join th1; - Thread.join th2; - Spec.cleanup sut; - let seq_sut = Spec.init () in - (* we reuse [check_seq_cons] to linearize and interpret sequentially *) - check_seq_cons pref_obs !obs1 !obs2 seq_sut [] - || Test.fail_reportf " Results incompatible with sequential execution\n\n%s" - @@ print_triple_vertical ~fig_indent:5 ~res_width:35 - (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r)) - (pref_obs,!obs1,!obs2)) -end - -(** Definitions for Effect interpretation *) - -(* Scheduler adapted from https://kcsrk.info/slides/retro_effects_simcorp.pdf *) -open Effect -open Effect.Deep - -type _ t += Fork : (unit -> unit) -> unit t - | Yield : unit t - -let enqueue k q = Queue.push k q -let dequeue q = - if Queue.is_empty q - then () (*Finished*) - else continue (Queue.pop q) () - -let start_sched main = - (* scheduler's queue of continuations *) - let q = Queue.create () in - let rec spawn = fun (type res) (f : unit -> res) -> - match_with f () - { retc = (fun _v -> dequeue q); (* value case *) - exnc = (fun e -> print_string (Printexc.to_string e); raise e); - effc = (fun (type a) (e : a t) -> match e with - | Yield -> Some (fun (k : (a, _) continuation) -> enqueue k q; dequeue q) - | Fork f -> Some (fun (k : (a, _) continuation) -> enqueue k q; spawn f) - | _ -> None ) } - in - spawn main - -(* short hands *) -let fork f = perform (Fork f) -let yield () = perform Yield - - -(** A functor to create all three (Domain, Thread, and Effect) test setups. - The result [include]s the output module from the [MakeDomThr] functor above *) -module Make(Spec : CmdSpec) -= struct - - (** A refined [CmdSpec] specification with generator-controlled [Yield] effects *) - module EffSpec - = struct - - type t = Spec.t - let init = Spec.init - let cleanup = Spec.cleanup - - type cmd = SchedYield | UserCmd of Spec.cmd [@@deriving qcheck] - - let show_cmd c = match c with - | SchedYield -> "" - | UserCmd c -> Spec.show_cmd c - - let gen_cmd = - (Gen.frequency - [(3,Gen.return SchedYield); - (5,Gen.map (fun c -> UserCmd c) Spec.gen_cmd)]) - - let shrink_cmd c = match c with - | SchedYield -> Iter.empty - | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c) - - type res = SchedYieldRes | UserRes of Spec.res - - let show_res r = match r with - | SchedYieldRes -> "" - | UserRes r -> Spec.show_res r - - let equal_res r r' = match r,r' with - | SchedYieldRes, SchedYieldRes -> true - | UserRes r, UserRes r' -> Spec.equal_res r r' - | _, _ -> false - - let run c sut = match c with - | SchedYield -> - (yield (); SchedYieldRes) - | UserCmd uc -> - let res = Spec.run uc sut in - UserRes res - end - - module EffTest = MakeDomThr(EffSpec) - - let filter_res rs = List.filter (fun (c,_) -> c <> EffSpec.SchedYield) rs - - (* Parallel agreement property based on effect-handler scheduler *) - let lin_prop_effect = - (fun (seq_pref,cmds1,cmds2) -> - let sut = Spec.init () in - (* exclude [Yield]s from sequential prefix *) - let pref_obs = EffTest.interp_plain sut (List.filter (fun c -> c <> EffSpec.SchedYield) seq_pref) in - let obs1,obs2 = ref [], ref [] in - let main () = - (* For now, we reuse [interp_thread] which performs useless [Thread.yield] on single-domain/fibered program *) - fork (fun () -> let tmp1 = EffTest.interp_thread sut cmds1 in obs1 := tmp1); - fork (fun () -> let tmp2 = EffTest.interp_thread sut cmds2 in obs2 := tmp2); in - let () = start_sched main in - let () = Spec.cleanup sut in - let seq_sut = Spec.init () in - (* exclude [Yield]s from sequential executions when searching for an interleaving *) - EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut [] - || Test.fail_reportf " Results incompatible with linearized model\n\n%s" - @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 - (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r)) - (pref_obs,!obs1,!obs2)) - - module FirstTwo = MakeDomThr(Spec) - include FirstTwo - - (* Linearizability test based on [Domain], [Thread], or [Effect] *) - let lin_test ~count ~name (lib : [ `Domain | `Thread | `Effect ]) = - let seq_len,par_len = 20,12 in - match lib with - | `Domain -> - let arb_cmd_triple = arb_cmds_par seq_len par_len in - let rep_count = 50 in - Test.make ~count ~retries:3 ~name - arb_cmd_triple (repeat rep_count lin_prop_domain) - | `Thread -> - let arb_cmd_triple = arb_cmds_par seq_len par_len in - let rep_count = 100 in - Test.make ~count ~retries:5 ~name - arb_cmd_triple (repeat rep_count lin_prop_thread) - | `Effect -> - (* this generator is over [EffSpec.cmd] including [SchedYield], not [Spec.cmd] like the above two *) - let arb_cmd_triple = EffTest.arb_cmds_par seq_len par_len in - let rep_count = 1 in - Test.make ~count ~retries:10 ~name - arb_cmd_triple (repeat rep_count lin_prop_effect) - - (* Negative linearizability test based on [Domain], [Thread], or [Effect] *) - let neg_lin_test ~count ~name (lib : [ `Domain | `Thread | `Effect ]) = - let seq_len,par_len = 20,12 in - match lib with - | `Domain -> - let arb_cmd_triple = arb_cmds_par seq_len par_len in - let rep_count = 50 in - Test.make_neg ~count ~retries:3 ~name - arb_cmd_triple (repeat rep_count lin_prop_domain) - | `Thread -> - let arb_cmd_triple = arb_cmds_par seq_len par_len in - let rep_count = 100 in - Test.make_neg ~count ~retries:5 ~name - arb_cmd_triple (repeat rep_count lin_prop_thread) - | `Effect -> - (* this generator is over [EffSpec.cmd] including [SchedYield], not [Spec.cmd] like the above two *) - let arb_cmd_triple = EffTest.arb_cmds_par seq_len par_len in - let rep_count = 1 in - Test.make_neg ~count ~retries:10 ~name - arb_cmd_triple (repeat rep_count lin_prop_effect) -end diff --git a/lib/lin_base.ml b/lib/lin_base.ml new file mode 100644 index 000000000..0d0e2ce85 --- /dev/null +++ b/lib/lin_base.ml @@ -0,0 +1,3 @@ +module Lin_internal = Lin_internal +module Lin_common = Lin_common +include Lin_common diff --git a/lib/lin_api.ml b/lib/lin_common.ml similarity index 99% rename from lib/lin_api.ml rename to lib/lin_common.ml index 0d301e728..d9f127aef 100644 --- a/lib/lin_api.ml +++ b/lib/lin_common.ml @@ -140,7 +140,7 @@ module type ApiSpec = sig val api : (int * t elem) list end -module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct +module MakeCmd (ApiSpec : ApiSpec) : Lin_internal.CmdSpec = struct type t = ApiSpec.t @@ -333,5 +333,3 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct Res (rty, apply_f f args state) end - -module Make (ApiSpec : ApiSpec) = Lin.Make (MakeCmd (ApiSpec)) diff --git a/lib/lin_api.mli b/lib/lin_common.mli similarity index 96% rename from lib/lin_api.mli rename to lib/lin_common.mli index 132390878..b972cc653 100644 --- a/lib/lin_api.mli +++ b/lib/lin_common.mli @@ -1,4 +1,4 @@ -(** The [Lin_api] module allows the user to describe the type signature of +(** This module allows the user to describe the type signature of a tested module interface using a DSL of type combinators. *) @@ -237,11 +237,6 @@ module type ApiSpec = (** {1 Generation of linearizability testing module from an API} *) -module MakeCmd : functor (ApiSpec : ApiSpec) -> Lin.CmdSpec +module MakeCmd : functor (Spec : ApiSpec) -> Lin_internal.CmdSpec (** Functor to map a combinator-based module signature description into a raw [Lin] description *) - -module Make : - functor (ApiSpec : ApiSpec) -> module type of Lin.Make (MakeCmd (ApiSpec)) -(** Functor to create linearizability tests from an combinator-based module - signature description *) diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml new file mode 100644 index 000000000..424cf92ff --- /dev/null +++ b/lib/lin_domain.ml @@ -0,0 +1,39 @@ +open Lin_base + +module Make_internal (Spec : Lin_internal.CmdSpec) = struct + module M = Lin_internal.Make(Spec) + include M + + (* operate over arrays to avoid needless allocation underway *) + let interp 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) + + (* Linearizability property based on [Domain] and an Atomic flag *) + let lin_prop_domain (seq_pref,cmds1,cmds2) = + let sut = Spec.init () in + let pref_obs = interp 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 cmds1) with exn -> Error exn) in + let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp 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 seq_sut = Spec.init () in + check_seq_cons pref_obs obs1 obs2 seq_sut [] + || QCheck.Test.fail_reportf " Results incompatible with sequential execution\n\n%s" + @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r)) + (pref_obs,obs1,obs2) + + let lin_test ~count ~name = + lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop_domain + + let neg_lin_test ~count ~name = + neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop_domain +end + +module Make (Spec : Lin_common.ApiSpec) = + Make_internal(Lin_common.MakeCmd(Spec)) diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml new file mode 100644 index 000000000..a3fd50fc6 --- /dev/null +++ b/lib/lin_effect.ml @@ -0,0 +1,126 @@ +open Lin_base + +(** Definitions for Effect interpretation *) + +(* Scheduler adapted from https://kcsrk.info/slides/retro_effects_simcorp.pdf *) +open Effect +open Effect.Deep + +type _ t += Fork : (unit -> unit) -> unit t + | Yield : unit t + +let enqueue k q = Queue.push k q +let dequeue q = + if Queue.is_empty q + then () (*Finished*) + else continue (Queue.pop q) () + +let start_sched main = + (* scheduler's queue of continuations *) + let q = Queue.create () in + let rec spawn = fun (type res) (f : unit -> res) -> + match_with f () + { retc = (fun _v -> dequeue q); (* value case *) + exnc = (fun e -> print_string (Printexc.to_string e); raise e); + effc = (fun (type a) (e : a t) -> match e with + | Yield -> Some (fun (k : (a, _) continuation) -> enqueue k q; dequeue q) + | Fork f -> Some (fun (k : (a, _) continuation) -> enqueue k q; spawn f) + | _ -> None ) } + in + spawn main + +(* short hands *) +let fork f = perform (Fork f) +let yield () = perform Yield + +module Make_internal (Spec : Lin_internal.CmdSpec) = struct + + + (** A refined [CmdSpec] specification with generator-controlled [Yield] effects *) + module EffSpec + = struct + open QCheck + + type t = Spec.t + let init = Spec.init + let cleanup = Spec.cleanup + + type cmd = SchedYield | UserCmd of Spec.cmd [@@deriving qcheck] + + let show_cmd c = match c with + | SchedYield -> "" + | UserCmd c -> Spec.show_cmd c + + let gen_cmd = + (Gen.frequency + [(3,Gen.return SchedYield); + (5,Gen.map (fun c -> UserCmd c) Spec.gen_cmd)]) + + let shrink_cmd c = match c with + | SchedYield -> Iter.empty + | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c) + + type res = SchedYieldRes | UserRes of Spec.res + + let show_res r = match r with + | SchedYieldRes -> "" + | UserRes r -> Spec.show_res r + + let equal_res r r' = match r,r' with + | SchedYieldRes, SchedYieldRes -> true + | UserRes r, UserRes r' -> Spec.equal_res r r' + | _, _ -> false + + let run c sut = match c with + | SchedYield -> + (yield (); SchedYieldRes) + | UserCmd uc -> + let res = Spec.run uc sut in + UserRes res + end + + module EffTest = Lin_internal.Make(EffSpec) + + let filter_res rs = List.filter (fun (c,_) -> c <> EffSpec.SchedYield) rs + + let rec interp sut cs = match cs with + | [] -> [] + | c::cs -> + let res = EffSpec.run c sut in + (c,res)::interp sut cs + + (* Parallel agreement property based on effect-handler scheduler *) + let lin_prop_effect = + (fun (seq_pref,cmds1,cmds2) -> + let sut = Spec.init () in + (* exclude [Yield]s from sequential prefix *) + let pref_obs = EffTest.interp_plain sut (List.filter (fun c -> c <> EffSpec.SchedYield) seq_pref) in + let obs1,obs2 = ref [], ref [] in + let main () = + fork (fun () -> let tmp1 = interp sut cmds1 in obs1 := tmp1); + fork (fun () -> let tmp2 = interp sut cmds2 in obs2 := tmp2); in + let () = start_sched main in + let () = Spec.cleanup sut in + let seq_sut = Spec.init () in + (* exclude [Yield]s from sequential executions when searching for an interleaving *) + EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut [] + || QCheck.Test.fail_reportf " Results incompatible with linearized model\n\n%s" + @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 + (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r)) + (pref_obs,!obs1,!obs2)) + + let lin_test ~count ~name = + let arb_cmd_triple = EffTest.arb_cmds_par 20 12 in + let rep_count = 1 in + QCheck.Test.make ~count ~retries:10 ~name + arb_cmd_triple (Util.repeat rep_count lin_prop_effect) + + let neg_lin_test ~count ~name = + let arb_cmd_triple = EffTest.arb_cmds_par 20 12 in + let rep_count = 1 in + QCheck.Test.make_neg ~count ~retries:10 ~name + arb_cmd_triple (Util.repeat rep_count lin_prop_effect) +end + +module Make (Spec : Lin_common.ApiSpec) = + Make_internal(Lin_common.MakeCmd(Spec)) diff --git a/lib/lin_internal.ml b/lib/lin_internal.ml new file mode 100644 index 000000000..f309ed343 --- /dev/null +++ b/lib/lin_internal.ml @@ -0,0 +1,130 @@ +open QCheck +include Util + +module type CmdSpec = sig + type t + (** The type of the system under test *) + + type cmd + (** The type of commands *) + + val show_cmd : cmd -> string + (** [show_cmd c] returns a string representing the command [c]. *) + + val gen_cmd : cmd Gen.t + (** A command generator. *) + + val shrink_cmd : cmd Shrink.t + (** A command shrinker. + To a first approximation you can use [Shrink.nil]. *) + + type res + (** The command result type *) + + val show_res : res -> string + (** [show_res r] returns a string representing the result [r]. *) + + val equal_res : res -> res -> bool + + val init : unit -> t + (** Initialize the system under test. *) + + val cleanup : t -> unit + (** Utility function to clean up [t] after each test instance, + e.g., for closing sockets, files, or resetting global parameters *) + + val run : cmd -> t -> res + (** [run c t] should interpret the command [c] over the system under test [t] (typically side-effecting). *) +end + +(** A functor to create test setups, for all backends (Domain, Thread and Effect). + We use it below, but it can also be used independently *) +module Make(Spec : CmdSpec) + = struct + + (* plain interpreter of a cmd list *) + let interp_plain sut cs = List.map (fun c -> (c, Spec.run c sut)) cs + + let rec gen_cmds fuel = + Gen.(if fuel = 0 + then return [] + else + Spec.gen_cmd >>= fun c -> + gen_cmds (fuel-1) >>= fun cs -> + return (c::cs)) + (** A fueled command list generator. *) + + let gen_cmds_size size_gen = Gen.sized_size size_gen gen_cmds + + let shrink_triple (seq,p1,p2) = + let open Iter in + (* Shrinking heuristic: + First reduce the cmd list sizes as much as possible, since the interleaving + is most costly over long cmd lists. *) + (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq)) + <+> + (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2)) + <+> + (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s)) + <+> + (map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1)) + <+> + (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2)) + <+> + (* Secondly reduce the cmd data of individual list elements *) + (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems Spec.shrink_cmd seq)) + <+> + (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems Spec.shrink_cmd p1)) + <+> + (map (fun p2' -> (seq,p1,p2')) (Shrink.list_elems Spec.shrink_cmd p2)) + + let arb_cmds_par seq_len par_len = + let gen_triple = + Gen.(int_range 2 (2*par_len) >>= fun dbl_plen -> + let seq_pref_gen = gen_cmds_size (int_bound seq_len) in + let par_len1 = dbl_plen/2 in + let par_gen1 = gen_cmds_size (return par_len1) in + let par_gen2 = gen_cmds_size (return (dbl_plen - par_len1)) in + triple seq_pref_gen par_gen1 par_gen2) in + make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple + + let rec check_seq_cons pref cs1 cs2 seq_sut seq_trace = match pref with + | (c,res)::pref' -> + if Spec.equal_res res (Spec.run c seq_sut) + then check_seq_cons pref' cs1 cs2 seq_sut (c::seq_trace) + else (Spec.cleanup seq_sut; false) + (* Invariant: call Spec.cleanup immediately after mismatch *) + | [] -> match cs1,cs2 with + | [],[] -> Spec.cleanup seq_sut; true + | [],(c2,res2)::cs2' -> + if Spec.equal_res res2 (Spec.run c2 seq_sut) + then check_seq_cons pref cs1 cs2' seq_sut (c2::seq_trace) + else (Spec.cleanup seq_sut; false) + | (c1,res1)::cs1',[] -> + if Spec.equal_res res1 (Spec.run c1 seq_sut) + then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace) + else (Spec.cleanup seq_sut; false) + | (c1,res1)::cs1',(c2,res2)::cs2' -> + (if Spec.equal_res res1 (Spec.run c1 seq_sut) + then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace) + else (Spec.cleanup seq_sut; false)) + || + (* rerun to get seq_sut to same cmd branching point *) + (let seq_sut' = Spec.init () in + let _ = interp_plain seq_sut' (List.rev seq_trace) in + if Spec.equal_res res2 (Spec.run c2 seq_sut') + then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace) + else (Spec.cleanup seq_sut'; false)) + + (* Linearizability test *) + let lin_test ~rep_count ~count ~retries ~name ~lin_prop = + let arb_cmd_triple = arb_cmds_par 20 12 in + Test.make ~count ~retries ~name + arb_cmd_triple (repeat rep_count lin_prop) + + (* Negative linearizability test *) + let neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop = + let arb_cmd_triple = arb_cmds_par 20 12 in + Test.make_neg ~count ~retries ~name + arb_cmd_triple (repeat rep_count lin_prop) +end diff --git a/lib/lin_thread.ml b/lib/lin_thread.ml new file mode 100644 index 000000000..3ec96eb41 --- /dev/null +++ b/lib/lin_thread.ml @@ -0,0 +1,46 @@ +open Lin_base + +module Make_internal (Spec : Lin_internal.CmdSpec) = struct + module M = Lin_internal.Make(Spec) + include M + + (* Note: On purpose we use + - a non-tail-recursive function and + - an (explicit) allocation in the loop body + since both trigger statistically significant more thread issues/interleaving *) + let rec interp_thread sut cs = match cs with + | [] -> [] + | c::cs -> + Thread.yield (); + let res = Spec.run c sut in + (c,res)::interp_thread sut cs + + (* Linearizability property based on [Thread] *) + let lin_prop_thread = + (fun (seq_pref, cmds1, cmds2) -> + let sut = Spec.init () in + let obs1, obs2 = ref [], ref [] in + let pref_obs = interp_plain sut seq_pref in + let wait = ref true in + let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := interp_thread sut cmds1) () in + let th2 = Thread.create (fun () -> wait := false; obs2 := interp_thread sut cmds2) () in + Thread.join th1; + Thread.join th2; + Spec.cleanup sut; + let seq_sut = Spec.init () in + (* we reuse [check_seq_cons] to linearize and interpret sequentially *) + check_seq_cons pref_obs !obs1 !obs2 seq_sut [] + || QCheck.Test.fail_reportf " Results incompatible with sequential execution\n\n%s" + @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 + (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r)) + (pref_obs,!obs1,!obs2)) + + let lin_test ~count ~name = + lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop_thread + + let neg_lin_test ~count ~name = + neg_lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop_thread +end + +module Make (Spec : Lin_common.ApiSpec) = + Make_internal(Lin_common.MakeCmd(Spec)) diff --git a/src/array/dune b/src/array/dune index 0129a445a..bf98065f0 100644 --- a/src/array/dune +++ b/src/array/dune @@ -25,7 +25,7 @@ (name lin_tests) (modules lin_tests) (flags (:standard -w -27)) - (libraries lin) + (libraries qcheck-lin.domain) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) ; (rule @@ -37,7 +37,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain)) (rule (alias runtest) diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml index dd32947ba..1703f0041 100644 --- a/src/array/lin_tests.ml +++ b/src/array/lin_tests.ml @@ -56,8 +56,8 @@ struct let cleanup _ = () end -module AT = Lin.Make(AConf) +module AT_domain = Lin_domain.Make_internal(AConf) ;; QCheck_base_runner.run_tests_main [ - AT.neg_lin_test `Domain ~count:1000 ~name:"Lin Array test with Domain"; + AT_domain.neg_lin_test ~count:1000 ~name:"Lin Array test with Domain"; ] diff --git a/src/array/lin_tests_dsl.ml b/src/array/lin_tests_dsl.ml index a273acceb..adedceb36 100644 --- a/src/array/lin_tests_dsl.ml +++ b/src/array/lin_tests_dsl.ml @@ -9,7 +9,7 @@ struct let init () = Array.make array_size 'a' let cleanup _ = () - open Lin_api + open Lin_base let int,char = nat_small,char_printable let array_to_seq a = List.to_seq (List.of_seq (Array.to_seq a)) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *) let api = @@ -26,8 +26,8 @@ struct ] end -module AT = Lin_api.Make(AConf) +module AT_domain = Lin_domain.Make(AConf) ;; QCheck_base_runner.run_tests_main [ - AT.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Array test with Domain"; + AT_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Array test with Domain"; ] diff --git a/src/atomic/dune b/src/atomic/dune index 170b1a848..887fac86c 100644 --- a/src/atomic/dune +++ b/src/atomic/dune @@ -31,7 +31,7 @@ (name lin_tests) (modules lin_tests) (flags (:standard -w -27)) - (libraries lin) + (libraries qcheck-lin.domain) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) ; (rule @@ -43,7 +43,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain)) (rule (alias runtest) diff --git a/src/atomic/lin_tests.ml b/src/atomic/lin_tests.ml index 56812170a..f4cae6e83 100644 --- a/src/atomic/lin_tests.ml +++ b/src/atomic/lin_tests.ml @@ -42,7 +42,7 @@ struct let cleanup _ = () end -module AT = Lin.Make(AConf) +module AT_domain = Lin_domain.Make_internal(AConf) (** A variant of the above with 3 Atomics *) module A3Conf = @@ -85,9 +85,9 @@ struct let cleanup _ = () end -module A3T = Lin.Make(A3Conf) +module A3T_domain = Lin_domain.Make_internal(A3Conf) ;; QCheck_base_runner.run_tests_main [ - AT.lin_test `Domain ~count:1000 ~name:"Lin Atomic test with Domain"; - A3T.lin_test `Domain ~count:1000 ~name:"Lin Atomic3 test with Domain"; + AT_domain.lin_test ~count:1000 ~name:"Lin Atomic test with Domain"; + A3T_domain.lin_test ~count:1000 ~name:"Lin Atomic3 test with Domain"; ] diff --git a/src/atomic/lin_tests_dsl.ml b/src/atomic/lin_tests_dsl.ml index 48d9ed3da..57a2d578e 100644 --- a/src/atomic/lin_tests_dsl.ml +++ b/src/atomic/lin_tests_dsl.ml @@ -1,5 +1,5 @@ -module Atomic_spec : Lin_api.ApiSpec = struct - open Lin_api (* FIXME add Gen.nat *) +module Atomic_spec : Lin_base.ApiSpec = struct + open Lin_base (* FIXME add Gen.nat *) type t = int Atomic.t let init () = Atomic.make 0 let cleanup _ = () @@ -13,9 +13,9 @@ module Atomic_spec : Lin_api.ApiSpec = struct val_ "Atomic.decr" Atomic.decr (t @-> returning unit) ] end -module Lin_atomic = Lin_api.Make (Atomic_spec) +module Lin_atomic_domain = Lin_domain.Make (Atomic_spec) let () = QCheck_base_runner.run_tests_main - [ Lin_atomic.lin_test `Domain ~count:1000 ~name:"Lin_api Atomic test with Domain"; + [ Lin_atomic_domain.lin_test ~count:1000 ~name:"Lin DSL Atomic test with Domain"; ] diff --git a/src/bigarray/dune b/src/bigarray/dune index bbd7a14f2..9c9d1cc62 100644 --- a/src/bigarray/dune +++ b/src/bigarray/dune @@ -12,7 +12,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain)) (executable (name stm_tests) diff --git a/src/bigarray/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml index 95aaa1061..ce82fd2c2 100644 --- a/src/bigarray/lin_tests_dsl.ml +++ b/src/bigarray/lin_tests_dsl.ml @@ -14,7 +14,7 @@ struct arr let cleanup _ = () - open Lin_api + open Lin_base let int = int_small let api = @@ -25,9 +25,9 @@ struct ] end -module BA1T = Lin_api.Make(BA1Conf) +module BA1T = Lin_domain.Make(BA1Conf) let _ = QCheck_base_runner.run_tests_main [ - BA1T.neg_lin_test `Domain ~count:5000 ~name:"Lin_api Bigarray.Array1 (of ints) test with Domain"; + BA1T.neg_lin_test ~count:5000 ~name:"Lin DSL Bigarray.Array1 (of ints) test with Domain"; ] diff --git a/src/bytes/dune b/src/bytes/dune index 68e1d8898..f5ea93fa2 100644 --- a/src/bytes/dune +++ b/src/bytes/dune @@ -12,7 +12,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain qcheck-lin.thread)) (executable (name stm_tests) diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml index fefb3eaf1..5f0a48e70 100644 --- a/src/bytes/lin_tests_dsl.ml +++ b/src/bytes/lin_tests_dsl.ml @@ -6,7 +6,8 @@ module BConf = struct let init () = Stdlib.Bytes.make 42 '0' let cleanup _ = () - open Lin_api + open Lin_base + let api = [ val_ "Bytes.get" Bytes.get (t @-> int @-> returning_or_exc char); val_ "Bytes.sub_string" Bytes.sub_string (t @-> int @-> int @-> returning_or_exc string); @@ -16,9 +17,10 @@ module BConf = struct val_ "Bytes.index_from" Bytes.index_from (t @-> int @-> char @-> returning_or_exc int)] end -module BT = Lin_api.Make(BConf) +module BT_domain = Lin_domain.Make(BConf) +module BT_thread = Lin_thread.Make(BConf) ;; QCheck_base_runner.run_tests_main [ - BT.lin_test `Domain ~count:1000 ~name:"Lin_api Bytes test with Domain"; - BT.lin_test `Thread ~count:1000 ~name:"Lin_api Bytes test with Thread"; + BT_domain.lin_test ~count:1000 ~name:"Lin DSL Bytes test with Domain"; + BT_thread.lin_test ~count:1000 ~name:"Lin DSL Bytes test with Thread"; ] diff --git a/src/ephemeron/dune b/src/ephemeron/dune index ff834a65d..cbc17cda1 100644 --- a/src/ephemeron/dune +++ b/src/ephemeron/dune @@ -20,7 +20,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain qcheck-lin.thread)) (rule (alias runtest) diff --git a/src/ephemeron/lin_tests_dsl.ml b/src/ephemeron/lin_tests_dsl.ml index c327ebabc..9b5898fcf 100644 --- a/src/ephemeron/lin_tests_dsl.ml +++ b/src/ephemeron/lin_tests_dsl.ml @@ -22,7 +22,7 @@ module EConf = let init () = E.create 42 let cleanup _ = () - open Lin_api + open Lin_base let int,string = nat_small, string_small_printable let api = [ val_ "Ephemeron.clear" E.clear (t @-> returning unit); @@ -38,9 +38,10 @@ module EConf = ] end -module ET = Lin_api.Make(EConf) +module ET_domain = Lin_domain.Make(EConf) +module ET_thread = Lin_thread.Make(EConf) ;; QCheck_base_runner.run_tests_main [ - ET.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Ephemeron test with Domain"; - ET.lin_test `Thread ~count:250 ~name:"Lin_api Ephemeron test with Thread"; + ET_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Ephemeron test with Domain"; + ET_thread.lin_test ~count:250 ~name:"Lin DSL Ephemeron test with Thread"; ] diff --git a/src/floatarray/dune b/src/floatarray/dune index e1b3ff75c..dd05e8bdd 100644 --- a/src/floatarray/dune +++ b/src/floatarray/dune @@ -24,7 +24,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain)) (rule (alias runtest) diff --git a/src/floatarray/lin_tests_dsl.ml b/src/floatarray/lin_tests_dsl.ml index c9fc8e52f..149b4a5dc 100644 --- a/src/floatarray/lin_tests_dsl.ml +++ b/src/floatarray/lin_tests_dsl.ml @@ -10,7 +10,7 @@ struct let init () = Float.Array.make array_size 0.0 let cleanup _ = () - open Lin_api + open Lin_base let int = int_small (* fully evaluate the iterator, otherwise we get too many @@ -33,9 +33,9 @@ struct ] end -module FAT = Lin_api.Make(FAConf) +module FAT = Lin_domain.Make(FAConf) let _ = QCheck_base_runner.run_tests_main [ - FAT.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Float.Array test with Domain"; + FAT.neg_lin_test ~count:1000 ~name:"Lin DSL Float.Array test with Domain"; ] diff --git a/src/hashtbl/dune b/src/hashtbl/dune index 4875acd84..848668f5c 100644 --- a/src/hashtbl/dune +++ b/src/hashtbl/dune @@ -25,7 +25,7 @@ (name lin_tests) (modules lin_tests) (flags (:standard -w -27)) - (libraries lin) + (libraries qcheck-lin.domain) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) ; (rule @@ -37,7 +37,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain)) (rule (alias runtest) diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml index c77e2773e..69f892cd4 100644 --- a/src/hashtbl/lin_tests.ml +++ b/src/hashtbl/lin_tests.ml @@ -1,5 +1,5 @@ open QCheck -open Lin +open Lin_base.Lin_internal (** ********************************************************************** *) (** Tests of thread-unsafe [Hashtbl] *) @@ -65,8 +65,8 @@ struct let cleanup _ = () end -module HT = Lin.Make(HConf) +module HT_domain = Lin_domain.Make_internal(HConf) ;; QCheck_base_runner.run_tests_main [ - HT.neg_lin_test `Domain ~count:1000 ~name:"Lin Hashtbl test with Domain"; + HT_domain.neg_lin_test ~count:1000 ~name:"Lin Hashtbl test with Domain"; ] diff --git a/src/hashtbl/lin_tests_dsl.ml b/src/hashtbl/lin_tests_dsl.ml index b0b05d513..3b4f49403 100644 --- a/src/hashtbl/lin_tests_dsl.ml +++ b/src/hashtbl/lin_tests_dsl.ml @@ -1,14 +1,14 @@ (* ********************************************************************** *) (* Tests of thread-unsafe [Hashtbl] *) (* ********************************************************************** *) -module HConf (*: Lin_api.ApiSpec*) = +module HConf (*: Lin_base.ApiSpec*) = struct type t = (char, int) Hashtbl.t let init () = Hashtbl.create ~random:false 42 let cleanup _ = () - open Lin_api + open Lin_base let int,char = nat_small,char_printable let api = [ val_ "Hashtbl.clear" Hashtbl.clear (t @-> returning unit); @@ -23,8 +23,8 @@ struct ] end -module HT = Lin_api.Make(HConf) +module HT_domain = Lin_domain.Make(HConf) ;; QCheck_base_runner.run_tests_main [ - HT.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Hashtbl test with Domain"; + HT_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Hashtbl test with Domain"; ] diff --git a/src/internal/cleanup.ml b/src/internal/cleanup.ml index 7c0148d51..75ff8cb4f 100644 --- a/src/internal/cleanup.ml +++ b/src/internal/cleanup.ml @@ -39,7 +39,7 @@ struct | Add i -> (let old = !r in r := i + old; RAdd) (* buggy: not atomic *) end -module RT = Lin.Make(RConf) +module RT = Lin_domain.Make_internal(RConf) ;; Test.check_exn (let seq_len,par_len = 20,15 in diff --git a/src/internal/dune b/src/internal/dune index a78c3d79e..3c61a6921 100644 --- a/src/internal/dune +++ b/src/internal/dune @@ -9,7 +9,7 @@ (executable (name util_print_test) (modules util_print_test) - (libraries lin)) + (libraries qcheck-multicoretests-util)) (rule (alias runtest) @@ -21,7 +21,7 @@ (executable (name cleanup) (modules cleanup) - (libraries lin) + (libraries qcheck-lin.domain) (preprocess (pps ppx_deriving.show ppx_deriving.eq))) (rule diff --git a/src/lazy/dune b/src/lazy/dune index 5a63f4f70..ef7820e9a 100644 --- a/src/lazy/dune +++ b/src/lazy/dune @@ -24,7 +24,7 @@ (executable (name lin_tests) (modules lin_tests) - (libraries lin) + (libraries qcheck-lin.domain) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) ; (rule @@ -36,7 +36,7 @@ (executable (name lin_tests_dsl) (modules lin_tests_dsl) - (libraries lin)) + (libraries qcheck-lin.domain)) ; (rule ; (alias runtest) diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml index cab3c50ad..7dbd5067b 100644 --- a/src/lazy/lin_tests.ml +++ b/src/lazy/lin_tests.ml @@ -1,5 +1,4 @@ open QCheck -open Lin (** parallel linearization tests of Lazy *) @@ -33,6 +32,7 @@ module Lazy : module LBase = struct + open Lin_base.Lin_internal type cmd = | Force | Force_val @@ -75,22 +75,22 @@ struct end -module LTlazy = Lin.Make(struct +module LTlazy = Lin_domain.Make_internal(struct include LBase let init () = lazy (work ()) end) -module LTfromval = Lin.Make(struct +module LTfromval = Lin_domain.Make_internal(struct include LBase let init () = Lazy.from_val 42 end) -module LTfromfun = Lin.Make(struct +module LTfromfun = Lin_domain.Make_internal(struct include LBase let init () = Lazy.from_fun work end) ;; QCheck_base_runner.run_tests_main (let count = 100 in - [LTlazy.neg_lin_test `Domain ~count ~name:"Lin Lazy test with Domain"; - LTfromval.lin_test `Domain ~count ~name:"Lin Lazy test with Domain from_val"; - LTfromfun.neg_lin_test `Domain ~count ~name:"Lin Lazy test with Domain from_fun"; + [LTlazy.neg_lin_test ~count ~name:"Lin Lazy test with Domain"; + LTfromval.lin_test ~count ~name:"Lin Lazy test with Domain from_val"; + LTfromfun.neg_lin_test ~count ~name:"Lin Lazy test with Domain from_fun"; ]) diff --git a/src/lazy/lin_tests_dsl.ml b/src/lazy/lin_tests_dsl.ml index fb3bb75d5..e292833d0 100644 --- a/src/lazy/lin_tests_dsl.ml +++ b/src/lazy/lin_tests_dsl.ml @@ -33,13 +33,13 @@ struct type t = int Lazy.t let cleanup _ = () - open Lin_api + open Lin_base (* hack to work around missing function generators *) let fun_gen _ty _ty' = let print_fun _ = "Stdlib.succ" in let fun_gen = QCheck.(make ~print:print_fun (Gen.return Stdlib.succ)) in - Lin_api.gen fun_gen print_fun + gen fun_gen print_fun let force_map f l = Lazy.force (Lazy.map f l) let force_map_val f l = Lazy.force (Lazy.map_val f l) @@ -57,17 +57,17 @@ struct end module LTlazyAPI = struct include LBase let init () = lazy (work ()) end -module LTlazy = Lin_api.Make(LTlazyAPI) +module LTlazy_domain = Lin_domain.Make(LTlazyAPI) module LTfromvalAPI = struct include LBase let init () = Lazy.from_val 42 end -module LTfromval = Lin_api.Make(LTfromvalAPI) +module LTfromval_domain = Lin_domain.Make(LTfromvalAPI) module LTfromfunAPI = struct include LBase let init () = Lazy.from_fun work end -module LTfromfun = Lin_api.Make(LTfromfunAPI) +module LTfromfun_domain = Lin_domain.Make(LTfromfunAPI) ;; QCheck_base_runner.run_tests_main (let count = 100 in - [LTlazy.neg_lin_test `Domain ~count ~name:"Lin_api Lazy test with Domain"; - LTfromval.lin_test `Domain ~count ~name:"Lin_api Lazy test with Domain from_val"; - LTfromfun.neg_lin_test `Domain ~count ~name:"Lin_api Lazy test with Domain from_fun"; + [LTlazy_domain.neg_lin_test ~count ~name:"Lin DSL Lazy test with Domain"; + LTfromval_domain.lin_test ~count ~name:"Lin DSL Lazy test with Domain from_val"; + LTfromfun_domain.neg_lin_test ~count ~name:"Lin DSL Lazy test with Domain from_fun"; ]) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index e5789ceac..2b961a33e 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -15,7 +15,7 @@ lin_tests_effect.exe ;; currently not run on CI lin_tests_thread_ref.exe ;; currently disabled under bytecode mode lin_tests_thread_conclist.exe - ;; Lin_api tests + ;; Lin DSL tests lin_tests_dsl_domain.exe lin_tests_dsl_effect.exe lin_tests_dsl_thread.exe)) ;; currently not run on CI @@ -82,25 +82,31 @@ (library (name lin_tests_dsl_common) (modules lin_tests_dsl_common) - (libraries lin CList)) + (libraries CList qcheck-lin.domain)) (library (name lin_tests_common) (modules lin_tests_common) - (libraries lin CList) + (libraries CList qcheck-lin.domain) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) -(executables - (names lin_tests_dsl_domain lin_tests_dsl_thread) - (modules lin_tests_dsl_domain lin_tests_dsl_thread) +(executable + (name lin_tests_dsl_domain) + (modules lin_tests_dsl_domain) (flags (:standard -w -27)) (libraries lin_tests_dsl_common)) +(executable + (name lin_tests_dsl_thread) + (modules lin_tests_dsl_thread) + (flags (:standard -w -27)) + (libraries lin_tests_dsl_common qcheck-lin.thread)) + (executable (name lin_tests_dsl_effect) (modules lin_tests_dsl_effect) (flags (:standard -w -27)) - (libraries lin_tests_dsl_common)) + (libraries lin_tests_dsl_common qcheck-lin.effect)) (rule (alias runtest) @@ -120,17 +126,23 @@ (deps lin_tests_dsl_effect.exe) (action (run ./%{deps} --verbose))) -(executables - (names lin_tests_domain lin_tests_thread_ref lin_tests_thread_conclist) - (modules lin_tests_domain lin_tests_thread_ref lin_tests_thread_conclist) +(executable + (name lin_tests_domain) + (modules lin_tests_domain) (flags (:standard -w -27)) (libraries lin_tests_common)) +(executables + (names lin_tests_thread_ref lin_tests_thread_conclist) + (modules lin_tests_thread_ref lin_tests_thread_conclist) + (flags (:standard -w -27)) + (libraries lin_tests_common qcheck-lin.thread)) + (executable (name lin_tests_effect) (modules lin_tests_effect) (flags (:standard -w -27)) - (libraries lin_tests_common) + (libraries lin_tests_common qcheck-lin.effect) (preprocess (pps ppx_deriving.show ppx_deriving.eq))) ; (rule diff --git a/src/neg_tests/lin_tests_common.ml b/src/neg_tests/lin_tests_common.ml index d0a47904c..88e9dead0 100644 --- a/src/neg_tests/lin_tests_common.ml +++ b/src/neg_tests/lin_tests_common.ml @@ -88,8 +88,8 @@ module RConf_int64 = struct let cleanup _ = () end -module RT_int = Lin.Make(RConf_int) -module RT_int64 = Lin.Make(RConf_int64) +module RT_int_domain = Lin_domain.Make_internal(RConf_int) +module RT_int64_domain = Lin_domain.Make_internal(RConf_int64) (** ********************************************************************** *) @@ -103,6 +103,8 @@ module CLConf (T : sig val shrink : t Shrink.t end) = struct + module Lin = Lin_base.Lin_internal + type t = T.t CList.conc_list Atomic.t type int' = T.t let gen_int' = Gen.(map T.of_int nat) @@ -137,5 +139,5 @@ module Int64 = struct include Stdlib.Int64 let shrink = Shrink.int64 end -module CLT_int = Lin.Make(CLConf (Int)) -module CLT_int64 = Lin.Make(CLConf (Int64)) +module CLT_int_domain = Lin_domain.Make_internal(CLConf (Int)) +module CLT_int64_domain = Lin_domain.Make_internal(CLConf (Int64)) diff --git a/src/neg_tests/lin_tests_domain.ml b/src/neg_tests/lin_tests_domain.ml index 74f1e4e09..092b1d34f 100644 --- a/src/neg_tests/lin_tests_domain.ml +++ b/src/neg_tests/lin_tests_domain.ml @@ -5,7 +5,7 @@ open Lin_tests_common ;; QCheck_base_runner.run_tests_main (let count = 15000 in - [RT_int.neg_lin_test `Domain ~count ~name:"Lin ref int test with Domain"; - RT_int64.neg_lin_test `Domain ~count ~name:"Lin ref int64 test with Domain"; - CLT_int.neg_lin_test `Domain ~count ~name:"Lin CList int test with Domain"; - CLT_int64.neg_lin_test `Domain ~count ~name:"Lin CList int64 test with Domain"]) + [RT_int_domain.neg_lin_test ~count ~name:"Lin ref int test with Domain"; + RT_int64_domain.neg_lin_test ~count ~name:"Lin ref int64 test with Domain"; + CLT_int_domain.neg_lin_test ~count ~name:"Lin CList int test with Domain"; + CLT_int64_domain.neg_lin_test ~count ~name:"Lin CList int64 test with Domain"]) diff --git a/src/neg_tests/lin_tests_dsl_common.ml b/src/neg_tests/lin_tests_dsl_common.ml index e93c6acd1..e11b163f4 100644 --- a/src/neg_tests/lin_tests_dsl_common.ml +++ b/src/neg_tests/lin_tests_dsl_common.ml @@ -1,4 +1,4 @@ -open Lin_api +open Lin_base (** ********************************************************************** *) (** Tests of a simple reference *) @@ -24,7 +24,7 @@ module Sut_int64 = let decr r = add r Int64.minus_one (* buggy: not atomic *) end -module Ref_int_spec : Lin_api.ApiSpec = struct +module Ref_int_spec : ApiSpec = struct type t = int ref let init () = Sut_int.init () let cleanup _ = () @@ -38,7 +38,7 @@ module Ref_int_spec : Lin_api.ApiSpec = struct ] end -module Ref_int64_spec : Lin_api.ApiSpec = struct +module Ref_int64_spec : ApiSpec = struct type t = int64 ref let init () = Sut_int64.init () let cleanup _ = () @@ -52,14 +52,14 @@ module Ref_int64_spec : Lin_api.ApiSpec = struct ] end -module RT_int = Lin_api.Make(Ref_int_spec) -module RT_int64 = Lin_api.Make(Ref_int64_spec) +module RT_int_domain = Lin_domain.Make(Ref_int_spec) +module RT_int64_domain = Lin_domain.Make(Ref_int64_spec) (** ********************************************************************** *) (** Tests of the buggy concurrent list CList *) (** ********************************************************************** *) -module CList_spec_int : Lin_api.ApiSpec = +module CList_spec_int : ApiSpec = struct type t = int CList.conc_list Atomic.t let init () = CList.list_init 0 @@ -71,7 +71,7 @@ struct ] end -module CList_spec_int64 : Lin_api.ApiSpec = +module CList_spec_int64 : ApiSpec = struct type t = int64 CList.conc_list Atomic.t let init () = CList.list_init Int64.zero @@ -83,6 +83,5 @@ struct ] end - -module CLT_int = Lin_api.Make(CList_spec_int) -module CLT_int64 = Lin_api.Make(CList_spec_int64) +module CLT_int_domain = Lin_domain.Make(CList_spec_int) +module CLT_int64_domain = Lin_domain.Make(CList_spec_int64) diff --git a/src/neg_tests/lin_tests_dsl_domain.ml b/src/neg_tests/lin_tests_dsl_domain.ml index 99181a6c5..a0ad1b028 100644 --- a/src/neg_tests/lin_tests_dsl_domain.ml +++ b/src/neg_tests/lin_tests_dsl_domain.ml @@ -5,7 +5,7 @@ open Lin_tests_dsl_common ;; QCheck_base_runner.run_tests_main (let count = 10000 in - [RT_int.neg_lin_test `Domain ~count ~name:"Lin_api ref int test with Domain"; - RT_int64.neg_lin_test `Domain ~count ~name:"Lin_api ref int64 test with Domain"; - CLT_int.neg_lin_test `Domain ~count ~name:"Lin_api CList int test with Domain"; - CLT_int64.neg_lin_test `Domain ~count ~name:"Lin_api CList int64 test with Domain"]) + [RT_int_domain.neg_lin_test ~count ~name:"Lin DSL ref int test with Domain"; + RT_int64_domain.neg_lin_test ~count ~name:"Lin DSL ref int64 test with Domain"; + CLT_int_domain.neg_lin_test ~count ~name:"Lin DSL CList int test with Domain"; + CLT_int64_domain.neg_lin_test ~count ~name:"Lin DSL CList int64 test with Domain"]) diff --git a/src/neg_tests/lin_tests_dsl_effect.ml b/src/neg_tests/lin_tests_dsl_effect.ml index 409e97481..97f0a6dd5 100644 --- a/src/neg_tests/lin_tests_dsl_effect.ml +++ b/src/neg_tests/lin_tests_dsl_effect.ml @@ -1,5 +1,5 @@ open Lin_tests_dsl_common -open Lin_api +open Lin_base (** This is a driver of the negative tests over the Effect module *) @@ -10,10 +10,10 @@ open Lin_api such as when interpreting these sequentially. *) module Sut_int' = struct include Sut_int - let add r i = let old = !r in Lin.yield (); set r (old+i) + let add r i = let old = !r in Lin_effect.yield (); set r (old+i) end -module Ref_int'_spec : Lin_api.ApiSpec = struct +module Ref_int'_spec : ApiSpec = struct type t = int ref let init () = Sut_int'.init () let cleanup _ = () @@ -26,14 +26,15 @@ module Ref_int'_spec : Lin_api.ApiSpec = struct ] end -module RT_int' = Lin_api.Make(Ref_int'_spec) +module RT_int_effect = Lin_effect.Make(Ref_int_spec) +module RT_int'_effect = Lin_effect.Make(Ref_int'_spec) module Sut_int64' = struct include Sut_int64 - let add r i = let old = !r in Lin.yield (); set r (Int64.add old i) + let add r i = let old = !r in Lin_effect.yield (); set r (Int64.add old i) end -module Ref_int64'_spec : Lin_api.ApiSpec = struct +module Ref_int64'_spec : ApiSpec = struct type t = int64 ref let init () = Sut_int64'.init () let cleanup _ = () @@ -46,25 +47,26 @@ module Ref_int64'_spec : Lin_api.ApiSpec = struct ] end -module RT_int64' = Lin_api.Make(Ref_int64'_spec) +module RT_int64_effect = Lin_effect.Make(Ref_int64_spec) +module RT_int64'_effect = Lin_effect.Make(Ref_int64'_spec) -module CList_spec_int' : Lin_api.ApiSpec = +module CList_spec_int' : ApiSpec = struct type t = int CList.conc_list Atomic.t let init () = CList.list_init 0 let cleanup _ = () - let add_node r i = Lin.yield (); CList.add_node r i + let add_node r i = Lin_effect.yield (); CList.add_node r i let api = [ val_ "CList.add_node" add_node (t @-> int @-> returning_or_exc bool); val_ "CList.member" CList.member (t @-> int @-> returning bool); ] end -module CList_spec_int64' : Lin_api.ApiSpec = +module CList_spec_int64' : ApiSpec = struct type t = int64 CList.conc_list Atomic.t let init () = CList.list_init Int64.zero - let add_node r i = Lin.yield (); CList.add_node r i + let add_node r i = Lin_effect.yield (); CList.add_node r i let cleanup _ = () let api = [ val_ "CList.add_node" add_node (t @-> int64 @-> returning_or_exc bool); @@ -72,19 +74,22 @@ struct ] end -module CLT_int' = Lin_api.Make(CList_spec_int') -module CLT_int64' = Lin_api.Make(CList_spec_int64') +module CLT_int_effect = Lin_effect.Make(CList_spec_int) +module CLT_int'_effect = Lin_effect.Make(CList_spec_int') +module CLT_int64_effect = Lin_effect.Make(CList_spec_int64) +module CLT_int64'_effect = Lin_effect.Make(CList_spec_int64') + ;; QCheck_base_runner.run_tests_main (let count = 20_000 in [ (* We don't expect the first four tests to fail as each `cmd` is completed before a `Yield` *) - RT_int.lin_test `Effect ~count ~name:"Lin_api ref int test with Effect"; - RT_int64.lin_test `Effect ~count ~name:"Lin_api ref int64 test with Effect"; - CLT_int.lin_test `Effect ~count ~name:"Lin_api CList int test with Effect"; - CLT_int64.lin_test `Effect ~count ~name:"Lin_api CList int64 test with Effect"; + RT_int_effect.lin_test ~count ~name:"Lin DSL ref int test with Effect"; + RT_int64_effect.lin_test ~count ~name:"Lin DSL ref int64 test with Effect"; + CLT_int_effect.lin_test ~count ~name:"Lin DSL CList int test with Effect"; + CLT_int64_effect.lin_test ~count ~name:"Lin DSL CList int64 test with Effect"; (* These next four tests are negative - and are expected to fail with exception `Unhandled` *) - RT_int'.neg_lin_test `Effect ~count ~name:"negative Lin_api ref int test with Effect"; - RT_int64'.neg_lin_test `Effect ~count ~name:"negative Lin_api ref int64 test with Effect"; - CLT_int'.neg_lin_test `Effect ~count ~name:"negative Lin_api CList int test with Effect"; - CLT_int64'.neg_lin_test `Effect ~count ~name:"negative Lin_api CList int64 test with Effect" + RT_int'_effect.neg_lin_test ~count ~name:"negative Lin DSL ref int test with Effect"; + RT_int64'_effect.neg_lin_test ~count ~name:"negative Lin DSL ref int64 test with Effect"; + CLT_int'_effect.neg_lin_test ~count ~name:"negative Lin DSL CList int test with Effect"; + CLT_int64'_effect.neg_lin_test ~count ~name:"negative Lin DSL CList int64 test with Effect" ]) diff --git a/src/neg_tests/lin_tests_dsl_thread.ml b/src/neg_tests/lin_tests_dsl_thread.ml index bffed5716..064db3e5e 100644 --- a/src/neg_tests/lin_tests_dsl_thread.ml +++ b/src/neg_tests/lin_tests_dsl_thread.ml @@ -2,10 +2,15 @@ open Lin_tests_dsl_common (** This is a driver of the negative tests over the Thread module *) +module RT_int_thread = Lin_thread.Make(Ref_int_spec) +module RT_int64_thread = Lin_thread.Make(Ref_int64_spec) +module CLT_int_thread = Lin_thread.Make(CList_spec_int) +module CLT_int64_thread = Lin_thread.Make(CList_spec_int64) + ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [RT_int.lin_test `Thread ~count ~name:"Lin_api ref int test with Thread"; - RT_int64.neg_lin_test `Thread ~count ~name:"Lin_api ref int64 test with Thread"; - CLT_int.lin_test `Thread ~count ~name:"Lin_api CList int test with Thread"; - CLT_int64.lin_test `Thread ~count ~name:"Lin_api CList int64 test with Thread"]) + [RT_int_thread.lin_test ~count ~name:"Lin ref int test with Thread"; (* unboxed, hence no allocations to trigger context switch *) + RT_int64_thread.neg_lin_test ~count:15000 ~name:"Lin ref int64 test with Thread"; + CLT_int_thread.lin_test ~count ~name:"Lin CList int test with Thread"; (* unboxed, hence no allocations to trigger context switch *) + CLT_int64_thread.lin_test ~count ~name:"Lin CList int64 test with Thread"]) (* not triggering context switch, unfortunately *) diff --git a/src/neg_tests/lin_tests_effect.ml b/src/neg_tests/lin_tests_effect.ml index 517d78bb2..09d5eb9f1 100644 --- a/src/neg_tests/lin_tests_effect.ml +++ b/src/neg_tests/lin_tests_effect.ml @@ -16,11 +16,13 @@ struct let run c r = match c with | Get -> RGet (Sut_int.get r) | Set i -> (Sut_int.set r i; RSet) - | Add i -> (try let tmp = Sut_int.get r in Lin.yield (); Sut_int.set r (tmp+i); RAdd (Ok ()) with exn -> RAdd (Error exn)) + | Add i -> (try let tmp = Sut_int.get r in Lin_effect.yield (); Sut_int.set r (tmp+i); RAdd (Ok ()) with exn -> RAdd (Error exn)) | Incr -> (Sut_int.incr r; RIncr) | Decr -> (Sut_int.decr r; RDecr) end -module RT_int' = Lin.Make(RConf_int') + +module RT_int_effect = Lin_effect.Make_internal(RConf_int) +module RT_int'_effect = Lin_effect.Make_internal(RConf_int') module RConf_int64' = struct @@ -30,42 +32,45 @@ struct let run c r = match c with | Get -> RGet (Sut_int64.get r) | Set i -> (Sut_int64.set r i; RSet) - | Add i -> (try let tmp = Sut_int.get r in Lin.yield (); Sut_int.set r (Int64.add tmp i); RAdd (Ok ()) with exn -> RAdd (Error exn)) + | Add i -> (try let tmp = Sut_int.get r in Lin_effect.yield (); Sut_int.set r (Int64.add tmp i); RAdd (Ok ()) with exn -> RAdd (Error exn)) | Incr -> (Sut_int64.incr r; RIncr) | Decr -> (Sut_int64.decr r; RDecr) end -module RT_int64' = Lin.Make(RConf_int64') +module RT_int64_effect = Lin_effect.Make_internal(RConf_int64) +module RT_int64'_effect = Lin_effect.Make_internal(RConf_int64') module CLConf_int' = struct include CLConf(Int) type res = RAdd_node of (bool,exn) result | RMember of bool [@@deriving show { with_path = false }, eq] let run c r = match c with - | Add_node i -> RAdd_node (try Lin.yield (); Ok (CList.add_node r i) with exn -> Error exn) + | Add_node i -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r i) with exn -> Error exn) | Member i -> RMember (CList.member r i) end -module CLT_int' = Lin.Make(CLConf_int') +module CLT_int_effect = Lin_effect.Make_internal(CLConf (Int)) +module CLT_int'_effect = Lin_effect.Make_internal(CLConf_int') module CLConf_int64' = struct include CLConf(Int64) type res = RAdd_node of (bool,exn) result | RMember of bool [@@deriving show { with_path = false }, eq] let run c r = match c with - | Add_node i -> RAdd_node (try Lin.yield (); Ok (CList.add_node r i) with exn -> Error exn) + | Add_node i -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r i) with exn -> Error exn) | Member i -> RMember (CList.member r i) end -module CLT_int64' = Lin.Make(CLConf_int64') +module CLT_int64_effect = Lin_effect.Make_internal(CLConf(Int64)) +module CLT_int64'_effect = Lin_effect.Make_internal(CLConf_int64') ;; QCheck_base_runner.run_tests_main (let count = 20_000 in [ (* We don't expect the first four tests to fail as each `cmd` is completed before a `Yield` *) - RT_int.lin_test `Effect ~count ~name:"Lin ref int test with Effect"; - RT_int64.lin_test `Effect ~count ~name:"Lin ref int64 test with Effect"; - CLT_int.lin_test `Effect ~count ~name:"Lin CList int test with Effect"; - CLT_int64.lin_test `Effect ~count ~name:"Lin CList int64 test with Effect"; + RT_int_effect.lin_test ~count ~name:"Lin ref int test with Effect"; + RT_int64_effect.lin_test ~count ~name:"Lin ref int64 test with Effect"; + CLT_int_effect.lin_test ~count ~name:"Lin CList int test with Effect"; + CLT_int64_effect.lin_test ~count ~name:"Lin CList int64 test with Effect"; (* These next four tests are negative - and are expected to fail with exception `Unhandled` *) - RT_int'.neg_lin_test `Effect ~count ~name:"negative Lin ref int test with Effect"; - RT_int64'.neg_lin_test `Effect ~count ~name:"negative Lin ref int64 test with Effect"; - CLT_int'.neg_lin_test `Effect ~count ~name:"negative Lin CList int test with Effect"; - CLT_int64'.neg_lin_test `Effect ~count ~name:"negative Lin CList int64 test with Effect" + RT_int'_effect.neg_lin_test ~count ~name:"negative Lin ref int test with Effect"; + RT_int64'_effect.neg_lin_test ~count ~name:"negative Lin ref int64 test with Effect"; + CLT_int'_effect.neg_lin_test ~count ~name:"negative Lin CList int test with Effect"; + CLT_int64'_effect.neg_lin_test ~count ~name:"negative Lin CList int64 test with Effect" ]) diff --git a/src/neg_tests/lin_tests_thread_conclist.ml b/src/neg_tests/lin_tests_thread_conclist.ml index cf81475b2..d1b4efa35 100644 --- a/src/neg_tests/lin_tests_thread_conclist.ml +++ b/src/neg_tests/lin_tests_thread_conclist.ml @@ -2,8 +2,11 @@ open Lin_tests_common (** This is a driver of the negative CList tests over the Thread module *) +module CLT_int_thread = Lin_thread.Make_internal(CLConf (Int)) +module CLT_int64_thread = Lin_thread.Make_internal(CLConf (Int64)) + ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [CLT_int.lin_test `Thread ~count ~name:"Lin CList int test with Thread"; (* unboxed, hence no allocations to trigger context switch *) - CLT_int64.lin_test `Thread ~count ~name:"Lin CList int64 test with Thread"]) (* not triggering context switch, unfortunately *) + [CLT_int_thread.lin_test ~count ~name:"Lin CList int test with Thread"; (* unboxed, hence no allocations to trigger context switch *) + CLT_int64_thread.lin_test ~count ~name:"Lin CList int64 test with Thread"]) (* not triggering context switch, unfortunately *) diff --git a/src/neg_tests/lin_tests_thread_ref.ml b/src/neg_tests/lin_tests_thread_ref.ml index 2eb89eef6..8d264b26f 100644 --- a/src/neg_tests/lin_tests_thread_ref.ml +++ b/src/neg_tests/lin_tests_thread_ref.ml @@ -2,6 +2,9 @@ open Lin_tests_common (** This is a driver of the negative ref tests over the Thread module *) +module RT_int_thread = Lin_thread.Make_internal(RConf_int) +module RT_int64_thread = Lin_thread.Make_internal(RConf_int64) + ;; if Sys.backend_type = Sys.Bytecode then @@ -9,5 +12,5 @@ then else QCheck_base_runner.run_tests_main (let count = 1000 in - [RT_int.lin_test `Thread ~count ~name:"Lin ref int test with Thread"; (* unboxed, hence no allocations to trigger context switch *) - RT_int64.neg_lin_test `Thread ~count:15000 ~name:"Lin ref int64 test with Thread"]) + [RT_int64_thread.lin_test ~count ~name:"Lin ref int test with Thread"; (* unboxed, hence no allocations to trigger context switch *) + RT_int64_thread.neg_lin_test ~count:15000 ~name:"Lin ref int64 test with Thread"]) diff --git a/src/queue/dune b/src/queue/dune index ccb8e1744..749c59657 100644 --- a/src/queue/dune +++ b/src/queue/dune @@ -12,7 +12,7 @@ (name lin_tests_dsl) (modules lin_tests_dsl) (flags (:standard -w -27)) - (libraries lin)) + (libraries qcheck-lin.domain qcheck-lin.thread)) (rule (alias runtest) @@ -24,7 +24,7 @@ (name lin_tests) (modules lin_tests) (flags (:standard -w -27)) - (libraries lin) + (libraries qcheck-lin.domain qcheck-lin.thread) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) ; (rule diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml index 40b2f90b6..0d9774b4b 100644 --- a/src/queue/lin_tests.ml +++ b/src/queue/lin_tests.ml @@ -1,5 +1,5 @@ open QCheck -open Lin +open Lin_base.Lin_internal module Spec = struct @@ -105,12 +105,14 @@ module QMutexConf = RClear end -module QMT = Lin.Make(QMutexConf) -module QT = Lin.Make(QConf) +module QMT_domain = Lin_domain.Make_internal(QMutexConf) +module QMT_thread = Lin_thread.Make_internal(QMutexConf) +module QT_domain = Lin_domain.Make_internal(QConf) +module QT_thread = Lin_thread.Make_internal(QConf) ;; QCheck_base_runner.run_tests_main [ - QMT.lin_test `Domain ~count:1000 ~name:"Lin Queue test with Domain and mutex"; - QMT.lin_test `Thread ~count:1000 ~name:"Lin Queue test with Thread and mutex"; - QT.neg_lin_test `Domain ~count:1000 ~name:"Lin Queue test with Domain without mutex"; - QT.lin_test `Thread ~count:1000 ~name:"Lin Queue test with Thread without mutex"; + QMT_domain.lin_test ~count:1000 ~name:"Lin Queue test with Domain and mutex"; + QMT_thread.lin_test ~count:1000 ~name:"Lin Queue test with Thread and mutex"; + QT_domain.neg_lin_test ~count:1000 ~name:"Lin Queue test with Domain without mutex"; + QT_thread.lin_test ~count:1000 ~name:"Lin Queue test with Thread without mutex"; ] diff --git a/src/queue/lin_tests_dsl.ml b/src/queue/lin_tests_dsl.ml index 7626b625d..3c3621515 100644 --- a/src/queue/lin_tests_dsl.ml +++ b/src/queue/lin_tests_dsl.ml @@ -1,5 +1,5 @@ -module Queue_spec : Lin_api.ApiSpec = struct - open Lin_api +module Queue_spec : Lin_base.ApiSpec = struct + open Lin_base type t = int Queue.t let init () = Queue.create () let cleanup _ = () @@ -17,10 +17,11 @@ module Queue_spec : Lin_api.ApiSpec = struct ] end -module Lin_queue = Lin_api.Make(Queue_spec) +module Lin_queue_domain = Lin_domain.Make(Queue_spec) +module Lin_queue_thread = Lin_thread.Make(Queue_spec) let () = QCheck_base_runner.run_tests_main [ - Lin_queue.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Queue test with Domain"; - Lin_queue.lin_test `Thread ~count:250 ~name:"Lin_api Queue test with Thread"; + Lin_queue_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Queue test with Domain"; + Lin_queue_thread.lin_test ~count:250 ~name:"Lin DSL Queue test with Thread"; ] diff --git a/src/stack/dune b/src/stack/dune index 57824ee16..71636f88d 100644 --- a/src/stack/dune +++ b/src/stack/dune @@ -12,7 +12,7 @@ (name lin_tests_dsl) (modules lin_tests_dsl) (flags (:standard -w -27)) - (libraries lin)) + (libraries qcheck-lin.domain qcheck-lin.thread)) (rule (alias runtest) @@ -24,7 +24,7 @@ (name lin_tests) (modules lin_tests) (flags (:standard -w -27)) - (libraries lin) + (libraries qcheck-lin.domain qcheck-lin.thread) (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) ; (rule diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml index a7fd752fd..b893dec24 100644 --- a/src/stack/lin_tests.ml +++ b/src/stack/lin_tests.ml @@ -1,5 +1,5 @@ open QCheck -open Lin +open Lin_base.Lin_internal module Spec = struct @@ -105,12 +105,14 @@ module SMutexConf = RLength l end -module ST = Lin.Make(SConf) -module SMT = Lin.Make(SMutexConf) +module ST_domain = Lin_domain.Make_internal(SConf) +module ST_thread = Lin_thread.Make_internal(SConf) +module SMT_domain = Lin_domain.Make_internal(SMutexConf) +module SMT_thread = Lin_thread.Make_internal(SMutexConf) ;; QCheck_base_runner.run_tests_main [ - SMT.lin_test `Domain ~count:1000 ~name:"Lin Stack test with Domain and mutex"; - SMT.lin_test `Thread ~count:1000 ~name:"Lin Stack test with Thread and mutex"; - ST.neg_lin_test `Domain ~count:1000 ~name:"Lin Stack test with Domain without mutex"; - ST.lin_test `Thread ~count:1000 ~name:"Lin Stack test with Thread without mutex"; + SMT_domain.lin_test ~count:1000 ~name:"Lin Stack test with Domain and mutex"; + SMT_thread.lin_test ~count:1000 ~name:"Lin Stack test with Thread and mutex"; + ST_domain.neg_lin_test ~count:1000 ~name:"Lin Stack test with Domain without mutex"; + ST_thread.lin_test ~count:1000 ~name:"Lin Stack test with Thread without mutex"; ] diff --git a/src/stack/lin_tests_dsl.ml b/src/stack/lin_tests_dsl.ml index dbe7c772a..4c0aac41f 100644 --- a/src/stack/lin_tests_dsl.ml +++ b/src/stack/lin_tests_dsl.ml @@ -1,5 +1,5 @@ -module Stack_spec : Lin_api.ApiSpec = struct - open Lin_api +module Stack_spec : Lin_base.ApiSpec = struct + open Lin_base type t = int Stack.t let init () = Stack.create () let cleanup _ = () @@ -17,10 +17,11 @@ module Stack_spec : Lin_api.ApiSpec = struct ] end -module Lin_stack = Lin_api.Make(Stack_spec) +module Stack_domain = Lin_domain.Make(Stack_spec) +module Stack_thread = Lin_thread.Make(Stack_spec) let () = QCheck_base_runner.run_tests_main [ - Lin_stack.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Stack test with Domain"; - Lin_stack.lin_test `Thread ~count:250 ~name:"Lin_api Stack test with Thread"; + Stack_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Stack test with Domain"; + Stack_thread.lin_test ~count:250 ~name:"Lin DSL Stack test with Thread"; ]