author | nipkow |
Tue, 05 Nov 2019 14:57:41 +0100 | |
changeset 71033 | c1b63124245c |
parent 69822 | 8c587dd44f51 |
child 72031 | b7cec26e41d1 |
permissions | -rw-r--r-- |
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, |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
20 |
gcSharePasses, |
50255 | 21 |
sizeAllocation, |
22 |
sizeAllocationFree, |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
23 |
sizeCode, |
50255 | 24 |
sizeHeap, |
25 |
sizeHeapFreeLastFullGC, |
|
26 |
sizeHeapFreeLastGC, |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
27 |
sizeStacks, |
50255 | 28 |
threadsInML, |
29 |
threadsTotal, |
|
30 |
threadsWaitCondVar, |
|
31 |
threadsWaitIO, |
|
32 |
threadsWaitMutex, |
|
33 |
threadsWaitSignal, |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
34 |
timeGCReal, |
50255 | 35 |
timeGCSystem, |
36 |
timeGCUser, |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
37 |
timeNonGCReal, |
50255 | 38 |
timeNonGCSystem, |
39 |
timeNonGCUser, |
|
50656 | 40 |
userCounters} = PolyML.Statistics.getLocalStats (); |
41 |
val user_counters = |
|
42 |
Vector.foldri |
|
63806 | 43 |
(fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res) |
50656 | 44 |
[] userCounters; |
50255 | 45 |
in |
63806 | 46 |
[("full_GCs", Value.print_int gcFullGCs), |
47 |
("partial_GCs", Value.print_int gcPartialGCs), |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
48 |
("share_passes", Value.print_int gcSharePasses), |
63806 | 49 |
("size_allocation", Value.print_int sizeAllocation), |
50 |
("size_allocation_free", Value.print_int sizeAllocationFree), |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
51 |
("size_code", Value.print_int sizeCode), |
63806 | 52 |
("size_heap", Value.print_int sizeHeap), |
53 |
("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC), |
|
54 |
("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC), |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
55 |
("size_stacks", Value.print_int sizeStacks), |
63806 | 56 |
("threads_in_ML", Value.print_int threadsInML), |
57 |
("threads_total", Value.print_int threadsTotal), |
|
58 |
("threads_wait_condvar", Value.print_int threadsWaitCondVar), |
|
59 |
("threads_wait_IO", Value.print_int threadsWaitIO), |
|
60 |
("threads_wait_mutex", Value.print_int threadsWaitMutex), |
|
61 |
("threads_wait_signal", Value.print_int threadsWaitSignal), |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
62 |
("time_elapsed", Value.print_real (Time.toReal timeNonGCReal)), |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
63806
diff
changeset
|
63 |
("time_elapsed_GC", Value.print_real (Time.toReal timeGCReal)), |
63806 | 64 |
("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)), |
65 |
("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @ |
|
50656 | 66 |
user_counters |
50255 | 67 |
end; |
68 |
||
69 |
end; |