clarified user counters: expose tasks to external monitor;
authorwenzelm
Wed, 15 Jul 2020 16:10:43 +0200
changeset 72268 254c324f31fd
parent 72267 aa6a36c730c9
child 72269 c6756adfef0f
clarified user counters: expose tasks to external monitor;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/ML/ml_statistics.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jul 15 12:43:36 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Jul 15 16:10:43 2020 +0200
@@ -176,22 +176,21 @@
 fun report_status () = (*requires SYNCHRONIZED*)
   if ! ML_statistics then
     let
-      val {ready, pending, running, passive, urgent, total} = Task_Queue.status (! queue);
+      val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
       val workers_total = length (! workers);
       val workers_active = count_workers Working;
       val workers_waiting = count_workers Waiting;
-      val stats =
-       [("now", Value.print_real (Time.toReal (Time.now ()))),
-        ("tasks_ready", Value.print_int ready),
-        ("tasks_pending", Value.print_int pending),
-        ("tasks_running", Value.print_int running),
-        ("tasks_passive", Value.print_int passive),
-        ("tasks_urgent", Value.print_int urgent),
-        ("tasks_total", Value.print_int total),
-        ("workers_total", Value.print_int workers_total),
-        ("workers_active", Value.print_int workers_active),
-        ("workers_waiting", Value.print_int workers_waiting)] @
-        ML_Statistics.get ();
+      val _ =
+        ML_Statistics.set
+         {tasks_ready = ready,
+          tasks_pending = pending,
+          tasks_running = running,
+          tasks_passive = passive,
+          tasks_urgent = urgent,
+          workers_total = workers_total,
+          workers_active = workers_active,
+          workers_waiting = workers_waiting};
+      val stats = ML_Statistics.get ();
     in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
   else ();
 
--- a/src/Pure/Concurrent/task_queue.ML	Wed Jul 15 12:43:36 2020 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Jul 15 16:10:43 2020 +0200
@@ -34,8 +34,7 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val total_jobs: queue -> int
-  val status: queue ->
-    {ready: int, pending: int, running: int, passive: int, urgent: int, total: int}
+  val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
   val cancel: queue -> group -> Thread.thread list
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
@@ -278,7 +277,7 @@
 
 (* queue status *)
 
-fun status (Queue {jobs, urgent, total, ...}) =
+fun status (Queue {jobs, urgent, ...}) =
   let
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
@@ -287,7 +286,7 @@
           | Running _ => (x, y, z + 1, w)
           | Passive _ => (x, y, z, w + 1)))
         jobs (0, 0, 0, 0);
-  in {ready = x, pending = y, running = z, passive = w, urgent = urgent, total = total} end;
+  in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
 
 
 
--- a/src/Pure/ML/ml_statistics.ML	Wed Jul 15 12:43:36 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Wed Jul 15 16:10:43 2020 +0200
@@ -6,6 +6,8 @@
 
 signature ML_STATISTICS =
 sig
+  val set: {tasks_ready: int, tasks_pending: int, tasks_running: int, tasks_passive: int,
+    tasks_urgent: int, workers_total: int, workers_active: int, workers_waiting: int} -> unit
   val get: unit -> (string * string) list
   val get_external: int -> (string * string) list
   val monitor: int -> real -> unit
@@ -32,7 +34,21 @@
   String.concatWith "," o map (fn (a, b) => a ^ "=" ^ b);
 
 
-(* make properties *)
+(* set user properties *)
+
+fun set {tasks_ready, tasks_pending, tasks_running, tasks_passive, tasks_urgent,
+    workers_total, workers_active, workers_waiting} =
+ (PolyML.Statistics.setUserCounter (0, tasks_ready);
+  PolyML.Statistics.setUserCounter (1, tasks_pending);
+  PolyML.Statistics.setUserCounter (2, tasks_running);
+  PolyML.Statistics.setUserCounter (3, tasks_passive);
+  PolyML.Statistics.setUserCounter (4, tasks_urgent);
+  PolyML.Statistics.setUserCounter (5, workers_total);
+  PolyML.Statistics.setUserCounter (6, workers_active);
+  PolyML.Statistics.setUserCounter (7, workers_waiting));
+
+
+(* get properties *)
 
 fun make_properties
    {gcFullGCs,
@@ -59,12 +75,27 @@
     timeNonGCUser,
     userCounters} =
   let
-    val user_counters =
-      Vector.foldri
-        (fn (i, j, res) => ("user_counter" ^ print_int i, print_int j) :: res)
-        [] userCounters;
+    val tasks_ready = Vector.sub (userCounters, 0);
+    val tasks_pending = Vector.sub (userCounters, 1);
+    val tasks_running = Vector.sub (userCounters, 2);
+    val tasks_passive = Vector.sub (userCounters, 3);
+    val tasks_urgent = Vector.sub (userCounters, 4);
+    val tasks_total = tasks_ready + tasks_pending + tasks_running + tasks_passive + tasks_urgent;
+    val workers_total = Vector.sub (userCounters, 5);
+    val workers_active = Vector.sub (userCounters, 6);
+    val workers_waiting = Vector.sub (userCounters, 7);
   in
-    [("full_GCs", print_int gcFullGCs),
+    [("now", print_real (Time.toReal (Time.now ()))),
+     ("tasks_ready", print_int tasks_ready),
+     ("tasks_pending", print_int tasks_pending),
+     ("tasks_running", print_int tasks_running),
+     ("tasks_passive", print_int tasks_passive),
+     ("tasks_urgent", print_int tasks_urgent),
+     ("tasks_total", print_int tasks_total),
+     ("workers_total", print_int workers_total),
+     ("workers_active", print_int workers_active),
+     ("workers_waiting", print_int workers_waiting),
+     ("full_GCs", print_int gcFullGCs),
      ("partial_GCs", print_int gcPartialGCs),
      ("share_passes", print_int gcSharePasses),
      ("size_allocation", print_int sizeAllocation),
@@ -83,13 +114,9 @@
      ("time_elapsed", print_real (Time.toReal timeNonGCReal)),
      ("time_elapsed_GC", print_real (Time.toReal timeGCReal)),
      ("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
-    user_counters
+     ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))]
   end;
 
-
-(* get properties *)
-
 fun get () =
   make_properties (PolyML.Statistics.getLocalStats ());