1.1 --- a/src/Pure/Concurrent/future.ML Tue Feb 01 22:24:28 2011 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Wed Feb 02 13:38:09 2011 +0100
1.3 @@ -449,12 +449,12 @@
1.4 else res);
1.5
1.6 fun join_next deps = (*requires SYNCHRONIZED*)
1.7 - if null deps then NONE
1.8 + if Task_Queue.finished_deps deps then NONE
1.9 else
1.10 - (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
1.11 - (NONE, []) => NONE
1.12 - | (NONE, deps') =>
1.13 - (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps')
1.14 + (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of
1.15 + (NONE, deps') =>
1.16 + if Task_Queue.finished_deps deps' then NONE
1.17 + else (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps')
1.18 | (SOME work, deps') => SOME (work, deps'));
1.19
1.20 fun execute_work NONE = ()
1.21 @@ -462,10 +462,6 @@
1.22 and join_work deps =
1.23 execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
1.24
1.25 -fun join_depend task deps =
1.26 - execute_work (SYNCHRONIZED "join" (fn () =>
1.27 - (Unsynchronized.change queue (Task_Queue.depend task deps); join_next deps)));
1.28 -
1.29 in
1.30
1.31 fun join_results xs =
1.32 @@ -474,10 +470,9 @@
1.33 if forall is_finished xs then ()
1.34 else if Multithreading.self_critical () then
1.35 error "Cannot join future values within critical section"
1.36 - else
1.37 - (case worker_task () of
1.38 - SOME task => join_depend task (map task_of xs)
1.39 - | NONE => List.app (ignore o Single_Assignment.await o result_of) xs);
1.40 + else if is_some (thread_data ()) then
1.41 + join_work (Task_Queue.init_deps (map task_of xs))
1.42 + else List.app (ignore o Single_Assignment.await o result_of) xs;
1.43 in map get_result xs end;
1.44
1.45 end;
1.46 @@ -544,7 +539,9 @@
1.47 Unsynchronized.change_result queue
1.48 (Task_Queue.dequeue_passive (Thread.self ()) task));
1.49 in if still_passive then execute (task, group, [job]) else () end);
1.50 - val _ = worker_waiting [task] (fn () => Single_Assignment.await result);
1.51 + val _ =
1.52 + worker_waiting (Task_Queue.init_deps [task])
1.53 + (fn () => Single_Assignment.await result);
1.54 in () end;
1.55
1.56 fun fulfill x res = fulfill_result x (Exn.Result res);