author | wenzelm |
Sat, 06 Nov 2010 17:55:32 +0100 | |
changeset 40393 | 2bb7ec08574a |
parent 40391 | src/Pure/ML-Systems/timing.ML@b0dafbfc05b7 |
child 42012 | 2c3fe3cbebae |
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 |
||
40336 | 7 |
val seconds = Time.fromReal; |
40300
d4487353b3a0
added convenience operation seconds: real -> time;
wenzelm
parents:
32935
diff
changeset
|
8 |
|
31686 | 9 |
fun start_timing () = |
10 |
let |
|
11 |
val real_timer = Timer.startRealTimer (); |
|
12 |
val real_time = Timer.checkRealTimer real_timer; |
|
13 |
val cpu_timer = Timer.startCPUTimer (); |
|
14 |
val cpu_times = Timer.checkCPUTimes cpu_timer; |
|
15 |
in (real_timer, real_time, cpu_timer, cpu_times) end; |
|
16 |
||
40391
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40336
diff
changeset
|
17 |
type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time}; |
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40336
diff
changeset
|
18 |
|
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40336
diff
changeset
|
19 |
fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing = |
31686 | 20 |
let |
21 |
val real_time2 = Timer.checkRealTimer real_timer; |
|
22 |
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; |
|
23 |
val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = |
|
24 |
Timer.checkCPUTimes cpu_timer; |
|
25 |
||
26 |
open Time; |
|
27 |
val elapsed = real_time2 - real_time; |
|
28 |
val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; |
|
29 |
val cpu = usr2 - usr + sys2 - sys + gc; |
|
32935
2218b970325a
show direct GC time (which is included in CPU time);
wenzelm
parents:
31757
diff
changeset
|
30 |
|
31686 | 31 |
val message = |
40393 | 32 |
(toString elapsed ^ "s elapsed time, " ^ |
33 |
toString cpu ^ "s cpu time, " ^ |
|
34 |
toString gc ^ "s GC time") handle Time.Time => ""; |
|
31686 | 35 |
in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end; |
36 |