more explicit ML profiling, with official Isabelle output;
authorwenzelm
Mon Dec 21 15:09:35 2015 +0100 (2015-12-21)
changeset 61885acdfc76a6c33
parent 61884 d4c89ea5e6dc
child 61886 5a9a85c4cfb3
more explicit ML profiling, with official Isabelle output;
NEWS
src/Pure/General/output.ML
src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML
src/Pure/ML-Systems/ml_profiling_polyml.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/NEWS	Mon Dec 21 14:18:57 2015 +0100
     1.2 +++ b/NEWS	Mon Dec 21 15:09:35 2015 +0100
     1.3 @@ -669,6 +669,13 @@
     1.4  tools, but can also cause INCOMPATIBILITY for tools that don't observe
     1.5  the proof context discipline.
     1.6  
     1.7 +* The following combinators for low-level profiling of the ML runtime
     1.8 +system are available:
     1.9 +
    1.10 +  profile_time          (*CPU time*)
    1.11 +  profile_time_thread   (*CPU time on this thread*)
    1.12 +  profile_allocations   (*overall heap allocations*)
    1.13 +
    1.14  
    1.15  *** System ***
    1.16  
     2.1 --- a/src/Pure/General/output.ML	Mon Dec 21 14:18:57 2015 +0100
     2.2 +++ b/src/Pure/General/output.ML	Mon Dec 21 15:09:35 2015 +0100
     2.3 @@ -10,6 +10,9 @@
     2.4    val tracing: string -> unit
     2.5    val warning: string -> unit
     2.6    val legacy_feature: string -> unit
     2.7 +  val profile_time: ('a -> 'b) -> 'a -> 'b
     2.8 +  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
     2.9 +  val profile_allocations: ('a -> 'b) -> 'a -> 'b
    2.10  end;
    2.11  
    2.12  signature OUTPUT =
    2.13 @@ -131,6 +134,40 @@
    2.14  fun protocol_message props ss = ! protocol_message_fn props (map output ss);
    2.15  fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
    2.16  
    2.17 +
    2.18 +(* profiling *)
    2.19 +
    2.20 +local
    2.21 +
    2.22 +fun output_profile title entries =
    2.23 +  let
    2.24 +    val body = entries
    2.25 +      |> sort (int_ord o apply2 fst)
    2.26 +      |> map (fn (count, name) =>
    2.27 +          let
    2.28 +            val c = string_of_int count;
    2.29 +            val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
    2.30 +          in prefix ^ c ^ " " ^ name end);
    2.31 +    val total = fold (curry (op +) o fst) entries 0;
    2.32 +  in
    2.33 +    if total = 0 then ()
    2.34 +    else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
    2.35 +  end;
    2.36 +
    2.37 +in
    2.38 +
    2.39 +fun profile_time f x =
    2.40 +  ML_Profiling.profile_time (output_profile "time profile:") f x;
    2.41 +
    2.42 +fun profile_time_thread f x =
    2.43 +  ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
    2.44 +
    2.45 +fun profile_allocations f x =
    2.46 +  ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
    2.47 +
    2.48 +end;
    2.49 +
    2.50 +
    2.51  end;
    2.52  
    2.53  structure Basic_Output: BASIC_OUTPUT = Output;
     3.1 --- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 14:18:57 2015 +0100
     3.2 +++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 15:09:35 2015 +0100
     3.3 @@ -4,14 +4,16 @@
     3.4  Profiling for Poly/ML 5.6.
     3.5  *)
     3.6  
     3.7 -fun profile 0 f x = f x
     3.8 -  | profile n f x =
     3.9 -      let
    3.10 -        val mode =
    3.11 -          (case n of
    3.12 -            1 => PolyML.Profiling.ProfileTime
    3.13 -          | 2 => PolyML.Profiling.ProfileAllocations
    3.14 -          | 3 => PolyML.Profiling.ProfileLongIntEmulation
    3.15 -          | 6 => PolyML.Profiling.ProfileTimeThisThread
    3.16 -          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
    3.17 -      in PolyML.Profiling.profile mode f x end;
    3.18 +structure ML_Profiling =
    3.19 +struct
    3.20 +
    3.21 +fun profile_time pr f x =
    3.22 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
    3.23 +
    3.24 +fun profile_time_thread pr f x =
    3.25 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
    3.26 +
    3.27 +fun profile_allocations pr f x =
    3.28 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
    3.29 +
    3.30 +end;
     4.1 --- a/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 14:18:57 2015 +0100
     4.2 +++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 15:09:35 2015 +0100
     4.3 @@ -4,10 +4,24 @@
     4.4  Profiling for Poly/ML.
     4.5  *)
     4.6  
     4.7 -fun profile 0 f x = f x
     4.8 -  | profile n f x =
     4.9 -      let
    4.10 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
    4.11 -        val res = Exn.capture f x;
    4.12 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
    4.13 -      in Exn.release res end;
    4.14 +structure ML_Profiling =
    4.15 +struct
    4.16 +
    4.17 +local
    4.18 +
    4.19 +fun profile n f x =
    4.20 +  let
    4.21 +    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
    4.22 +    val res = Exn.capture f x;
    4.23 +    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
    4.24 +  in Exn.release res end;
    4.25 +
    4.26 +in
    4.27 +
    4.28 +fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
    4.29 +fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
    4.30 +fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
    4.31 +
    4.32 +end;
    4.33 +
    4.34 +end;
     5.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 14:18:57 2015 +0100
     5.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 15:09:35 2015 +0100
     5.3 @@ -74,7 +74,12 @@
     5.4    (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
     5.5  
     5.6  (*dummy implementation*)
     5.7 -fun profile (n: int) f x = f x;
     5.8 +structure ML_Profiling =
     5.9 +struct
    5.10 +  fun profile_time (_: (int * string) list -> unit) f x = f x;
    5.11 +  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
    5.12 +  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
    5.13 +end;
    5.14  
    5.15  (*dummy implementation*)
    5.16  fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();