src/Pure/System/java_statistics.scala
author wenzelm
Thu, 06 Jun 2024 22:03:20 +0200
changeset 80271 198fc882ec0f
parent 77708 f137bf5d3d94
permissions -rw-r--r--
tuned whitespace;
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
77708
f137bf5d3d94 clarified signature: more explicit types;
wenzelm
parents: 75393
diff changeset
    13
  sealed case class Memory_Status(heap_size: Space, heap_free: Space) {
f137bf5d3d94 clarified signature: more explicit types;
wenzelm
parents: 75393
diff changeset
    14
    def heap_used: Space = heap_size.used(heap_free)
f137bf5d3d94 clarified signature: more explicit types;
wenzelm
parents: 75393
diff changeset
    15
    def heap_used_fraction: Double = heap_size.used_fraction(heap_free)
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    16
  }
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73164
diff changeset
    18
  def memory_status(): Memory_Status = {
77708
f137bf5d3d94 clarified signature: more explicit types;
wenzelm
parents: 75393
diff changeset
    19
    val heap_size = Space.bytes(Runtime.getRuntime.totalMemory())
f137bf5d3d94 clarified signature: more explicit types;
wenzelm
parents: 75393
diff changeset
    20
    val heap_free = Space.bytes(Runtime.getRuntime.freeMemory())
73164
e2132e1553a9 proper heap_free;
wenzelm
parents: 72250
diff changeset
    21
    Memory_Status(heap_size, heap_free)
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    22
  }
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    23
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    24
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    25
  /* JVM statistics */
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    26
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73164
diff changeset
    27
  def jvm_statistics(): Properties.T = {
72250
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    28
    val status = memory_status()
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    29
    val threads = Thread.activeCount()
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    30
    val workers = Isabelle_Thread.pool.getPoolSize
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    31
    val workers_active = Isabelle_Thread.pool.getActiveCount
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    32
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    33
    List(
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    34
      "java_heap_size" -> status.heap_size.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    35
      "java_heap_used" -> status.heap_used.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    36
      "java_threads_total" -> threads.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    37
      "java_workers_total" -> workers.toString,
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    38
      "java_workers_active" -> workers_active.toString)
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    39
  }
13976f92a2d0 clarified modules;
wenzelm
parents:
diff changeset
    40
}