| 72250 |      1 | /*  Title:      Pure/System/java_statistics.scala
 | 
|  |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | Java runtime statistics.
 | 
|  |      5 | */
 | 
|  |      6 | 
 | 
|  |      7 | package isabelle
 | 
|  |      8 | 
 | 
|  |      9 | 
 | 
|  |     10 | object Java_Statistics
 | 
|  |     11 | {
 | 
|  |     12 |   /* memory status */
 | 
|  |     13 | 
 | 
|  |     14 |   sealed case class Memory_Status(heap_size: Long, heap_free: Long)
 | 
|  |     15 |   {
 | 
|  |     16 |     def heap_used: Long = (heap_size - heap_free) max 0
 | 
|  |     17 |     def heap_used_fraction: Double =
 | 
|  |     18 |       if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
 | 
|  |     19 |   }
 | 
|  |     20 | 
 | 
|  |     21 |   def memory_status(): Memory_Status =
 | 
|  |     22 |   {
 | 
|  |     23 |     val heap_size = Runtime.getRuntime.totalMemory()
 | 
| 73164 |     24 |     val heap_free = Runtime.getRuntime.freeMemory()
 | 
|  |     25 |     Memory_Status(heap_size, heap_free)
 | 
| 72250 |     26 |   }
 | 
|  |     27 | 
 | 
|  |     28 | 
 | 
|  |     29 |   /* JVM statistics */
 | 
|  |     30 | 
 | 
|  |     31 |   def jvm_statistics(): Properties.T =
 | 
|  |     32 |   {
 | 
|  |     33 |     val status = memory_status()
 | 
|  |     34 |     val threads = Thread.activeCount()
 | 
|  |     35 |     val workers = Isabelle_Thread.pool.getPoolSize
 | 
|  |     36 |     val workers_active = Isabelle_Thread.pool.getActiveCount
 | 
|  |     37 | 
 | 
|  |     38 |     List(
 | 
|  |     39 |       "java_heap_size" -> status.heap_size.toString,
 | 
|  |     40 |       "java_heap_used" -> status.heap_used.toString,
 | 
|  |     41 |       "java_threads_total" -> threads.toString,
 | 
|  |     42 |       "java_workers_total" -> workers.toString,
 | 
|  |     43 |       "java_workers_active" -> workers_active.toString)
 | 
|  |     44 |   }
 | 
|  |     45 | }
 |