diff --git a/lib/lin_common.ml b/lib/lin_common.ml index d9f127aef..79359efd4 100644 --- a/lib/lin_common.ml +++ b/lib/lin_common.ml @@ -133,19 +133,19 @@ let val_ name value fntyp = let val_freq freq name value fntyp = (freq, Elem (name, fntyp, value)) -module type ApiSpec = sig +module type InterfaceSpec = sig type t val init : unit -> t val cleanup : t -> unit val api : (int * t elem) list end -module MakeCmd (ApiSpec : ApiSpec) : Lin_internal.CmdSpec = struct +module Make_test_repr (InterfaceSpec : InterfaceSpec) : Lin_internal.TestRepr = struct - type t = ApiSpec.t + type t = InterfaceSpec.t - let init = ApiSpec.init - let cleanup = ApiSpec.cleanup + let init = InterfaceSpec.init + let cleanup = InterfaceSpec.cleanup (* Typed argument list and return type descriptor *) module Args = struct @@ -251,7 +251,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin_internal.CmdSpec = struct (wgt, gen_args_of_desc fdesc >>= fun args -> let print = gen_printer name fdesc in let shrink = gen_shrinker_of_desc fdesc in - return (Cmd (name, args, rty, print, shrink, f)))) ApiSpec.api + return (Cmd (name, args, rty, print, shrink, f)))) InterfaceSpec.api let gen_cmd : cmd QCheck.Gen.t = QCheck.Gen.frequency api diff --git a/lib/lin_common.mli b/lib/lin_common.mli index b972cc653..aa5366280 100644 --- a/lib/lin_common.mli +++ b/lib/lin_common.mli @@ -144,10 +144,10 @@ val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty and have their elements generated by the [t] combinator. *) val t : ('a, constructible, 'a, noncombinable) ty -(** The [t] combinator represents the type [ApiSpec.t] of the system under test. *) +(** The [t] combinator represents the type [InterfaceSpec.t] of the system under test. *) val state : ('a, constructible, 'a, noncombinable) ty -(** The [state] combinator represents the type [ApiSpec.t] of the system under test. +(** The [state] combinator represents the type [InterfaceSpec.t] of the system under test. It is an alias for the [t] combinator. *) val or_exn : @@ -219,7 +219,7 @@ val val_freq : int -> string -> 'f -> ('f, 'r, 's) Fun.fn -> int * 's elem (** The required description of a module signature *) -module type ApiSpec = +module type InterfaceSpec = sig type t (** The type of the system under test *) @@ -237,6 +237,7 @@ module type ApiSpec = (** {1 Generation of linearizability testing module from an API} *) -module MakeCmd : functor (Spec : ApiSpec) -> Lin_internal.CmdSpec +module Make_test_repr : functor (Spec : InterfaceSpec) -> + Lin_internal.TestRepr (** Functor to map a combinator-based module signature description into a raw [Lin] description *) diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 424cf92ff..da6155f42 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -1,6 +1,6 @@ open Lin_base -module Make_internal (Spec : Lin_internal.CmdSpec) = struct +module Make_internal (Spec : Lin_internal.TestRepr) = struct module M = Lin_internal.Make(Spec) include M @@ -35,5 +35,5 @@ module Make_internal (Spec : Lin_internal.CmdSpec) = struct 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)) +module Make (Spec : Lin_common.InterfaceSpec) = + Make_internal(Lin_common.Make_test_repr(Spec)) diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml index a3fd50fc6..77745da3f 100644 --- a/lib/lin_effect.ml +++ b/lib/lin_effect.ml @@ -33,10 +33,10 @@ let start_sched main = let fork f = perform (Fork f) let yield () = perform Yield -module Make_internal (Spec : Lin_internal.CmdSpec) = struct +module Make_internal (Spec : Lin_internal.TestRepr) = struct - (** A refined [CmdSpec] specification with generator-controlled [Yield] effects *) + (** A refined [TestRepr] specification with generator-controlled [Yield] effects *) module EffSpec = struct open QCheck @@ -122,5 +122,5 @@ module Make_internal (Spec : Lin_internal.CmdSpec) = struct arb_cmd_triple (Util.repeat rep_count lin_prop_effect) end -module Make (Spec : Lin_common.ApiSpec) = - Make_internal(Lin_common.MakeCmd(Spec)) +module Make (Spec : Lin_common.InterfaceSpec) = + Make_internal(Lin_common.Make_test_repr(Spec)) diff --git a/lib/lin_internal.ml b/lib/lin_internal.ml index f309ed343..4bc4842db 100644 --- a/lib/lin_internal.ml +++ b/lib/lin_internal.ml @@ -1,7 +1,7 @@ open QCheck include Util -module type CmdSpec = sig +module type TestRepr = sig type t (** The type of the system under test *) @@ -39,7 +39,7 @@ 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) +module Make(Spec : TestRepr) = struct (* plain interpreter of a cmd list *) diff --git a/lib/lin_thread.ml b/lib/lin_thread.ml index 3ec96eb41..253b027a2 100644 --- a/lib/lin_thread.ml +++ b/lib/lin_thread.ml @@ -1,6 +1,6 @@ open Lin_base -module Make_internal (Spec : Lin_internal.CmdSpec) = struct +module Make_internal (Spec : Lin_internal.TestRepr) = struct module M = Lin_internal.Make(Spec) include M @@ -42,5 +42,5 @@ module Make_internal (Spec : Lin_internal.CmdSpec) = struct 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)) +module Make (Spec : Lin_common.InterfaceSpec) = + Make_internal(Lin_common.Make_test_repr(Spec)) diff --git a/src/atomic/lin_tests_dsl.ml b/src/atomic/lin_tests_dsl.ml index 57a2d578e..2e40e2bdf 100644 --- a/src/atomic/lin_tests_dsl.ml +++ b/src/atomic/lin_tests_dsl.ml @@ -1,4 +1,4 @@ -module Atomic_spec : Lin_base.ApiSpec = struct +module Atomic_spec : Lin_base.InterfaceSpec = struct open Lin_base (* FIXME add Gen.nat *) type t = int Atomic.t let init () = Atomic.make 0 diff --git a/src/hashtbl/lin_tests_dsl.ml b/src/hashtbl/lin_tests_dsl.ml index 3b4f49403..ad47e6dc8 100644 --- a/src/hashtbl/lin_tests_dsl.ml +++ b/src/hashtbl/lin_tests_dsl.ml @@ -1,7 +1,7 @@ (* ********************************************************************** *) (* Tests of thread-unsafe [Hashtbl] *) (* ********************************************************************** *) -module HConf (*: Lin_base.ApiSpec*) = +module HConf (*: Lin_base.InterfaceSpec*) = struct type t = (char, int) Hashtbl.t diff --git a/src/neg_tests/lin_tests_dsl_common.ml b/src/neg_tests/lin_tests_dsl_common.ml index e11b163f4..3d7bed149 100644 --- a/src/neg_tests/lin_tests_dsl_common.ml +++ b/src/neg_tests/lin_tests_dsl_common.ml @@ -24,7 +24,7 @@ module Sut_int64 = let decr r = add r Int64.minus_one (* buggy: not atomic *) end -module Ref_int_spec : ApiSpec = struct +module Ref_int_spec : InterfaceSpec = struct type t = int ref let init () = Sut_int.init () let cleanup _ = () @@ -38,7 +38,7 @@ module Ref_int_spec : ApiSpec = struct ] end -module Ref_int64_spec : ApiSpec = struct +module Ref_int64_spec : InterfaceSpec = struct type t = int64 ref let init () = Sut_int64.init () let cleanup _ = () @@ -59,7 +59,7 @@ module RT_int64_domain = Lin_domain.Make(Ref_int64_spec) (** Tests of the buggy concurrent list CList *) (** ********************************************************************** *) -module CList_spec_int : ApiSpec = +module CList_spec_int : InterfaceSpec = 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 : ApiSpec = +module CList_spec_int64 : InterfaceSpec = struct type t = int64 CList.conc_list Atomic.t let init () = CList.list_init Int64.zero diff --git a/src/neg_tests/lin_tests_dsl_effect.ml b/src/neg_tests/lin_tests_dsl_effect.ml index 97f0a6dd5..c3a363bf2 100644 --- a/src/neg_tests/lin_tests_dsl_effect.ml +++ b/src/neg_tests/lin_tests_dsl_effect.ml @@ -13,7 +13,7 @@ module Sut_int' = struct let add r i = let old = !r in Lin_effect.yield (); set r (old+i) end -module Ref_int'_spec : ApiSpec = struct +module Ref_int'_spec : InterfaceSpec = struct type t = int ref let init () = Sut_int'.init () let cleanup _ = () @@ -34,7 +34,7 @@ module Sut_int64' = struct let add r i = let old = !r in Lin_effect.yield (); set r (Int64.add old i) end -module Ref_int64'_spec : ApiSpec = struct +module Ref_int64'_spec : InterfaceSpec = struct type t = int64 ref let init () = Sut_int64'.init () let cleanup _ = () @@ -51,7 +51,7 @@ module RT_int64_effect = Lin_effect.Make(Ref_int64_spec) module RT_int64'_effect = Lin_effect.Make(Ref_int64'_spec) -module CList_spec_int' : ApiSpec = +module CList_spec_int' : InterfaceSpec = struct type t = int CList.conc_list Atomic.t let init () = CList.list_init 0 @@ -62,7 +62,7 @@ struct val_ "CList.member" CList.member (t @-> int @-> returning bool); ] end -module CList_spec_int64' : ApiSpec = +module CList_spec_int64' : InterfaceSpec = struct type t = int64 CList.conc_list Atomic.t let init () = CList.list_init Int64.zero diff --git a/src/queue/lin_tests_dsl.ml b/src/queue/lin_tests_dsl.ml index 3c3621515..e104d2326 100644 --- a/src/queue/lin_tests_dsl.ml +++ b/src/queue/lin_tests_dsl.ml @@ -1,4 +1,4 @@ -module Queue_spec : Lin_base.ApiSpec = struct +module Queue_spec : Lin_base.InterfaceSpec = struct open Lin_base type t = int Queue.t let init () = Queue.create () diff --git a/src/stack/lin_tests_dsl.ml b/src/stack/lin_tests_dsl.ml index 4c0aac41f..84cc3daa3 100644 --- a/src/stack/lin_tests_dsl.ml +++ b/src/stack/lin_tests_dsl.ml @@ -1,4 +1,4 @@ -module Stack_spec : Lin_base.ApiSpec = struct +module Stack_spec : Lin_base.InterfaceSpec = struct open Lin_base type t = int Stack.t let init () = Stack.create ()