Add native compute profiling, BZ#5170

7 files changed, 168 insertions, 14 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b3b0df5c8..ba9b21bfd 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}. If there's an existing file with
+  the specified name, \Coq{} will append a number to it to avoid name collisions. 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..de0afd5e3 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -26,6 +26,62 @@ 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
+
+(* counter so we don't overwrite existing profiles *)
+let profile_filename_counter = ref 0
+(* flag to guard against (unlikely) counter wraparound *)
+let profile_saw_zero_counter = ref false
+  
+(* find unused profile filename *)
+let get_available_profile_filename () =
+  let basename = get_profile_filename () in
+  let rec find_name () =
+    let ct = !profile_filename_counter in
+    let _ = assert (not (ct = 0 && !profile_saw_zero_counter)) in
+    let possible_name =
+      if ct = 0 then (
+	profile_saw_zero_counter := true;
+	basename )
+      else basename ^ "." ^ (string_of_int ct) in
+    if Sys.file_exists possible_name
+    then (
+      incr profile_filename_counter;
+      find_name ()
+    )
+    else possible_name
+  in
+  let name = find_name () in
+  incr profile_filename_counter;
+  name
+	
+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 +435,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 () =
+  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 profile_fn = get_available_profile_filename () 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"; "-p"; string_of_int coq_pid; "-o"; profile_fn|]
+      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 () =
+  match profiler_platform () with
+    "Unix (Linux)" -> start_profiler_linux ()
+  | _ ->
+     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 +494,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 =