author | haftmann |
Sat, 10 Nov 2018 07:57:20 +0000 | |
changeset 69276 | 3d954183b707 |
parent 68129 | b73678836f8e |
child 69822 | 8c587dd44f51 |
permissions | -rw-r--r-- |
65477 | 1 |
/* Title: Pure/ML/ml_statistics.scala |
50685 | 2 |
Author: Makarius |
3 |
||
4 |
ML runtime statistics. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
65858 | 10 |
import scala.annotation.tailrec |
51432 | 11 |
import scala.collection.mutable |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
12 |
import scala.collection.immutable.{SortedSet, SortedMap} |
50691 | 13 |
import scala.swing.{Frame, Component} |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
14 |
|
50689 | 15 |
import org.jfree.data.xy.{XYSeries, XYSeriesCollection} |
16 |
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} |
|
17 |
import org.jfree.chart.plot.PlotOrientation |
|
18 |
||
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
19 |
|
50685 | 20 |
object ML_Statistics |
21 |
{ |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
22 |
/* properties */ |
50690 | 23 |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
24 |
val Now = new Properties.Double("now") |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
25 |
def now(props: Properties.T): Double = Now.unapply(props).get |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
26 |
|
50690 | 27 |
|
65866 | 28 |
/* heap */ |
50690 | 29 |
|
65858 | 30 |
val HEAP_SIZE = "size_heap" |
31 |
||
65866 | 32 |
def heap_scale(x: Long): Long = x / 1024 / 1024 |
33 |
def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong |
|
34 |
||
35 |
||
36 |
/* standard fields */ |
|
37 |
||
65864 | 38 |
type Fields = (String, List[String]) |
65051 | 39 |
|
40 |
val tasks_fields: Fields = |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
57869
diff
changeset
|
41 |
("Future tasks", |
68129 | 42 |
List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", |
43 |
"tasks_urgent", "tasks_total")) |
|
57869 | 44 |
|
65051 | 45 |
val workers_fields: Fields = |
57869 | 46 |
("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
47 |
||
65051 | 48 |
val GC_fields: Fields = |
49 |
("GCs", List("partial_GCs", "full_GCs")) |
|
50690 | 50 |
|
65051 | 51 |
val heap_fields: Fields = |
65858 | 52 |
("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free", |
50690 | 53 |
"size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
54 |
||
65051 | 55 |
val threads_fields: Fields = |
50690 | 56 |
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
57 |
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
|
58 |
||
65051 | 59 |
val time_fields: Fields = |
60 |
("Time", List("time_CPU", "time_GC")) |
|
51432 | 61 |
|
65051 | 62 |
val speed_fields: Fields = |
63 |
("Speed", List("speed_CPU", "speed_GC")) |
|
50690 | 64 |
|
65053 | 65 |
|
66 |
val all_fields: List[Fields] = |
|
57869 | 67 |
List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields, |
68 |
time_fields, speed_fields) |
|
65053 | 69 |
|
70 |
val main_fields: List[Fields] = |
|
71 |
List(tasks_fields, workers_fields, heap_fields) |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
72 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
73 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
74 |
/* content interpretation */ |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
75 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
76 |
final case class Entry(time: Double, data: Map[String, Double]) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
77 |
{ |
65858 | 78 |
def get(field: String): Double = data.getOrElse(field, 0.0) |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
79 |
} |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
80 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
81 |
val empty: ML_Statistics = apply(Nil) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
82 |
|
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
83 |
def apply(ml_statistics: List[Properties.T], heading: String = "", |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
84 |
domain: String => Boolean = (key: String) => true): ML_Statistics = |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
85 |
{ |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
86 |
require(ml_statistics.forall(props => Now.unapply(props).isDefined)) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
87 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
88 |
val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
89 |
val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
90 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
91 |
val fields = |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
92 |
SortedSet.empty[String] ++ |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
93 |
(for { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
94 |
props <- ml_statistics.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
95 |
(x, _) <- props.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
96 |
if x != Now.name && domain(x) } yield x) |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
97 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
98 |
val content = |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
99 |
{ |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
100 |
var last_edge = Map.empty[String, (Double, Double, Double)] |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
101 |
val result = new mutable.ListBuffer[ML_Statistics.Entry] |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
102 |
for (props <- ml_statistics) { |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
103 |
val time = now(props) - time_start |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
104 |
require(time >= 0.0) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
105 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
106 |
// rising edges -- relative speed |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
107 |
val speeds = |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
108 |
(for { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
109 |
(key, value) <- props.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
110 |
a <- Library.try_unprefix("time", key) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
111 |
b = "speed" + a if domain(b) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
112 |
} |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
113 |
yield { |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
114 |
val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0)) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
115 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
116 |
val x1 = time |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
117 |
val y1 = java.lang.Double.parseDouble(value) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
118 |
val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
119 |
|
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
120 |
if (y1 > y0) { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
121 |
last_edge += (a -> (x1, y1, s1)) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
122 |
(b, s1.toString) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
123 |
} |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
124 |
else (b, s0.toString) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
125 |
}).toList |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
126 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
127 |
val data = |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
128 |
SortedMap.empty[String, Double] ++ |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
129 |
(for { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
130 |
(x, y) <- props.iterator ++ speeds.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
131 |
if x != Now.name && domain(x) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
132 |
z = java.lang.Double.parseDouble(y) if z != 0.0 |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
133 |
} yield { (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) }) |
65866 | 134 |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
135 |
result += ML_Statistics.Entry(time, data) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
136 |
} |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
137 |
result.toList |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
138 |
} |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
139 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
140 |
new ML_Statistics(heading, fields, content, time_start, duration) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
141 |
} |
50685 | 142 |
} |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
143 |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
144 |
final class ML_Statistics private( |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
145 |
val heading: String, |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
146 |
val fields: Set[String], |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
147 |
val content: List[ML_Statistics.Entry], |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
148 |
val time_start: Double, |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
149 |
val duration: Double) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
150 |
{ |
65858 | 151 |
/* content */ |
152 |
||
153 |
def maximum(field: String): Double = |
|
154 |
(0.0 /: content)({ case (m, e) => m max e.get(field) }) |
|
155 |
||
156 |
def average(field: String): Double = |
|
157 |
{ |
|
158 |
@tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double = |
|
159 |
list match { |
|
160 |
case Nil => acc |
|
161 |
case e :: es => |
|
162 |
val t = e.time |
|
163 |
sum(t, es, (t - t0) * e.get(field) + acc) |
|
164 |
} |
|
165 |
content match { |
|
166 |
case Nil => 0.0 |
|
167 |
case List(e) => e.get(field) |
|
168 |
case e :: es => sum(e.time, es, 0.0) / duration |
|
169 |
} |
|
170 |
} |
|
171 |
||
172 |
def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong |
|
173 |
def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong |
|
65854 | 174 |
|
50689 | 175 |
|
176 |
/* charts */ |
|
177 |
||
65864 | 178 |
def update_data(data: XYSeriesCollection, selected_fields: List[String]) |
50689 | 179 |
{ |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
180 |
data.removeAllSeries |
50689 | 181 |
for { |
50690 | 182 |
field <- selected_fields.iterator |
50689 | 183 |
series = new XYSeries(field) |
184 |
} { |
|
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
185 |
content.foreach(entry => series.add(entry.time, entry.get(field))) |
50689 | 186 |
data.addSeries(series) |
187 |
} |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
188 |
} |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
189 |
|
65864 | 190 |
def chart(title: String, selected_fields: List[String]): JFreeChart = |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
191 |
{ |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
192 |
val data = new XYSeriesCollection |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
193 |
update_data(data, selected_fields) |
50689 | 194 |
|
195 |
ChartFactory.createXYLineChart(title, "time", "value", data, |
|
196 |
PlotOrientation.VERTICAL, true, true, true) |
|
197 |
} |
|
198 |
||
65051 | 199 |
def chart(fields: ML_Statistics.Fields): JFreeChart = |
200 |
chart(fields._1, fields._2) |
|
50691 | 201 |
|
65053 | 202 |
def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = |
65051 | 203 |
fields.map(chart(_)).foreach(c => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
53189
diff
changeset
|
204 |
GUI_Thread.later { |
50854 | 205 |
new Frame { |
51615
072a7249e1ac
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
51432
diff
changeset
|
206 |
iconImage = GUI.isabelle_image() |
65851 | 207 |
title = heading |
50854 | 208 |
contents = Component.wrap(new ChartPanel(c)) |
209 |
visible = true |
|
210 |
} |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
211 |
}) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
212 |
} |