src/Pure/Concurrent/future.ML
changeset 42561 b5d7b15166bf
parent 42560 a4c822915eaa
child 42563 73dde8006820
     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);