62459
|
1 |
(* Title: Pure/ML/ml_statistics.ML
|
50255
|
2 |
Author: Makarius
|
|
3 |
|
62945
|
4 |
ML runtime statistics.
|
50255
|
5 |
*)
|
|
6 |
|
|
7 |
signature ML_STATISTICS =
|
|
8 |
sig
|
|
9 |
val get: unit -> Properties.T
|
|
10 |
end;
|
|
11 |
|
|
12 |
structure ML_Statistics: ML_STATISTICS =
|
|
13 |
struct
|
|
14 |
|
|
15 |
fun get () =
|
|
16 |
let
|
|
17 |
val
|
|
18 |
{gcFullGCs,
|
|
19 |
gcPartialGCs,
|
|
20 |
sizeAllocation,
|
|
21 |
sizeAllocationFree,
|
|
22 |
sizeHeap,
|
|
23 |
sizeHeapFreeLastFullGC,
|
|
24 |
sizeHeapFreeLastGC,
|
|
25 |
threadsInML,
|
|
26 |
threadsTotal,
|
|
27 |
threadsWaitCondVar,
|
|
28 |
threadsWaitIO,
|
|
29 |
threadsWaitMutex,
|
|
30 |
threadsWaitSignal,
|
|
31 |
timeGCSystem,
|
|
32 |
timeGCUser,
|
|
33 |
timeNonGCSystem,
|
|
34 |
timeNonGCUser,
|
50656
|
35 |
userCounters} = PolyML.Statistics.getLocalStats ();
|
|
36 |
val user_counters =
|
|
37 |
Vector.foldri
|
63806
|
38 |
(fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
|
50656
|
39 |
[] userCounters;
|
50255
|
40 |
in
|
63806
|
41 |
[("full_GCs", Value.print_int gcFullGCs),
|
|
42 |
("partial_GCs", Value.print_int gcPartialGCs),
|
|
43 |
("size_allocation", Value.print_int sizeAllocation),
|
|
44 |
("size_allocation_free", Value.print_int sizeAllocationFree),
|
|
45 |
("size_heap", Value.print_int sizeHeap),
|
|
46 |
("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
|
|
47 |
("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
|
|
48 |
("threads_in_ML", Value.print_int threadsInML),
|
|
49 |
("threads_total", Value.print_int threadsTotal),
|
|
50 |
("threads_wait_condvar", Value.print_int threadsWaitCondVar),
|
|
51 |
("threads_wait_IO", Value.print_int threadsWaitIO),
|
|
52 |
("threads_wait_mutex", Value.print_int threadsWaitMutex),
|
|
53 |
("threads_wait_signal", Value.print_int threadsWaitSignal),
|
|
54 |
("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
|
|
55 |
("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
|
50656
|
56 |
user_counters
|
50255
|
57 |
end;
|
|
58 |
|
|
59 |
end;
|