--- a/src/Pure/Concurrent/future.ML Fri Feb 04 17:25:12 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Feb 04 20:40:25 2011 +0100
@@ -403,19 +403,18 @@
(case group of
NONE => worker_subgroup ()
| SOME grp => grp);
- fun enqueue e (minimal, queue) =
+ fun enqueue e queue =
let
val (result, job) = future_job grp e;
- val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
+ val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
val future = Future {promised = false, task = task, result = result};
- in (future, (minimal orelse minimal', queue')) end;
+ in (future, queue') end;
in
SYNCHRONIZED "enqueue" (fn () =>
let
- val (futures, minimal) =
- Unsynchronized.change_result queue (fn q =>
- let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
- in ((futures, minimal), q') end);
+ val (futures, queue') = fold_map enqueue es (! queue);
+ val _ = queue := queue';
+ val minimal = forall (not o Task_Queue.known_task queue') deps;
val _ = if minimal then signal work_available else ();
val _ = scheduler_check ();
in futures end)
--- a/src/Pure/Concurrent/task_queue.ML Fri Feb 04 17:25:12 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Fri Feb 04 20:40:25 2011 +0100
@@ -26,14 +26,14 @@
val waiting: task -> task list -> (unit -> 'a) -> 'a
type queue
val empty: queue
+ val known_task: queue -> task -> bool
val all_passive: queue -> bool
val status: queue -> {ready: int, pending: int, running: int, passive: int}
val cancel: queue -> group -> bool
val cancel_all: queue -> group list
val finish: task -> queue -> bool * queue
val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
- val enqueue: string -> group -> task list -> int -> (bool -> bool) ->
- queue -> (task * bool) * queue
+ 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 * queue
val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue
@@ -185,6 +185,8 @@
val empty = make_queue Inttab.empty Task_Graph.empty;
+fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
+
(* job status *)
@@ -276,8 +278,7 @@
val jobs' = jobs
|> Task_Graph.new_node (task, Job [job])
|> fold (add_job task) deps;
- val minimal = null (get_deps jobs' task);
- in ((task, minimal), make_queue groups' jobs') end;
+ in (task, make_queue groups' jobs') end;
fun extend task job (Queue {groups, jobs}) =
(case try (get_job jobs) task of