# HG changeset patch # User wenzelm # Date 1363351597 -3600 # Node ID 903be59d96650e072f0d9b6fa4dd895d88f77c8e # Parent 9d3ba9775988dd78c303694abc3ae1a0045be43c simplified time_CPU and time_GC; derive relative speed from time (considered as step function); diff -r 9d3ba9775988 -r 903be59d9665 src/Pure/ML/ml_statistics_polyml-5.5.0.ML --- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Fri Mar 15 10:49:28 2013 +0100 +++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Fri Mar 15 13:46:37 2013 +0100 @@ -51,10 +51,8 @@ ("threads_wait_IO", Markup.print_int threadsWaitIO), ("threads_wait_mutex", Markup.print_int threadsWaitMutex), ("threads_wait_signal", Markup.print_int threadsWaitSignal), - ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)), - ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)), - ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)), - ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))] @ + ("time_CPU", signed_string_of_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)), + ("time_GC", signed_string_of_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @ user_counters end; diff -r 9d3ba9775988 -r 903be59d9665 src/Pure/Tools/ml_statistics.scala --- a/src/Pure/Tools/ml_statistics.scala Fri Mar 15 10:49:28 2013 +0100 +++ b/src/Pure/Tools/ml_statistics.scala Fri Mar 15 13:46:37 2013 +0100 @@ -7,6 +7,7 @@ package isabelle +import scala.collection.mutable import scala.collection.immutable.{SortedSet, SortedMap} import scala.swing.{Frame, Component} @@ -42,8 +43,9 @@ ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) - val time_fields = - ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user")) + val time_fields = ("Time", List("time_CPU", "time_GC")) + + val speed_fields = ("Speed", List("speed_CPU", "speed_GC")) val tasks_fields = ("Future tasks", @@ -53,7 +55,8 @@ ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) val standard_fields = - List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) + List(GC_fields, heap_fields, threads_fields, time_fields, speed_fields, + tasks_fields, workers_fields) } final class ML_Statistics private(val name: String, val stats: List[Properties.T]) @@ -72,15 +75,34 @@ yield x) val content: List[ML_Statistics.Entry] = - stats.map(props => { + { + var last_edge = Map.empty[String, (Double, Double, Double)] + val result = new mutable.ListBuffer[ML_Statistics.Entry] + for (props <- stats) { val time = now(props) - time_start require(time >= 0.0) + + // rising edges -- relative speed + val speeds = + for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield { + val (x0, y0, s0) = last_edge.get(a) getOrElse (0.0, 0.0, 0.0) + + val x1 = time + val y1 = java.lang.Double.parseDouble(value) + val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) + + val b = ("speed" + a).intern + if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0) + } + val data = - SortedMap.empty[String, Double] ++ + SortedMap.empty[String, Double] ++ speeds ++ (for ((x, y) <- props.iterator if x != Now.name) yield (x, java.lang.Double.parseDouble(y))) - ML_Statistics.Entry(time, data) - }) + result += ML_Statistics.Entry(time, data) + } + result.toList + } /* charts */