diff options
Diffstat (limited to 'dev/bench/render_results')
| -rwxr-xr-x | dev/bench/render_results | 434 |
1 files changed, 434 insertions, 0 deletions
diff --git a/dev/bench/render_results b/dev/bench/render_results new file mode 100755 index 0000000000..72affd70b2 --- /dev/null +++ b/dev/bench/render_results @@ -0,0 +1,434 @@ +#! /usr/bin/env ocaml + +(* ASSUMPTIONS: + - the 1-st command line argument (working directory): + - designates an existing readable directory + - which contains *.time and *.perf files produced by bench.sh script + - the 2-nd command line argument (number of iterations): + - is a positive integer + - the 3-rd command line argument (minimal user time): + - is a positive floating point number + - the 4-th command line argument determines the name of the column according to which the resulting table will be sorted. + Valid values are: + - package_name + - user_time_pdiff + - the rest of the command line-arguments + - are names of benchamarked Coq OPAM packages for which bench.sh script generated *.time and *.perf files + *) + +#use "topfind";; +#require "unix";; +#print_depth 100000000;; +#print_length 100000000;; + +open Printf +open Unix +;; + +let _ = Printexc.record_backtrace true +;; + +type ('a,'b) pkg_timings = { + user_time : 'a; + num_instr : 'b; + num_cycles : 'b; + num_mem : 'b; + num_faults : 'b; +} +;; + +let reduce_pkg_timings (m_f : 'a list -> 'c) (m_a : 'b list -> 'd) (t : ('a,'b) pkg_timings list) : ('c,'d) pkg_timings = + { user_time = m_f @@ List.map (fun x -> x.user_time) t + ; num_instr = m_a @@ List.map (fun x -> x.num_instr) t + ; num_cycles = m_a @@ List.map (fun x -> x.num_cycles) t + ; num_mem = m_a @@ List.map (fun x -> x.num_mem) t + ; num_faults = m_a @@ List.map (fun x -> x.num_faults) t + } +;; + +(******************************************************************************) +(* BEGIN Copied from batteries, to remove *) +(******************************************************************************) +let run_and_read cmd = + (* This code is before the open of BatInnerIO + to avoid using batteries' wrapped IOs *) + let string_of_file fn = + let buff_size = 1024 in + let buff = Buffer.create buff_size in + let ic = open_in fn in + let line_buff = Bytes.create buff_size in + begin + let was_read = ref (input ic line_buff 0 buff_size) in + while !was_read <> 0 do + Buffer.add_subbytes buff line_buff 0 !was_read; + was_read := input ic line_buff 0 buff_size; + done; + close_in ic; + end; + Buffer.contents buff + in + let tmp_fn = Filename.temp_file "" "" in + let cmd_to_run = cmd ^ " > " ^ tmp_fn in + let status = Unix.system cmd_to_run in + let output = string_of_file tmp_fn in + Unix.unlink tmp_fn; + (status, output) +;; + +let ( %> ) f g x = g (f x) +;; + +let run = run_and_read %> snd +;; + +module Float = struct + let nan = Pervasives.nan +end + +module Tuple4 = struct + + let first (x,_,_,_) = x + let second (_,y,_,_) = y + let third (_,_,z,_) = z + let fourth (_,_,_,z) = z + +end +;; + +module List = struct + include List + + let rec init_tailrec_aux acc i n f = + if i >= n then acc + else init_tailrec_aux (f i :: acc) (i+1) n f + + let rec init_aux i n f = + if i >= n then [] + else + let r = f i in + r :: init_aux (i+1) n f + + let rev_init_threshold = + match Sys.backend_type with + | Sys.Native | Sys.Bytecode -> 10_000 + (* We don't known the size of the stack, better be safe and assume it's small. *) + | Sys.Other _ -> 50 + + let init len f = + if len < 0 then invalid_arg "List.init" else + if len > rev_init_threshold then rev (init_tailrec_aux [] 0 len f) + else init_aux 0 len f + + let rec drop n = function + | _ :: l when n > 0 -> drop (n-1) l + | l -> l + + let reduce f = function + | [] -> + invalid_arg "List.reduce: Empty List" + | h :: t -> + fold_left f h t + + let min l = reduce Pervasives.min l + let max l = reduce Pervasives.max l + +end +;; + +module String = struct + + include String + + let rchop ?(n = 1) s = + if n < 0 then + invalid_arg "String.rchop: number of characters to chop is negative" + else + let slen = length s in + if slen <= n then "" else sub s 0 (slen - n) + +end +;; + +(******************************************************************************) +(* END Copied from batteries, to remove *) +(******************************************************************************) + +let mk_pkg_timings work_dir pkg_name suffix iteration = + let command_prefix = "cat " ^ work_dir ^ "/" ^ pkg_name ^ suffix ^ string_of_int iteration in + let time_command_output = command_prefix ^ ".time" |> run |> String.rchop ~n:1 |> String.split_on_char ' ' in + + let nth x i = List.nth i x in + + { user_time = time_command_output |> nth 0 |> float_of_string + (* Perf can indeed be not supported in some systems, so we must fail gracefully *) + ; num_instr = + (try command_prefix ^ ".perf | grep instructions:u | awk '{print $1}' | sed 's/,//g'" |> + run |> String.rchop ~n:1 |> int_of_string + with Failure _ -> 0) + ; num_cycles = + (try command_prefix ^ ".perf | grep cycles:u | awk '{print $1}' | sed 's/,//g'" |> + run |> String.rchop ~n:1 |> int_of_string + with Failure _ -> 0) + ; num_mem = time_command_output |> nth 1 |> int_of_string + ; num_faults = time_command_output |> nth 2 |> int_of_string + } +;; + +(* process command line paramters *) +assert (Array.length Sys.argv > 5); +let work_dir = Sys.argv.(1) in +let num_of_iterations = int_of_string Sys.argv.(2) in +let new_coq_version = Sys.argv.(3) in +let old_coq_version = Sys.argv.(4) in +let minimal_user_time = float_of_string Sys.argv.(5) in +let sorting_column = Sys.argv.(6) in +let coq_opam_packages = Sys.argv |> Array.to_list |> List.drop 7 in + +(* ASSUMPTIONS: + + "working_dir" contains all the files produced by the following command: + + two_points_on_the_same_branch.sh $working_directory $coq_repository $coq_branch[:$new:$old] $num_of_iterations coq_opam_package_1 coq_opam_package_2 ... coq_opam_package_N +-sf +*) + +(* Run a given bash command; + wait until it termines; + check if its exit status is 0; + return its whole stdout as a string. *) + +let proportional_difference_of_integers new_value old_value = + if old_value = 0 + then Float.nan + else float_of_int (new_value - old_value) /. float_of_int old_value *. 100.0 +in + +let count_number_of_digits_before_decimal_point = + log10 %> floor %> int_of_float %> succ %> max 1 +in + +(* parse the *.time and *.perf files *) +coq_opam_packages +|> List.map + (fun package_name -> + package_name,(* compilation_results_for_NEW : (float * int * int * int) list *) + List.init num_of_iterations succ |> List.map (mk_pkg_timings work_dir package_name ".NEW."), + List.init num_of_iterations succ |> List.map (mk_pkg_timings work_dir package_name ".OLD.")) + +(* from the list of measured values, select just the minimal ones *) + +|> List.map + (fun ((package_name : string), + (new_measurements : (float, int) pkg_timings list), + (old_measurements : (float, int) pkg_timings list)) -> + let f_min : float list -> float = List.min in + let i_min : int list -> int = List.min in + package_name, + reduce_pkg_timings f_min i_min new_measurements, + reduce_pkg_timings f_min i_min old_measurements + ) + +(* compute the "proportional differences in % of the NEW measurement and the OLD measurement" of all measured values *) +|> List.map + (fun (package_name, new_t, old_t) -> + package_name, new_t, old_t, + { user_time = (new_t.user_time -. old_t.user_time) /. old_t.user_time *. 100.0 + ; num_instr = proportional_difference_of_integers new_t.num_instr old_t.num_instr + ; num_cycles = proportional_difference_of_integers new_t.num_cycles old_t.num_cycles + ; num_mem = proportional_difference_of_integers new_t.num_mem old_t.num_mem + ; num_faults = proportional_difference_of_integers new_t.num_faults old_t.num_faults + }) + +(* sort the table with results *) +|> List.sort + (match sorting_column with + | "user_time_pdiff" -> + fun (_,_,_,perf1) (_,_,_,perf2) -> + compare perf1.user_time perf2.user_time + | "package_name" -> + fun (n1,_,_,_) (n2,_,_,_) -> compare n1 n2 + | _ -> + assert false + ) + +(* Keep only measurements that took at least "minimal_user_time" (in seconds). *) + +|> List.filter + (fun (_, new_t, old_t, _) -> + minimal_user_time <= new_t.user_time && minimal_user_time <= old_t.user_time) + +(* Below we take the measurements and format them to stdout. *) + +|> fun measurements -> + + let precision = 2 in + + (* the labels that we will print *) + let package_name__label = "package_name" in + let new__label = "NEW" in + let old__label = "OLD" in + let proportional_difference__label = "PDIFF" in + + (* the lengths of labels that we will print *) + let new__label__length = String.length new__label in + let proportional_difference__label__length = String.length proportional_difference__label in + + (* widths of individual columns of the table *) + let package_name__width = + max (measurements |> List.map (Tuple4.first %> String.length) |> List.max) + (String.length package_name__label) in + + let llf proj = + let lls = count_number_of_digits_before_decimal_point (List.max proj) + 1 + precision in + max lls new__label__length in + + let lli proj = + let lls = count_number_of_digits_before_decimal_point (float_of_int (List.(max proj))) + 1 + precision in + max lls new__label__length in + + let new_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.second measurements in + let old_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.third measurements in + + let llp proj = + let lls = + count_number_of_digits_before_decimal_point List.(max List.(map abs_float proj)) + 2 + precision in + max lls proportional_difference__label__length in + + let perc_timing_width = reduce_pkg_timings llp llp @@ List.map Tuple4.fourth measurements in + + (* print the table *) + let rec make_dashes = function + | 0 -> "" + | count -> "─" ^ make_dashes (pred count) + in + + let vertical_separator left_glyph middle_glyph right_glyph = + sprintf "%s─%s─%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s\n" + left_glyph + (make_dashes package_name__width) + middle_glyph + (make_dashes new_timing_width.user_time) + (make_dashes old_timing_width.user_time) + (make_dashes perc_timing_width.user_time) + middle_glyph + (make_dashes new_timing_width.num_cycles) + (make_dashes old_timing_width.num_cycles) + (make_dashes perc_timing_width.num_cycles) + middle_glyph + (make_dashes new_timing_width.num_instr) + (make_dashes old_timing_width.num_instr) + (make_dashes perc_timing_width.num_instr) + middle_glyph + (make_dashes new_timing_width.num_mem) + (make_dashes old_timing_width.num_mem) + (make_dashes perc_timing_width.num_mem) + middle_glyph + (make_dashes new_timing_width.num_faults) + (make_dashes old_timing_width.num_faults) + (make_dashes perc_timing_width.num_faults) + right_glyph + in + + let center_string string width = + let string_length = String.length string in + let width = max width string_length in + let left_hfill = (width - string_length) / 2 in + let right_hfill = width - left_hfill - string_length in + String.make left_hfill ' ' ^ string ^ String.make right_hfill ' ' + in + printf "\n"; + print_string (vertical_separator "┌" "┬" "┐"); + "│" ^ String.make (1 + package_name__width + 1) ' ' ^ "│" + ^ center_string "user time [s]" (1 + new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ^ "│" + ^ center_string "CPU cycles" (1 + new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) ^ "│" + ^ center_string "CPU instructions" (1 + new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ^ "│" + ^ center_string "max resident mem [KB]" (1 + new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ^ "│" + ^ center_string "mem faults" (1 + new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) + ^ "│\n" |> print_string; + printf "│%*s │ %*s│ %*s│ %*s│ %*s│ %*s│\n" + (1 + package_name__width) "" + (new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) "" + (new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) "" + (new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) "" + (new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) "" + (new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) ""; + printf "│ %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │\n" + package_name__width package_name__label + new_timing_width.user_time new__label + old_timing_width.user_time old__label + perc_timing_width.user_time proportional_difference__label + new_timing_width.num_cycles new__label + old_timing_width.num_cycles old__label + perc_timing_width.num_cycles proportional_difference__label + new_timing_width.num_instr new__label + old_timing_width.num_instr old__label + perc_timing_width.num_instr proportional_difference__label + new_timing_width.num_mem new__label + old_timing_width.num_mem old__label + perc_timing_width.num_mem proportional_difference__label + new_timing_width.num_faults new__label + old_timing_width.num_faults old__label + perc_timing_width.num_faults proportional_difference__label; + measurements |> List.iter + (fun (package_name, new_t, old_t, perc) -> + print_string (vertical_separator "├" "┼" "┤"); + printf "│ %*s │ %*.*f %*.*f %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │\n" + package_name__width package_name + new_timing_width.user_time precision new_t.user_time + old_timing_width.user_time precision old_t.user_time + perc_timing_width.user_time precision perc.user_time + new_timing_width.num_cycles new_t.num_cycles + old_timing_width.num_cycles old_t.num_cycles + perc_timing_width.num_cycles precision perc.num_cycles + new_timing_width.num_instr new_t.num_instr + old_timing_width.num_instr old_t.num_instr + perc_timing_width.num_instr precision perc.num_instr + new_timing_width.num_mem new_t.num_mem + old_timing_width.num_mem old_t.num_mem + perc_timing_width.num_mem precision perc.num_mem + new_timing_width.num_faults new_t.num_faults + old_timing_width.num_faults old_t.num_faults + perc_timing_width.num_faults precision perc.num_faults); + +print_string (vertical_separator "└" "┴" "┘"); + +(* ejgallego: disable this as it is very verbose and brings up little info in the log. *) +if false then begin +printf " + +PDIFF = proportional difference between measurements done for the NEW and the OLD Coq version + = (NEW_measurement - OLD_measurement) / OLD_measurement * 100%% + +NEW = %s +OLD = %s + +Columns: + + 1. user time [s] + + Total number of CPU-seconds that the process used directly (in user mode), in seconds. + (In other words, \"%%U\" quantity provided by the \"/usr/bin/time\" command.) + + 2. CPU cycles + + Total number of CPU-cycles that the process used directly (in user mode). + (In other words, \"cycles:u\" quantity provided by the \"/usr/bin/perf\" command.) + + 3. CPU instructions + + Total number of CPU-instructions that the process used directly (in user mode). + (In other words, \"instructions:u\" quantity provided by the \"/usr/bin/perf\" command.) + + 4. max resident mem [KB] + + Maximum resident set size of the process during its lifetime, in Kilobytes. + (In other words, \"%%M\" quantity provided by the \"/usr/bin/time\" command.) + + 5. mem faults + + Number of major, or I/O-requiring, page faults that occurred while the process was running. + These are faults where the page has actually migrated out of primary memory. + (In other words, \"%%F\" quantity provided by the \"/usr/bin/time\" command.) + +" new_coq_version old_coq_version; +end |