author | wenzelm |
Thu, 04 Nov 2010 10:22:59 +0100 | |
changeset 40336 | 755862729f8d |
parent 40300 | d4487353b3a0 |
child 40391 | b0dafbfc05b7 |
permissions | -rw-r--r-- |
31686 | 1 |
(* Title: Pure/ML-Systems/timing.ML |
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 |
||
17 |
fun end_timing (real_timer, real_time, cpu_timer, cpu_times) = |
|
18 |
let |
|
19 |
val real_time2 = Timer.checkRealTimer real_timer; |
|
20 |
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; |
|
21 |
val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = |
|
22 |
Timer.checkCPUTimes cpu_timer; |
|
23 |
||
24 |
open Time; |
|
25 |
val elapsed = real_time2 - real_time; |
|
26 |
val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; |
|
27 |
val cpu = usr2 - usr + sys2 - sys + gc; |
|
32935
2218b970325a
show direct GC time (which is included in CPU time);
wenzelm
parents:
31757
diff
changeset
|
28 |
|
31686 | 29 |
val message = |
30 |
(toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^ |
|
32935
2218b970325a
show direct GC time (which is included in CPU time);
wenzelm
parents:
31757
diff
changeset
|
31 |
toString gc ^ "s GC time") handle Time.Time => ""; |
31686 | 32 |
in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end; |
33 |