more memory fields;
authorwenzelm
Sat Feb 23 21:33:09 2019 +0100 (8 weeks ago ago)
changeset 70013b614e3e4146a
parent 70012 b35c3839d5d1
child 70014 c3500cec8290
more memory fields;
src/Pure/Admin/build_status.scala
src/Pure/ML/ml_statistics.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat Feb 23 21:32:29 2019 +0100
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat Feb 23 21:33:09 2019 +0100
     1.3 @@ -116,6 +116,10 @@
     1.4            "ml_timing_elapsed",
     1.5            "ml_timing_cpu",
     1.6            "ml_timing_gc",
     1.7 +          "maximum_code",
     1.8 +          "average_code",
     1.9 +          "maximum_stack",
    1.10 +          "average_stack",
    1.11            "maximum_heap",
    1.12            "average_heap",
    1.13            "stored_heap",
    1.14 @@ -135,6 +139,10 @@
    1.15              entry.ml_timing.elapsed.ms,
    1.16              entry.ml_timing.cpu.ms,
    1.17              entry.ml_timing.gc.ms,
    1.18 +            entry.maximum_code,
    1.19 +            entry.average_code,
    1.20 +            entry.maximum_stack,
    1.21 +            entry.average_stack,
    1.22              entry.maximum_heap,
    1.23              entry.average_heap,
    1.24              entry.stored_heap,
    1.25 @@ -151,6 +159,10 @@
    1.26      afp_version: String,
    1.27      timing: Timing,
    1.28      ml_timing: Timing,
    1.29 +    maximum_code: Long,
    1.30 +    average_code: Long,
    1.31 +    maximum_stack: Long,
    1.32 +    average_stack: Long,
    1.33      maximum_heap: Long,
    1.34      average_heap: Long,
    1.35      stored_heap: Long,
    1.36 @@ -299,9 +311,13 @@
    1.37                      Build_Log.Data.ml_timing_elapsed,
    1.38                      Build_Log.Data.ml_timing_cpu,
    1.39                      Build_Log.Data.ml_timing_gc),
    1.40 -                maximum_heap = ml_stats.maximum_heap_size,
    1.41 -                average_heap = ml_stats.average_heap_size,
    1.42 -                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
    1.43 +                maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong,
    1.44 +                average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong,
    1.45 +                maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong,
    1.46 +                average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong,
    1.47 +                maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong,
    1.48 +                average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
    1.49 +                stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
    1.50                  status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
    1.51                  errors =
    1.52                    Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors),
    1.53 @@ -353,9 +369,6 @@
    1.54      def clean_name(name: String): String =
    1.55        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.56  
    1.57 -    def print_heap(x: Long): Option[String] =
    1.58 -      if (x == 0L) None else Some(x.toString + " M")
    1.59 -
    1.60      HTML.write_document(target_dir, "index.html",
    1.61        List(HTML.title("Isabelle build status")),
    1.62        List(HTML.chapter("Isabelle build status"),
    1.63 @@ -409,7 +422,11 @@
    1.64                        entry.timing.resources.minutes,
    1.65                        entry.ml_timing.elapsed.minutes,
    1.66                        entry.ml_timing.resources.minutes,
    1.67 -                      entry.maximum_heap,
    1.68 +                      entry.maximum_code,
    1.69 +                      entry.maximum_code,
    1.70 +                      entry.average_stack,
    1.71 +                      entry.maximum_stack,
    1.72 +                      entry.average_heap,
    1.73                        entry.average_heap,
    1.74                        entry.stored_heap).mkString(" "))))
    1.75  
    1.76 @@ -530,11 +547,19 @@
    1.77                      List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))),
    1.78                    HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
    1.79                    HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
    1.80 -                print_heap(session.head.maximum_heap).map(s =>
    1.81 +                ML_Statistics.mem_print(session.head.maximum_code).map(s =>
    1.82 +                  HTML.text("maximum code:") -> HTML.text(s)).toList :::
    1.83 +                ML_Statistics.mem_print(session.head.average_code).map(s =>
    1.84 +                  HTML.text("average code:") -> HTML.text(s)).toList :::
    1.85 +                ML_Statistics.mem_print(session.head.maximum_stack).map(s =>
    1.86 +                  HTML.text("maximum stack:") -> HTML.text(s)).toList :::
    1.87 +                ML_Statistics.mem_print(session.head.average_stack).map(s =>
    1.88 +                  HTML.text("average stack:") -> HTML.text(s)).toList :::
    1.89 +                ML_Statistics.mem_print(session.head.maximum_heap).map(s =>
    1.90                    HTML.text("maximum heap:") -> HTML.text(s)).toList :::
    1.91 -                print_heap(session.head.average_heap).map(s =>
    1.92 +                ML_Statistics.mem_print(session.head.average_heap).map(s =>
    1.93                    HTML.text("average heap:") -> HTML.text(s)).toList :::
    1.94 -                print_heap(session.head.stored_heap).map(s =>
    1.95 +                ML_Statistics.mem_print(session.head.stored_heap).map(s =>
    1.96                    HTML.text("stored heap:") -> HTML.text(s)).toList :::
    1.97                  proper_string(session.head.isabelle_version).map(s =>
    1.98                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
     2.1 --- a/src/Pure/ML/ml_statistics.scala	Sat Feb 23 21:32:29 2019 +0100
     2.2 +++ b/src/Pure/ML/ml_statistics.scala	Sat Feb 23 21:33:09 2019 +0100
     2.3 @@ -25,13 +25,22 @@
     2.4    def now(props: Properties.T): Double = Now.unapply(props).get
     2.5  
     2.6  
     2.7 -  /* heap */
     2.8 +  /* memory fields (mega bytes) */
     2.9 +
    2.10 +  def mem_print(x: Long): Option[String] =
    2.11 +    if (x == 0L) None else Some(x.toString + " M")
    2.12 +
    2.13 +  def mem_scale(x: Long): Long = x / 1024 / 1024
    2.14  
    2.15 +  def mem_field_scale(name: String, x: Double): Double =
    2.16 +    if (heap_fields._2.contains(name) || program_fields._2.contains(name))
    2.17 +      mem_scale(x.toLong).toDouble
    2.18 +    else x
    2.19 +
    2.20 +  val CODE_SIZE = "size_code"
    2.21 +  val STACK_SIZE = "size_stacks"
    2.22    val HEAP_SIZE = "size_heap"
    2.23  
    2.24 -  def heap_scale(x: Long): Long = x / 1024 / 1024
    2.25 -  def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong
    2.26 -
    2.27  
    2.28    /* standard fields */
    2.29  
    2.30 @@ -134,7 +143,7 @@
    2.31                (x, y) <- props.iterator ++ speeds.iterator
    2.32                if x != Now.name && domain(x)
    2.33                z = java.lang.Double.parseDouble(y) if z != 0.0
    2.34 -            } yield { (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) })
    2.35 +            } yield { (x.intern, mem_field_scale(x, z)) })
    2.36  
    2.37          result += ML_Statistics.Entry(time, data)
    2.38        }
    2.39 @@ -173,19 +182,14 @@
    2.40      }
    2.41    }
    2.42  
    2.43 -  def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong
    2.44 -  def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong
    2.45 -
    2.46  
    2.47    /* charts */
    2.48  
    2.49    def update_data(data: XYSeriesCollection, selected_fields: List[String])
    2.50    {
    2.51      data.removeAllSeries
    2.52 -    for {
    2.53 -      field <- selected_fields.iterator
    2.54 -      series = new XYSeries(field)
    2.55 -    } {
    2.56 +    for (field <- selected_fields) {
    2.57 +      val series = new XYSeries(field)
    2.58        content.foreach(entry => series.add(entry.time, entry.get(field)))
    2.59        data.addSeries(series)
    2.60      }