wenzelm@51700
|
1 |
/* Title: Pure/ML/ml_statistics.ML
|
wenzelm@51700
|
2 |
Author: Makarius
|
wenzelm@51700
|
3 |
|
wenzelm@51700
|
4 |
ML runtime statistics.
|
wenzelm@51700
|
5 |
*/
|
wenzelm@51700
|
6 |
|
wenzelm@51700
|
7 |
package isabelle
|
wenzelm@51700
|
8 |
|
wenzelm@51700
|
9 |
|
wenzelm@51703
|
10 |
import scala.collection.immutable.{SortedSet, SortedMap}
|
wenzelm@51706
|
11 |
import scala.swing.{Frame, Component}
|
wenzelm@51703
|
12 |
|
wenzelm@51704
|
13 |
import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
|
wenzelm@51704
|
14 |
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
|
wenzelm@51704
|
15 |
import org.jfree.chart.plot.PlotOrientation
|
wenzelm@51704
|
16 |
|
wenzelm@51703
|
17 |
|
wenzelm@51700
|
18 |
object ML_Statistics
|
wenzelm@51700
|
19 |
{
|
wenzelm@51705
|
20 |
/* content interpretation */
|
wenzelm@51705
|
21 |
|
wenzelm@51705
|
22 |
final case class Entry(time: Double, data: Map[String, Double])
|
wenzelm@51705
|
23 |
|
wenzelm@51705
|
24 |
def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
|
wenzelm@51792
|
25 |
def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
|
wenzelm@51705
|
26 |
|
wenzelm@51712
|
27 |
val empty = apply(Nil)
|
wenzelm@51712
|
28 |
|
wenzelm@51705
|
29 |
|
wenzelm@51705
|
30 |
/* standard fields */
|
wenzelm@51705
|
31 |
|
wenzelm@51705
|
32 |
val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
|
wenzelm@51705
|
33 |
|
wenzelm@51705
|
34 |
val heap_fields =
|
wenzelm@51705
|
35 |
("Heap", List("size_heap", "size_allocation", "size_allocation_free",
|
wenzelm@51705
|
36 |
"size_heap_free_last_full_GC", "size_heap_free_last_GC"))
|
wenzelm@51705
|
37 |
|
wenzelm@51705
|
38 |
val threads_fields =
|
wenzelm@51705
|
39 |
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
|
wenzelm@51705
|
40 |
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
|
wenzelm@51705
|
41 |
|
wenzelm@51705
|
42 |
val time_fields =
|
wenzelm@51705
|
43 |
("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
|
wenzelm@51705
|
44 |
|
wenzelm@51705
|
45 |
val tasks_fields =
|
wenzelm@51989
|
46 |
("Future tasks",
|
wenzelm@51989
|
47 |
List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
|
wenzelm@51705
|
48 |
|
wenzelm@51705
|
49 |
val workers_fields =
|
wenzelm@51705
|
50 |
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
|
wenzelm@51705
|
51 |
|
wenzelm@51705
|
52 |
val standard_fields =
|
wenzelm@51705
|
53 |
List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
|
wenzelm@51700
|
54 |
}
|
wenzelm@51703
|
55 |
|
wenzelm@51703
|
56 |
final class ML_Statistics private(val stats: List[Properties.T])
|
wenzelm@51703
|
57 |
{
|
wenzelm@51705
|
58 |
val Now = new Properties.Double("now")
|
wenzelm@51712
|
59 |
def now(props: Properties.T): Double = Now.unapply(props).get
|
wenzelm@51703
|
60 |
|
wenzelm@51712
|
61 |
require(stats.forall(props => Now.unapply(props).isDefined))
|
wenzelm@51705
|
62 |
|
wenzelm@51712
|
63 |
val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
|
wenzelm@51712
|
64 |
val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
|
wenzelm@51703
|
65 |
|
wenzelm@51704
|
66 |
val fields: Set[String] =
|
wenzelm@51703
|
67 |
SortedSet.empty[String] ++
|
wenzelm@51705
|
68 |
(for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
|
wenzelm@51703
|
69 |
yield x)
|
wenzelm@51703
|
70 |
|
wenzelm@51703
|
71 |
val content: List[ML_Statistics.Entry] =
|
wenzelm@51703
|
72 |
stats.map(props => {
|
wenzelm@51712
|
73 |
val time = now(props) - time_start
|
wenzelm@51703
|
74 |
require(time >= 0.0)
|
wenzelm@51703
|
75 |
val data =
|
wenzelm@51703
|
76 |
SortedMap.empty[String, Double] ++
|
wenzelm@51705
|
77 |
(for ((x, y) <- props.iterator if x != Now.name)
|
wenzelm@51703
|
78 |
yield (x, java.lang.Double.parseDouble(y)))
|
wenzelm@51703
|
79 |
ML_Statistics.Entry(time, data)
|
wenzelm@51703
|
80 |
})
|
wenzelm@51704
|
81 |
|
wenzelm@51704
|
82 |
|
wenzelm@51704
|
83 |
/* charts */
|
wenzelm@51704
|
84 |
|
wenzelm@51712
|
85 |
def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
|
wenzelm@51704
|
86 |
{
|
wenzelm@51712
|
87 |
data.removeAllSeries
|
wenzelm@51704
|
88 |
for {
|
wenzelm@51705
|
89 |
field <- selected_fields.iterator
|
wenzelm@51704
|
90 |
series = new XYSeries(field)
|
wenzelm@51704
|
91 |
} {
|
wenzelm@51704
|
92 |
content.foreach(entry => series.add(entry.time, entry.data(field)))
|
wenzelm@51704
|
93 |
data.addSeries(series)
|
wenzelm@51704
|
94 |
}
|
wenzelm@51712
|
95 |
}
|
wenzelm@51712
|
96 |
|
wenzelm@51712
|
97 |
def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
|
wenzelm@51712
|
98 |
{
|
wenzelm@51712
|
99 |
val data = new XYSeriesCollection
|
wenzelm@51712
|
100 |
update_data(data, selected_fields)
|
wenzelm@51704
|
101 |
|
wenzelm@51704
|
102 |
ChartFactory.createXYLineChart(title, "time", "value", data,
|
wenzelm@51704
|
103 |
PlotOrientation.VERTICAL, true, true, true)
|
wenzelm@51704
|
104 |
}
|
wenzelm@51704
|
105 |
|
wenzelm@51712
|
106 |
def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
|
wenzelm@51706
|
107 |
|
wenzelm@51706
|
108 |
def standard_frames: Unit =
|
wenzelm@51712
|
109 |
ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
|
wenzelm@51706
|
110 |
Swing_Thread.later {
|
wenzelm@51869
|
111 |
new Frame {
|
wenzelm@51869
|
112 |
iconImage = Isabelle_System.get_icon().getImage
|
wenzelm@51870
|
113 |
title = "ML statistics"
|
wenzelm@51869
|
114 |
contents = Component.wrap(new ChartPanel(c))
|
wenzelm@51869
|
115 |
visible = true
|
wenzelm@51869
|
116 |
}
|
wenzelm@51712
|
117 |
})
|
wenzelm@51703
|
118 |
}
|
wenzelm@51703
|
119 |
|