src/Pure/ML/ml_statistics.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 63806 c54a53ef1873
child 69822 8c587dd44f51
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62459
     1
(*  Title:      Pure/ML/ml_statistics.ML
wenzelm@50255
     2
    Author:     Makarius
wenzelm@50255
     3
wenzelm@62945
     4
ML runtime statistics.
wenzelm@50255
     5
*)
wenzelm@50255
     6
wenzelm@50255
     7
signature ML_STATISTICS =
wenzelm@50255
     8
sig
wenzelm@50255
     9
  val get: unit -> Properties.T
wenzelm@50255
    10
end;
wenzelm@50255
    11
wenzelm@50255
    12
structure ML_Statistics: ML_STATISTICS =
wenzelm@50255
    13
struct
wenzelm@50255
    14
wenzelm@50255
    15
fun get () =
wenzelm@50255
    16
  let
wenzelm@50255
    17
    val
wenzelm@50255
    18
     {gcFullGCs,
wenzelm@50255
    19
      gcPartialGCs,
wenzelm@50255
    20
      sizeAllocation,
wenzelm@50255
    21
      sizeAllocationFree,
wenzelm@50255
    22
      sizeHeap,
wenzelm@50255
    23
      sizeHeapFreeLastFullGC,
wenzelm@50255
    24
      sizeHeapFreeLastGC,
wenzelm@50255
    25
      threadsInML,
wenzelm@50255
    26
      threadsTotal,
wenzelm@50255
    27
      threadsWaitCondVar,
wenzelm@50255
    28
      threadsWaitIO,
wenzelm@50255
    29
      threadsWaitMutex,
wenzelm@50255
    30
      threadsWaitSignal,
wenzelm@50255
    31
      timeGCSystem,
wenzelm@50255
    32
      timeGCUser,
wenzelm@50255
    33
      timeNonGCSystem,
wenzelm@50255
    34
      timeNonGCUser,
wenzelm@50656
    35
      userCounters} = PolyML.Statistics.getLocalStats ();
wenzelm@50656
    36
    val user_counters =
wenzelm@50656
    37
      Vector.foldri
wenzelm@63806
    38
        (fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
wenzelm@50656
    39
        [] userCounters;
wenzelm@50255
    40
  in
wenzelm@63806
    41
    [("full_GCs", Value.print_int gcFullGCs),
wenzelm@63806
    42
     ("partial_GCs", Value.print_int gcPartialGCs),
wenzelm@63806
    43
     ("size_allocation", Value.print_int sizeAllocation),
wenzelm@63806
    44
     ("size_allocation_free", Value.print_int sizeAllocationFree),
wenzelm@63806
    45
     ("size_heap", Value.print_int sizeHeap),
wenzelm@63806
    46
     ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
wenzelm@63806
    47
     ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
wenzelm@63806
    48
     ("threads_in_ML", Value.print_int threadsInML),
wenzelm@63806
    49
     ("threads_total", Value.print_int threadsTotal),
wenzelm@63806
    50
     ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
wenzelm@63806
    51
     ("threads_wait_IO", Value.print_int threadsWaitIO),
wenzelm@63806
    52
     ("threads_wait_mutex", Value.print_int threadsWaitMutex),
wenzelm@63806
    53
     ("threads_wait_signal", Value.print_int threadsWaitSignal),
wenzelm@63806
    54
     ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
wenzelm@63806
    55
     ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
wenzelm@50656
    56
    user_counters
wenzelm@50255
    57
  end;
wenzelm@50255
    58
wenzelm@50255
    59
end;