1(*  Title:      Pure/General/timing.ML
2    Author:     Makarius
3
4Basic support for time measurement.
5*)
6
7signature BASIC_TIMING =
8sig
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
13end
14
15signature TIMING =
16sig
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: string -> Position.T -> timing -> unit
27  val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b
28end
29
30structure Timing: TIMING =
31struct
32
33(* type timing *)
34
35type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
36
37
38(* timer control *)
39
40abstype 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}}
43with
44
45fun 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
53fun 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
65end;
66
67fun 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
76val min_time = Time.fromMilliseconds 1;
77
78fun is_relevant_time time = time >= min_time;
79
80fun is_relevant {elapsed, cpu, gc} =
81  is_relevant_time elapsed orelse
82  is_relevant_time cpu orelse
83  is_relevant_time gc;
84
85fun 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
90fun 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
102fun timeit e = cond_timeit true "" e;
103fun timeap f x = timeit (fn () => f x);
104fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
105
106fun protocol_message name pos t =
107  if is_relevant t then
108    let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos
109    in Output.try_protocol_message (props @ Markup.timing_properties t) [] end
110  else ();
111
112fun protocol name pos f x =
113  let
114    val (t, result) = timing (Exn.interruptible_capture f) x;
115    val _ = protocol_message name pos t;
116  in Exn.release result end;
117
118end;
119
120structure Basic_Timing: BASIC_TIMING = Timing;
121open Basic_Timing;
122