author | wenzelm |
Fri, 18 Jan 2013 23:33:17 +0100 | |
changeset 50982 | a7aa17a1f721 |
parent 50981 | 1791a90a94fb |
child 51240 | a7a04b449e8b |
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 |
||
50982 | 24 |
def apply(name: String, stats: List[Properties.T]): ML_Statistics = |
25 |
new ML_Statistics(name, stats) |
|
50690 | 26 |
|
50982 | 27 |
def apply(info: Build.Log_Info): ML_Statistics = |
28 |
apply(info.name, info.stats) |
|
29 |
||
30 |
val empty = apply("", Nil) |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
31 |
|
50690 | 32 |
|
33 |
/* standard fields */ |
|
34 |
||
35 |
val GC_fields = ("GCs", List("partial_GCs", "full_GCs")) |
|
36 |
||
37 |
val heap_fields = |
|
38 |
("Heap", List("size_heap", "size_allocation", "size_allocation_free", |
|
39 |
"size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
|
40 |
||
41 |
val threads_fields = |
|
42 |
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
|
43 |
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
|
44 |
||
45 |
val time_fields = |
|
46 |
("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user")) |
|
47 |
||
48 |
val tasks_fields = |
|
50974
55f8bd61b029
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
wenzelm
parents:
50855
diff
changeset
|
49 |
("Future tasks", |
55f8bd61b029
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
wenzelm
parents:
50855
diff
changeset
|
50 |
List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive")) |
50690 | 51 |
|
52 |
val workers_fields = |
|
53 |
("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
|
54 |
||
55 |
val standard_fields = |
|
56 |
List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) |
|
50685 | 57 |
} |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
58 |
|
50982 | 59 |
final class ML_Statistics private(val name: String, val stats: List[Properties.T]) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
60 |
{ |
50690 | 61 |
val Now = new Properties.Double("now") |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
62 |
def now(props: Properties.T): Double = Now.unapply(props).get |
50690 | 63 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
64 |
require(stats.forall(props => Now.unapply(props).isDefined)) |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
65 |
|
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
|
50689 | 69 |
val fields: Set[String] = |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
70 |
SortedSet.empty[String] ++ |
50690 | 71 |
(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
|
72 |
yield x) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
73 |
|
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
74 |
val content: List[ML_Statistics.Entry] = |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
75 |
stats.map(props => { |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
76 |
val time = now(props) - time_start |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
77 |
require(time >= 0.0) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
78 |
val data = |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
79 |
SortedMap.empty[String, Double] ++ |
50690 | 80 |
(for ((x, y) <- props.iterator if x != Now.name) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
81 |
yield (x, java.lang.Double.parseDouble(y))) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
82 |
ML_Statistics.Entry(time, data) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
83 |
}) |
50689 | 84 |
|
85 |
||
86 |
/* charts */ |
|
87 |
||
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
88 |
def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) |
50689 | 89 |
{ |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
90 |
data.removeAllSeries |
50689 | 91 |
for { |
50690 | 92 |
field <- selected_fields.iterator |
50689 | 93 |
series = new XYSeries(field) |
94 |
} { |
|
95 |
content.foreach(entry => series.add(entry.time, entry.data(field))) |
|
96 |
data.addSeries(series) |
|
97 |
} |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
98 |
} |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
99 |
|
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
100 |
def chart(title: String, selected_fields: Iterable[String]): JFreeChart = |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
101 |
{ |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
102 |
val data = new XYSeriesCollection |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
103 |
update_data(data, selected_fields) |
50689 | 104 |
|
105 |
ChartFactory.createXYLineChart(title, "time", "value", data, |
|
106 |
PlotOrientation.VERTICAL, true, true, true) |
|
107 |
} |
|
108 |
||
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
109 |
def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) |
50691 | 110 |
|
50981 | 111 |
def show_standard_frames(): Unit = |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
112 |
ML_Statistics.standard_fields.map(chart(_)).foreach(c => |
50691 | 113 |
Swing_Thread.later { |
50854 | 114 |
new Frame { |
115 |
iconImage = Isabelle_System.get_icon().getImage |
|
50982 | 116 |
title = name |
50854 | 117 |
contents = Component.wrap(new ChartPanel(c)) |
118 |
visible = true |
|
119 |
} |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
120 |
}) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
121 |
} |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
122 |