# HG changeset patch # User wenzelm # Date 1525888417 -7200 # Node ID b73678836f8ed1bcbbf3d89814fdbcacaa872921 # Parent 4646124e683e7c384091b8a243c844ab8e286670 record total number of tasks; diff -r 4646124e683e -r b73678836f8e src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed May 09 15:07:20 2018 +0100 +++ b/src/Pure/Concurrent/future.ML Wed May 09 19:53:37 2018 +0200 @@ -171,10 +171,10 @@ fun report_status () = (*requires SYNCHRONIZED*) if ! ML_statistics then let - val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue); - val total = length (! workers); - val active = count_workers Working; - val waiting = count_workers Waiting; + val {ready, pending, running, passive, urgent, total} = 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), @@ -182,9 +182,10 @@ ("tasks_running", Value.print_int running), ("tasks_passive", Value.print_int passive), ("tasks_urgent", Value.print_int urgent), - ("workers_total", Value.print_int total), - ("workers_active", Value.print_int active), - ("workers_waiting", Value.print_int waiting)] @ + ("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 (); in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end else (); diff -r 4646124e683e -r b73678836f8e src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed May 09 15:07:20 2018 +0100 +++ b/src/Pure/Concurrent/task_queue.ML Wed May 09 19:53:37 2018 +0200 @@ -32,7 +32,9 @@ val group_tasks: queue -> group list -> task list val known_task: queue -> task -> bool val all_passive: queue -> bool - val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int} + val total_jobs: queue -> int + val status: queue -> + {ready: int, pending: int, running: int, passive: int, urgent: int, total: int} val cancel: queue -> group -> Thread.thread list val cancel_all: queue -> group list * Thread.thread list val finish: task -> queue -> bool * queue @@ -217,10 +219,12 @@ (* queue *) -datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int}; +datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int, total: int}; -fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent}; -val empty = make_queue Inttab.empty Task_Graph.empty 0; +fun make_queue groups jobs urgent total = + Queue {groups = groups, jobs = jobs, urgent = urgent, total = total}; + +val empty = make_queue Inttab.empty Task_Graph.empty 0 0; fun group_tasks (Queue {groups, ...}) gs = fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g))) @@ -249,10 +253,12 @@ fun all_passive (Queue {jobs, ...}) = is_none (Task_Graph.get_first active_job jobs); +fun total_jobs (Queue {total, ...}) = total; + (* queue status *) -fun status (Queue {jobs, urgent, ...}) = +fun status (Queue {jobs, urgent, total, ...}) = let val (x, y, z, w) = Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) => @@ -261,7 +267,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} end; + in {ready = x, pending = y, running = z, passive = w, urgent = urgent, total = total} end; @@ -295,35 +301,38 @@ (* finish *) -fun finish task (Queue {groups, jobs, urgent}) = +fun finish task (Queue {groups, jobs, urgent, total}) = let val group = group_of_task task; val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups; val jobs' = Task_Graph.del_node task jobs; + val total' = total - 1; val maximal = Task_Graph.is_maximal jobs task; - in (maximal, make_queue groups' jobs' urgent) end; + in (maximal, make_queue groups' jobs' urgent total') end; (* enroll *) -fun enroll thread name group (Queue {groups, jobs, urgent}) = +fun enroll thread name group (Queue {groups, jobs, urgent, total}) = let val task = new_task group name NONE; val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Running thread); - in (task, make_queue groups' jobs' urgent) end; + val total' = total + 1; + in (task, make_queue groups' jobs' urgent total') end; (* enqueue *) -fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) = +fun enqueue_passive group name abort (Queue {groups, jobs, urgent, total}) = let val task = new_task group name NONE; val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Passive abort); - in (task, make_queue groups' jobs' urgent) end; + val total' = total + 1; + in (task, make_queue groups' jobs' urgent total') end; -fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) = +fun enqueue name group deps pri job (Queue {groups, jobs, urgent, total}) = let val task = new_task group name (SOME pri); val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; @@ -331,39 +340,40 @@ |> Task_Graph.new_node (task, Job [job]) |> fold (add_job task) deps; val urgent' = if pri >= urgent_pri then urgent + 1 else urgent; - in (task, make_queue groups' jobs' urgent') end; + val total' = total + 1; + in (task, make_queue groups' jobs' urgent' total') end; -fun extend task job (Queue {groups, jobs, urgent}) = +fun extend task job (Queue {groups, jobs, urgent, total}) = (case try (get_job jobs) task of - SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent) + SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent total) | _ => NONE); (* dequeue *) -fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent}) = +fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent, total}) = (case try (get_job jobs) task of SOME (Passive _) => let val jobs' = set_job task (Running thread) jobs - in (SOME true, make_queue groups jobs' urgent) end + in (SOME true, make_queue groups jobs' urgent total) end | SOME _ => (SOME false, queue) | NONE => (NONE, queue)); -fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent}) = +fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent, total}) = if not urgent_only orelse urgent > 0 then (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of SOME (result as (task, _)) => let val jobs' = set_job task (Running thread) jobs; val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent; - in (SOME result, make_queue groups jobs' urgent') end + in (SOME result, make_queue groups jobs' urgent' total) end | NONE => (NONE, queue)) else (NONE, queue); (* dequeue wrt. dynamic dependencies *) -fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent}) = +fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent, total}) = let fun ready [] rest = (NONE, rev rest) | ready (task :: tasks) rest = @@ -388,7 +398,7 @@ let val jobs' = set_job task (Running thread) jobs; val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent; - in ((SOME res, deps'), make_queue groups jobs' urgent') end; + in ((SOME res, deps'), make_queue groups jobs' urgent' total) end; in (case ready deps [] of (SOME res, deps') => result res deps' diff -r 4646124e683e -r b73678836f8e src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Wed May 09 15:07:20 2018 +0100 +++ b/src/Pure/ML/ml_statistics.scala Wed May 09 19:53:37 2018 +0200 @@ -39,7 +39,8 @@ val tasks_fields: Fields = ("Future tasks", - List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent")) + List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", + "tasks_urgent", "tasks_total")) val workers_fields: Fields = ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))