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