src/Pure/Tools/ml_statistics.scala
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 57869 9665f79a7181
child 60610 f52b4b0c10c4
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
     1 /*  Title:      Pure/Tools/ml_statistics.scala
     2     Author:     Makarius
     3 
     4 ML runtime statistics.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 import scala.collection.immutable.{SortedSet, SortedMap}
    12 import scala.swing.{Frame, Component}
    13 
    14 import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
    15 import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
    16 import org.jfree.chart.plot.PlotOrientation
    17 
    18 
    19 object ML_Statistics
    20 {
    21   /* content interpretation */
    22 
    23   final case class Entry(time: Double, data: Map[String, Double])
    24 
    25   def apply(name: String, stats: List[Properties.T]): ML_Statistics =
    26     new ML_Statistics(name, stats)
    27 
    28   def apply(info: Build.Log_Info): ML_Statistics =
    29     apply(info.name, info.stats)
    30 
    31   val empty = apply("", Nil)
    32 
    33 
    34   /* standard fields */
    35 
    36   val tasks_fields =
    37     ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
    38 
    39   val workers_fields =
    40     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    41 
    42   val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
    43 
    44   val heap_fields =
    45     ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
    46       "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
    47 
    48   val threads_fields =
    49     ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
    50       "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
    51 
    52   val time_fields = ("Time", List("time_CPU", "time_GC"))
    53 
    54   val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
    55 
    56   val standard_fields =
    57     List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
    58       time_fields, speed_fields)
    59 }
    60 
    61 final class ML_Statistics private(val name: String, val stats: List[Properties.T])
    62 {
    63   val Now = new Properties.Double("now")
    64   def now(props: Properties.T): Double = Now.unapply(props).get
    65 
    66   require(stats.forall(props => Now.unapply(props).isDefined))
    67 
    68   val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
    69   val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
    70 
    71   val fields: Set[String] =
    72     SortedSet.empty[String] ++
    73       (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
    74         yield x)
    75 
    76   val content: List[ML_Statistics.Entry] =
    77   {
    78     var last_edge = Map.empty[String, (Double, Double, Double)]
    79     val result = new mutable.ListBuffer[ML_Statistics.Entry]
    80     for (props <- stats) {
    81       val time = now(props) - time_start
    82       require(time >= 0.0)
    83 
    84       // rising edges -- relative speed
    85       val speeds =
    86         for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
    87           val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
    88 
    89           val x1 = time
    90           val y1 = java.lang.Double.parseDouble(value)
    91           val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
    92 
    93           val b = ("speed" + a).intern
    94           if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
    95         }
    96 
    97       val data =
    98         SortedMap.empty[String, Double] ++ speeds ++
    99           (for ((x, y) <- props.iterator if x != Now.name)
   100             yield (x, java.lang.Double.parseDouble(y)))
   101       result += ML_Statistics.Entry(time, data)
   102     }
   103     result.toList
   104   }
   105 
   106 
   107   /* charts */
   108 
   109   def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
   110   {
   111     data.removeAllSeries
   112     for {
   113       field <- selected_fields.iterator
   114       series = new XYSeries(field)
   115     } {
   116       content.foreach(entry => series.add(entry.time, entry.data(field)))
   117       data.addSeries(series)
   118     }
   119   }
   120 
   121   def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
   122   {
   123     val data = new XYSeriesCollection
   124     update_data(data, selected_fields)
   125 
   126     ChartFactory.createXYLineChart(title, "time", "value", data,
   127       PlotOrientation.VERTICAL, true, true, true)
   128   }
   129 
   130   def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
   131 
   132   def show_standard_frames(): Unit =
   133     ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
   134       GUI_Thread.later {
   135         new Frame {
   136           iconImage = GUI.isabelle_image()
   137           title = name
   138           contents = Component.wrap(new ChartPanel(c))
   139           visible = true
   140         }
   141       })
   142 }
   143