author | haftmann |
Mon, 08 Feb 2010 17:12:22 +0100 | |
changeset 35045 | a77d200e6503 |
parent 32935 | 2218b970325a |
child 40300 | d4487353b3a0 |
permissions | -rw-r--r-- |
31686 | 1 |
(* Title: Pure/ML-Systems/timing.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Compiler-independent timing functions. |
|
5 |
*) |
|
6 |
||
7 |
fun start_timing () = |
|
8 |
let |
|
9 |
val real_timer = Timer.startRealTimer (); |
|
10 |
val real_time = Timer.checkRealTimer real_timer; |
|
11 |
val cpu_timer = Timer.startCPUTimer (); |
|
12 |
val cpu_times = Timer.checkCPUTimes cpu_timer; |
|
13 |
in (real_timer, real_time, cpu_timer, cpu_times) end; |
|
14 |
||
15 |
fun end_timing (real_timer, real_time, cpu_timer, cpu_times) = |
|
16 |
let |
|
17 |
val real_time2 = Timer.checkRealTimer real_timer; |
|
18 |
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; |
|
19 |
val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = |
|
20 |
Timer.checkCPUTimes cpu_timer; |
|
21 |
||
22 |
open Time; |
|
23 |
val elapsed = real_time2 - real_time; |
|
24 |
val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; |
|
25 |
val cpu = usr2 - usr + sys2 - sys + gc; |
|
32935
2218b970325a
show direct GC time (which is included in CPU time);
wenzelm
parents:
31757
diff
changeset
|
26 |
|
31686 | 27 |
val message = |
28 |
(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
|
29 |
toString gc ^ "s GC time") handle Time.Time => ""; |
31686 | 30 |
in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end; |
31 |