1/*  Title:      Pure/ML/ml_statistics.scala
2    Author:     Makarius
3
4ML runtime statistics.
5*/
6
7package isabelle
8
9
10import scala.annotation.tailrec
11import scala.collection.mutable
12import scala.collection.immutable.{SortedSet, SortedMap}
13import scala.swing.{Frame, Component}
14
15import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
16import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
17import org.jfree.chart.plot.PlotOrientation
18
19
20object ML_Statistics
21{
22  /* properties */
23
24  val Now = new Properties.Double("now")
25  def now(props: Properties.T): Double = Now.unapply(props).get
26
27
28  /* heap */
29
30  val HEAP_SIZE = "size_heap"
31
32  def heap_scale(x: Long): Long = x / 1024 / 1024
33  def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong
34
35
36  /* standard fields */
37
38  type Fields = (String, List[String])
39
40  val tasks_fields: Fields =
41    ("Future tasks",
42      List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive",
43        "tasks_urgent", "tasks_total"))
44
45  val workers_fields: Fields =
46    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
47
48  val GC_fields: Fields =
49    ("GCs", List("partial_GCs", "full_GCs"))
50
51  val heap_fields: Fields =
52    ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
53      "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
54
55  val threads_fields: Fields =
56    ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
57      "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
58
59  val time_fields: Fields =
60    ("Time", List("time_CPU", "time_GC"))
61
62  val speed_fields: Fields =
63    ("Speed", List("speed_CPU", "speed_GC"))
64
65
66  val all_fields: List[Fields] =
67    List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
68      time_fields, speed_fields)
69
70  val main_fields: List[Fields] =
71    List(tasks_fields, workers_fields, heap_fields)
72
73
74  /* content interpretation */
75
76  final case class Entry(time: Double, data: Map[String, Double])
77  {
78    def get(field: String): Double = data.getOrElse(field, 0.0)
79  }
80
81  val empty: ML_Statistics = apply(Nil)
82
83  def apply(ml_statistics: List[Properties.T], heading: String = "",
84    domain: String => Boolean = (key: String) => true): ML_Statistics =
85  {
86    require(ml_statistics.forall(props => Now.unapply(props).isDefined))
87
88    val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
89    val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
90
91    val fields =
92      SortedSet.empty[String] ++
93        (for {
94          props <- ml_statistics.iterator
95          (x, _) <- props.iterator
96          if x != Now.name && domain(x) } yield x)
97
98    val content =
99    {
100      var last_edge = Map.empty[String, (Double, Double, Double)]
101      val result = new mutable.ListBuffer[ML_Statistics.Entry]
102      for (props <- ml_statistics) {
103        val time = now(props) - time_start
104        require(time >= 0.0)
105
106        // rising edges -- relative speed
107        val speeds =
108          (for {
109            (key, value) <- props.iterator
110            a <- Library.try_unprefix("time", key)
111            b = "speed" + a if domain(b)
112          }
113          yield {
114            val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
115
116            val x1 = time
117            val y1 = java.lang.Double.parseDouble(value)
118            val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
119
120            if (y1 > y0) {
121              last_edge += (a -> (x1, y1, s1))
122              (b, s1.toString)
123            }
124            else (b, s0.toString)
125          }).toList
126
127        val data =
128          SortedMap.empty[String, Double] ++
129            (for {
130              (x, y) <- props.iterator ++ speeds.iterator
131              if x != Now.name && domain(x)
132              z = java.lang.Double.parseDouble(y) if z != 0.0
133            } yield { (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) })
134
135        result += ML_Statistics.Entry(time, data)
136      }
137      result.toList
138    }
139
140    new ML_Statistics(heading, fields, content, time_start, duration)
141  }
142}
143
144final class ML_Statistics private(
145  val heading: String,
146  val fields: Set[String],
147  val content: List[ML_Statistics.Entry],
148  val time_start: Double,
149  val duration: Double)
150{
151  /* content */
152
153  def maximum(field: String): Double =
154    (0.0 /: content)({ case (m, e) => m max e.get(field) })
155
156  def average(field: String): Double =
157  {
158    @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double =
159      list match {
160        case Nil => acc
161        case e :: es =>
162          val t = e.time
163          sum(t, es, (t - t0) * e.get(field) + acc)
164      }
165    content match {
166      case Nil => 0.0
167      case List(e) => e.get(field)
168      case e :: es => sum(e.time, es, 0.0) / duration
169    }
170  }
171
172  def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong
173  def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong
174
175
176  /* charts */
177
178  def update_data(data: XYSeriesCollection, selected_fields: List[String])
179  {
180    data.removeAllSeries
181    for {
182      field <- selected_fields.iterator
183      series = new XYSeries(field)
184    } {
185      content.foreach(entry => series.add(entry.time, entry.get(field)))
186      data.addSeries(series)
187    }
188  }
189
190  def chart(title: String, selected_fields: List[String]): JFreeChart =
191  {
192    val data = new XYSeriesCollection
193    update_data(data, selected_fields)
194
195    ChartFactory.createXYLineChart(title, "time", "value", data,
196      PlotOrientation.VERTICAL, true, true, true)
197  }
198
199  def chart(fields: ML_Statistics.Fields): JFreeChart =
200    chart(fields._1, fields._2)
201
202  def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
203    fields.map(chart(_)).foreach(c =>
204      GUI_Thread.later {
205        new Frame {
206          iconImage = GUI.isabelle_image()
207          title = heading
208          contents = Component.wrap(new ChartPanel(c))
209          visible = true
210        }
211      })
212}
213