src/Pure/General/timing.ML
author wenzelm
Sat Nov 04 12:39:25 2017 +0100 (12 months ago)
changeset 67001 b34fbf33a7ea
parent 67000 1698e9ccef2d
child 67932 04352338f7f3
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/General/timing.ML
     2     Author:     Makarius
     3 
     4 Basic support for time measurement.
     5 *)
     6 
     7 signature BASIC_TIMING =
     8 sig
     9   val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
    10   val timeit: (unit -> 'a) -> 'a
    11   val timeap: ('a -> 'b) -> 'a -> 'b
    12   val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    13 end
    14 
    15 signature TIMING =
    16 sig
    17   include BASIC_TIMING
    18   type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
    19   type start
    20   val start: unit -> start
    21   val result: start -> timing
    22   val timing: ('a -> 'b) -> 'a -> timing * 'b
    23   val is_relevant_time: Time.time -> bool
    24   val is_relevant: timing -> bool
    25   val message: timing -> string
    26   val protocol_message: Properties.T -> timing -> unit
    27   val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b
    28 end
    29 
    30 structure Timing: TIMING =
    31 struct
    32 
    33 (* type timing *)
    34 
    35 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
    36 
    37 
    38 (* timer control *)
    39 
    40 abstype start = Start of
    41   Timer.real_timer * Time.time * Timer.cpu_timer *
    42     {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
    43 with
    44 
    45 fun start () =
    46   let
    47     val real_timer = Timer.startRealTimer ();
    48     val real_time = Timer.checkRealTimer real_timer;
    49     val cpu_timer = Timer.startCPUTimer ();
    50     val cpu_times = Timer.checkCPUTimes cpu_timer;
    51   in Start (real_timer, real_time, cpu_timer, cpu_times) end;
    52 
    53 fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
    54   let
    55     val real_time2 = Timer.checkRealTimer real_timer;
    56     val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    57     val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
    58       Timer.checkCPUTimes cpu_timer;
    59 
    60     val elapsed = real_time2 - real_time;
    61     val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    62     val cpu = usr2 - usr + sys2 - sys + gc;
    63   in {elapsed = elapsed, cpu = cpu, gc = gc} end;
    64 
    65 end;
    66 
    67 fun timing f x =
    68   let
    69     val start = start ();
    70     val y = f x;
    71   in (result start, y) end;
    72 
    73 
    74 (* timing messages *)
    75 
    76 val min_time = Time.fromMilliseconds 1;
    77 
    78 fun is_relevant_time time = time >= min_time;
    79 
    80 fun is_relevant {elapsed, cpu, gc} =
    81   is_relevant_time elapsed orelse
    82   is_relevant_time cpu orelse
    83   is_relevant_time gc;
    84 
    85 fun message {elapsed, cpu, gc} =
    86   Value.print_time elapsed ^ "s elapsed time, " ^
    87   Value.print_time cpu ^ "s cpu time, " ^
    88   Value.print_time gc ^ "s GC time" handle Time.Time => "";
    89 
    90 fun cond_timeit enabled msg e =
    91   if enabled then
    92     let
    93       val (t, result) = timing (Exn.interruptible_capture e) ();
    94       val _ =
    95         if is_relevant t then
    96           let val end_msg = message t
    97           in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
    98         else ();
    99     in Exn.release result end
   100   else e ();
   101 
   102 fun timeit e = cond_timeit true "" e;
   103 fun timeap f x = timeit (fn () => f x);
   104 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
   105 
   106 fun protocol_message props t =
   107   if is_relevant t then
   108     Output.try_protocol_message (props @ Markup.timing_properties t) []
   109   else ();
   110 
   111 fun protocol props f x =
   112   let
   113     val (t, result) = timing (Exn.interruptible_capture f) x;
   114     val _ = protocol_message props t;
   115   in Exn.release result end;
   116 
   117 end;
   118 
   119 structure Basic_Timing: BASIC_TIMING = Timing;
   120 open Basic_Timing;