From 005919c8781fbdf957f8de044375373b6ccc6e86 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 11 May 2022 08:38:38 +0200 Subject: [PATCH 1/4] initial precond support: generate and filter --- lib/STM.ml | 45 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 38 insertions(+), 7 deletions(-) diff --git a/lib/STM.ml b/lib/STM.ml index c0cc131b0..34b952612 100644 --- a/lib/STM.ml +++ b/lib/STM.ml @@ -167,7 +167,35 @@ struct 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) - let rec check_obs pref cs1 cs2 s = match pref with + (* checks that all interleavings of a cmd triple satisfies all preconditions *) + let rec all_interleavings_ok pref cs1 cs2 s = + match pref with + | c::pref' -> + Spec.precond c s && + let s' = Spec.next_state c s in + all_interleavings_ok pref' cs1 cs2 s' + | [] -> + match cs1,cs2 with + | [],[] -> true + | [],c2::cs2' -> + Spec.precond c2 s && + let s' = Spec.next_state c2 s in + all_interleavings_ok pref cs1 cs2' s' + | c1::cs1',[] -> + Spec.precond c1 s && + let s' = Spec.next_state c1 s in + all_interleavings_ok pref cs1' cs2 s' + | c1::cs1',c2::cs2' -> + (Spec.precond c1 s && + let s' = Spec.next_state c1 s in + all_interleavings_ok pref cs1' cs2 s') + && + (Spec.precond c2 s && + let s' = Spec.next_state c2 s in + all_interleavings_ok pref cs1 cs2' s') + + let rec check_obs pref cs1 cs2 s = + match pref with | p::pref' -> let b,s' = check_and_next p s in b && check_obs pref' cs1 cs2 s' @@ -193,7 +221,7 @@ struct let open Iter in let shrink_cmd = Option.value Spec.(arb_cmd init_state).shrink ~default:Shrink.nil in Shrink.filter - (fun (seq,p1,p2) -> cmds_ok Spec.init_state (seq@p1) && cmds_ok Spec.init_state (seq@p2)) + (fun (seq,p1,p2) -> all_interleavings_ok seq p1 p2 Spec.init_state) (fun (seq,p1,p2) -> (map (fun seq' -> (seq',p1,p2)) (Shrink.list ~shrink:shrink_cmd seq)) <+> @@ -209,16 +237,18 @@ struct let seq_pref_gen = gen_cmds_size Spec.init_state (Gen.int_bound seq_len) in let gen_triple = Gen.(seq_pref_gen >>= fun seq_pref -> + int_range 2 (2*par_len) >>= fun dbl_plen -> let spawn_state = List.fold_left (fun st c -> Spec.next_state c st) Spec.init_state seq_pref in - let par = gen_cmds_size spawn_state (Gen.int_bound par_len) in - map2 (fun par1 par2 -> (seq_pref,par1,par2)) par par) in + let par_len1 = dbl_plen/2 in + let par_gen1 = gen_cmds_size spawn_state (return par_len1) in + let par_gen2 = gen_cmds_size spawn_state (return (dbl_plen - par_len1)) in + triple (return seq_pref) par_gen1 par_gen2) in make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple (* Parallel agreement property based on [Domain] *) let agree_prop_par = (fun (seq_pref,cmds1,cmds2) -> - assume (cmds_ok Spec.init_state (seq_pref@cmds1)); - assume (cmds_ok Spec.init_state (seq_pref@cmds2)); + assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state); let sut = Spec.init_sut () in let pref_obs = interp_sut_res sut seq_pref in let wait = Atomic.make true in @@ -237,7 +267,8 @@ struct 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) + let max_gen = 2*count in (* precond filtering may require extra generation: max. 2*count though *) + Test.make ~retries:15 ~max_gen ~count ~name:("parallel " ^ name) (arb_cmds_par seq_len par_len) (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *) end From 6299c2b309b952de93798c2de34a449b7a4f2f44 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 11 May 2022 08:39:46 +0200 Subject: [PATCH 2/4] add STM tests of Domainslib.Chan --- src/domainslib/chan_tests.ml | 81 ++++++++++++++++++++++++++++++++++++ src/domainslib/dune | 15 +++++++ 2 files changed, 96 insertions(+) create mode 100644 src/domainslib/chan_tests.ml diff --git a/src/domainslib/chan_tests.ml b/src/domainslib/chan_tests.ml new file mode 100644 index 000000000..9677e1cbc --- /dev/null +++ b/src/domainslib/chan_tests.ml @@ -0,0 +1,81 @@ +open QCheck +open Domainslib + +(** This is a parallel test of Domainslib.Chan *) + +module ChConf = +struct + type state = int list + type sut = int Domainslib.Chan.t + type cmd = + | Send of int + | Send_poll of int + | Recv + | Recv_poll [@@deriving show { with_path = false }] + + let capacity = 8 + + let arb_cmd s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (if s=[] + then + Gen.oneof + [Gen.map (fun i -> Send i) int_gen; + Gen.map (fun i -> Send_poll i) int_gen; + Gen.return Recv_poll] (* don't generate blocking Recv cmds on an empty channel *) + else + if List.length s >= capacity + then + Gen.oneof + [Gen.map (fun i -> Send_poll i) int_gen; + Gen.return Recv; + Gen.return Recv_poll] (* don't generate blocking Send cmds on a full channel *) + else + Gen.oneof + [Gen.map (fun i -> Send i) int_gen; + Gen.map (fun i -> Send_poll i) int_gen; + Gen.return Recv; + Gen.return Recv_poll]) + let init_state = [] + let init_sut () = Chan.make_bounded capacity + let cleanup _ = () + + let next_state c s = match c with + | Send i -> if List.length s < capacity then s@[i] else s + | Send_poll i -> if List.length s < capacity then s@[i] else s + | Recv -> begin match s with [] -> [] | _::s' -> s' end + | Recv_poll -> begin match s with [] -> [] | _::s' -> s' end + + let precond c s = match c,s with + | Recv, [] -> false + | Send _, _ -> List.length s < capacity + | _, _ -> true + + type res = RSend | RSend_poll of bool | RRecv of int | RRecv_poll of int option [@@deriving show { with_path = false }] + + let run c chan = + match c with + | Send i -> (Chan.send chan i; RSend) + | Send_poll i -> RSend_poll (Chan.send_poll chan i) + | Recv -> RRecv (Chan.recv chan) + | Recv_poll -> RRecv_poll (Chan.recv_poll chan) + + let postcond c s res = match c,res with + | Send _, RSend -> (List.length s < capacity) + | Send_poll _, RSend_poll res -> res = (List.length s < capacity) + | Recv, RRecv res -> (match s with [] -> false | res'::_ -> res=res') + | Recv_poll, RRecv_poll opt -> (match s with [] -> None | res'::_ -> Some res') = opt + | _,_ -> false +end + + +module ChT = STM.Make(ChConf) +;; +Util.set_ci_printing () +;; +QCheck_runner.run_tests_main + (let count,name = 1000,"global Domainslib.Chan test" in [ + ChT.agree_test ~count ~name; + ChT.agree_test_par ~count ~name; + ]) diff --git a/src/domainslib/dune b/src/domainslib/dune index 750a4156a..c7f3bad57 100644 --- a/src/domainslib/dune +++ b/src/domainslib/dune @@ -45,3 +45,18 @@ (package multicoretests) (deps task_parallel.exe) (action (run ./%{deps} --no-colors --verbose))) + + +;; STM test of Domainslib.Chan + +(executable + (name chan_tests) + (modes native byte) + (modules chan_tests) + (libraries util qcheck STM domainslib) + (preprocess (pps ppx_deriving.show))) + +(rule + (alias runtest) + (deps chan_tests.exe) + (action (run ./%{deps} --no-colors --verbose))) From eb1846a038fda71d342520f44741e567cb5a658b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 18 May 2022 14:39:48 +0200 Subject: [PATCH 3/4] bump max_gen to 3*count --- lib/STM.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/STM.ml b/lib/STM.ml index 34b952612..47ef5bc33 100644 --- a/lib/STM.ml +++ b/lib/STM.ml @@ -267,7 +267,7 @@ struct let agree_test_par ~count ~name = let rep_count = 25 in let seq_len,par_len = 20,12 in - let max_gen = 2*count in (* precond filtering may require extra generation: max. 2*count though *) + let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *) Test.make ~retries:15 ~max_gen ~count ~name:("parallel " ^ name) (arb_cmds_par seq_len par_len) (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *) From 2a4cf5cfe5a47ce8ea9025bcfff8ff3e41c710f7 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 18 May 2022 17:18:16 +0200 Subject: [PATCH 4/4] bump count to 200 --- src/lazy/lazy_stm_test.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lazy/lazy_stm_test.ml b/src/lazy/lazy_stm_test.ml index f3e4ed725..ae62840e4 100644 --- a/src/lazy/lazy_stm_test.ml +++ b/src/lazy/lazy_stm_test.ml @@ -107,7 +107,7 @@ module LTfromfun = STM.Make(struct Util.set_ci_printing () ;; QCheck_runner.run_tests_main - (let count = 100 in + (let count = 200 in [LTlazy.agree_test ~count ~name:"lazy test"; LTfromval.agree_test ~count ~name:"lazy test from_val"; LTfromfun.agree_test ~count ~name:"lazy test from_fun";