diff --git a/multicoretests.opam b/multicoretests.opam index ed682fa79..156ac4aac 100644 --- a/multicoretests.opam +++ b/multicoretests.opam @@ -39,6 +39,5 @@ build: [ ] dev-repo: "git+https://github.com/jmid/multicoretests.git" pin-depends: [ -# ["kcas.0.14" "git+https://github.com/ocaml-multicore/kcas#master"] ["lockfree.v0.2.0" "git+https://github.com/ocaml-multicore/lockfree#main"] ] diff --git a/src/README.md b/src/README.md index 06c1355f7..f47856dd6 100644 --- a/src/README.md +++ b/src/README.md @@ -68,9 +68,6 @@ Tests utilizing the linearizability tests of Lin.ml: - [stack/lin_tests.ml](stack/lin_tests.ml) and [stack/lin_tests_dsl.ml](stack/lin_tests_dsl.ml) contain experimental `Lin` and `Lin_api`-tests of `Stack` - - [kcas/lin_tests.ml](kcas/lin_tests.ml) and [kcas/lin_tests_dsl.ml](kcas/lin_tests_dsl.ml) - contain experimental `Lin` and `Lin_api`-tests of `Kcas` and `Kcas.W1` (Note: `Kcas` is subsumed by `Stdlib.Atomic`). - Tests of the underlying spawn/async functionality of `Domain`, diff --git a/src/dune b/src/dune index 6a79c543e..bb1f6a5d9 100644 --- a/src/dune +++ b/src/dune @@ -24,5 +24,4 @@ ;; other libs (alias domainslib/default) (alias lockfree/default) - ;; (alias kcas/default) -- kcas tests disabled )) diff --git a/src/kcas/README.md b/src/kcas/README.md deleted file mode 100644 index bc32de9cd..000000000 --- a/src/kcas/README.md +++ /dev/null @@ -1,10 +0,0 @@ -Tests of the kcas library -========================= - -The kcas library predates the OCaml multicore memory model described -in the [PLDI'18-paper](https://kcsrk.info/papers/pldi18-memory.pdf). -Since then kcas has been subsumed by the Atomic module that was added -to the Stdlib. - -This is a placeholder for a few experimental tests of the kcas -library, developed before I realized the above. diff --git a/src/kcas/dune b/src/kcas/dune deleted file mode 100644 index 2b9c0a3d2..000000000 --- a/src/kcas/dune +++ /dev/null @@ -1,33 +0,0 @@ -;; Linearizability tests of the kcas library - -;; this prevents the tests from running on a default build -(alias - (name default) - (package multicoretests) - (deps lin_tests.exe lin_tests_dsl.exe)) - -(executable - (name lin_tests) - (modules lin_tests) - (flags (:standard -w -27)) - (libraries qcheck-lin.domain kcas) - (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))) - -; disable kcas test for now -; (rule -; (alias runtest) -; (package multicoretests) -; (deps lin_tests.exe) -; (action (run ./%{deps} --verbose))) - -(executable - (name lin_tests_dsl) - (modules lin_tests_dsl) - (libraries qcheck-lin.domain kcas) - (preprocess (pps ppx_deriving.show ppx_deriving.eq))) - -; (rule -; (alias runtest) -; (package multicoretests) -; (deps lin_tests_dsl.exe) -; (action (run ./%{deps} --verbose))) diff --git a/src/kcas/lin_tests.ml b/src/kcas/lin_tests.ml deleted file mode 100644 index a8f1d09c8..000000000 --- a/src/kcas/lin_tests.ml +++ /dev/null @@ -1,117 +0,0 @@ -open QCheck - -(** ********************************************************************** *) -(** Tests of [Kcas] *) -(** ********************************************************************** *) -module KConf = -struct - type t = int Kcas.ref - - (* missing: equal, is_on_ref, kCAS -- mk_cas, commit (already tested as [set] *) - type cmd = - | Get - | Set of int' - | Cas of int' * int' - | TryMapNone - (*| TryMapSome*) (* Seq,exec cannot fail - hence not linearizable with [try_map] *) - | MapNone - | MapSome - | Incr - | Decr [@@deriving qcheck, show { with_path = false }] - and int' = (int [@gen Gen.nat]) - - let shrink_cmd = Shrink.nil - - type res = - | RGet of int - | RSet - | RCas of bool - | RTryMapNone of int cas_result - (*| RTryMapSome of int cas_result*) - | RMapNone of int cas_result - | RMapSome of int cas_result - | RIncr - | RDecr [@@deriving show { with_path = false }, eq] - and 'a cas_result - = 'a Kcas.cas_result = - | Aborted - | Failed - | Success of 'a [@deriving show { with_path = false }, eq] - - let init () = Kcas.ref 0 - - let run c r = match c with - | Get -> RGet (Kcas.get r) - | Set i -> (Kcas.set r i; RSet) - | Cas (i,j) -> RCas (Kcas.cas r i j) - | TryMapNone -> RTryMapNone (Kcas.try_map r (fun _ -> None)) - (*| TryMapSome -> RTryMapSome (Kcas.try_map r (fun i -> Some i))*) - | MapNone -> RMapNone (Kcas.map r (fun _ -> None)) - | MapSome -> RMapSome (Kcas.map r (fun i -> Some i)) - | Incr -> (Kcas.incr r; RIncr) - | Decr -> (Kcas.decr r; RDecr) - let cleanup _ = () -end - -module KT = Lin_domain.Make_internal(KConf) - - -(** ********************************************************************** *) -(** Tests of [Kcas.W1] *) -(** ********************************************************************** *) -module KW1Conf = -struct - type t = int Kcas.W1.ref - - type cmd = - | Get - | Set of int' - | Cas of int' * int' - | TryMapNone - (*| TryMapSome*) (* Seq,exec cannot fail - hence not linearizable with [try_map] *) - | MapNone - | MapSome - | Incr - | Decr [@@deriving qcheck, show { with_path = false }] - and int' = (int [@gen Gen.nat]) - - let shrink_cmd = Shrink.nil - - type res = - | RGet of int - | RSet - | RCas of bool - | RTryMapNone of int cas_result - (*| RTryMapSome of int cas_result*) - | RMapNone of int cas_result - | RMapSome of int cas_result - | RIncr - | RDecr [@@deriving show { with_path = false }, eq] - and 'a cas_result - = 'a Kcas.cas_result = - | Aborted - | Failed - | Success of 'a [@deriving show { with_path = false }, eq] - - let init () = Kcas.W1.ref 0 - - let run c r = match c with - | Get -> RGet (Kcas.W1.get r) - | Set i -> (Kcas.W1.set r i; RSet) - | Cas (i,j) -> RCas (Kcas.W1.cas r i j) - | TryMapNone -> RTryMapNone (Kcas.W1.try_map r (fun _ -> None)) - (*| TryMapSome -> RTryMapSome (Kcas.W1.try_map r (fun i -> Some i))*) - | MapNone -> RMapNone (Kcas.W1.map r (fun _ -> None)) - | MapSome -> RMapSome (Kcas.W1.map r (fun i -> Some i)) - | Incr -> (Kcas.W1.incr r; RIncr) - | Decr -> (Kcas.W1.decr r; RDecr) - let cleanup _ = () -end - -module KW1T = Lin_domain.Make_internal(KW1Conf) -;; -QCheck_base_runner.run_tests_main [ - (* Kcas tests *) - KT.neg_lin_test ~count:1000 ~name:"Lin Kcas test with Domain"; - KW1T.lin_test ~count:1000 ~name:"Lin Kcas.W1 test with Domain"; -] diff --git a/src/kcas/lin_tests_dsl.ml b/src/kcas/lin_tests_dsl.ml deleted file mode 100644 index 877f384ce..000000000 --- a/src/kcas/lin_tests_dsl.ml +++ /dev/null @@ -1,81 +0,0 @@ -(* ********************************************************************** *) -(* Tests of [Kcas] *) -(* ********************************************************************** *) -module Common = -struct - type 'a cas_result - = 'a Kcas.cas_result = - | Aborted - | Failed - | Success of 'a [@@deriving show { with_path = false }, eq] - - let cas_result 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_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_base.gen fun_gen print_fun -end - -module KConf = -struct - type t = int Kcas.ref - let init () = Kcas.ref 0 - let cleanup _ = () - - open Lin_base - let int = nat_small - let fun_none,fun_some,cas_result = Common.(fun_none,fun_some,cas_result) - let api = - [ val_ "Kcas.get" Kcas.get (t @-> returning int); - val_ "Kcas.set" Kcas.set (t @-> int @-> returning unit); - val_ "Kcas.cas" Kcas.cas (t @-> int @-> int @-> returning bool); - val_ "Kcas.try_map" Kcas.try_map (t @-> fun_none int @-> returning (cas_result int)); - val_ "Kcas.try_map" Kcas.try_map (t @-> fun_some int @-> returning (cas_result int)); (* Seq,exec cannot fail - hence not linearizable with [try_map] *) - val_ "Kcas.map" Kcas.map (t @-> fun_none int @-> returning (cas_result int)); - val_ "Kcas.map" Kcas.map (t @-> fun_some int @-> returning (cas_result int)); - val_ "Kcas.incr" Kcas.incr (t @-> returning unit); - val_ "Kcas.decr" Kcas.decr (t @-> returning unit); - ] -end - -module KT = Lin_domain.Make(KConf) - - -(* ********************************************************************** *) -(* Tests of [Kcas.W1] *) -(* ********************************************************************** *) -module KW1Conf = -struct - type t = int Kcas.W1.ref - let init () = Kcas.W1.ref 0 - let cleanup _ = () - - open Lin_base - let int = nat_small - let fun_none,fun_some,cas_result = Common.(fun_none,fun_some,cas_result) - let api = - [ val_ "Kcas.W1.get" Kcas.W1.get (t @-> returning int); - val_ "Kcas.W1.set" Kcas.W1.set (t @-> int @-> returning unit); - val_ "Kcas.W1.cas" Kcas.W1.cas (t @-> int @-> int @-> returning bool); - val_ "Kcas.W1.try_map" Kcas.W1.try_map (t @-> fun_none int @-> returning (cas_result int)); - (*val_ "Kcas.W1.try_map" Kcas.W1.try_map (t @-> fun_some int @-> returning (cas_result int));*) (* Seq,exec cannot fail - hence not linearizable with [try_map] *) - val_ "Kcas.W1.map" Kcas.W1.map (t @-> fun_none int @-> returning (cas_result int)); - val_ "Kcas.W1.map" Kcas.W1.map (t @-> fun_some int @-> returning (cas_result int)); - val_ "Kcas.W1.incr" Kcas.W1.incr (t @-> returning unit); - val_ "Kcas.W1.decr" Kcas.W1.decr (t @-> returning unit); - ] -end - -module KW1T = Lin_domain.Make(KW1Conf) -;; -QCheck_base_runner.run_tests_main [ - 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"; -]