1 /* Title: Pure/Tools/ml_statistics.scala |
|
2 Author: Makarius |
|
3 |
|
4 ML runtime statistics. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import scala.collection.mutable |
|
11 import scala.collection.immutable.{SortedSet, SortedMap} |
|
12 import scala.swing.{Frame, Component} |
|
13 |
|
14 import org.jfree.data.xy.{XYSeries, XYSeriesCollection} |
|
15 import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} |
|
16 import org.jfree.chart.plot.PlotOrientation |
|
17 |
|
18 |
|
19 object ML_Statistics |
|
20 { |
|
21 /* content interpretation */ |
|
22 |
|
23 final case class Entry(time: Double, data: Map[String, Double]) |
|
24 |
|
25 def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics = |
|
26 new ML_Statistics(session_name, ml_statistics) |
|
27 |
|
28 val empty = apply("", Nil) |
|
29 |
|
30 |
|
31 /* standard fields */ |
|
32 |
|
33 type Fields = (String, Iterable[String]) |
|
34 |
|
35 val tasks_fields: Fields = |
|
36 ("Future tasks", |
|
37 List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent")) |
|
38 |
|
39 val workers_fields: Fields = |
|
40 ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
|
41 |
|
42 val GC_fields: Fields = |
|
43 ("GCs", List("partial_GCs", "full_GCs")) |
|
44 |
|
45 val heap_fields: Fields = |
|
46 ("Heap", List("size_heap", "size_allocation", "size_allocation_free", |
|
47 "size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
|
48 |
|
49 val threads_fields: Fields = |
|
50 ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
|
51 "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
|
52 |
|
53 val time_fields: Fields = |
|
54 ("Time", List("time_CPU", "time_GC")) |
|
55 |
|
56 val speed_fields: Fields = |
|
57 ("Speed", List("speed_CPU", "speed_GC")) |
|
58 |
|
59 |
|
60 val all_fields: List[Fields] = |
|
61 List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields, |
|
62 time_fields, speed_fields) |
|
63 |
|
64 val main_fields: List[Fields] = |
|
65 List(tasks_fields, workers_fields, heap_fields) |
|
66 } |
|
67 |
|
68 final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T]) |
|
69 { |
|
70 val Now = new Properties.Double("now") |
|
71 def now(props: Properties.T): Double = Now.unapply(props).get |
|
72 |
|
73 require(ml_statistics.forall(props => Now.unapply(props).isDefined)) |
|
74 |
|
75 val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) |
|
76 val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start |
|
77 |
|
78 val fields: Set[String] = |
|
79 SortedSet.empty[String] ++ |
|
80 (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name) |
|
81 yield x) |
|
82 |
|
83 val content: List[ML_Statistics.Entry] = |
|
84 { |
|
85 var last_edge = Map.empty[String, (Double, Double, Double)] |
|
86 val result = new mutable.ListBuffer[ML_Statistics.Entry] |
|
87 for (props <- ml_statistics) { |
|
88 val time = now(props) - time_start |
|
89 require(time >= 0.0) |
|
90 |
|
91 // rising edges -- relative speed |
|
92 val speeds = |
|
93 for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield { |
|
94 val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0)) |
|
95 |
|
96 val x1 = time |
|
97 val y1 = java.lang.Double.parseDouble(value) |
|
98 val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) |
|
99 |
|
100 val b = ("speed" + a).intern |
|
101 if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0) |
|
102 } |
|
103 |
|
104 val data = |
|
105 SortedMap.empty[String, Double] ++ speeds ++ |
|
106 (for ((x, y) <- props.iterator if x != Now.name) |
|
107 yield (x, java.lang.Double.parseDouble(y))) |
|
108 result += ML_Statistics.Entry(time, data) |
|
109 } |
|
110 result.toList |
|
111 } |
|
112 |
|
113 |
|
114 /* charts */ |
|
115 |
|
116 def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) |
|
117 { |
|
118 data.removeAllSeries |
|
119 for { |
|
120 field <- selected_fields.iterator |
|
121 series = new XYSeries(field) |
|
122 } { |
|
123 content.foreach(entry => series.add(entry.time, entry.data(field))) |
|
124 data.addSeries(series) |
|
125 } |
|
126 } |
|
127 |
|
128 def chart(title: String, selected_fields: Iterable[String]): JFreeChart = |
|
129 { |
|
130 val data = new XYSeriesCollection |
|
131 update_data(data, selected_fields) |
|
132 |
|
133 ChartFactory.createXYLineChart(title, "time", "value", data, |
|
134 PlotOrientation.VERTICAL, true, true, true) |
|
135 } |
|
136 |
|
137 def chart(fields: ML_Statistics.Fields): JFreeChart = |
|
138 chart(fields._1, fields._2) |
|
139 |
|
140 def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = |
|
141 fields.map(chart(_)).foreach(c => |
|
142 GUI_Thread.later { |
|
143 new Frame { |
|
144 iconImage = GUI.isabelle_image() |
|
145 title = session_name |
|
146 contents = Component.wrap(new ChartPanel(c)) |
|
147 visible = true |
|
148 } |
|
149 }) |
|
150 } |
|
151 |
|