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