improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
--- a/NEWS Mon Jun 29 19:27:07 2015 +0200
+++ b/NEWS Mon Jun 29 20:55:46 2015 +0200
@@ -7,6 +7,12 @@
New in this Isabelle version
----------------------------
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Improved scheduling for urgent print tasks (e.g. command state output,
+interactive queries) wrt. long-running background tasks.
+
+
*** Isar ***
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jun 29 20:55:46 2015 +0200
@@ -408,7 +408,7 @@
val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
val _ =
- Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
+ Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, output_result} =>
(case try Toplevel.proof_of st of
SOME state =>
let
--- a/src/Pure/Concurrent/future.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jun 29 20:55:46 2015 +0200
@@ -159,7 +159,7 @@
fun report_status () = (*requires SYNCHRONIZED*)
if ! ML_statistics then
let
- val {ready, pending, running, passive} = Task_Queue.status (! queue);
+ val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
val total = length (! workers);
val active = count_workers Working;
val waiting = count_workers Waiting;
@@ -169,6 +169,7 @@
("tasks_pending", Markup.print_int pending),
("tasks_running", Markup.print_int running),
("tasks_passive", Markup.print_int passive),
+ ("tasks_urgent", Markup.print_int urgent),
("workers_total", Markup.print_int total),
("workers_active", Markup.print_int active),
("workers_waiting", Markup.print_int waiting)] @
@@ -245,12 +246,12 @@
(Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ()));
signal work_available;
NONE)
- else if count_workers Working > ! max_active then
- (worker_wait Sleeping work_available; worker_next ())
else
- (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
- NONE => (worker_wait Sleeping work_available; worker_next ())
- | some => (signal work_available; some));
+ let val urgent_only = count_workers Working > ! max_active in
+ (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of
+ NONE => (worker_wait Sleeping work_available; worker_next ())
+ | some => (signal work_available; some))
+ end;
fun worker_loop name =
(case SYNCHRONIZED name (fn () => worker_next ()) of
--- a/src/Pure/Concurrent/task_queue.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Mon Jun 29 20:55:46 2015 +0200
@@ -15,6 +15,7 @@
val group_status: group -> exn list
val str_of_group: group -> string
val str_of_groups: group -> string
+ val urgent_pri: int
type task
val dummy_task: task
val group_of_task: task -> group
@@ -31,7 +32,7 @@
val group_tasks: queue -> group -> task list
val known_task: queue -> task -> bool
val all_passive: queue -> bool
- val status: queue -> {ready: int, pending: int, running: int, passive: 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
@@ -40,7 +41,7 @@
val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
- val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue
+ val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
val dequeue_deps: Thread.thread -> task list -> queue ->
(((task * (bool -> bool) list) option * task list) * queue)
end;
@@ -97,6 +98,8 @@
(* tasks *)
+val urgent_pri = 1000;
+
type timing = Time.time * Time.time * string list; (*run, wait, wait dependencies*)
val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
@@ -214,10 +217,10 @@
(* queue *)
-datatype queue = Queue of {groups: groups, jobs: jobs};
+datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int};
-fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
-val empty = make_queue Inttab.empty Task_Graph.empty;
+fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
+val empty = make_queue Inttab.empty Task_Graph.empty 0;
fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
@@ -233,6 +236,10 @@
else NONE
| ready_job _ = NONE;
+fun ready_job_urgent false = ready_job
+ | ready_job_urgent true = (fn entry as (task, _) =>
+ if pri_of_task task >= urgent_pri then ready_job entry else NONE);
+
fun active_job (task, (Running _, _)) = SOME (task, [])
| active_job arg = ready_job arg;
@@ -241,7 +248,7 @@
(* queue status *)
-fun status (Queue {jobs, ...}) =
+fun status (Queue {jobs, urgent, ...}) =
let
val (x, y, z, w) =
Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
@@ -250,7 +257,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} end;
+ in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
@@ -258,7 +265,7 @@
(* cancel -- peers and sub-groups *)
-fun cancel (Queue {groups, jobs}) group =
+fun cancel (Queue {groups, jobs, ...}) group =
let
val _ = cancel_group group Exn.Interrupt;
val running =
@@ -284,70 +291,75 @@
(* finish *)
-fun finish task (Queue {groups, jobs}) =
+fun finish task (Queue {groups, jobs, urgent}) =
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 maximal = Task_Graph.is_maximal jobs task;
- in (maximal, make_queue groups' jobs') end;
+ in (maximal, make_queue groups' jobs' urgent) end;
(* enroll *)
-fun enroll thread name group (Queue {groups, jobs}) =
+fun enroll thread name group (Queue {groups, jobs, urgent}) =
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') end;
+ in (task, make_queue groups' jobs' urgent) end;
(* enqueue *)
-fun enqueue_passive group abort (Queue {groups, jobs}) =
+fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
let
val task = new_task group "passive" 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') end;
+ in (task, make_queue groups' jobs' urgent) end;
-fun enqueue name group deps pri job (Queue {groups, jobs}) =
+fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =
let
val task = new_task group name (SOME pri);
val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
val jobs' = jobs
|> Task_Graph.new_node (task, Job [job])
|> fold (add_job task) deps;
- in (task, make_queue groups' jobs') end;
+ val urgent' = if pri >= urgent_pri then urgent + 1 else urgent;
+ in (task, make_queue groups' jobs' urgent') end;
-fun extend task job (Queue {groups, jobs}) =
+fun extend task job (Queue {groups, jobs, urgent}) =
(case try (get_job jobs) task of
- SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs))
+ SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent)
| _ => NONE);
(* dequeue *)
-fun dequeue_passive thread task (queue as Queue {groups, jobs}) =
+fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent}) =
(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') end
+ in (SOME true, make_queue groups jobs' urgent) end
| SOME _ => (SOME false, queue)
| NONE => (NONE, queue));
-fun dequeue thread (queue as Queue {groups, jobs}) =
- (case Task_Graph.get_first ready_job jobs of
- SOME (result as (task, _)) =>
- let val jobs' = set_job task (Running thread) jobs
- in (SOME result, make_queue groups jobs') end
- | NONE => (NONE, queue));
+fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent}) =
+ 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
+ | NONE => (NONE, queue))
+ else (NONE, queue);
(* dequeue wrt. dynamic dependencies *)
-fun dequeue_deps thread deps (queue as Queue {groups, jobs}) =
+fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent}) =
let
fun ready [] rest = (NONE, rev rest)
| ready (task :: tasks) rest =
@@ -369,8 +381,10 @@
end;
fun result (res as (task, _)) deps' =
- let val jobs' = set_job task (Running thread) jobs
- in ((SOME res, deps'), make_queue groups jobs') end;
+ 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
(case ready deps [] of
(SOME res, deps') => result res deps'
--- a/src/Pure/ML/ml_compiler_polyml.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Jun 29 20:55:46 2015 +0200
@@ -62,7 +62,8 @@
if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
then
Execution.print
- {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
+ {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
+ output
else output ()
end;
--- a/src/Pure/PIDE/command.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/PIDE/command.ML Mon Jun 29 20:55:46 2015 +0200
@@ -350,7 +350,7 @@
print_function "Execution.print"
(fn {args, exec_id, ...} =>
if null args then
- SOME {delay = NONE, pri = 1, persistent = false, strict = false,
+ SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false,
print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
else NONE);
@@ -358,7 +358,7 @@
print_function "print_state"
(fn {keywords, command_name, ...} =>
if Keyword.is_printed keywords command_name then
- SOME {delay = NONE, pri = 1, persistent = false, strict = false,
+ SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
else NONE);
--- a/src/Pure/PIDE/protocol.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Jun 29 20:55:46 2015 +0200
@@ -94,7 +94,7 @@
(singleton o Future.forks)
{name = "Document.update/remove", group = NONE,
deps = maps Future.group_snapshot (maps Execution.peek removed),
- pri = 1, interrupts = false}
+ pri = Task_Queue.urgent_pri + 2, interrupts = false}
(fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
val _ =
--- a/src/Pure/PIDE/query_operation.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Jun 29 20:55:46 2015 +0200
@@ -7,17 +7,17 @@
signature QUERY_OPERATION =
sig
- val register: string ->
+ val register: {name: string, pri: int} ->
({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
end;
structure Query_Operation: QUERY_OPERATION =
struct
-fun register name f =
+fun register {name, pri} f =
Command.print_function name
(fn {args = instance :: args, ...} =>
- SOME {delay = NONE, pri = 0, persistent = false, strict = false,
+ SOME {delay = NONE, pri = pri, persistent = false, strict = false,
print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
let
fun result s = Output.result [(Markup.instanceN, instance)] [s];
--- a/src/Pure/Tools/find_consts.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML Mon Jun 29 20:55:46 2015 +0200
@@ -163,14 +163,15 @@
(* PIDE query operation *)
val _ =
- Query_Operation.register "find_consts" (fn {state, args, output_result} =>
- (case try Toplevel.context_of state of
- SOME ctxt =>
- let
- val [query_arg] = args;
- val query = read_query Position.none query_arg;
- in output_result (Pretty.string_of (pretty_consts ctxt query)) end
- | NONE => error "Unknown context"));
+ Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
+ (fn {state, args, output_result} =>
+ (case try Toplevel.context_of state of
+ SOME ctxt =>
+ let
+ val [query_arg] = args;
+ val query = read_query Position.none query_arg;
+ in output_result (Pretty.string_of (pretty_consts ctxt query)) end
+ | NONE => error "Unknown context"));
end;
--- a/src/Pure/Tools/find_theorems.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Jun 29 20:55:46 2015 +0200
@@ -547,16 +547,17 @@
(** PIDE query operation **)
val _ =
- Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
- if can Toplevel.context_of st then
- let
- val [limit_arg, allow_dups_arg, query_arg] = args;
- val state = proof_state st;
- val opt_limit = Int.fromString limit_arg;
- val rem_dups = allow_dups_arg = "false";
- val criteria = read_query Position.none query_arg;
- in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
- else error "Unknown context");
+ Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
+ (fn {state = st, args, output_result} =>
+ if can Toplevel.context_of st then
+ let
+ val [limit_arg, allow_dups_arg, query_arg] = args;
+ val state = proof_state st;
+ val opt_limit = Int.fromString limit_arg;
+ val rem_dups = allow_dups_arg = "false";
+ val criteria = read_query Position.none query_arg;
+ in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+ else error "Unknown context");
end;
--- a/src/Pure/Tools/ml_statistics.scala Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/ml_statistics.scala Mon Jun 29 20:55:46 2015 +0200
@@ -34,7 +34,8 @@
/* standard fields */
val tasks_fields =
- ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+ ("Future tasks",
+ List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))
val workers_fields =
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
--- a/src/Pure/Tools/print_operation.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/print_operation.ML Mon Jun 29 20:55:46 2015 +0200
@@ -45,15 +45,16 @@
report ());
val _ =
- Query_Operation.register "print_operation" (fn {state, args, output_result} =>
- let
- val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
- fun err s = Pretty.mark_str (Markup.bad, s);
- fun print name =
- (case AList.lookup (op =) (Synchronized.value print_operations) name of
- SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
- | NONE => [err ("Unknown print operation: " ^ quote name)]);
- in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
+ Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
+ (fn {state, args, output_result} =>
+ let
+ val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
+ fun err s = Pretty.mark_str (Markup.bad, s);
+ fun print name =
+ (case AList.lookup (op =) (Synchronized.value print_operations) name of
+ SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
+ | NONE => [err ("Unknown print operation: " ^ quote name)]);
+ in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
end;