author  wenzelm 
Fri, 07 Aug 2020 15:13:50 +0200  
changeset 72111  b9ded33bd58c 
parent 72041  7b112eedc859 
child 72113  2d9e40cfe9af 
permissions  rwrr 
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 

72038
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

9 
val set: {tasks_ready: int, tasks_pending: int, tasks_running: int, tasks_passive: int, 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

10 
tasks_urgent: int, workers_total: int, workers_active: int, workers_waiting: int} > unit 
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

11 
val get: unit > (string * string) list 
72032  12 
val get_external: int > (string * string) list 
13 
val monitor: int > real > unit 

50255  14 
end; 
15 

16 
structure ML_Statistics: ML_STATISTICS = 

17 
struct 

18 

72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

19 
(* print *) 
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_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

22 

b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

23 
fun print_real0 x = 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

24 
let val s = Real.fmt (StringCvt.GEN NONE) x in 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

25 
(case String.fields (fn c => c = #".") s of 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

26 
[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

27 
 _ => s) 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

28 
end; 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

29 

b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

30 
fun print_real x = 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

31 
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

32 

72032  33 
val print_properties = 
34 
String.concatWith "," o map (fn (a, b) => a ^ "=" ^ b); 

72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

35 

72032  36 

72038
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

37 
(* set user properties *) 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

38 

254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

39 
fun set {tasks_ready, tasks_pending, tasks_running, tasks_passive, tasks_urgent, 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

40 
workers_total, workers_active, workers_waiting} = 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

41 
(PolyML.Statistics.setUserCounter (0, tasks_ready); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

42 
PolyML.Statistics.setUserCounter (1, tasks_pending); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

43 
PolyML.Statistics.setUserCounter (2, tasks_running); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

44 
PolyML.Statistics.setUserCounter (3, tasks_passive); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

45 
PolyML.Statistics.setUserCounter (4, tasks_urgent); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

46 
PolyML.Statistics.setUserCounter (5, workers_total); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

47 
PolyML.Statistics.setUserCounter (6, workers_active); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

48 
PolyML.Statistics.setUserCounter (7, workers_waiting)); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

49 

254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

50 

254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

51 
(* get properties *) 
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

52 

72041
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

53 
local 
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

54 

72032  55 
fun make_properties 
56 
{gcFullGCs, 

57 
gcPartialGCs, 

58 
gcSharePasses, 

59 
sizeAllocation, 

60 
sizeAllocationFree, 

61 
sizeCode, 

62 
sizeHeap, 

63 
sizeHeapFreeLastFullGC, 

64 
sizeHeapFreeLastGC, 

65 
sizeStacks, 

66 
threadsInML, 

67 
threadsTotal, 

68 
threadsWaitCondVar, 

69 
threadsWaitIO, 

70 
threadsWaitMutex, 

71 
threadsWaitSignal, 

72 
timeGCReal, 

73 
timeGCSystem, 

74 
timeGCUser, 

75 
timeNonGCReal, 

76 
timeNonGCSystem, 

77 
timeNonGCUser, 

72041
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

78 
userCounters, ...} = 
50255  79 
let 
72038
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

80 
val tasks_ready = Vector.sub (userCounters, 0); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

81 
val tasks_pending = Vector.sub (userCounters, 1); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

82 
val tasks_running = Vector.sub (userCounters, 2); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

83 
val tasks_passive = Vector.sub (userCounters, 3); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

84 
val tasks_urgent = Vector.sub (userCounters, 4); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

85 
val tasks_total = tasks_ready + tasks_pending + tasks_running + tasks_passive + tasks_urgent; 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

86 
val workers_total = Vector.sub (userCounters, 5); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

87 
val workers_active = Vector.sub (userCounters, 6); 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

88 
val workers_waiting = Vector.sub (userCounters, 7); 
50255  89 
in 
72038
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

90 
[("now", print_real (Time.toReal (Time.now ()))), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

91 
("tasks_ready", print_int tasks_ready), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

92 
("tasks_pending", print_int tasks_pending), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

93 
("tasks_running", print_int tasks_running), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

94 
("tasks_passive", print_int tasks_passive), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

95 
("tasks_urgent", print_int tasks_urgent), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

96 
("tasks_total", print_int tasks_total), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

97 
("workers_total", print_int workers_total), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

98 
("workers_active", print_int workers_active), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

99 
("workers_waiting", print_int workers_waiting), 
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

100 
("full_GCs", print_int gcFullGCs), 
72031
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

101 
("partial_GCs", print_int gcPartialGCs), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

102 
("share_passes", print_int gcSharePasses), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

103 
("size_allocation", print_int sizeAllocation), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

104 
("size_allocation_free", print_int sizeAllocationFree), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

105 
("size_code", print_int sizeCode), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

106 
("size_heap", print_int sizeHeap), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

107 
("size_heap_free_last_full_GC", print_int sizeHeapFreeLastFullGC), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

108 
("size_heap_free_last_GC", print_int sizeHeapFreeLastGC), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

109 
("size_stacks", print_int sizeStacks), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

110 
("threads_in_ML", print_int threadsInML), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

111 
("threads_total", print_int threadsTotal), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

112 
("threads_wait_condvar", print_int threadsWaitCondVar), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

113 
("threads_wait_IO", print_int threadsWaitIO), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

114 
("threads_wait_mutex", print_int threadsWaitMutex), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

115 
("threads_wait_signal", print_int threadsWaitSignal), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

116 
("time_elapsed", print_real (Time.toReal timeNonGCReal)), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

117 
("time_elapsed_GC", print_real (Time.toReal timeGCReal)), 
b7cec26e41d1
clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents:
69822
diff
changeset

118 
("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)), 
72038
254c324f31fd
clarified user counters: expose tasks to external monitor;
wenzelm
parents:
72033
diff
changeset

119 
("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] 
50255  120 
end; 
121 

72041
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

122 
in 
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

123 

72032  124 
fun get () = 
125 
make_properties (PolyML.Statistics.getLocalStats ()); 

126 

127 
fun get_external pid = 

128 
make_properties (PolyML.Statistics.getRemoteStats pid); 

129 

72041
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

130 
end; 
7b112eedc859
more robust wrt. experimental changes in Poly/ML;
wenzelm
parents:
72040
diff
changeset

131 

72032  132 

133 
(* monitor process *) 

134 

135 
fun monitor pid delay = 

136 
let 

137 
fun loop () = 

138 
(TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n"); 

139 
TextIO.flushOut TextIO.stdOut; 

140 
OS.Process.sleep (Time.fromReal delay); 

141 
loop ()); 

72040  142 
fun exit () = OS.Process.exit OS.Process.success; 
72111
b9ded33bd58c
clarified catchall handler  avoid confusion of Interrupt vs. Exn.Interrupt in varying ML contexts;
wenzelm
parents:
72041
diff
changeset

143 
in loop () handle _ (*sic!*) => exit () end; 
72032  144 

50255  145 
end; 