src/Pure/ML/ml_statistics.ML
author nipkow
Tue, 05 Nov 2019 14:57:41 +0100
changeset 71033 c1b63124245c
parent 69822 8c587dd44f51
child 72031 b7cec26e41d1
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62459
7a5d88dd8cc9 support only polyml-5.3.0 and polyml-5.6;
wenzelm
parents: 51990
diff changeset
     1
(*  Title:      Pure/ML/ml_statistics.ML
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     3
62945
c38c08889aa9 tuned comments;
wenzelm
parents: 62459
diff changeset
     4
ML runtime statistics.
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     5
*)
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     6
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     7
signature ML_STATISTICS =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     8
sig
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     9
  val get: unit -> Properties.T
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    10
end;
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    11
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    12
structure ML_Statistics: ML_STATISTICS =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    13
struct
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    14
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    15
fun get () =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    16
  let
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    17
    val
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    18
     {gcFullGCs,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    19
      gcPartialGCs,
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    20
      gcSharePasses,
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    21
      sizeAllocation,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    22
      sizeAllocationFree,
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    23
      sizeCode,
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    24
      sizeHeap,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    25
      sizeHeapFreeLastFullGC,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    26
      sizeHeapFreeLastGC,
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    27
      sizeStacks,
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    28
      threadsInML,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    29
      threadsTotal,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    30
      threadsWaitCondVar,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    31
      threadsWaitIO,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    32
      threadsWaitMutex,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    33
      threadsWaitSignal,
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    34
      timeGCReal,
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    35
      timeGCSystem,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    36
      timeGCUser,
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    37
      timeNonGCReal,
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    38
      timeNonGCSystem,
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    39
      timeNonGCUser,
50656
561d79d7031f include user counters as well;
wenzelm
parents: 50280
diff changeset
    40
      userCounters} = PolyML.Statistics.getLocalStats ();
561d79d7031f include user counters as well;
wenzelm
parents: 50280
diff changeset
    41
    val user_counters =
561d79d7031f include user counters as well;
wenzelm
parents: 50280
diff changeset
    42
      Vector.foldri
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    43
        (fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
50656
561d79d7031f include user counters as well;
wenzelm
parents: 50280
diff changeset
    44
        [] userCounters;
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    45
  in
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    46
    [("full_GCs", Value.print_int gcFullGCs),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    47
     ("partial_GCs", Value.print_int gcPartialGCs),
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    48
     ("share_passes", Value.print_int gcSharePasses),
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    49
     ("size_allocation", Value.print_int sizeAllocation),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    50
     ("size_allocation_free", Value.print_int sizeAllocationFree),
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    51
     ("size_code", Value.print_int sizeCode),
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    52
     ("size_heap", Value.print_int sizeHeap),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    53
     ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    54
     ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    55
     ("size_stacks", Value.print_int sizeStacks),
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    56
     ("threads_in_ML", Value.print_int threadsInML),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    57
     ("threads_total", Value.print_int threadsTotal),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    58
     ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    59
     ("threads_wait_IO", Value.print_int threadsWaitIO),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    60
     ("threads_wait_mutex", Value.print_int threadsWaitMutex),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    61
     ("threads_wait_signal", Value.print_int threadsWaitSignal),
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    62
     ("time_elapsed", Value.print_real (Time.toReal timeNonGCReal)),
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 63806
diff changeset
    63
     ("time_elapsed_GC", Value.print_real (Time.toReal timeGCReal)),
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    64
     ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
c54a53ef1873 clarified modules;
wenzelm
parents: 62945
diff changeset
    65
     ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
50656
561d79d7031f include user counters as well;
wenzelm
parents: 50280
diff changeset
    66
    user_counters
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    67
  end;
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    68
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    69
end;