Fix Lin libraries after split

Add a Lin_base module, as the entrypoint of the qcheck-lin.base library

Author: shym

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)

lib/lin_base.ml

@@ -0,0 +1,3 @@
+module Lin_internal = Lin_internal
+module Lin_common = Lin_common
+include Lin_common

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))

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 *)

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))

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))

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

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))