author | wenzelm |
Wed, 09 Jan 2013 13:38:57 +0100 | |
changeset 50781 | a0f22c2d60cc |
parent 50777 | 20126dd9772c |
child 51217 | 65ab2c4f4c32 |
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 |
44440 | 23 |
val is_relevant: timing -> bool |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
24 |
val message: timing -> string |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
25 |
end |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
26 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
27 |
structure Timing: TIMING = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
28 |
struct |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
29 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
30 |
(* timer control *) |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
31 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
32 |
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
|
33 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
34 |
abstype start = Start of |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
35 |
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
|
36 |
{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
|
37 |
with |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
38 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
39 |
fun start () = |
31686 | 40 |
let |
41 |
val real_timer = Timer.startRealTimer (); |
|
42 |
val real_time = Timer.checkRealTimer real_timer; |
|
43 |
val cpu_timer = Timer.startCPUTimer (); |
|
44 |
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
|
45 |
in Start (real_timer, real_time, cpu_timer, cpu_times) end; |
31686 | 46 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
47 |
fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) = |
31686 | 48 |
let |
49 |
val real_time2 = Timer.checkRealTimer real_timer; |
|
50 |
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; |
|
51 |
val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = |
|
52 |
Timer.checkCPUTimes cpu_timer; |
|
53 |
||
54 |
open Time; |
|
55 |
val elapsed = real_time2 - real_time; |
|
56 |
val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; |
|
57 |
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
|
58 |
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
|
59 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
60 |
end; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
61 |
|
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
62 |
fun timing f x = |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
63 |
let |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
64 |
val start = start (); |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
65 |
val y = f x; |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
66 |
in (result start, y) end; |
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
67 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
68 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
69 |
(* timing messages *) |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
70 |
|
42819 | 71 |
val min_time = Time.fromMilliseconds 1; |
72 |
||
73 |
fun is_relevant {elapsed, cpu, gc} = |
|
74 |
Time.>= (elapsed, min_time) orelse |
|
75 |
Time.>= (cpu, min_time) orelse |
|
76 |
Time.>= (gc, min_time); |
|
77 |
||
44440 | 78 |
fun message {elapsed, cpu, gc} = |
79 |
Time.toString elapsed ^ "s elapsed time, " ^ |
|
80 |
Time.toString cpu ^ "s cpu time, " ^ |
|
81 |
Time.toString gc ^ "s GC time" handle Time.Time => ""; |
|
82 |
||
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
83 |
fun cond_timeit enabled msg e = |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
84 |
if enabled then |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
85 |
let |
42042 | 86 |
val (timing, result) = timing (Exn.interruptible_capture e) (); |
42819 | 87 |
val _ = |
88 |
if is_relevant timing then |
|
89 |
let val end_msg = message timing |
|
90 |
in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end |
|
91 |
else (); |
|
42013
1694cc477045
pure Timing.timing, without any exception handling;
wenzelm
parents:
42012
diff
changeset
|
92 |
in Exn.release result end |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
93 |
else e (); |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
94 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
95 |
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
|
96 |
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
|
97 |
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
|
98 |
|
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
99 |
end; |
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 |
structure Basic_Timing: BASIC_TIMING = Timing; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
102 |
open Basic_Timing; |
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
40393
diff
changeset
|
103 |