author | wenzelm |
Wed, 02 Jan 2013 21:39:54 +0100 | |
changeset 50690 | 03c4d75e8e32 |
parent 50689 | 0607d557d073 |
child 50691 | 20beafe66748 |
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} |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
11 |
|
50689 | 12 |
import org.jfree.data.xy.{XYSeries, XYSeriesCollection} |
13 |
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} |
|
14 |
import org.jfree.chart.plot.PlotOrientation |
|
15 |
||
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
16 |
|
50685 | 17 |
object ML_Statistics |
18 |
{ |
|
50690 | 19 |
/* content interpretation */ |
20 |
||
21 |
final case class Entry(time: Double, data: Map[String, Double]) |
|
22 |
||
23 |
def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats) |
|
24 |
def apply(log: Path): ML_Statistics = apply(read_log(log)) |
|
25 |
||
26 |
||
27 |
/* standard fields */ |
|
28 |
||
29 |
val GC_fields = ("GCs", List("partial_GCs", "full_GCs")) |
|
30 |
||
31 |
val heap_fields = |
|
32 |
("Heap", List("size_heap", "size_allocation", "size_allocation_free", |
|
33 |
"size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
|
34 |
||
35 |
val threads_fields = |
|
36 |
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
|
37 |
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
|
38 |
||
39 |
val time_fields = |
|
40 |
("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user")) |
|
41 |
||
42 |
val tasks_fields = |
|
43 |
("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive")) |
|
44 |
||
45 |
val workers_fields = |
|
46 |
("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
|
47 |
||
48 |
val standard_fields = |
|
49 |
List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) |
|
50 |
||
51 |
||
50685 | 52 |
/* read properties from build log */ |
53 |
||
54 |
private val line_prefix = "\fML_statistics = " |
|
55 |
||
56 |
private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]" |
|
57 |
||
58 |
private object Parser extends Parse.Parser |
|
59 |
{ |
|
60 |
private def stat: Parser[(String, String)] = |
|
61 |
keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^ |
|
62 |
{ case _ ~ x ~ _ ~ y ~ _ => (x, y) } |
|
63 |
private def stats: Parser[Properties.T] = |
|
64 |
keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]") |
|
65 |
||
66 |
def parse_stats(s: String): Properties.T = |
|
67 |
{ |
|
68 |
parse_all(stats, Token.reader(syntax.scan(s))) match { |
|
69 |
case Success(result, _) => result |
|
70 |
case bad => error(bad.toString) |
|
71 |
} |
|
72 |
} |
|
73 |
} |
|
74 |
||
75 |
def read_log(log: Path): List[Properties.T] = |
|
76 |
for { |
|
77 |
line <- split_lines(File.read_gzip(log)) |
|
78 |
if line.startsWith(line_prefix) |
|
79 |
stats = line.substring(line_prefix.length) |
|
80 |
} yield Parser.parse_stats(stats) |
|
81 |
} |
|
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
82 |
|
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
83 |
final class ML_Statistics private(val stats: List[Properties.T]) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
84 |
{ |
50690 | 85 |
val Now = new Properties.Double("now") |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
86 |
|
50690 | 87 |
require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined)) |
88 |
||
89 |
val time_start = Now.unapply(stats.head).get |
|
90 |
val duration = Now.unapply(stats.last).get - time_start |
|
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
91 |
|
50689 | 92 |
val fields: Set[String] = |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
93 |
SortedSet.empty[String] ++ |
50690 | 94 |
(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
|
95 |
yield x) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
96 |
|
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
97 |
val content: List[ML_Statistics.Entry] = |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
98 |
stats.map(props => { |
50690 | 99 |
val time = Now.unapply(props).get - time_start |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
100 |
require(time >= 0.0) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
101 |
val data = |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
102 |
SortedMap.empty[String, Double] ++ |
50690 | 103 |
(for ((x, y) <- props.iterator if x != Now.name) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
104 |
yield (x, java.lang.Double.parseDouble(y))) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
105 |
ML_Statistics.Entry(time, data) |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
106 |
}) |
50689 | 107 |
|
108 |
||
109 |
/* charts */ |
|
110 |
||
50690 | 111 |
def chart(title: String, selected_fields: Iterable[String]): JFreeChart = |
50689 | 112 |
{ |
113 |
val data = new XYSeriesCollection |
|
114 |
||
115 |
for { |
|
50690 | 116 |
field <- selected_fields.iterator |
50689 | 117 |
series = new XYSeries(field) |
118 |
} { |
|
119 |
content.foreach(entry => series.add(entry.time, entry.data(field))) |
|
120 |
data.addSeries(series) |
|
121 |
} |
|
122 |
||
123 |
ChartFactory.createXYLineChart(title, "time", "value", data, |
|
124 |
PlotOrientation.VERTICAL, true, true, true) |
|
125 |
} |
|
126 |
||
50690 | 127 |
def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel = |
128 |
new ChartPanel(chart(title, selected_fields)) |
|
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
129 |
} |
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
130 |