Skip to content

Commit

Permalink
Merge pull request #365 from ocaml-multicore/weak-hashset-predictable
Browse files Browse the repository at this point in the history 
Weak test revisions
  • Loading branch information
@jmid
jmid authored Jun 13, 2023
2 parents 518f903 + f3d0160 commit c08b00a
Show file tree
Hide file tree
Showing 5 changed files with 109 additions and 137 deletions.
16 changes: 0 additions & 16 deletions src/weak/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,19 +15,3 @@
(libraries qcheck-stm.sequential qcheck-stm.domain)
(action (run %{test} --verbose))
)

(test
(name lin_tests_dsl)
(modules lin_tests_dsl)
(package multicoretests)
(libraries qcheck-lin.domain)
(action (run %{test} --verbose))
)

(test
(name lin_tests_dsl_hashset)
(modules lin_tests_dsl_hashset)
(package multicoretests)
(libraries qcheck-lin.domain)
(action (run %{test} --verbose))
)
29 changes: 0 additions & 29 deletions src/weak/lin_tests_dsl.ml
View file

This file was deleted.

34 changes: 0 additions & 34 deletions src/weak/lin_tests_dsl_hashset.ml
View file

This file was deleted.

65 changes: 46 additions & 19 deletions src/weak/stm_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,12 @@ module WConf =
struct
type cmd =
| Length
| Set of int * int64 option
| Set of int * data option
| Get of int
| Get_copy of int
| Check of int
| Fill of int * int * int64 option
| Fill of int * int * data option
and data = int64

let pp_cmd par fmt x =
let open Util.Pp in
Expand All @@ -26,20 +27,31 @@ struct

let show_cmd = Util.Pp.to_show pp_cmd

type state = int64 option list
type sut = int64 Weak.t
type state = data option list
type sut = data Weak.t

let shrink_cmd c = match c with
| Length -> Iter.empty
| Set (i, d_opt) -> Iter.map (fun i -> Set (i,d_opt)) (Shrink.int i)
| Get i -> Iter.map (fun i -> Get i) (Shrink.int i)
| Get_copy i -> Iter.map (fun i -> Get_copy i) (Shrink.int i)
| Check i -> Iter.map (fun i -> Check i) (Shrink.int i)
| Fill (i,j,d_opt) ->
Iter.(map (fun i -> Fill (i,j,d_opt)) (Shrink.int i)
<+>
map (fun j -> Fill (i,j,d_opt)) (Shrink.int j))

