Merge pull request #1 from n-osborne/thread

Tests linearizability with threads

lib/dune

@@ -11,4 +11,4 @@
 (library
  (name lin)
  (modules lin)
- (libraries qcheck))
+ (libraries threads qcheck))

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

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

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";
 ]

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";
    ])

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";
 ]

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";
 ]

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

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

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

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";
 ]