Merge pull request #201 from jmid/post-refactor-polish

Adjust README and kcas after STM and Lin refactoring

Author: jmid

README.md

@@ -81,7 +81,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);
@@ -91,7 +91,7 @@ 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";
@@ -103,7 +103,7 @@ bindings `init` and `cleanup` for setting it up and tearing it down.
 The `api` then contains a list of type signature descriptions using
 combinators `unit`, `bool`, `int`, `returning`, `returning_or_exc`,
 ... in the style of [Ctypes](https://github.com/ocamllabs/ocaml-ctypes).
-The functor `Lin_api.Make` expects a description of the tested
+The functor `Lin_domain.Make` expects a description of the tested
 commands and outputs a module with a QCheck test `lin_test` that
 performs the linearizability test.
 
@@ -164,7 +164,7 @@ given below:
 
 ``` ocaml
 open QCheck
-open STM
+open STM_base
 
 (** parallel STM tests of Hashtbl *)
 
@@ -222,12 +222,13 @@ struct
     | _ -> false
 end
 
-module HTest = STM.Make(HashtblModel)
+module HT_seq = STM_sequential.Make(HashtblModel)
+module HT_dom = STM_domain.Make(HashtblModel)
 ;;
 QCheck_base_runner.run_tests_main
   (let count = 200 in
-   [HTest.agree_test     ~count ~name:"Hashtbl test";
-    HTest.agree_test_par ~count ~name:"Hashtbl test"; ])
+   [HT_seq.agree_test     ~count ~name:"Hashtbl test sequential";
+    HT_dom.agree_test_par ~count ~name:"Hashtbl test parallel"; ])
 ```
 
 Again this requires a type `sut` for the system under test, and
@@ -257,18 +258,19 @@ example, this compares the Boolean result `r` from `Hashtbl.mem` with
 the result from `List.mem_assoc`. Similarly `precond` expresses a
 pre-condition.
 
-The module is phrased as a functor `STM.Make` and the resulting module
-contains functions
- - `agree_test` to test whether the model agrees with the `sut` across
+The module is phrased as functors:
+ - the functor `STM_sequential.Make` produces a module with a function
+   `agree_test` to test whether the model agrees with the `sut` across
    a sequential run of an arbitrary command sequence and
- - `agree_test_par` which tests in parallel by `spawn`ing two domains
+ - the functor `STM_domain.Make` produces a module with a function
+   `agree_test_par` which tests in parallel by `spawn`ing two domains
    with `Domain` similarly to `Lin` and searches for a sequential
    interleaving over the model.
 
 When running the above with the command `dune exec doc/example/stm_tests.exe`
 one may obtain the following output:
 ```
-Messages for test parallel Hashtbl test:
+Messages for test Hashtbl test parallel:
 
   Results incompatible with linearized model
 
@@ -313,11 +315,6 @@ property can be done in two different ways:
    cheaper so we can run more, Con: more tests are required to trigger a race)
 
 
-In `STM` a functor `STM.AddGC` is also available. It inserts calls to
-`Gc.minor()` at random points between the executed commands.
-
-
-
 Issues
 ======
 

src/kcas/dune

@@ -10,7 +10,7 @@
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
- (libraries lin kcas)
+ (libraries qcheck-lin.domain kcas)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
 
 ; disable kcas test for now
@@ -23,7 +23,7 @@
 (executable
  (name lin_tests_dsl)
  (modules lin_tests_dsl)
- (libraries lin kcas)
+ (libraries qcheck-lin.domain kcas)
  (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule

src/kcas/lin_tests.ml

@@ -53,7 +53,7 @@ struct
   let cleanup _ = ()
 end
 
-module KT = Lin.Make(KConf)
+module KT = Lin_domain.Make_internal(KConf)
 
 
 (** ********************************************************************** *)
@@ -108,10 +108,10 @@ struct
   let cleanup _ = ()
 end
 
-module KW1T = Lin.Make(KW1Conf)
+module KW1T = Lin_domain.Make_internal(KW1Conf)
 ;;
 QCheck_base_runner.run_tests_main [
   (* Kcas tests *)
-  KT.neg_lin_test `Domain ~count:1000 ~name:"Lin Kcas test with Domain";
-  KW1T.lin_test   `Domain ~count:1000 ~name:"Lin Kcas.W1 test with Domain";
+  KT.neg_lin_test ~count:1000 ~name:"Lin Kcas test with Domain";
+  KW1T.lin_test   ~count:1000 ~name:"Lin Kcas.W1 test with Domain";
 ]

src/kcas/lin_tests_dsl.ml

@@ -10,17 +10,17 @@ struct
     | Success of 'a [@@deriving show { with_path = false }, eq]
 
   let cas_result ty =
-    Lin_api.deconstructible (show_cas_result (fun fmt a -> Format.pp_print_string fmt (Lin_api.print ty a))) (equal_cas_result (Lin_api.equal ty))
+    Lin_base.deconstructible (show_cas_result (fun fmt a -> Format.pp_print_string fmt (Lin_base.print ty a))) (equal_cas_result (Lin_base.equal ty))
 
   let fun_none _ty =
     let print_fun _ = "(fun _ -> None)" in
     let fun_gen = QCheck.(make ~print:print_fun (Gen.return (fun _ -> None))) in
-    Lin_api.gen fun_gen print_fun
+    Lin_base.gen fun_gen print_fun
 
   let fun_some _ty =
     let print_fun _ = "(fun i -> Some i)" in
     let fun_gen = QCheck.(make ~print:print_fun (Gen.return (fun i -> Some i))) in
-    Lin_api.gen fun_gen print_fun
+    Lin_base.gen fun_gen print_fun
 end
 
 module KConf =
@@ -29,7 +29,7 @@ struct
   let init () = Kcas.ref 0
   let cleanup _ = ()
 
-  open Lin_api
+  open Lin_base
   let int = nat_small
   let fun_none,fun_some,cas_result = Common.(fun_none,fun_some,cas_result)
   let api =
@@ -45,7 +45,7 @@ struct
     ]
 end
 
-module KT = Lin_api.Make(KConf)
+module KT = Lin_domain.Make(KConf)
 
 
 (* ********************************************************************** *)
@@ -57,7 +57,7 @@ struct
   let init () = Kcas.W1.ref 0
   let cleanup _ = ()
 
-  open Lin_api
+  open Lin_base
   let int = nat_small
   let fun_none,fun_some,cas_result = Common.(fun_none,fun_some,cas_result)
   let api =
@@ -73,9 +73,9 @@ struct
     ]
 end
 
-module KW1T = Lin_api.Make(KW1Conf)
+module KW1T = Lin_domain.Make(KW1Conf)
 ;;
 QCheck_base_runner.run_tests_main [
-  KT.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Kcas test with Domain";
-  KW1T.lin_test   `Domain ~count:1000 ~name:"Lin_api Kcas.W1 test with Domain";
+  KT.neg_lin_test ~count:1000 ~name:"Lin_api Kcas test with Domain";
+  KW1T.lin_test   ~count:1000 ~name:"Lin_api Kcas.W1 test with Domain";
 ]