src/Pure/General/timing.ML
author wenzelm
Tue Apr 09 20:16:52 2013 +0200 (2013-04-09 ago)
changeset 51662 3391a493f39a
parent 51606 2843cc095a57
child 56333 38f1422ef473
permissions -rw-r--r--
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
     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     open Time;
    61     val elapsed = real_time2 - real_time;
    62     val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    63     val cpu = usr2 - usr + sys2 - sys + gc;
    64   in {elapsed = elapsed, cpu = cpu, gc = gc} end;
    65 
    66 end;
    67 
    68 fun timing f x =
    69   let
    70     val start = start ();
    71     val y = f x;
    72   in (result start, y) end;
    73 
    74 
    75 (* timing messages *)
    76 
    77 val min_time = Time.fromMilliseconds 1;
    78 
    79 fun is_relevant_time time = Time.>= (time, min_time);
    80 
    81 fun is_relevant {elapsed, cpu, gc} =
    82   is_relevant_time elapsed orelse
    83   is_relevant_time cpu orelse
    84   is_relevant_time gc;
    85 
    86 fun message {elapsed, cpu, gc} =
    87   Time.toString elapsed ^ "s elapsed time, " ^
    88   Time.toString cpu ^ "s cpu time, " ^
    89   Time.toString gc ^ "s GC time" handle Time.Time => "";
    90 
    91 fun cond_timeit enabled msg e =
    92   if enabled then
    93     let
    94       val (t, result) = timing (Exn.interruptible_capture e) ();
    95       val _ =
    96         if is_relevant t then
    97           let val end_msg = message t
    98           in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
    99         else ();
   100     in Exn.release result end
   101   else e ();
   102 
   103 fun timeit e = cond_timeit true "" e;
   104 fun timeap f x = timeit (fn () => f x);
   105 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
   106 
   107 fun protocol_message props t =
   108   Output.try_protocol_message (props @ Markup.timing_properties t) "";
   109 
   110 fun protocol props f x =
   111   let
   112     val (t, result) = timing (Exn.interruptible_capture f) x;
   113     val _ = protocol_message props t;
   114   in Exn.release result end;
   115 
   116 end;
   117 
   118 structure Basic_Timing: BASIC_TIMING = Timing;
   119 open Basic_Timing;
   120