Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

STM clean-up #63

Merged
merged 4 commits into from
May 18, 2022
Merged

STM clean-up #63

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
10e15f4
clean-up STM interface, stick w/repeat-retries combination
jmid May 10, 2022
e68c6d3
add int64 ref test
jmid May 10, 2022
69e1a94
whitespace cleanups
jmid May 10, 2022
5f250f4
expecting 4 failures w/the new int64 ref test
jmid May 10, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 4 additions & 31 deletions lib/STM.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,10 +85,6 @@ module Make(Spec : StmSpec) (*: StmTest *)
val arb_cmds_par : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
val agree_prop_par : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
val agree_test_par : count:int -> name:string -> Test.t
val agree_test_par_retries : count:int -> name:string -> Test.t
val agree_test_par_comb : count:int -> name:string -> Test.t

val agree_test_suite : count:int -> name:string -> Test.t list
end
=
struct
Expand Down Expand Up @@ -237,36 +233,13 @@ struct
(fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
(pref_obs,obs1,obs2))

(* Parallel agreement test based on [Domain] and [repeat] *)
let agree_test_par ~count ~name =
let rep_count = 50 in
let seq_len,par_len = 20,12 in
Test.make ~count ~name:("parallel " ^ name ^ " (w/repeat)")
(arb_cmds_par seq_len par_len)
(repeat rep_count agree_prop_par)

(* Parallel agreement test based on [Domain] and [~retries] *)
let agree_test_par_retries ~count ~name =
let rep_count = 200 in
let seq_len,par_len = 20,12 in
Test.make ~retries:rep_count ~count ~name:("parallel " ^ name ^ " (w/shrink retries)")
(arb_cmds_par seq_len par_len) agree_prop_par

(* Parallel agreement test based on [Domain] which combines [repeat] and [~retries] *)
let agree_test_par_comb ~count ~name =
let rep_count = 15 in
let agree_test_par ~count ~name =
let rep_count = 25 in
let seq_len,par_len = 20,12 in
Test.make ~retries:15 ~count ~name:("parallel " ^ name ^ " (w/repeat-retries comb.)")
Test.make ~retries:15 ~count ~name:("parallel " ^ name)
(arb_cmds_par seq_len par_len)
(repeat rep_count agree_prop_par) (* 15 times each, then 15 * 15 times when shrinking *)

let agree_test_suite ~count ~name =
[ agree_test ~count ~name;
agree_test_par ~count ~name;
agree_test_par_retries ~count ~name;
agree_test_par_comb ~count ~name;
]

(repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *)
end

(** ********************************************************************** *)
Expand Down
10 changes: 5 additions & 5 deletions src/buffer/buffer_stm_test.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ struct
then Gen.return 0
else Gen.int_bound (len - 1));
])

let init_state = []

let rev_explode s =
Expand All @@ -53,7 +53,7 @@ struct
let explode s = List.rev (rev_explode s)
let to_string s = List.rev s
|> List.map (fun c -> Printf.sprintf "%c" c)
|> String.concat ""
|> String.concat ""

(* changed *)
let next_state c s = match c with
Expand All @@ -74,7 +74,7 @@ struct
| _::_,0 -> []
| c::cs,_ -> c::trunc cs (n-1) in
List.rev (trunc (List.rev s) i)

let init_sut () = Buffer.create 16
let cleanup b = Buffer.reset b

Expand All @@ -95,7 +95,7 @@ struct
| RAdd_string
| RAdd_bytes
| RTruncate of (unit, exn) result [@@deriving show { with_path = false }]

(* changed *)
let run c b = match c with
| Contents -> RContent (Buffer.contents b)
Expand All @@ -109,7 +109,7 @@ struct
| Add_string str -> Buffer.add_string b str; RAdd_string
| Add_bytes bytes -> Buffer.add_bytes b bytes; RAdd_bytes
| Truncate i -> RTruncate (Util.protect (Buffer.truncate b) i)

