author  wenzelm 
Fri, 18 Jan 2013 16:20:09 +0100  
changeset 50974  55f8bd61b029 
parent 50855  3f9a24e7349e 
permissions  rwrr 
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 = 

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

46 
("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

47 
List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive")) 
50690  48 

49 
val workers_fields = 

50 
("Worker threads", List("workers_total", "workers_active", "workers_waiting")) 

51 

52 
val standard_fields = 

53 
List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) 

50685  54 
} 
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

55 

f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

56 
final class ML_Statistics private(val stats: List[Properties.T]) 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

57 
{ 
50690  58 
val Now = new Properties.Double("now") 
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

59 
def now(props: Properties.T): Double = Now.unapply(props).get 
50690  60 

50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

61 
require(stats.forall(props => Now.unapply(props).isDefined)) 
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

62 

82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

63 
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

64 
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

65 

50689  66 
val fields: Set[String] = 
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

67 
SortedSet.empty[String] ++ 
50690  68 
(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

69 
yield x) 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

70 

f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

71 
val content: List[ML_Statistics.Entry] = 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

72 
stats.map(props => { 
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

73 
val time = now(props)  time_start 
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

74 
require(time >= 0.0) 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

75 
val data = 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

76 
SortedMap.empty[String, Double] ++ 
50690  77 
(for ((x, y) < props.iterator if x != Now.name) 
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

78 
yield (x, java.lang.Double.parseDouble(y))) 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

79 
ML_Statistics.Entry(time, data) 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

80 
}) 
50689  81 

82 

83 
/* charts */ 

84 

50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

85 
def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) 
50689  86 
{ 
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

87 
data.removeAllSeries 
50689  88 
for { 
50690  89 
field < selected_fields.iterator 
50689  90 
series = new XYSeries(field) 
91 
} { 

92 
content.foreach(entry => series.add(entry.time, entry.data(field))) 

93 
data.addSeries(series) 

94 
} 

50697
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 

82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

97 
def chart(title: String, selected_fields: Iterable[String]): JFreeChart = 
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 
val data = new XYSeriesCollection 
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

100 
update_data(data, selected_fields) 
50689  101 

102 
ChartFactory.createXYLineChart(title, "time", "value", data, 

103 
PlotOrientation.VERTICAL, true, true, true) 

104 
} 

105 

50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

106 
def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) 
50691  107 

108 
def standard_frames: Unit = 

50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

109 
ML_Statistics.standard_fields.map(chart(_)).foreach(c => 
50691  110 
Swing_Thread.later { 
50854  111 
new Frame { 
112 
iconImage = Isabelle_System.get_icon().getImage 

50855  113 
title = "ML statistics" 
50854  114 
contents = Component.wrap(new ChartPanel(c)) 
115 
visible = true 

116 
} 

50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset

117 
}) 
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

118 
} 
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset

119 