From 731293f208534a601b7a5ade22a43791ab435aa7 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 14 Nov 2022 15:40:31 +0100 Subject: [PATCH 1/6] Split up Lin modules to separate threads, domains and effects This commit only moves lines into their respective new modules so that it is possible to check that it does no other refactoring. Thus it obviously does not build Bisection: skip --- lib/lin.ml | 325 ---------------------------- lib/{lin_api.ml => lin_common.ml} | 0 lib/{lin_api.mli => lin_common.mli} | 0 lib/lin_domain.ml | 35 +++ lib/lin_effect.ml | 115 ++++++++++ lib/lin_internal.ml | 137 ++++++++++++ lib/lin_thread.ml | 42 ++++ 7 files changed, 329 insertions(+), 325 deletions(-) delete mode 100644 lib/lin.ml rename lib/{lin_api.ml => lin_common.ml} (100%) rename lib/{lin_api.mli => lin_common.mli} (100%) create mode 100644 lib/lin_domain.ml create mode 100644 lib/lin_effect.ml create mode 100644 lib/lin_internal.ml create mode 100644 lib/lin_thread.ml 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_api.ml b/lib/lin_common.ml similarity index 100% rename from lib/lin_api.ml rename to lib/lin_common.ml diff --git a/lib/lin_api.mli b/lib/lin_common.mli similarity index 100% rename from lib/lin_api.mli rename to lib/lin_common.mli diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml new file mode 100644 index 000000000..c92bf709f --- /dev/null +++ b/lib/lin_domain.ml @@ -0,0 +1,35 @@ + (* 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 [] + || 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) + + | `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) + + | `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) diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml new file mode 100644 index 000000000..f927754af --- /dev/null +++ b/lib/lin_effect.ml @@ -0,0 +1,115 @@ +(** 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 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)) + + | `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) + + | `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) diff --git a/lib/lin_internal.ml b/lib/lin_internal.ml new file mode 100644 index 000000000..da63ba426 --- /dev/null +++ b/lib/lin_internal.ml @@ -0,0 +1,137 @@ +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 + + 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)) +end + +(** 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 + + 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 + + (* 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 +end diff --git a/lib/lin_thread.ml b/lib/lin_thread.ml new file mode 100644 index 000000000..397689684 --- /dev/null +++ b/lib/lin_thread.ml @@ -0,0 +1,42 @@ + (* 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 [] + || 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)) + + | `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) + + | `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) From 6059efc3820b3523ed604a87d6936ce6a66afc25 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 14 Nov 2022 17:44:42 +0100 Subject: [PATCH 2/6] Fix Lin libraries after split Add a Lin_base module, as the entrypoint of the qcheck-lin.base library --- lib/dune | 27 +++++++++++++++++++++----- lib/lin_base.ml | 3 +++ lib/lin_common.ml | 4 +--- lib/lin_common.mli | 7 +------ lib/lin_domain.ml | 28 +++++++++++++++------------ lib/lin_effect.ml | 47 ++++++++++++++++++++++++++++----------------- lib/lin_internal.ml | 33 +++++++++++++------------------ lib/lin_thread.ml | 28 +++++++++++++++------------ 8 files changed, 101 insertions(+), 76 deletions(-) create mode 100644 lib/lin_base.ml 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_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_common.ml b/lib/lin_common.ml index 0d301e728..d9f127aef 100644 --- a/lib/lin_common.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_common.mli b/lib/lin_common.mli index 132390878..5f9c6c830 100644 --- a/lib/lin_common.mli +++ b/lib/lin_common.mli @@ -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 index c92bf709f..424cf92ff 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -1,3 +1,9 @@ +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 @@ -17,19 +23,17 @@ 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 + || 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) - | `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) + 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 - | `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) +module Make (Spec : Lin_common.ApiSpec) = + Make_internal(Lin_common.MakeCmd(Spec)) diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml index f927754af..a3fd50fc6 100644 --- a/lib/lin_effect.ml +++ b/lib/lin_effect.ml @@ -1,3 +1,5 @@ +open Lin_base + (** Definitions for Effect interpretation *) (* Scheduler adapted from https://kcsrk.info/slides/retro_effects_simcorp.pdf *) @@ -31,11 +33,13 @@ let start_sched main = 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 @@ -75,10 +79,16 @@ let yield () = perform Yield UserRes res end - module EffTest = MakeDomThr(EffSpec) + 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) -> @@ -87,29 +97,30 @@ let yield () = perform Yield 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 + 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 [] - || Test.fail_reportf " Results incompatible with linearized model\n\n%s" + || 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)) - | `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) - - | `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) + 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 index da63ba426..f309ed343 100644 --- a/lib/lin_internal.ml +++ b/lib/lin_internal.ml @@ -37,9 +37,9 @@ module type CmdSpec = sig (** [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. +(** 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 MakeDomThr(Spec : CmdSpec) +module Make(Spec : CmdSpec) = struct (* plain interpreter of a cmd list *) @@ -115,23 +115,16 @@ module MakeDomThr(Spec : CmdSpec) 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)) -end - -(** 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 - - 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 - (* 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 + (* 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 index 397689684..3ec96eb41 100644 --- a/lib/lin_thread.ml +++ b/lib/lin_thread.ml @@ -1,3 +1,9 @@ +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 @@ -24,19 +30,17 @@ 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 + || 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)) - | `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) + 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 - | `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) +module Make (Spec : Lin_common.ApiSpec) = + Make_internal(Lin_common.MakeCmd(Spec)) From ddf2e9b0d3772b429cd9555029ab8a5c4edbb55f Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 14 Nov 2022 18:36:01 +0100 Subject: [PATCH 3/6] Adapt the multicore tests to the new Lin interface --- src/array/dune | 4 +- src/array/lin_tests.ml | 4 +- src/array/lin_tests_dsl.ml | 6 +-- src/atomic/dune | 4 +- src/atomic/lin_tests.ml | 8 ++-- src/atomic/lin_tests_dsl.ml | 8 ++-- src/bigarray/dune | 2 +- src/bigarray/lin_tests_dsl.ml | 6 +-- src/bytes/dune | 2 +- src/bytes/lin_tests_dsl.ml | 10 +++-- src/ephemeron/dune | 2 +- src/ephemeron/lin_tests_dsl.ml | 9 +++-- src/floatarray/dune | 2 +- src/floatarray/lin_tests_dsl.ml | 6 +-- src/hashtbl/dune | 4 +- src/hashtbl/lin_tests.ml | 6 +-- src/hashtbl/lin_tests_dsl.ml | 8 ++-- src/internal/cleanup.ml | 2 +- src/internal/dune | 4 +- src/lazy/dune | 4 +- src/lazy/lin_tests.ml | 14 +++---- src/lazy/lin_tests_dsl.ml | 16 ++++---- src/neg_tests/dune | 32 ++++++++++----- src/neg_tests/lin_tests_common.ml | 10 +++-- src/neg_tests/lin_tests_domain.ml | 8 ++-- src/neg_tests/lin_tests_dsl_common.ml | 19 +++++---- src/neg_tests/lin_tests_dsl_domain.ml | 8 ++-- src/neg_tests/lin_tests_dsl_effect.ml | 47 ++++++++++++---------- src/neg_tests/lin_tests_dsl_thread.ml | 13 ++++-- src/neg_tests/lin_tests_effect.ml | 37 +++++++++-------- src/neg_tests/lin_tests_thread_conclist.ml | 7 +++- src/neg_tests/lin_tests_thread_ref.ml | 7 +++- src/queue/dune | 4 +- src/queue/lin_tests.ml | 16 ++++---- src/queue/lin_tests_dsl.ml | 11 ++--- src/stack/dune | 4 +- src/stack/lin_tests.ml | 16 ++++---- src/stack/lin_tests_dsl.ml | 11 ++--- 38 files changed, 212 insertions(+), 169 deletions(-) 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..c96ddfd46 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_api 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..b0d7d7eb7 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_api 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..a2990c325 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_api 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..c37b36c7a 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_api Bytes test with Domain"; + BT_thread.lin_test ~count:1000 ~name:"Lin_api 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..d5e0e5f3d 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_api Ephemeron test with Domain"; + ET_thread.lin_test ~count:250 ~name:"Lin_api 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..741ad6c37 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_api 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..5d862de0f 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_api 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..2eef7246e 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_api Lazy test with Domain"; + LTfromval_domain.lin_test ~count ~name:"Lin_api Lazy test with Domain from_val"; + LTfromfun_domain.neg_lin_test ~count ~name:"Lin_api Lazy test with Domain from_fun"; ]) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index e5789ceac..1eca13d96 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -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..f04ac0026 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_api ref int test with Domain"; + RT_int64_domain.neg_lin_test ~count ~name:"Lin_api ref int64 test with Domain"; + CLT_int_domain.neg_lin_test ~count ~name:"Lin_api CList int test with Domain"; + CLT_int64_domain.neg_lin_test ~count ~name:"Lin_api 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..82b9b8d9e 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_api ref int test with Effect"; + RT_int64_effect.lin_test ~count ~name:"Lin_api ref int64 test with Effect"; + CLT_int_effect.lin_test ~count ~name:"Lin_api CList int test with Effect"; + CLT_int64_effect.lin_test ~count ~name:"Lin_api 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_api ref int test with Effect"; + RT_int64'_effect.neg_lin_test ~count ~name:"negative Lin_api ref int64 test with Effect"; + CLT_int'_effect.neg_lin_test ~count ~name:"negative Lin_api CList int test with Effect"; + CLT_int64'_effect.neg_lin_test ~count ~name:"negative Lin_api 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..ac962ab80 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_api Queue test with Domain"; + Lin_queue_thread.lin_test ~count:250 ~name:"Lin_api 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..8209fb8c7 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_api Stack test with Domain"; + Stack_thread.lin_test ~count:250 ~name:"Lin_api Stack test with Thread"; ] From 1b4d4772fb01cbe1f95a4db2419a4fd914258c80 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Tue, 15 Nov 2022 16:05:49 +0100 Subject: [PATCH 4/6] Adapt the example Lin test to the new interface --- doc/example/dune | 2 +- doc/example/lin_tests_dsl.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) 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"; ] From 0ddb5a92efe18659fda796805878263ddb57a398 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Tue, 15 Nov 2022 19:30:07 +0100 Subject: [PATCH 5/6] Fix an occurrence of Lin_api in comment --- lib/lin_common.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/lin_common.mli b/lib/lin_common.mli index 5f9c6c830..b972cc653 100644 --- a/lib/lin_common.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. *) From fd1e200b77feb5be5ba5f42d8f2d12941b4b69d7 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Tue, 15 Nov 2022 19:31:01 +0100 Subject: [PATCH 6/6] Rename "Lin_api" into "Lin DSL" in test descriptions --- src/array/lin_tests_dsl.ml | 2 +- src/atomic/lin_tests_dsl.ml | 2 +- src/bigarray/lin_tests_dsl.ml | 2 +- src/bytes/lin_tests_dsl.ml | 4 ++-- src/ephemeron/lin_tests_dsl.ml | 4 ++-- src/floatarray/lin_tests_dsl.ml | 2 +- src/hashtbl/lin_tests_dsl.ml | 2 +- src/lazy/lin_tests_dsl.ml | 6 +++--- src/neg_tests/dune | 2 +- src/neg_tests/lin_tests_dsl_domain.ml | 8 ++++---- src/neg_tests/lin_tests_dsl_effect.ml | 16 ++++++++-------- src/queue/lin_tests_dsl.ml | 4 ++-- src/stack/lin_tests_dsl.ml | 4 ++-- 13 files changed, 29 insertions(+), 29 deletions(-) diff --git a/src/array/lin_tests_dsl.ml b/src/array/lin_tests_dsl.ml index c96ddfd46..adedceb36 100644 --- a/src/array/lin_tests_dsl.ml +++ b/src/array/lin_tests_dsl.ml @@ -29,5 +29,5 @@ end module AT_domain = Lin_domain.Make(AConf) ;; QCheck_base_runner.run_tests_main [ - AT_domain.neg_lin_test ~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/lin_tests_dsl.ml b/src/atomic/lin_tests_dsl.ml index b0d7d7eb7..57a2d578e 100644 --- a/src/atomic/lin_tests_dsl.ml +++ b/src/atomic/lin_tests_dsl.ml @@ -17,5 +17,5 @@ module Lin_atomic_domain = Lin_domain.Make (Atomic_spec) let () = QCheck_base_runner.run_tests_main - [ Lin_atomic_domain.lin_test ~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/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml index a2990c325..ce82fd2c2 100644 --- a/src/bigarray/lin_tests_dsl.ml +++ b/src/bigarray/lin_tests_dsl.ml @@ -29,5 +29,5 @@ module BA1T = Lin_domain.Make(BA1Conf) let _ = QCheck_base_runner.run_tests_main [ - BA1T.neg_lin_test ~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/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml index c37b36c7a..5f0a48e70 100644 --- a/src/bytes/lin_tests_dsl.ml +++ b/src/bytes/lin_tests_dsl.ml @@ -21,6 +21,6 @@ module BT_domain = Lin_domain.Make(BConf) module BT_thread = Lin_thread.Make(BConf) ;; QCheck_base_runner.run_tests_main [ - BT_domain.lin_test ~count:1000 ~name:"Lin_api Bytes test with Domain"; - BT_thread.lin_test ~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/lin_tests_dsl.ml b/src/ephemeron/lin_tests_dsl.ml index d5e0e5f3d..9b5898fcf 100644 --- a/src/ephemeron/lin_tests_dsl.ml +++ b/src/ephemeron/lin_tests_dsl.ml @@ -42,6 +42,6 @@ module ET_domain = Lin_domain.Make(EConf) module ET_thread = Lin_thread.Make(EConf) ;; QCheck_base_runner.run_tests_main [ - ET_domain.neg_lin_test ~count:1000 ~name:"Lin_api Ephemeron test with Domain"; - ET_thread.lin_test ~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/lin_tests_dsl.ml b/src/floatarray/lin_tests_dsl.ml index 741ad6c37..149b4a5dc 100644 --- a/src/floatarray/lin_tests_dsl.ml +++ b/src/floatarray/lin_tests_dsl.ml @@ -37,5 +37,5 @@ module FAT = Lin_domain.Make(FAConf) let _ = QCheck_base_runner.run_tests_main [ - FAT.neg_lin_test ~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/lin_tests_dsl.ml b/src/hashtbl/lin_tests_dsl.ml index 5d862de0f..3b4f49403 100644 --- a/src/hashtbl/lin_tests_dsl.ml +++ b/src/hashtbl/lin_tests_dsl.ml @@ -26,5 +26,5 @@ end module HT_domain = Lin_domain.Make(HConf) ;; QCheck_base_runner.run_tests_main [ - HT_domain.neg_lin_test ~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/lazy/lin_tests_dsl.ml b/src/lazy/lin_tests_dsl.ml index 2eef7246e..e292833d0 100644 --- a/src/lazy/lin_tests_dsl.ml +++ b/src/lazy/lin_tests_dsl.ml @@ -67,7 +67,7 @@ module LTfromfun_domain = Lin_domain.Make(LTfromfunAPI) ;; QCheck_base_runner.run_tests_main (let count = 100 in - [LTlazy_domain.neg_lin_test ~count ~name:"Lin_api Lazy test with Domain"; - LTfromval_domain.lin_test ~count ~name:"Lin_api Lazy test with Domain from_val"; - LTfromfun_domain.neg_lin_test ~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 1eca13d96..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 diff --git a/src/neg_tests/lin_tests_dsl_domain.ml b/src/neg_tests/lin_tests_dsl_domain.ml index f04ac0026..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_domain.neg_lin_test ~count ~name:"Lin_api ref int test with Domain"; - RT_int64_domain.neg_lin_test ~count ~name:"Lin_api ref int64 test with Domain"; - CLT_int_domain.neg_lin_test ~count ~name:"Lin_api CList int test with Domain"; - CLT_int64_domain.neg_lin_test ~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 82b9b8d9e..97f0a6dd5 100644 --- a/src/neg_tests/lin_tests_dsl_effect.ml +++ b/src/neg_tests/lin_tests_dsl_effect.ml @@ -83,13 +83,13 @@ 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_effect.lin_test ~count ~name:"Lin_api ref int test with Effect"; - RT_int64_effect.lin_test ~count ~name:"Lin_api ref int64 test with Effect"; - CLT_int_effect.lin_test ~count ~name:"Lin_api CList int test with Effect"; - CLT_int64_effect.lin_test ~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'_effect.neg_lin_test ~count ~name:"negative Lin_api ref int test with Effect"; - RT_int64'_effect.neg_lin_test ~count ~name:"negative Lin_api ref int64 test with Effect"; - CLT_int'_effect.neg_lin_test ~count ~name:"negative Lin_api CList int test with Effect"; - CLT_int64'_effect.neg_lin_test ~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/queue/lin_tests_dsl.ml b/src/queue/lin_tests_dsl.ml index ac962ab80..3c3621515 100644 --- a/src/queue/lin_tests_dsl.ml +++ b/src/queue/lin_tests_dsl.ml @@ -22,6 +22,6 @@ module Lin_queue_thread = Lin_thread.Make(Queue_spec) let () = QCheck_base_runner.run_tests_main [ - Lin_queue_domain.neg_lin_test ~count:1000 ~name:"Lin_api Queue test with Domain"; - Lin_queue_thread.lin_test ~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/lin_tests_dsl.ml b/src/stack/lin_tests_dsl.ml index 8209fb8c7..4c0aac41f 100644 --- a/src/stack/lin_tests_dsl.ml +++ b/src/stack/lin_tests_dsl.ml @@ -22,6 +22,6 @@ module Stack_thread = Lin_thread.Make(Stack_spec) let () = QCheck_base_runner.run_tests_main [ - Stack_domain.neg_lin_test ~count:1000 ~name:"Lin_api Stack test with Domain"; - Stack_thread.lin_test ~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"; ]