From 10e15f46191e2ee06f0f8ba3b1152cf57507c99e Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 10 May 2022 10:33:04 +0200 Subject: [PATCH 1/4] clean-up STM interface, stick w/repeat-retries combination --- lib/STM.ml | 35 ++++------------------------------- 1 file changed, 4 insertions(+), 31 deletions(-) diff --git a/lib/STM.ml b/lib/STM.ml index 79fa383ae..c0cc131b0 100644 --- a/lib/STM.ml +++ b/lib/STM.ml @@ -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 @@ -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 (** ********************************************************************** *) From e68c6d3b528fe66a5b58fe1da4dd97f12540b878 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 10 May 2022 10:33:31 +0200 Subject: [PATCH 2/4] add int64 ref test --- src/neg_tests/ref_test.ml | 105 ++++++++++++++++++++++++++++++++------ 1 file changed, 88 insertions(+), 17 deletions(-) diff --git a/src/neg_tests/ref_test.ml b/src/neg_tests/ref_test.ml index 8b3123e98..11240cd7e 100644 --- a/src/neg_tests/ref_test.ml +++ b/src/neg_tests/ref_test.ml @@ -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 @@ -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 @@ -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 @@ -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*) @@ -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)"; + ]) From 69e1a9496e8c288c722b58e2ef10fc9b46748c65 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 10 May 2022 16:49:26 +0200 Subject: [PATCH 3/4] whitespace cleanups --- src/buffer/buffer_stm_test.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/buffer/buffer_stm_test.ml b/src/buffer/buffer_stm_test.ml index f7fe63274..41393362a 100644 --- a/src/buffer/buffer_stm_test.ml +++ b/src/buffer/buffer_stm_test.ml @@ -42,7 +42,7 @@ struct then Gen.return 0 else Gen.int_bound (len - 1)); ]) - + let init_state = [] let rev_explode s = @@ -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 @@ -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 @@ -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) @@ -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 From 5f250f4fe20c63929be857157db10c7f70d86262 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 10 May 2022 18:08:21 +0200 Subject: [PATCH 4/4] expecting 4 failures w/the new int64 ref test --- src/neg_tests/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/neg_tests/dune b/src/neg_tests/dune index 947736dc5..0d4c37d5a 100644 --- a/src/neg_tests/dune +++ b/src/neg_tests/dune @@ -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)