src/Pure/ML/ml_statistics.ML
author wenzelm
Wed, 15 Jul 2020 20:06:45 +0200
changeset 72271 7b112eedc859
parent 72270 bc85d93aad23
child 72341 b9ded33bd58c
permissions -rw-r--r--
more robust wrt. experimental changes in Poly/ML;
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
72268
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
     9
  val set: {tasks_ready: int, tasks_pending: int, tasks_running: int, tasks_passive: int,
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    10
    tasks_urgent: int, workers_total: int, workers_active: int, workers_waiting: int} -> unit
72261
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    11
  val get: unit -> (string * string) list
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    12
  val get_external: int -> (string * string) list
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    13
  val monitor: int -> real -> unit
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    14
end;
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    15
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    16
structure ML_Statistics: ML_STATISTICS =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    17
struct
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    18
72261
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    19
(* print *)
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    20
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    21
fun print_int x = if x < 0 then "-" ^ Int.toString (~ x) else Int.toString x;
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    22
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    23
fun print_real0 x =
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    24
  let val s = Real.fmt (StringCvt.GEN NONE) x in
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    25
    (case String.fields (fn c => c = #".") s of
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    26
      [a, b] => if List.all (fn c => c = #"0") (String.explode b) then a else s
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    27
    | _ => s)
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    28
  end;
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    29
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    30
fun print_real x =
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    31
  if x < 0.0 then "-" ^ print_real0 (~ x) else print_real0 x;
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    32
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    33
val print_properties =
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    34
  String.concatWith "," o map (fn (a, b) => a ^ "=" ^ b);
72261
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    35
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    36
72268
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    37
(* set user properties *)
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    38
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    39
fun set {tasks_ready, tasks_pending, tasks_running, tasks_passive, tasks_urgent,
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    40
    workers_total, workers_active, workers_waiting} =
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    41
 (PolyML.Statistics.setUserCounter (0, tasks_ready);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    42
  PolyML.Statistics.setUserCounter (1, tasks_pending);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    43
  PolyML.Statistics.setUserCounter (2, tasks_running);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    44
  PolyML.Statistics.setUserCounter (3, tasks_passive);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    45
  PolyML.Statistics.setUserCounter (4, tasks_urgent);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    46
  PolyML.Statistics.setUserCounter (5, workers_total);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    47
  PolyML.Statistics.setUserCounter (6, workers_active);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    48
  PolyML.Statistics.setUserCounter (7, workers_waiting));
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    49
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    50
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    51
(* get properties *)
72261
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
    52
72271
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
    53
local
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
    54
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    55
fun make_properties
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    56
   {gcFullGCs,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    57
    gcPartialGCs,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    58
    gcSharePasses,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    59
    sizeAllocation,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    60
    sizeAllocationFree,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    61
    sizeCode,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    62
    sizeHeap,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    63
    sizeHeapFreeLastFullGC,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    64
    sizeHeapFreeLastGC,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    65
    sizeStacks,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    66
    threadsInML,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    67
    threadsTotal,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    68
    threadsWaitCondVar,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    69
    threadsWaitIO,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    70
    threadsWaitMutex,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    71
    threadsWaitSignal,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    72
    timeGCReal,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    73
    timeGCSystem,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    74
    timeGCUser,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    75
    timeNonGCReal,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    76
    timeNonGCSystem,
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
    77
    timeNonGCUser,
72271
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
    78
    userCounters, ...} =
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    79
  let
72268
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    80
    val tasks_ready = Vector.sub (userCounters, 0);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    81
    val tasks_pending = Vector.sub (userCounters, 1);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    82
    val tasks_running = Vector.sub (userCounters, 2);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    83
    val tasks_passive = Vector.sub (userCounters, 3);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    84
    val tasks_urgent = Vector.sub (userCounters, 4);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    85
    val tasks_total = tasks_ready + tasks_pending + tasks_running + tasks_passive + tasks_urgent;
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    86
    val workers_total = Vector.sub (userCounters, 5);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    87
    val workers_active = Vector.sub (userCounters, 6);
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    88
    val workers_waiting = Vector.sub (userCounters, 7);
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    89
  in
72268
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    90
    [("now", print_real (Time.toReal (Time.now ()))),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    91
     ("tasks_ready", print_int tasks_ready),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    92
     ("tasks_pending", print_int tasks_pending),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    93
     ("tasks_running", print_int tasks_running),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    94
     ("tasks_passive", print_int tasks_passive),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    95
     ("tasks_urgent", print_int tasks_urgent),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    96
     ("tasks_total", print_int tasks_total),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    97
     ("workers_total", print_int workers_total),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    98
     ("workers_active", print_int workers_active),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
    99
     ("workers_waiting", print_int workers_waiting),
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
   100
     ("full_GCs", print_int gcFullGCs),
72261
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   101
     ("partial_GCs", print_int gcPartialGCs),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   102
     ("share_passes", print_int gcSharePasses),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   103
     ("size_allocation", print_int sizeAllocation),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   104
     ("size_allocation_free", print_int sizeAllocationFree),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   105
     ("size_code", print_int sizeCode),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   106
     ("size_heap", print_int sizeHeap),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   107
     ("size_heap_free_last_full_GC", print_int sizeHeapFreeLastFullGC),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   108
     ("size_heap_free_last_GC", print_int sizeHeapFreeLastGC),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   109
     ("size_stacks", print_int sizeStacks),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   110
     ("threads_in_ML", print_int threadsInML),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   111
     ("threads_total", print_int threadsTotal),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   112
     ("threads_wait_condvar", print_int threadsWaitCondVar),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   113
     ("threads_wait_IO", print_int threadsWaitIO),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   114
     ("threads_wait_mutex", print_int threadsWaitMutex),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   115
     ("threads_wait_signal", print_int threadsWaitSignal),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   116
     ("time_elapsed", print_real (Time.toReal timeNonGCReal)),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   117
     ("time_elapsed_GC", print_real (Time.toReal timeGCReal)),
b7cec26e41d1 clarified modules: ML_Statistics within bootstrap environment;
wenzelm
parents: 70002
diff changeset
   118
     ("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
72268
254c324f31fd clarified user counters: expose tasks to external monitor;
wenzelm
parents: 72263
diff changeset
   119
     ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))]
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
   120
  end;
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
   121
72271
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
   122
in
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
   123
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   124
fun get () =
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   125
  make_properties (PolyML.Statistics.getLocalStats ());
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   126
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   127
fun get_external pid =
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   128
  make_properties (PolyML.Statistics.getRemoteStats pid);
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   129
72271
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
   130
end;
7b112eedc859 more robust wrt. experimental changes in Poly/ML;
wenzelm
parents: 72270
diff changeset
   131
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   132
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   133
(* monitor process *)
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   134
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   135
fun monitor pid delay =
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   136
  let
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   137
    fun loop () =
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   138
      (TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n");
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   139
       TextIO.flushOut TextIO.stdOut;
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   140
       OS.Process.sleep (Time.fromReal delay);
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   141
       loop ());
72270
bc85d93aad23 more robust: handle unavailable statistics;
wenzelm
parents: 72268
diff changeset
   142
    fun exit () = OS.Process.exit OS.Process.success;
bc85d93aad23 more robust: handle unavailable statistics;
wenzelm
parents: 72268
diff changeset
   143
  in loop () handle Interrupt => exit () | Fail _ => exit () end;
72262
a25c7c686176 support for monitoring of external ML process;
wenzelm
parents: 72261
diff changeset
   144
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
   145
end;