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