author | wenzelm |
Sun, 20 Jun 2004 09:28:35 +0200 | |
changeset 14979 | 245955f0c579 |
parent 14519 | 4ca3608fdf4f |
permissions | -rw-r--r-- |
14519
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/cpu-timer-gc.ML |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
2 |
ID: $Id$ |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
4 |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
5 |
Implementation of timing functions, building on implementations where |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
6 |
the return type of Timer.checkCPUTimer includes a gc field. |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
7 |
*) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
8 |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
9 |
(*Note start point for timing*) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
10 |
fun startTiming() = |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
11 |
let val CPUtimer = Timer.startCPUTimer(); |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
12 |
val time = Timer.checkCPUTimer(CPUtimer) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
13 |
in (CPUtimer,time) end; |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
14 |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
15 |
(*Finish timing and return string*) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
16 |
fun endTiming (CPUtimer, {gc,sys,usr}) = |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
17 |
let open Time (*...for Time.toString, Time.+ and Time.- *) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
18 |
val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
19 |
in "User " ^ toString (usr2-usr) ^ |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
20 |
" GC " ^ toString (gc2-gc) ^ |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
21 |
" All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^ |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
22 |
" secs" |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
23 |
handle Time => "" |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
24 |
end; |
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
25 |
|
14979 | 26 |
fun checkTimer timer = |
27 |
let val {sys, usr, gc} = Timer.checkCPUTimer timer |
|
28 |
in (sys, usr, gc) end; |