src/Pure/System/java_statistics.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73164 e2132e1553a9
child 77708 f137bf5d3d94
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/java_statistics.scala
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     3
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     4
Java runtime statistics.
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     6
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     8
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
     9
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73164
diff changeset
    10
object Java_Statistics {
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    11
  /* memory status */
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73164
diff changeset
    13
  sealed case class Memory_Status(heap_size: Long, heap_free: Long) {
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    14
    def heap_used: Long = (heap_size - heap_free) max 0
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    15
    def heap_used_fraction: Double =
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    16
      if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    17
  }
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73164
diff changeset
    19
  def memory_status(): Memory_Status = {
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    20
    val heap_size = Runtime.getRuntime.totalMemory()
73164
e2132e1553a9 proper heap_free;
wenzelm
parents: 72250
diff changeset
    21
    val heap_free = Runtime.getRuntime.freeMemory()
e2132e1553a9 proper heap_free;
wenzelm
parents: 72250
diff changeset
    22
    Memory_Status(heap_size, heap_free)
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    23
  }
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    24
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    25
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    26
  /* JVM statistics */
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    27
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73164
diff changeset
    28
  def jvm_statistics(): Properties.T = {
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    29
    val status = memory_status()
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    30
    val threads = Thread.activeCount()
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    31
    val workers = Isabelle_Thread.pool.getPoolSize
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    32
    val workers_active = Isabelle_Thread.pool.getActiveCount
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    33
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    34
    List(
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    35
      "java_heap_size" -> status.heap_size.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    36
      "java_heap_used" -> status.heap_used.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    37
      "java_threads_total" -> threads.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    38
      "java_workers_total" -> workers.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    39
      "java_workers_active" -> workers_active.toString)
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    40
  }
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    41
}