author | wenzelm |
Wed, 03 Apr 2013 21:48:43 +0200 | |
changeset 51606 | 2843cc095a57 |
parent 51228 | dff3471dd8bc |
child 51662 | 3391a493f39a |
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 |
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
26 |
val status: ('a -> 'b) -> 'a -> 'b |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
27 |
end |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
28 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
29 |
structure Timing: TIMING = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
30 |
struct |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
31 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
32 |
(* type timing *) |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
33 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
34 |
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
|
35 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
36 |
|
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
37 |
(* timer control *) |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50781
diff
changeset
|
38 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
39 |
abstype start = Start of |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
40 |
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
|
41 |
{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
|
42 |
with |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
43 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
44 |
fun start () = |
31686 | 45 |
let |
46 |
val real_timer = Timer.startRealTimer (); |
|
47 |
val real_time = Timer.checkRealTimer real_timer; |
|
48 |
val cpu_timer = Timer.startCPUTimer (); |
|
49 |
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
|
50 |
in Start (real_timer, real_time, cpu_timer, cpu_times) end; |
31686 | 51 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
52 |
fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) = |
31686 | 53 |
let |
54 |
val real_time2 = Timer.checkRealTimer real_timer; |
|
55 |
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; |
|
56 |
val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = |
|
57 |
Timer.checkCPUTimes cpu_timer; |
|
58 |
||
59 |
open Time; |
|
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; |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
63 |
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
|
64 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
65 |
end; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
66 |
|
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
67 |
fun timing f x = |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
68 |
let |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
69 |
val start = start (); |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
70 |
val y = f x; |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
71 |
in (result start, y) end; |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
72 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
73 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
74 |
(* timing messages *) |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
75 |
|
42819 | 76 |
val min_time = Time.fromMilliseconds 1; |
77 |
||
51228 | 78 |
fun is_relevant_time time = Time.>= (time, min_time); |
79 |
||
42819 | 80 |
fun is_relevant {elapsed, cpu, gc} = |
51228 | 81 |
is_relevant_time elapsed orelse |
82 |
is_relevant_time cpu orelse |
|
83 |
is_relevant_time gc; |
|
42819 | 84 |
|
44440 | 85 |
fun message {elapsed, cpu, gc} = |
86 |
Time.toString elapsed ^ "s elapsed time, " ^ |
|
87 |
Time.toString cpu ^ "s cpu time, " ^ |
|
88 |
Time.toString gc ^ "s GC time" handle Time.Time => ""; |
|
89 |
||
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
90 |
fun cond_timeit enabled msg e = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
91 |
if enabled then |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
92 |
let |
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
93 |
val (t, result) = timing (Exn.interruptible_capture e) (); |
42819 | 94 |
val _ = |
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
95 |
if is_relevant t then |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
96 |
let val end_msg = message t |
42819 | 97 |
in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end |
98 |
else (); |
|
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
99 |
in Exn.release result end |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
100 |
else e (); |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
101 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
|
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
106 |
fun status f x = |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
107 |
let |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
108 |
val (t, result) = timing (Exn.interruptible_capture f) x; |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
109 |
val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else (); |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
110 |
in Exn.release result end; |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51228
diff
changeset
|
111 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
112 |
end; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
113 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
114 |
structure Basic_Timing: BASIC_TIMING = Timing; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
115 |
open Basic_Timing; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
116 |