diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 16 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 32 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 2 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 104 | ||||
| -rw-r--r-- | pretyping/nativenorm.mli | 7 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 16 |
8 files changed, 169 insertions, 14 deletions
@@ -63,6 +63,10 @@ Tactics Ltac definition or a Tactic Notation. - New option `Set Ltac Batch Debug` on top of `Set Ltac Debug` for non-interactive Ltac debug output. +- On Linux, "native_compute" calls can be profiled using the "perf" + utility. The command "Set NativeCompute Profiling" enables + profiling, and "Set NativeCompute Profile Filename" customizes + the profile filename. Gallina diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b3b0df5c8..6e2735700 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3269,7 +3269,7 @@ The call-by-value strategy is the one used in ML languages: the arguments of a function call are systematically weakly evaluated first. Despite the lazy strategy always performs fewer reductions than the call-by-value strategy, the latter is generally more efficient for -evaluating purely computational expressions (i.e. with few dead code). +evaluating purely computational expressions (i.e. with little dead code). \begin{Variants} \item {\tt compute} \tacindex{compute}\\ @@ -3317,6 +3317,20 @@ evaluating purely computational expressions (i.e. with few dead code). compilation cost is higher, so it is worth using only for intensive computations. + On Linux, if you have the {\tt perf} profiler installed, you can profile {\tt native\_compute} evaluations. + The command + \begin{quote} + {\tt Set Native Compute Profiling} + \end{quote} + enables profiling. Use the command + \begin{quote} + {\tt Set NativeCompute Profile Filename \str} + \end{quote} + to specify the profile output; the default is {\tt native\_compute\_profile.data}. The actual filename used + will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means + you can individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on + the profile file to see the results. Consult the {\tt perf} documentation for more details. + \end{Variants} % Obsolete? Anyway not very important message diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d2f050d3b..a62a079da 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -132,7 +132,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code penv sigma prefix t1 t2 in - match compile ml_filename code with + match compile ml_filename code ~profile:false with | (true, fn) -> begin if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 02e02b031..665ddf7a6 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -64,7 +64,7 @@ let warn_native_compiler_failed = in CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print -let call_compiler ml_filename = +let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in @@ -74,14 +74,26 @@ let call_compiler ml_filename = let remove f = if Sys.file_exists f then Sys.remove f in remove link_filename; remove (f ^ ".cmi"); + let initial_args = + if Dynlink.is_native then + ["opt"; "-shared"] + else + ["ocamlc"; "-c"] + in + let profile_args = + if profile then + ["-g"] + else + [] + in let args = - (if Dynlink.is_native then "opt" else "ocamlc") - ::(if Dynlink.is_native then "-shared" else "-c") - ::"-o"::link_filename - ::"-rectypes" - ::"-w"::"a" - ::include_dirs - @ ["-impl"; ml_filename] in + initial_args @ + profile_args @ + ("-o"::link_filename + ::"-rectypes" + ::"-w"::"a" + ::include_dirs) @ + ["-impl"; ml_filename] in if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (ocamlfind ()) args in @@ -95,9 +107,9 @@ let call_compiler ml_filename = warn_native_compiler_failed (Inr e); false, link_filename -let compile fn code = +let compile fn code ~profile:profile = write_ml_code fn code; - let r = call_compiler fn in + let r = call_compiler ~profile fn in if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; r diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index e8b51dc36..a262a9f58 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -19,7 +19,7 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> bool * string +val compile : string -> global list -> profile:bool -> bool * string val compile_library : Names.dir_path -> global list -> string -> bool diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 5142af356..39c2ceeba 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -26,6 +26,59 @@ module RelDecl = Context.Rel.Declaration exception Find_at of int +(* profiling *) + +let profiling_enabled = ref false + +(* for supported platforms, filename for profiler results *) + +let profile_filename = ref "native_compute_profile.data" + +let profiler_platform () = + match [@warning "-8"] Sys.os_type with + | "Unix" -> + let in_ch = Unix.open_process_in "uname" in + let uname = input_line in_ch in + let _ = close_in in_ch in + Format.sprintf "Unix (%s)" uname + | "Win32" -> "Windows (Win32)" + | "Cygwin" -> "Windows (Cygwin)" + +let get_profile_filename () = !profile_filename + +let set_profile_filename fn = + profile_filename := fn + +(* find unused profile filename *) +let get_available_profile_filename () = + let profile_filename = get_profile_filename () in + let dir = Filename.dirname profile_filename in + let base = Filename.basename profile_filename in + (* starting with OCaml 4.04, could use Filename.remove_extension and Filename.extension, which + gets rid of need for exception-handling here + *) + let (name,ext) = + try + let nm = Filename.chop_extension base in + let nm_len = String.length nm in + let ex = String.sub base nm_len (String.length base - nm_len) in + (nm,ex) + with Invalid_argument _ -> (base,"") + in + try + (* unlikely race: fn deleted, another process uses fn *) + Filename.temp_file ~temp_dir:dir (name ^ "_") ext + with Sys_error s -> + let msg = "When trying to find native_compute profile output file: " ^ s in + let _ = Feedback.msg_info (Pp.str msg) in + assert false + +let get_profiling_enabled () = + !profiling_enabled + +let set_profiling_enabled b = + profiling_enabled := b + let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do @@ -379,6 +432,52 @@ let evars_of_evar_map sigma = Nativelambda.evars_typ = Evd.existential_type sigma; Nativelambda.evars_metas = Evd.meta_type sigma } +(* fork perf process, return profiler's process id *) +let start_profiler_linux profile_fn = + let coq_pid = Unix.getpid () in (* pass pid of running coqtop *) + (* we don't want to see perf's console output *) + let dev_null = Unix.descr_of_out_channel (open_out_bin "/dev/null") in + let _ = Feedback.msg_info (Pp.str ("Profiling to file " ^ profile_fn)) in + let perf = "perf" in + let profiler_pid = + Unix.create_process + perf + [|perf; "record"; "-g"; "-o"; profile_fn; "-p"; string_of_int coq_pid |] + Unix.stdin dev_null dev_null + in + (* doesn't seem to be a way to test whether process creation succeeded *) + if !Flags.debug then + Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn)); + Some profiler_pid + +(* kill profiler via SIGINT *) +let stop_profiler_linux m_pid = + match m_pid with + | Some pid -> ( + let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in + try + Unix.kill pid Sys.sigint; + let _ = Unix.waitpid [] pid in () + with Unix.Unix_error (Unix.ESRCH,"kill","") -> + Feedback.msg_info (Pp.str "Could not stop native code profiler, no such process") + ) + | None -> () + +let start_profiler () = + let profile_fn = get_available_profile_filename () in + match profiler_platform () with + "Unix (Linux)" -> start_profiler_linux profile_fn + | _ -> + let _ = Feedback.msg_info + (Pp.str (Format.sprintf "Native_compute profiling not supported on the platform: %s" + (profiler_platform ()))) in + None + +let stop_profiler m_pid = + match profiler_platform() with + "Unix (Linux)" -> stop_profiler_linux m_pid + | _ -> () + let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in @@ -392,12 +491,15 @@ let native_norm env sigma c ty = *) let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in - match Nativelib.compile ml_filename code with + let profile = get_profiling_enabled () in + match Nativelib.compile ml_filename code ~profile:profile with | true, fn -> if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); + let profiler_pid = if profile then start_profiler () else None in let t0 = Sys.time () in Nativelib.call_linker ~fatal:true prefix fn (Some upd); let t1 = Sys.time () in + if profile then stop_profiler profiler_pid; let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); let res = nf_val env sigma !Nativelib.rt1 ty in diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 4e7f2110d..579a7d2ac 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -12,6 +12,13 @@ open Evd (** This module implements normalization by evaluation to OCaml code *) +val get_profile_filename : unit -> string +val set_profile_filename : string -> unit + +val get_profiling_enabled : unit -> bool +val set_profiling_enabled : bool -> unit + + val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f63ed6f4..8738e58e8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1457,6 +1457,22 @@ let _ = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } +let _ = + declare_string_option + { optdepr = false; + optname = "native_compute profiler output"; + optkey = ["NativeCompute"; "Profile"; "Filename"]; + optread = Nativenorm.get_profile_filename; + optwrite = Nativenorm.set_profile_filename } + +let _ = + declare_bool_option + { optdepr = false; + optname = "enable native compute profiling"; + optkey = ["NativeCompute"; "Profiling"]; + optread = Nativenorm.get_profiling_enabled; + optwrite = Nativenorm.set_profiling_enabled } + let vernac_set_strategy locality l = let local = make_locality locality in let glob_ref r = |