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