From 51d4d83316f91abb25ea331bfdc1dcba17362dc8 Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Tue, 15 Aug 2017 10:31:09 -0400
Subject: Add native compute profiling, BZ#5170

---
 pretyping/nativenorm.ml | 107 +++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 106 insertions(+), 1 deletion(-)

(limited to 'pretyping/nativenorm.ml')

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
-- 
cgit v1.2.3