let arb_cmd s =
let int_gen = Gen.(oneof [small_nat; int_bound (List.length s - 1)]) in
let int64_gen = Gen.(map Int64.of_int small_int) in
QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*)
Gen.(oneof
[ return Length;
map2 (fun i c -> Set (i,c)) int_gen (option int64_gen);
map (fun i -> Get i) int_gen;
map (fun i -> Get_copy i) int_gen;
map (fun i -> Check i) int_gen;
map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen (option int64_gen); (* hack: reusing int_gen for length *)
QCheck.make ~print:show_cmd ~shrink:shrink_cmd
Gen.(frequency
[ 1,return Length;
1,map2 (fun i c -> Set (i,c)) int_gen (option int64_gen);
2,map (fun i -> Get i) int_gen;
2,map (fun i -> Get_copy i) int_gen;
2,map (fun i -> Check i) int_gen;
1,map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen (option int64_gen); (* hack: reusing int_gen for length *)
])

let weak_size = 16
Expand All @@ -59,7 +71,7 @@ struct
List.mapi (fun j c' -> if i <= j && j <= i+l-1 then c else c') s
else s

let init_sut () = Weak.create weak_size
let init_sut () = Gc.minor (); Weak.create weak_size
let cleanup _ = ()

let precond c _s = match c with
Expand Down Expand Up @@ -99,9 +111,24 @@ struct
end

module WeakSTM_seq = STM_sequential.Make(WConf)
(*module WeakSTM_dom = STM_domain.Make(WConf)*)
;;
QCheck_base_runner.run_tests_main
[ WeakSTM_seq.agree_test ~count:1000 ~name:"STM Weak test sequential";
(*WeakSTM_dom.neg_agree_test_par ~count:1000 ~name:"STM Weak test parallel";*)
]
module WeakSTM_dom = STM_domain.Make(WConf)


(* Beware: hoop jumping to enable a full major Gc run between the two tests!
We need that to avoid the state of the second test depending on the resulting
GC state of the first test and don't want to exit after the first run
(as QCheck_base_runner.run_tests_main does). *)
let cli_args = QCheck_base_runner.Raw.parse_cli ~full_options:false Sys.argv
let run_tests l =
QCheck_base_runner.run_tests l
~colors:cli_args.cli_colors
~verbose:cli_args.cli_verbose
~long:cli_args.cli_long_tests ~out:stdout ~rand:cli_args.cli_rand
let status_seq =
run_tests
[ WeakSTM_seq.agree_test ~count:1000 ~name:"STM Weak test sequential"; ]
let () = Gc.full_major ()
let status_par =
run_tests
[ WeakSTM_dom.neg_agree_test_par ~count:2000 ~name:"STM Weak test parallel"; ]
let _ = exit (if status_seq=0 && status_par=0 then 0 else 1)
102 changes: 63 additions & 39 deletions src/weak/stm_tests_hashset.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,11 @@ struct
| Find_all of data
| Count
| Stats
and data = string
and data = int64

let pp_cmd par fmt x =
let open Util.Pp in
let pp_data = pp_string in
let pp_data = pp_int64 in
match x with
| Clear -> cst0 "Clear" fmt
| Merge x -> cst1 pp_data "Merge" par fmt x
Expand All @@ -39,39 +39,48 @@ struct

type state = data list

module WHS = Weak.Make(String)
module Int64 =
struct
[@@@warning "-unused-value-declaration"]
(* support Int64.hash added in 5.1, without triggering an 'unused hash' error *)
external seeded_hash_param :
int -> int -> int -> 'a -> int = "caml_hash" [@@noalloc]
let hash x = seeded_hash_param 10 100 0 x
include Stdlib.Int64
end
module WHS = Weak.Make(Int64)
type sut = WHS.t

let shrink_string s = Shrink.string ~shrink:Shrink.nil s
let shrink_data d = Shrink.int64 d

let shrink_cmd c = match c with
| Clear -> Iter.empty
| Merge d -> Iter.map (fun d -> Merge d) (shrink_string d)
| Add d -> Iter.map (fun d -> Add d) (shrink_string d)
| Remove d -> Iter.map (fun d -> Remove d) (shrink_string d)
| Find d -> Iter.map (fun d -> Find d) (shrink_string d)
| Find_opt d -> Iter.map (fun d -> Find_opt d) (shrink_string d)
| Find_all d -> Iter.map (fun d -> Find_all d) (shrink_string d)
| Mem d -> Iter.map (fun d -> Mem d) (shrink_string d)
| Merge d -> Iter.map (fun d -> Merge d) (shrink_data d)
| Add d -> Iter.map (fun d -> Add d) (shrink_data d)
| Remove d -> Iter.map (fun d -> Remove d) (shrink_data d)
| Find d -> Iter.map (fun d -> Find d) (shrink_data d)
| Find_opt d -> Iter.map (fun d -> Find_opt d) (shrink_data d)
| Find_all d -> Iter.map (fun d -> Find_all d) (shrink_data d)
| Mem d -> Iter.map (fun d -> Mem d) (shrink_data d)
| Count -> Iter.empty
| Stats -> Iter.empty

let arb_cmd s =
let data_gen = match s with
| [] -> Gen.string_small
| _::_ -> Gen.(oneof [oneofl s; string_small]) in
| [] -> Gen.(map Int64.of_int small_int)
| _::_ -> Gen.(oneof [oneofl s; map Int64.of_int small_int]) in
QCheck.make ~print:show_cmd ~shrink:shrink_cmd
Gen.(oneof
[ return Clear;
map (fun d -> Merge d) data_gen;
map (fun d -> Add d) data_gen;
map (fun d -> Remove d) data_gen;
map (fun d -> Find d) data_gen;
map (fun d -> Find_opt d) data_gen;
map (fun d -> Find_all d) data_gen;
map (fun d -> Mem d) data_gen;
return Count;
return Stats;
Gen.(frequency
[ 1,return Clear;
1,map (fun d -> Merge d) data_gen;
1,map (fun d -> Add d) data_gen;
1,map (fun d -> Remove d) data_gen;
1,map (fun d -> Find d) data_gen;
1,map (fun d -> Find_opt d) data_gen;
1,map (fun d -> Find_all d) data_gen;
1,map (fun d -> Mem d) data_gen;
3,return Count;
2,return Stats;
])

let init_state = []
Expand All @@ -93,7 +102,8 @@ struct
| Stats -> s

let weak_size = 16
let init_sut () = WHS.create weak_size
(* The SUT state is GC dependent - run a minor GC to have a clean starting point *)
let init_sut () = Gc.minor (); WHS.create weak_size
let cleanup _ = ()

let precond c _s = match c with
Expand All @@ -113,34 +123,34 @@ struct

let run c hs = match c with
| Clear -> Res (unit, WHS.clear hs)
| Merge d -> Res (result string exn, protect (WHS.merge hs) d)
| Merge d -> Res (result int64 exn, protect (WHS.merge hs) d)
| Add d -> Res (result unit exn, protect (WHS.add hs) d)
| Remove d -> Res (result unit exn, protect (WHS.remove hs) d)
| Find d -> Res (result string exn, protect (WHS.find hs) d)
| Find_opt d -> Res (result (option string) exn, protect (WHS.find_opt hs) d)
| Find_all d -> Res (result (list string) exn, protect (WHS.find_all hs) d)
| Find d -> Res (result int64 exn, protect (WHS.find hs) d)
| Find_opt d -> Res (result (option int64) exn, protect (WHS.find_opt hs) d)
| Find_all d -> Res (result (list int64) exn, protect (WHS.find_all hs) d)
| Mem d -> Res (result bool exn, protect (WHS.mem hs) d)
| Count -> Res (int, WHS.count hs)
| Stats -> Res (tup6 int int int int int int, WHS.stats hs)

let postcond c (s:data list) res = match c, res with
| Clear, Res ((Unit,_),()) -> true
| Merge d, Res ((Result (String,Exn),_),r) ->
| Merge d, Res ((Result (Int64,Exn),_),r) ->
(match r with
| Error e -> e = Invalid_argument "index out of bounds"
| Ok r -> if List.mem d s then r = d else r == d)
| Add _, Res ((Result (Unit,Exn),_),r) ->
r = Error (Invalid_argument "index out of bounds") || r = Ok ()
| Remove _, Res ((Result (Unit,Exn),_),r) ->
r = Error (Invalid_argument "index out of bounds") || r = Ok ()
| Find d, Res ((Result (String,Exn),_),r) ->
| Find d, Res ((Result (Int64,Exn),_),r) ->
r = Error (Invalid_argument "index out of bounds") ||
r = Error Not_found ||
(List.mem d s && r = Ok d)
| Find_opt d, Res ((Result (Option String,Exn),_),r) ->
| Find_opt d, Res ((Result (Option Int64,Exn),_),r) ->
r = Error (Invalid_argument "index out of bounds") ||
r = Ok None || r = Ok (Some d)
| Find_all d, Res ((Result (List String,Exn),_),r) ->
| Find_all d, Res ((Result (List Int64,Exn),_),r) ->
(match r with
| Error e -> e = Invalid_argument "index out of bounds"
| Ok r -> List.for_all (fun d' -> d' = d) r)
Expand All @@ -157,9 +167,23 @@ struct
end

module WeakHashsetSTM_seq = STM_sequential.Make(WHSConf)
(*module WeakHashsetSTM_dom = STM_domain.Make(WHSConf)*)
;;
QCheck_base_runner.run_tests_main
[ WeakHashsetSTM_seq.agree_test ~count:1000 ~name:"STM Weak HashSet test sequential";
(*WeakHashsetSTM_dom.neg_agree_test_par ~count:1000 ~name:"STM Weak HashSet test parallel";*)
]
module WeakHashsetSTM_dom = STM_domain.Make(WHSConf)

(* Beware: hoop jumping to enable a full major Gc run between the two tests!
We need that to avoid the state of the second test depending on the resulting
GC state of the first test and don't want to exit after the first run
(as QCheck_base_runner.run_tests_main does). *)
let cli_args = QCheck_base_runner.Raw.parse_cli ~full_options:false Sys.argv
let run_tests l =
QCheck_base_runner.run_tests l
~colors:cli_args.cli_colors
~verbose:cli_args.cli_verbose
~long:cli_args.cli_long_tests ~out:stdout ~rand:cli_args.cli_rand
let status_seq =
run_tests
[ WeakHashsetSTM_seq.agree_test ~count:1000 ~name:"STM Weak HashSet test sequential" ]
let () = Gc.full_major ()
let status_par =
run_tests
[ WeakHashsetSTM_dom.neg_agree_test_par ~count:2000 ~name:"STM Weak HashSet test parallel" ]
let _ = exit (if status_seq=0 && status_par=0 then 0 else 1)

0 comments on commit c08b00a

Please sign in to comment.