# HG changeset patch # User wenzelm # Date 1597324290 -7200 # Node ID 36a34f3a8cb80bbadbe35e8e14148920ff82a672 # Parent d2dc9bc3a3e17dd34aeaa9acc4267713067ab643 support JVM runtime statistics; diff -r d2dc9bc3a3e1 -r 36a34f3a8cb8 src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Thu Aug 13 14:41:28 2020 +0200 +++ b/src/Pure/ML/ml_statistics.scala Thu Aug 13 15:11:30 2020 +0200 @@ -99,8 +99,8 @@ private def consume(props: Properties.T): Unit = synchronized { if (session != null) { - val stats = Session.Runtime_Statistics(session.xml_cache.props(props)) - session.runtime_statistics.post(stats) + val props1 = (session.xml_cache.props(props ::: Platform.jvm_statistics())) + session.runtime_statistics.post(Session.Runtime_Statistics(props1)) } } @@ -172,12 +172,21 @@ private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC") + val java_heap_fields: Fields = + ("Java heap", List("java_heap_size", "java_heap_used")) + + val java_thread_fields: Fields = + ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active")) + val main_fields: List[Fields] = List(heap_fields, tasks_fields, workers_fields) - val all_fields: List[Fields] = - main_fields ::: List(threads_fields, GC_fields, program_fields, time_fields, speed_fields) + val other_fields: List[Fields] = + List(threads_fields, GC_fields, program_fields, time_fields, speed_fields, + java_heap_fields, java_thread_fields) + + val all_fields: List[Fields] = main_fields ::: other_fields /* content interpretation */ diff -r d2dc9bc3a3e1 -r 36a34f3a8cb8 src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Thu Aug 13 14:41:28 2020 +0200 +++ b/src/Pure/System/platform.scala Thu Aug 13 15:11:30 2020 +0200 @@ -68,4 +68,24 @@ /* JVM name */ val jvm_name: String = System.getProperty("java.vm.name", "") + + + /* JVM statistics */ + + def jvm_statistics(): Properties.T = + { + val heap_size = Runtime.getRuntime.totalMemory() + val heap_used = heap_size - Runtime.getRuntime.freeMemory() + + val threads = Thread.activeCount() + val workers = Isabelle_Thread.pool.getPoolSize + val workers_active = Isabelle_Thread.pool.getActiveCount + + List( + "java_heap_size" -> heap_size.toString, + "java_heap_used" -> heap_used.toString, + "java_threads_total" -> threads.toString, + "java_workers_total" -> workers.toString, + "java_workers_active" -> workers_active.toString) + } }