(* added *)
let postcond c s res = match c, res with
| Contents, RContent str -> explode str = List.rev s
Expand Down
2 changes: 1 addition & 1 deletion src/neg_tests/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
(action
(progn
(bash "(./ref_test.exe --no-colors --verbose || echo 'test run triggered an error') | tee ref-output.txt")
(run %{bin:check_error_count} "neg_tests/ref_test" 2 ref-output.txt))))
(run %{bin:check_error_count} "neg_tests/ref_test" 4 ref-output.txt))))

(library
(name CList)
Expand Down
105 changes: 88 additions & 17 deletions src/neg_tests/ref_test.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ open QCheck

(** This is a parallel test of refs *)

module Sut =
module Sut_int =
struct
let init () = ref 0
let get r = !r
Expand All @@ -12,16 +12,26 @@ module Sut =
let decr r = decr r (* buggy: not atomic *)
end

module RConf =
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 sut = int ref
type state = int
type cmd =
| Get
| Set of int
| Add of int
| Incr
| Decr [@@deriving show { with_path = false }]
type state = int
type sut = int ref

let arb_cmd _s =
let int_gen = Gen.nat in
Expand All @@ -35,7 +45,7 @@ struct
])

let init_state = 0
let init_sut () = Sut.init ()
let init_sut () = Sut_int.init ()
let cleanup _ = ()

let next_state c s = match c with
Expand All @@ -50,11 +60,11 @@ struct
type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }]

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 postcond c s res = match c,res with
| Get, RGet v -> v = s (*&& v<>42*) (*an injected bug*)
Expand All @@ -65,16 +75,77 @@ struct
| _,_ -> false
end

module RConf_int64 =
struct
type sut = int64 ref
type state = int64
type cmd =
| Get
| Set of int64
| Add of int64
| Incr
| Decr [@@deriving show { with_path = false }]

let arb_cmd _s =
let int64_gen = Gen.(map Int64.of_int nat) in
QCheck.make ~print:show_cmd
(Gen.oneof
[Gen.return Get;
Gen.map (fun i -> Set i) int64_gen;
Gen.map (fun i -> Add i) int64_gen;
Gen.return Incr;
Gen.return Decr;
])

let init_state = 0L
let init_sut () = Sut_int64.init ()
let cleanup _ = ()

let next_state c s = match c with
| Get -> s
| Set i -> i (*if i<>1213 then i else s*) (* an artificial fault *)
| Add i -> Int64.add s i
| Incr -> Int64.succ s
| Decr -> Int64.pred s

let precond _ _ = true

type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }]

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 postcond c s res = match c,res with
| Get, RGet v -> v = s (*&& v<>42L*) (*an injected bug*)
| Set _, RSet -> true
| Add _, RAdd -> true
| Incr, RIncr -> true
| Decr, RDecr -> true
| _,_ -> false
end


module RT_int = STM.Make(RConf_int)
module RT_int64 = STM.Make(RConf_int64)

module RT = STM.Make(RConf)
module RConf_int_GC = STM.AddGC(RConf_int)
module RConf_int64_GC = STM.AddGC(RConf_int64)

module RConfGC = STM.AddGC(RConf)
module RTGC = STM.Make(RConfGC)
module RT_int_GC = STM.Make(RConf_int_GC)
module RT_int64_GC = STM.Make(RConf_int64_GC)
;;
Util.set_ci_printing ()
;;
QCheck_runner.run_tests_main
(let count,name = 1000,"global ref test" in
[RT.agree_test ~count ~name;
RT.agree_test_par ~count ~name;
RTGC.agree_test_par ~count ~name:"global ref test (w/AddGC functor)"])
(let count = 1000 in
[RT_int.agree_test ~count ~name:"global int ref test";
RT_int.agree_test_par ~count ~name:"global int ref test";
RT_int_GC.agree_test_par ~count ~name:"global int ref test (w/AddGC functor)";
RT_int.agree_test ~count ~name:"global int64 ref test";
RT_int.agree_test_par ~count ~name:"global int64 ref test";
RT_int_GC.agree_test_par ~count ~name:"global int64 ref test (w/AddGC functor)";
])