From bf617290641d234f951600d33fa455d42256f1da Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 15 Aug 2023 16:23:19 +0200 Subject: [PATCH 01/10] Disable bytes char shrinking for Lin Out_channel test --- src/io/lin_tests_spec_io.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/io/lin_tests_spec_io.ml b/src/io/lin_tests_spec_io.ml index 82e86ebee..b3888dcf6 100644 --- a/src/io/lin_tests_spec_io.ml +++ b/src/io/lin_tests_spec_io.ml @@ -76,7 +76,14 @@ module OCConf : Lin.Spec = struct let lift f (_, chan) = f chan open Lin - let int,int64,string,bytes = nat_small,nat64_small,string_small,bytes_small + let int,int64,string = nat_small,nat64_small,string_small + + (* disable bytes char shrinking as too many shrinking candidates + triggers long Out_channel shrink runs on Mingw + Cygwin *) + let bytes = + let bytes = QCheck.(set_shrink Shrink.(bytes ~shrink:nil) bytes_small) in + gen_deconstructible bytes (print Lin.bytes) Bytes.equal + let api = [ (* Only one t is tested, so skip stdout, stderr and opening functions *) From d5ff92a21ccbce6e84eb75d7d58e39cf10a8290d Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 15 Aug 2023 16:24:10 +0200 Subject: [PATCH 02/10] Disable string char shrinking for Lin Out_channel test --- src/io/lin_tests_spec_io.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/io/lin_tests_spec_io.ml b/src/io/lin_tests_spec_io.ml index b3888dcf6..df32430dc 100644 --- a/src/io/lin_tests_spec_io.ml +++ b/src/io/lin_tests_spec_io.ml @@ -76,10 +76,13 @@ module OCConf : Lin.Spec = struct let lift f (_, chan) = f chan open Lin - let int,int64,string = nat_small,nat64_small,string_small + let int,int64 = nat_small,nat64_small - (* disable bytes char shrinking as too many shrinking candidates + (* disable string and bytes char shrinking as too many shrinking candidates triggers long Out_channel shrink runs on Mingw + Cygwin *) + let string = + let string = QCheck.(set_shrink Shrink.(string ~shrink:nil) string_small) in + gen_deconstructible string (print Lin.string) String.equal let bytes = let bytes = QCheck.(set_shrink Shrink.(bytes ~shrink:nil) bytes_small) in gen_deconstructible bytes (print Lin.bytes) Bytes.equal From 2433827343b1a80030dae97943fe969403cd70fe Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 17 Aug 2023 11:23:46 +0200 Subject: [PATCH 03/10] Remove lift to reduce allocations --- src/io/lin_tests_spec_io.ml | 48 +++++++++++++++++++------------------ 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/src/io/lin_tests_spec_io.ml b/src/io/lin_tests_spec_io.ml index df32430dc..1cff74e53 100644 --- a/src/io/lin_tests_spec_io.ml +++ b/src/io/lin_tests_spec_io.ml @@ -65,15 +65,17 @@ end module OCConf : Lin.Spec = struct (* a path and an open channel to that file; we need to keep the path to cleanup after the test run *) - type t = string * Out_channel.t + type t = Out_channel.t + let path = ref "" - let init () = Filename.open_temp_file "lin-dsl-" "" - let cleanup (path, chan) = - Out_channel.close chan ; - Sys.remove path + let init () = + let p,ch = Filename.open_temp_file "lin-dsl-" "" in + path := p; + ch - (* turn [f: Out_channel.t -> ...] into [lift f: t -> ...] *) - let lift f (_, chan) = f chan + let cleanup chan = + Out_channel.close chan; + Sys.remove !path open Lin let int,int64 = nat_small,nat64_small @@ -99,21 +101,21 @@ module OCConf : Lin.Spec = struct (* val_ "Out_channel.with_open_text" Out_channel.with_open_text (string @-> (t @-> 'a) @-> returning 'a) ; *) (* val_ "Out_channel.with_open_gen" Out_channel.with_open_gen (open_flag list @-> int @-> string @-> (t @-> 'a) @-> returning 'a) ; *) - val_ "Out_channel.seek" (lift Out_channel.seek) (t @-> int64 @-> returning_or_exc unit) ; - val_freq 3 "Out_channel.pos" (lift Out_channel.pos) (t @-> returning_or_exc int64) ; - val_freq 3 "Out_channel.length" (lift Out_channel.length) (t @-> returning_or_exc int64) ; - val_ "Out_channel.close" (lift Out_channel.close) (t @-> returning_or_exc unit) ; - val_ "Out_channel.close_noerr" (lift Out_channel.close_noerr) (t @-> returning unit) ; - val_ "Out_channel.flush" (lift Out_channel.flush) (t @-> returning_or_exc unit) ; - val_ "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ; - val_ "Out_channel.output_char" (lift Out_channel.output_char) (t @-> char @-> returning_or_exc unit) ; - val_ "Out_channel.output_byte" (lift Out_channel.output_byte) (t @-> int @-> returning_or_exc unit) ; - val_ "Out_channel.output_string" (lift Out_channel.output_string) (t @-> string @-> returning_or_exc unit) ; - val_ "Out_channel.output_bytes" (lift Out_channel.output_bytes) (t @-> bytes @-> returning_or_exc unit) ; - val_ "Out_channel.output" (lift Out_channel.output) (t @-> bytes @-> int @-> int @-> returning_or_exc unit) ; - val_ "Out_channel.output_substring" (lift Out_channel.output_substring) (t @-> string @-> int @-> int @-> returning_or_exc unit) ; - val_ "Out_channel.set_binary_mode" (lift Out_channel.set_binary_mode) (t @-> bool @-> returning_or_exc unit) ; - val_ "Out_channel.set_buffered" (lift Out_channel.set_buffered) (t @-> bool @-> returning_or_exc unit) ; - val_ "Out_channel.is_buffered" (lift Out_channel.is_buffered) (t @-> returning_or_exc bool) ; + val_ "Out_channel.seek" Out_channel.seek (t @-> int64 @-> returning_or_exc unit) ; + val_freq 3 "Out_channel.pos" Out_channel.pos (t @-> returning_or_exc int64) ; + val_freq 3 "Out_channel.length" Out_channel.length (t @-> returning_or_exc int64) ; + val_ "Out_channel.close" Out_channel.close (t @-> returning_or_exc unit) ; + val_ "Out_channel.close_noerr" Out_channel.close_noerr (t @-> returning unit) ; + val_ "Out_channel.flush" Out_channel.flush (t @-> returning_or_exc unit) ; + val_ "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ; + val_ "Out_channel.output_char" Out_channel.output_char (t @-> char @-> returning_or_exc unit) ; + val_ "Out_channel.output_byte" Out_channel.output_byte (t @-> int @-> returning_or_exc unit) ; + val_ "Out_channel.output_string" Out_channel.output_string (t @-> string @-> returning_or_exc unit) ; + val_ "Out_channel.output_bytes" Out_channel.output_bytes (t @-> bytes @-> returning_or_exc unit) ; + val_ "Out_channel.output" Out_channel.output (t @-> bytes @-> int @-> int @-> returning_or_exc unit) ; + val_ "Out_channel.output_substring" Out_channel.output_substring (t @-> string @-> int @-> int @-> returning_or_exc unit) ; + val_ "Out_channel.set_binary_mode" Out_channel.set_binary_mode (t @-> bool @-> returning_or_exc unit) ; + val_ "Out_channel.set_buffered" Out_channel.set_buffered (t @-> bool @-> returning_or_exc unit) ; + val_ "Out_channel.is_buffered" Out_channel.is_buffered (t @-> returning_or_exc bool) ; ] end From ba20a6f8aee7b7aaf2a498d00345c4e2cbce2f00 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 17 Aug 2023 11:25:29 +0200 Subject: [PATCH 04/10] Adjust frequencies to reduce flush_all-triggered allocations --- src/io/lin_tests_spec_io.ml | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/io/lin_tests_spec_io.ml b/src/io/lin_tests_spec_io.ml index 1cff74e53..527ffa245 100644 --- a/src/io/lin_tests_spec_io.ml +++ b/src/io/lin_tests_spec_io.ml @@ -101,21 +101,21 @@ module OCConf : Lin.Spec = struct (* val_ "Out_channel.with_open_text" Out_channel.with_open_text (string @-> (t @-> 'a) @-> returning 'a) ; *) (* val_ "Out_channel.with_open_gen" Out_channel.with_open_gen (open_flag list @-> int @-> string @-> (t @-> 'a) @-> returning 'a) ; *) - val_ "Out_channel.seek" Out_channel.seek (t @-> int64 @-> returning_or_exc unit) ; - val_freq 3 "Out_channel.pos" Out_channel.pos (t @-> returning_or_exc int64) ; - val_freq 3 "Out_channel.length" Out_channel.length (t @-> returning_or_exc int64) ; - val_ "Out_channel.close" Out_channel.close (t @-> returning_or_exc unit) ; - val_ "Out_channel.close_noerr" Out_channel.close_noerr (t @-> returning unit) ; - val_ "Out_channel.flush" Out_channel.flush (t @-> returning_or_exc unit) ; - val_ "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ; - val_ "Out_channel.output_char" Out_channel.output_char (t @-> char @-> returning_or_exc unit) ; - val_ "Out_channel.output_byte" Out_channel.output_byte (t @-> int @-> returning_or_exc unit) ; - val_ "Out_channel.output_string" Out_channel.output_string (t @-> string @-> returning_or_exc unit) ; - val_ "Out_channel.output_bytes" Out_channel.output_bytes (t @-> bytes @-> returning_or_exc unit) ; - val_ "Out_channel.output" Out_channel.output (t @-> bytes @-> int @-> int @-> returning_or_exc unit) ; - val_ "Out_channel.output_substring" Out_channel.output_substring (t @-> string @-> int @-> int @-> returning_or_exc unit) ; - val_ "Out_channel.set_binary_mode" Out_channel.set_binary_mode (t @-> bool @-> returning_or_exc unit) ; - val_ "Out_channel.set_buffered" Out_channel.set_buffered (t @-> bool @-> returning_or_exc unit) ; - val_ "Out_channel.is_buffered" Out_channel.is_buffered (t @-> returning_or_exc bool) ; + val_freq 10 "Out_channel.seek" Out_channel.seek (t @-> int64 @-> returning_or_exc unit) ; + val_freq 20 "Out_channel.pos" Out_channel.pos (t @-> returning_or_exc int64) ; + val_freq 20 "Out_channel.length" Out_channel.length (t @-> returning_or_exc int64) ; + val_freq 10 "Out_channel.close" Out_channel.close (t @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.close_noerr" Out_channel.close_noerr (t @-> returning unit) ; + val_freq 10 "Out_channel.flush" Out_channel.flush (t @-> returning_or_exc unit) ; + val_freq 1 "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.output_char" Out_channel.output_char (t @-> char @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.output_byte" Out_channel.output_byte (t @-> int @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.output_string" Out_channel.output_string (t @-> string @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.output_bytes" Out_channel.output_bytes (t @-> bytes @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.output" Out_channel.output (t @-> bytes @-> int @-> int @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.output_substring" Out_channel.output_substring (t @-> string @-> int @-> int @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.set_binary_mode" Out_channel.set_binary_mode (t @-> bool @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.set_buffered" Out_channel.set_buffered (t @-> bool @-> returning_or_exc unit) ; + val_freq 10 "Out_channel.is_buffered" Out_channel.is_buffered (t @-> returning_or_exc bool) ; ] end From 6c8db20adee709998417dd73da2ece6ff792512f Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 30 Aug 2023 15:36:08 +0200 Subject: [PATCH 05/10] Comment out Out_channel.flush_all to keep GC manageable --- src/io/lin_tests_spec_io.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/io/lin_tests_spec_io.ml b/src/io/lin_tests_spec_io.ml index 527ffa245..5c4999b47 100644 --- a/src/io/lin_tests_spec_io.ml +++ b/src/io/lin_tests_spec_io.ml @@ -107,7 +107,7 @@ module OCConf : Lin.Spec = struct val_freq 10 "Out_channel.close" Out_channel.close (t @-> returning_or_exc unit) ; val_freq 10 "Out_channel.close_noerr" Out_channel.close_noerr (t @-> returning unit) ; val_freq 10 "Out_channel.flush" Out_channel.flush (t @-> returning_or_exc unit) ; - val_freq 1 "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ; + (*val_freq 1 "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ;*) val_freq 10 "Out_channel.output_char" Out_channel.output_char (t @-> char @-> returning_or_exc unit) ; val_freq 10 "Out_channel.output_byte" Out_channel.output_byte (t @-> int @-> returning_or_exc unit) ; val_freq 10 "Out_channel.output_string" Out_channel.output_string (t @-> string @-> returning_or_exc unit) ; From e1a1de31a6cff43649e27810d804fafce3e6f256 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 28 Aug 2023 14:20:33 +0200 Subject: [PATCH 06/10] Reduce allocations when restarting check_seq_cons search --- lib/lin.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/lib/lin.ml b/lib/lin.ml index ab7b12873..b7b8b2480 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -47,6 +47,9 @@ struct (* plain interpreter of a cmd list *) let interp_plain sut cs = List.map (fun c -> (c, Spec.run c sut)) cs + (* plain interpreter ignoring the output and allocating less *) + let interp_plain_ignore sut cs = List.iter (fun c -> ignore (Spec.run c sut)) cs + let rec gen_cmds fuel = Gen.(if fuel = 0 then return [] @@ -113,7 +116,7 @@ struct || (* rerun to get seq_sut to same cmd branching point *) (let seq_sut' = Spec.init () in - let _ = interp_plain seq_sut' (List.rev seq_trace) in + let _ = interp_plain_ignore seq_sut' (List.rev seq_trace) in if Spec.equal_res res2 (Spec.run c2 seq_sut') then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace) else (Spec.cleanup seq_sut'; false)) From 460b97c88439eac44a23eb81856977b19066d4cd Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 30 Aug 2023 15:08:59 +0200 Subject: [PATCH 07/10] Steps to bring Out_channel tests in src/io/lin_tests.ml up to speed with Lin DSL ones --- src/io/lin_tests.ml | 78 +++++++++++++++++++++++++++++---------------- 1 file changed, 51 insertions(+), 27 deletions(-) diff --git a/src/io/lin_tests.ml b/src/io/lin_tests.ml index de797dade..0aeb50aaf 100644 --- a/src/io/lin_tests.ml +++ b/src/io/lin_tests.ml @@ -71,57 +71,81 @@ end module Out_channel_ops = struct - type t = string * Out_channel.t (* Filename and corresponding channel *) - - type cmd = Flush | Close | Write of string + type t = Out_channel.t + let path = ref "" + + type cmd = + | Seek of int64 + | Close + | Flush + | Output_string of string + | Set_binary_mode of bool + | Set_buffered of bool + | Is_buffered let show_cmd = let open Printf in function - | Flush -> "Flush" - | Write s -> sprintf "Write %s" s + | Seek i -> sprintf "Seek %Li" i | Close -> "Close" + | Flush -> "Flush" + | Output_string s -> sprintf "Output_string %s" s + | Set_binary_mode b -> sprintf "Set_binary_mode %s" QCheck.Print.(bool b) + | Set_buffered b -> sprintf "Set_buffered %s" QCheck.Print.(bool b) + | Is_buffered -> "Is_buffered" let gen_cmd = let open QCheck.Gen in frequency - [3, return Flush; - 1, return Close; - 6, map (fun s -> Write s) string; + [10, map (fun i -> Seek (Int64.of_int i)) small_nat; + 10, return Close; + 10, return Flush; + 10, map (fun s -> Output_string s) string_small; + 10, map (fun b -> Set_binary_mode b) bool; + 10, map (fun b -> Set_buffered b) bool; + 10, return Is_buffered; ] let shrink_cmd _ = QCheck.Iter.empty - type res = (unit, exn) result + type inner_res = Unit | Bool of bool + type res = (inner_res, exn) result let show_res = let open Printf in function - | Ok () -> sprintf "()" - | Error e -> sprintf "exception %s" (Printexc.to_string e) + | Ok r -> (match r with + | Unit -> sprintf "()" + | Bool b -> QCheck.Print.(bool b) + ) + | Error e -> sprintf "exception %s" (Printexc.to_string e) let equal_res = (=) let init () = - let filename = Filename.temp_file "fuzz_stdlib" "" in - filename, Out_channel.open_text filename + let p,ch = Filename.open_temp_file "lin-dsl-" "" in + path := p; + ch - let cleanup (filename, chan) = + let cleanup chan = Out_channel.close chan; - try Sys.remove filename with Sys_error _ -> () + Sys.remove !path - let run cmd (_,chan) = + let run cmd chan = match cmd with - | Flush -> - begin try Out_channel.flush chan; Ok () - with e -> Error e - end - | Write s -> - begin try Out_channel.output_string chan s; Ok () - with e -> Error e - end + | Seek i -> + (try Out_channel.seek chan i; Ok Unit with e -> Error e) | Close -> - begin try Out_channel.close chan; Ok () - with e -> Error e - end + (try Out_channel.close chan; Ok Unit with e -> Error e) + | Flush -> + (try Out_channel.flush chan; Ok Unit with e -> Error e) + | Output_string s -> + (try Out_channel.output_string chan s; Ok Unit with e -> Error e) + | Set_binary_mode b -> + (try Out_channel.set_binary_mode chan b; Ok Unit with e -> Error e) + | Set_buffered b -> + (try Out_channel.set_buffered chan b; Ok Unit with e -> Error e) + | Is_buffered -> + (try Ok (Bool (Out_channel.is_buffered chan)) with e -> Error e) + end module Out_channel_lin = Lin_domain.Make_internal (Out_channel_ops) [@@alert "-internal"] From f7223d66b17148e91c90887a7d8d56fec318fe9b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 30 Aug 2023 15:09:44 +0200 Subject: [PATCH 08/10] Swap test order to match module declaration order --- src/io/lin_tests.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/io/lin_tests.ml b/src/io/lin_tests.ml index 0aeb50aaf..c5296af29 100644 --- a/src/io/lin_tests.ml +++ b/src/io/lin_tests.ml @@ -148,13 +148,13 @@ module Out_channel_ops = struct end -module Out_channel_lin = Lin_domain.Make_internal (Out_channel_ops) [@@alert "-internal"] module In_channel_lin = Lin_domain.Make_internal (In_channel_ops) [@@alert "-internal"] +module Out_channel_lin = Lin_domain.Make_internal (Out_channel_ops) [@@alert "-internal"] let () = QCheck_base_runner.run_tests_main - [ Out_channel_lin.lin_test ~count:1000 ~name:"Lin Out_channel test with domains"; - In_channel_lin.lin_test ~count:1000 ~name:"Lin In_channel test with domains"; + [ In_channel_lin.lin_test ~count:1000 ~name:"Lin In_channel test with domains"; + Out_channel_lin.lin_test ~count:1000 ~name:"Lin Out_channel test with domains"; ] let () = From 1b50d2ffcf089cec80c473a9710e03e217434894 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 31 Aug 2023 22:08:50 +0200 Subject: [PATCH 09/10] Address review: cleaner call to interp_plain_ignore --- lib/lin.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/lin.ml b/lib/lin.ml index b7b8b2480..8751100fe 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -116,7 +116,7 @@ struct || (* rerun to get seq_sut to same cmd branching point *) (let seq_sut' = Spec.init () in - let _ = interp_plain_ignore seq_sut' (List.rev seq_trace) in + interp_plain_ignore seq_sut' (List.rev seq_trace); if Spec.equal_res res2 (Spec.run c2 seq_sut') then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace) else (Spec.cleanup seq_sut'; false)) From bb94d344de3219288a6a462b66760189b0b58f8d Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 31 Aug 2023 22:13:42 +0200 Subject: [PATCH 10/10] Add a CHANGES entry for the Lin allocation improvement --- CHANGES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index eabe19628..55ca68a60 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,8 @@ ## Next +- #387: Reduce needless allocations in `Lin`'s sequential consistency + search, as part of an `Out_channel` test cleanup - #368: Switch `STM_domain.agree_prop_par_asym` from using `Semaphore.Binary` to using an `int Atomic.t` which improves the error rate across platforms and backends