# HG changeset patch # User wenzelm # Date 1594822243 -7200 # Node ID 254c324f31fd1572c1a34dad3966e7e7480dc812 # Parent aa6a36c730c97fbba69fa72f6a7821b14c4ec1da clarified user counters: expose tasks to external monitor; diff -r aa6a36c730c9 -r 254c324f31fd src/Pure/Concurrent/future.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 (); diff -r aa6a36c730c9 -r 254c324f31fd src/Pure/Concurrent/task_queue.ML --- 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; diff -r aa6a36c730c9 -r 254c324f31fd src/Pure/ML/ml_statistics.ML --- 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 ());