author | wenzelm |
Mon, 13 Jul 2020 23:23:35 +0200 | |
changeset 72033 | 70bfda10f597 |
parent 72032 | a25c7c686176 |
child 72038 | 254c324f31fd |
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 |
|
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
9 |
val get: unit -> (string * string) list |
72032 | 10 |
val get_external: int -> (string * string) list |
11 |
val monitor: int -> real -> unit |
|
50255 | 12 |
end; |
13 |
||
14 |
structure ML_Statistics: ML_STATISTICS = |
|
15 |
struct |
|
16 |
||
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
17 |
(* print *) |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
18 |
|
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
19 |
fun print_int x = if x < 0 then "-" ^ Int.toString (~ x) else Int.toString x; |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
20 |
|
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
21 |
fun print_real0 x = |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
22 |
let val s = Real.fmt (StringCvt.GEN NONE) x in |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
23 |
(case String.fields (fn c => c = #".") s of |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
24 |
[a, b] => if List.all (fn c => c = #"0") (String.explode b) then a else s |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
25 |
| _ => s) |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
26 |
end; |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
27 |
|
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
28 |
fun print_real x = |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
29 |
if x < 0.0 then "-" ^ print_real0 (~ x) else print_real0 x; |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
30 |
|
72032 | 31 |
val print_properties = |
32 |
String.concatWith "," o map (fn (a, b) => a ^ "=" ^ b); |
|
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
33 |
|
72032 | 34 |
|
35 |
(* make properties *) |
|
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
36 |
|
72032 | 37 |
fun make_properties |
38 |
{gcFullGCs, |
|
39 |
gcPartialGCs, |
|
40 |
gcSharePasses, |
|
41 |
sizeAllocation, |
|
42 |
sizeAllocationFree, |
|
43 |
sizeCode, |
|
44 |
sizeHeap, |
|
45 |
sizeHeapFreeLastFullGC, |
|
46 |
sizeHeapFreeLastGC, |
|
47 |
sizeStacks, |
|
48 |
threadsInML, |
|
49 |
threadsTotal, |
|
50 |
threadsWaitCondVar, |
|
51 |
threadsWaitIO, |
|
52 |
threadsWaitMutex, |
|
53 |
threadsWaitSignal, |
|
54 |
timeGCReal, |
|
55 |
timeGCSystem, |
|
56 |
timeGCUser, |
|
57 |
timeNonGCReal, |
|
58 |
timeNonGCSystem, |
|
59 |
timeNonGCUser, |
|
60 |
userCounters} = |
|
50255 | 61 |
let |
50656 | 62 |
val user_counters = |
63 |
Vector.foldri |
|
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
64 |
(fn (i, j, res) => ("user_counter" ^ print_int i, print_int j) :: res) |
50656 | 65 |
[] userCounters; |
50255 | 66 |
in |
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
67 |
[("full_GCs", print_int gcFullGCs), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
68 |
("partial_GCs", print_int gcPartialGCs), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
69 |
("share_passes", print_int gcSharePasses), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
70 |
("size_allocation", print_int sizeAllocation), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
71 |
("size_allocation_free", print_int sizeAllocationFree), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
72 |
("size_code", print_int sizeCode), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
73 |
("size_heap", print_int sizeHeap), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
74 |
("size_heap_free_last_full_GC", print_int sizeHeapFreeLastFullGC), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
75 |
("size_heap_free_last_GC", print_int sizeHeapFreeLastGC), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
76 |
("size_stacks", print_int sizeStacks), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
77 |
("threads_in_ML", print_int threadsInML), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
78 |
("threads_total", print_int threadsTotal), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
79 |
("threads_wait_condvar", print_int threadsWaitCondVar), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
80 |
("threads_wait_IO", print_int threadsWaitIO), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
81 |
("threads_wait_mutex", print_int threadsWaitMutex), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
82 |
("threads_wait_signal", print_int threadsWaitSignal), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
83 |
("time_elapsed", print_real (Time.toReal timeNonGCReal)), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
84 |
("time_elapsed_GC", print_real (Time.toReal timeGCReal)), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
85 |
("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)), |
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset
|
86 |
("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @ |
50656 | 87 |
user_counters |
50255 | 88 |
end; |
89 |
||
72032 | 90 |
|
91 |
(* get properties *) |
|
92 |
||
93 |
fun get () = |
|
94 |
make_properties (PolyML.Statistics.getLocalStats ()); |
|
95 |
||
96 |
fun get_external pid = |
|
97 |
make_properties (PolyML.Statistics.getRemoteStats pid); |
|
98 |
||
99 |
||
100 |
(* monitor process *) |
|
101 |
||
102 |
fun monitor pid delay = |
|
103 |
let |
|
104 |
fun loop () = |
|
105 |
(TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n"); |
|
106 |
TextIO.flushOut TextIO.stdOut; |
|
107 |
OS.Process.sleep (Time.fromReal delay); |
|
108 |
loop ()); |
|
72033 | 109 |
in loop () handle Interrupt => OS.Process.exit OS.Process.success end; |
72032 | 110 |
|
50255 | 111 |
end; |