author | wenzelm |
Wed, 20 Feb 2013 15:22:22 +0100 | |
changeset 51228 | dff3471dd8bc |
parent 51217 | 65ab2c4f4c32 |
child 51606 | 2843cc095a57 |
permissions | -rw-r--r-- |
40393 | 1 |
(* Title: Pure/General/timing.ML |
31686 | 2 |
Author: Makarius |
3 |
||
40336 | 4 |
Basic support for time measurement. |
31686 | 5 |
*) |
6 |
||
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
7 |
signature BASIC_TIMING = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
8 |
sig |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
9 |
val cond_timeit: bool -> string -> (unit -> 'a) -> 'a |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
10 |
val timeit: (unit -> 'a) -> 'a |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
11 |
val timeap: ('a -> 'b) -> 'a -> 'b |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
12 |
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
13 |
end |
40300
d4487353b3a0
added convenience operation seconds: real -> time;
wenzelm
parents:
32935
diff
changeset
|
14 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
15 |
signature TIMING = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
16 |
sig |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
17 |
include BASIC_TIMING |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
18 |
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time} |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
19 |
type start |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
20 |
val start: unit -> start |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
21 |
val result: start -> timing |
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
22 |
val timing: ('a -> 'b) -> 'a -> timing * 'b |
51228 | 23 |
val is_relevant_time: Time.time -> bool |
44440 | 24 |
val is_relevant: timing -> bool |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
25 |
val message: timing -> string |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
26 |
end |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
27 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
28 |
structure Timing: TIMING = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
29 |
struct |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
30 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
31 |
(* type timing *) |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
32 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
33 |
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
34 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
35 |
|
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
36 |
(* timer control *) |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
37 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
38 |
abstype start = Start of |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
39 |
Timer.real_timer * Time.time * Timer.cpu_timer * |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
40 |
{gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}} |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
41 |
with |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
42 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
43 |
fun start () = |
31686 | 44 |
let |
45 |
val real_timer = Timer.startRealTimer (); |
|
46 |
val real_time = Timer.checkRealTimer real_timer; |
|
47 |
val cpu_timer = Timer.startCPUTimer (); |
|
48 |
val cpu_times = Timer.checkCPUTimes cpu_timer; |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
49 |
in Start (real_timer, real_time, cpu_timer, cpu_times) end; |
31686 | 50 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
51 |
fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) = |
31686 | 52 |
let |
53 |
val real_time2 = Timer.checkRealTimer real_timer; |
|
54 |
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; |
|
55 |
val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = |
|
56 |
Timer.checkCPUTimes cpu_timer; |
|
57 |
||
58 |
open Time; |
|
59 |
val elapsed = real_time2 - real_time; |
|
60 |
val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; |
|
61 |
val cpu = usr2 - usr + sys2 - sys + gc; |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
62 |
in {elapsed = elapsed, cpu = cpu, gc = gc} end; |
32935
2218b970325a
show direct GC time (which is included in CPU time);
wenzelm
parents:
31757
diff
changeset
|
63 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
64 |
end; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
65 |
|
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
66 |
fun timing f x = |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
67 |
let |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
68 |
val start = start (); |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
69 |
val y = f x; |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
70 |
in (result start, y) end; |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
71 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
72 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
73 |
(* timing messages *) |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
74 |
|
42819 | 75 |
val min_time = Time.fromMilliseconds 1; |
76 |
||
51228 | 77 |
fun is_relevant_time time = Time.>= (time, min_time); |
78 |
||
42819 | 79 |
fun is_relevant {elapsed, cpu, gc} = |
51228 | 80 |
is_relevant_time elapsed orelse |
81 |
is_relevant_time cpu orelse |
|
82 |
is_relevant_time gc; |
|
42819 | 83 |
|
44440 | 84 |
fun message {elapsed, cpu, gc} = |
85 |
Time.toString elapsed ^ "s elapsed time, " ^ |
|
86 |
Time.toString cpu ^ "s cpu time, " ^ |
|
87 |
Time.toString gc ^ "s GC time" handle Time.Time => ""; |
|
88 |
||
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
89 |
fun cond_timeit enabled msg e = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
90 |
if enabled then |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
91 |
let |
42042 | 92 |
val (timing, result) = timing (Exn.interruptible_capture e) (); |
42819 | 93 |
val _ = |
94 |
if is_relevant timing then |
|
95 |
let val end_msg = message timing |
|
96 |
in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end |
|
97 |
else (); |
|
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
98 |
in Exn.release result end |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
99 |
else e (); |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
100 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
101 |
fun timeit e = cond_timeit true "" e; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
102 |
fun timeap f x = timeit (fn () => f x); |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
103 |
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
104 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
105 |
end; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
106 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
107 |
structure Basic_Timing: BASIC_TIMING = Timing; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
108 |
open Basic_Timing; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
109 |