From f6a4599b852a32351163eb272d14718e32b58cec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Jul 2017 13:12:03 +0200
Subject: A less intrusive Profile.close_profile.

No need to call Gc functions nor Unix timing functions when there is
nothing to report.

Moreover, PMP observed problems with these functions in the
debugger. PMP also reported that Gc.minor takes some noticeable time,
so no need to trigger some when unneeded.
---
 lib/profile.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index b669161858..78bf35621a 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -317,15 +317,15 @@ let adjust_time ov_bc ov_ad e =
      owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
 
 let close_profile print =
-  let dw = spent_alloc () in
-  let t = get_time () in
-  match !stack with
-    | [outside] ->
-	outside.tottime <- outside.tottime + t;
-	outside.owntime <- outside.owntime + t;
-	ajoute_ownalloc outside dw;
-	ajoute_totalloc outside dw;
-	if !prof_table <> [] then begin
+  if !prof_table <> [] then begin
+      let dw = spent_alloc () in
+      let t = get_time () in
+      match !stack with
+      | [outside] ->
+	  outside.tottime <- outside.tottime + t;
+	  outside.owntime <- outside.owntime + t;
+	  ajoute_ownalloc outside dw;
+	  ajoute_totalloc outside dw;
 	  let ov_bc = time_overhead_B_C () (* B+C overhead *) in
 	  let ov_ad = time_overhead_A_D () (* A+D overhead *) in
 	  let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
@@ -346,8 +346,8 @@ let close_profile print =
 	  in
 	  if print then format_profile updated_data;
 	  init_profile ()
-	end
-    | _ -> failwith "Inconsistency"
+      | _ -> failwith "Inconsistency"
+    end
 
 let print_profile () = close_profile true
 
-- 
cgit v1.2.3


From c3ca30ca418ed0eca804d09fe6f1ff9d3ff0aa32 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Jul 2017 15:16:05 +0200
Subject: Also a less intrusive Profile.init_profile.

Calling it only when there is something to profile, or when profiling
is explicitly required with the profile flags, so that profiling in
plugins is possible.
---
 lib/profile.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index 78bf35621a..0bc226a450 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -85,6 +85,9 @@ let init_alloc = ref 0.0
 let reset_profile () = List.iter reset_record !prof_table
 
 let init_profile () =
+  (* We test Flags.profile as a way to support declaring profiled
+     functions in plugins *)
+  if !prof_table <> [] || Flags.profile then begin
   let outside = create_record () in
   stack := [outside];
   last_alloc := get_alloc ();
@@ -92,6 +95,7 @@ let init_profile () =
   init_time := get_time ();
   outside.tottime <- - !init_time;
   outside.owntime <- - !init_time
+  end
 
 let ajoute n o =
   o.owntime <- o.owntime + n.owntime;
@@ -358,9 +362,6 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialization, may be overridden *)
-let _ = init_profile ()
-
 (******************************)
 (* Entry points for profiling *)
 let profile1 e f a =
-- 
cgit v1.2.3