diff --git a/lib/dune b/lib/dune index 04b78f980..999eb6e84 100644 --- a/lib/dune +++ b/lib/dune @@ -11,4 +11,4 @@ (library (name lin) (modules lin) - (libraries qcheck)) + (libraries threads qcheck)) diff --git a/lib/lin.ml b/lib/lin.ml index 559a5a9af..95a5da6e1 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -40,7 +40,7 @@ let rec repeat n prop = fun input -> module Make(Spec : CmdSpec) (*: StmTest *) -= struct + = struct (* Horrible copy-paste for now, please FIXME *) let print_triple_vertical ?(fig_indent=10) ?(res_width=20) show (seq,cmds1,cmds2) = @@ -79,6 +79,13 @@ module Make(Spec : CmdSpec) (*: StmTest *) 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) + (* use a ref to a list given by the parent thread to put the results in as a thread does not + return a value *) + let interp_thread res sut cs = + let cs_arr = Array.of_list cs in + let res_arr = Array.map (fun c -> Thread.yield (); Spec.run c sut) cs_arr in + res := List.combine cs (Array.to_list res_arr) + let rec gen_cmds fuel = Gen.(if fuel = 0 then return [] @@ -137,7 +144,7 @@ module Make(Spec : CmdSpec) (*: StmTest *) Spec.cleanup seq_sut'; b) (* Linearizability property based on [Domain] and an Atomic flag *) - let lin_prop = + let lin_prop_domain = (fun (seq_pref,cmds1,cmds2) -> let sut = Spec.init () in let pref_obs = interp sut seq_pref in @@ -156,10 +163,30 @@ module Make(Spec : CmdSpec) (*: StmTest *) (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 pref_obs, obs1, obs2 = ref [], ref [], ref [] in + interp_thread pref_obs sut seq_pref; + let th1 = Thread.create (Thread.yield (); interp_thread obs1 sut) cmds1 in + let th2 = Thread.create (interp_thread obs2 sut) cmds2 in + Thread.join th1; Thread.join th2; Spec.cleanup sut; + let seq_sut = Spec.init () in + (* we should be able to reuse [check_seq_cons] *) + let b = check_seq_cons !pref_obs !obs1 !obs2 seq_sut [] in + Spec.cleanup seq_sut; + b + || 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 test based on [Domain] *) - let lin_test ~count ~name = + let lin_test ~count ~name (lib : [ `Domain | `Thread ]) = let rep_count = 50 in let seq_len,par_len = 20,15 in + let lin_prop = match lib with `Domain -> lin_prop_domain | ` Thread -> lin_prop_thread in Test.make ~count ~retries:3 ~name:("Linearizable " ^ name) (arb_cmds_par seq_len par_len) (repeat rep_count lin_prop) end diff --git a/src/domainslib/dune b/src/domainslib/dune index c892de117..1718fbc1e 100644 --- a/src/domainslib/dune +++ b/src/domainslib/dune @@ -58,7 +58,7 @@ (modules task_parallel) (libraries util qcheck domainslib)) -(rule - (alias runtest) - (deps task_parallel.exe) - (action (run ./%{deps} --no-colors --verbose))) +; (rule +; (alias runtest) +; (deps task_parallel.exe) +; (action (run ./%{deps} --no-colors --verbose))) diff --git a/src/kcas/lin_tests.ml b/src/kcas/lin_tests.ml index 14c4a5bd3..57b274065 100644 --- a/src/kcas/lin_tests.ml +++ b/src/kcas/lin_tests.ml @@ -110,6 +110,6 @@ Util.set_ci_printing () ;; QCheck_runner.run_tests_main [ (* Kcas tests *) - KT.lin_test ~count:1000 ~name:"Kcas test"; - KW1T.lin_test ~count:1000 ~name:"Kcas.W1 test"; + KT.lin_test `Domain ~count:1000 ~name:"Kcas test"; + KW1T.lin_test `Domain ~count:1000 ~name:"Kcas.W1 test"; ] diff --git a/src/lazy_lin_test.ml b/src/lazy_lin_test.ml index ff2f564da..3bfed64ec 100644 --- a/src/lazy_lin_test.ml +++ b/src/lazy_lin_test.ml @@ -77,7 +77,7 @@ Util.set_ci_printing () ;; QCheck_runner.run_tests_main (let count = 100 in - [LTlazy.lin_test ~count ~name:"lazy test"; - LTfromval.lin_test ~count ~name:"lazy test from_val"; - LTfromfun.lin_test ~count ~name:"lazy test from_fun"; + [LTlazy.lin_test `Domain ~count ~name:"lazy test"; + LTfromval.lin_test `Domain ~count ~name:"lazy test from_val"; + LTfromfun.lin_test `Domain ~count ~name:"lazy test from_fun"; ]) diff --git a/src/lin_tests.ml b/src/lin_tests.ml index 640789d20..52b36baeb 100644 --- a/src/lin_tests.ml +++ b/src/lin_tests.ml @@ -138,7 +138,7 @@ module HT = Lin.Make(HConf) Util.set_ci_printing () ;; QCheck_runner.run_tests_main [ - AT.lin_test ~count:1000 ~name:"Atomic test"; - A3T.lin_test ~count:1000 ~name:"Atomic3 test"; - HT.lin_test ~count:1000 ~name:"Hashtbl test"; + AT.lin_test `Domain ~count:1000 ~name:"Atomic test with domains"; + A3T.lin_test `Domain ~count:1000 ~name:"Atomic3 test with domains"; + HT.lin_test `Domain ~count:1000 ~name:"Hashtbl test with domains"; ] diff --git a/src/lockfree/lin_tests.ml b/src/lockfree/lin_tests.ml index 8620672a3..47ee6371f 100644 --- a/src/lockfree/lin_tests.ml +++ b/src/lockfree/lin_tests.ml @@ -134,8 +134,8 @@ Util.set_ci_printing () ;; QCheck_runner.run_tests_main [ (* Lockfree tests *) - LFLT.lin_test ~count:1000 ~name:"lockfree list test"; - LFOLT.lin_test ~count:1000 ~name:"lockfree ordered list test"; - LFHT.lin_test ~count:1000 ~name:"lockfree Hash test"; - LFBT.lin_test ~count:1000 ~name:"lockfree Bag test"; + LFLT.lin_test `Domain ~count:1000 ~name:"lockfree list test"; + LFOLT.lin_test `Domain ~count:1000 ~name:"lockfree ordered list test"; + LFHT.lin_test `Domain ~count:1000 ~name:"lockfree Hash test"; + LFBT.lin_test `Domain ~count:1000 ~name:"lockfree Bag test"; ] diff --git a/src/neg_tests/CList.ml b/src/neg_tests/CList.ml index 69ef0fcc2..51dfe5a0f 100644 --- a/src/neg_tests/CList.ml +++ b/src/neg_tests/CList.ml @@ -1,6 +1,7 @@ (** a simple concurrent list - from Sadiq *) -type conc_list = { value: int; next: conc_list option } +module Make (T : sig type t end) = struct +type conc_list = { value: T.t; next: conc_list option } let rec add_node list_head n = (* try to add a new node to head *) @@ -30,3 +31,5 @@ let member list_head n = let add_and_check list_head n () = assert(add_node list_head n); assert(member list_head n) + +end diff --git a/src/neg_tests/conclist_test.ml b/src/neg_tests/conclist_test.ml index 0997849b9..b47a2d5cf 100644 --- a/src/neg_tests/conclist_test.ml +++ b/src/neg_tests/conclist_test.ml @@ -2,14 +2,18 @@ open QCheck (** This is a parallel test of the buggy concurrent list CList *) -module CLConf = +module CLConf (T : sig type t val dummy : t val f : int -> t val pp : t -> string end) = struct - type cmd = Add_node of int | Member of int [@@deriving show { with_path = false }] - type state = int list - type sut = CList.conc_list Atomic.t + module CL = CList.Make (struct type t = T.t end) + let pp_t fmt t = Format.fprintf fmt "%s" (T.pp t) + type cmd = + | Add_node of T.t [@printer pp_t] + | Member of T.t [@printer pp_t] [@@deriving show { with_path = false }] + type state = T.t list + type sut = CL.conc_list Atomic.t let arb_cmd s = - let int_gen = Gen.nat in + let int_gen = fun st -> Gen.nat st |> T.f in let mem_gen = if s=[] then int_gen @@ -20,8 +24,8 @@ struct [ Gen.map (fun i -> Add_node i) int_gen; Gen.map (fun i -> Member i) mem_gen; ]) - let init_state = [0] - let init_sut () = CList.list_init 0 + let init_state = [ T.dummy ] + let init_sut () = CL.list_init T.dummy let cleanup _ = () let next_state c s = match c with @@ -31,8 +35,8 @@ struct type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }] let run c r = match c with - | Add_node i -> RAdd_node (CList.add_node r i) - | Member i -> RMember (CList.member r i) + | Add_node i -> RAdd_node (CL.add_node r i) + | Member i -> RMember (CL.member r i) let precond _ _ = true @@ -42,11 +46,28 @@ struct | _,_ -> false end -module CLT = STM.Make(CLConf) +module T_int = struct + type t = int + let dummy = 0 + let f i = i + let pp = Int.to_string +end + +module T_int64 = struct + type t = int64 + let dummy = Int64.zero + let f = Int64.of_int + let pp = Int64.to_string +end + +module CLT_int = STM.Make(CLConf(T_int)) +module CLT_int64 = STM.Make(CLConf(T_int64)) ;; Util.set_ci_printing () ;; QCheck_runner.run_tests_main (let count,name = 1000,"CList test" in - [CLT.agree_test ~count ~name; - CLT.agree_test_par ~count ~name;]) + [CLT_int.agree_test ~count ~name; + CLT_int64.agree_test ~count ~name; + CLT_int.agree_test ~count ~name; + CLT_int64.agree_test_par ~count ~name;]) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index a8cb237b0..34e27e82c 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -61,4 +61,4 @@ (with-accepted-exit-codes 1 (with-stdout-to "lin-output.txt" (run ./lin_tests.exe --no-colors --verbose))) (cat lin-output.txt) - (run %{bin:check_error_count} "lin_tests" 2 lin-output.txt)))) + (run %{bin:check_error_count} "lin_tests" 5 lin-output.txt)))) diff --git a/src/neg_tests/lin_tests.ml b/src/neg_tests/lin_tests.ml index caba5f7e4..979908fd0 100644 --- a/src/neg_tests/lin_tests.ml +++ b/src/neg_tests/lin_tests.ml @@ -3,17 +3,27 @@ open QCheck (** ********************************************************************** *) (** Tests of a simple reference *) (** ********************************************************************** *) -module Sut = +module Sut_int = struct let init () = ref 0 let get r = !r let set r i = r:=i - let add r i = let old = !r in r:=i + old (* buggy: not atomic *) - let incr r = incr r (* buggy: not guaranteed to be atomic *) - let decr r = decr r (* buggy: not guaranteed to be atomic *) + let add r i = let old = !r in r:= i + old (* buggy: not atomic *) + let incr r = incr r (* buggy: not atomic *) + let decr r = decr r (* buggy: not atomic *) end -module RConf = struct +module Sut_int64 = + struct + let init () = ref Int64.zero + let get r = !r + let set r i = r:=i + let add r i = let old = !r in r:= Int64.add i old (* buggy: not atomic *) + let incr r = add r Int64.one (* buggy: not atomic *) + let decr r = add r Int64.minus_one (* buggy: not atomic *) +end + +module RConf_int = struct type t = int ref type cmd = @@ -26,50 +36,101 @@ module RConf = struct type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }] - let init () = Sut.init () + let init () = Sut_int.init () let run c r = match c with - | Get -> RGet (Sut.get r) - | Set i -> (Sut.set r i; RSet) - | Add i -> (Sut.add r i; RAdd) - | Incr -> (Sut.incr r; RIncr) - | Decr -> (Sut.decr r; RDecr) + | Get -> RGet (Sut_int.get r) + | Set i -> (Sut_int.set r i; RSet) + | Add i -> (Sut_int.add r i; RAdd) + | Incr -> (Sut_int.incr r; RIncr) + | Decr -> (Sut_int.decr r; RDecr) let cleanup _ = () end -module RT = Lin.Make(RConf) + +module RConf_int64 = struct + type t = int64 ref + + type cmd = + | Get + | Set of int' + | Add of int' + | Incr + | Decr [@@deriving qcheck, show { with_path = false }] + and int' = int64 [@gen Gen.ui64] + + type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }] + + let init () = Sut_int64.init () + + let run c r = match c with + | Get -> RGet (Sut_int64.get r) + | Set i -> (Sut_int64.set r i; RSet) + | Add i -> (Sut_int64.add r i; RAdd) + | Incr -> (Sut_int64.incr r; RIncr) + | Decr -> (Sut_int64.decr r; RDecr) + + let cleanup _ = () +end + +module RT_int = Lin.Make(RConf_int) +module RT_int64 = Lin.Make(RConf_int64) (** ********************************************************************** *) (** Tests of the buggy concurrent list CList *) (** ********************************************************************** *) -module CLConf = +module CLConf (T : sig type t val dummy : t val f : int -> t val pp : t -> string end) = struct - type t = CList.conc_list Atomic.t + module CL = CList.Make (struct type t = T.t end) + type t = CL.conc_list Atomic.t + let pp_t fmt t = Format.fprintf fmt "%s" (T.pp t) + let gen_int' st = Gen.nat st |> T.f + + type int' = T.t type cmd = - | Add_node of int' - | Member of int' [@@deriving qcheck, show { with_path = false }] - and int' = int [@gen Gen.nat] + | Add_node of int' [@printer pp_t] + | Member of int' [@printer pp_t] [@@deriving qcheck, show { with_path = false }] type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }] - let init () = CList.list_init 0 + let init () = CL.list_init T.dummy let run c r = match c with - | Add_node i -> RAdd_node (CList.add_node r i) - | Member i -> RMember (CList.member r i) + | Add_node i -> RAdd_node (CL.add_node r i) + | Member i -> RMember (CL.member r i) let cleanup _ = () end -module CLT = Lin.Make(CLConf) +module T_int = struct + type t = int + let dummy = 0 + let f i = i + let pp = Int.to_string +end + +module T_int64 = struct + type t = int64 + let dummy = Int64.zero + let f = Int64.of_int + let pp = Int64.to_string +end + +module CLT_int = Lin.Make(CLConf (T_int)) +module CLT_int64 = Lin.Make(CLConf (T_int64)) ;; Util.set_ci_printing () ;; QCheck_runner.run_tests_main [ - RT.lin_test ~count:1000 ~name:"ref test"; - CLT.lin_test ~count:1000 ~name:"CList test"; + RT_int.lin_test `Domain ~count:1000 ~name:"ref int test with Domains"; + RT_int64.lin_test `Domain ~count:1000 ~name:"ref int64 test with Domains"; + RT_int64.lin_test `Thread ~count:1000 ~name:"ref int64 test with Threads"; + CLT_int.lin_test `Domain ~count:1000 ~name:"CList int test with Domains"; + CLT_int.lin_test `Thread ~count:1000 ~name:"CList int test with Threads"; + CLT_int64.lin_test `Domain ~count:1000 ~name:"CList test64 with Domains"; + CLT_int64.lin_test `Thread ~count:1000 ~name:"CList test64 with Threads"; ]