--- 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 ());