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