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