replaced join_all by join_results, which returns Exn.results;
authorwenzelm
Wed, 10 Sep 2008 21:50:30 +0200
changeset 28193 7ed74d0ba607
parent 28192 6d977729c8fa
child 28194 c6dad24124f1
replaced join_all by join_results, which returns Exn.results; join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Sep 10 20:28:01 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Sep 10 21:50:30 2008 +0200
@@ -16,7 +16,7 @@
   val future: group option -> task list -> (unit -> 'a) -> 'a T
   val fork: (unit -> 'a) -> 'a T
   val cancel: 'a T -> unit
-  val join_all: 'a T list -> 'a list
+  val join_results: 'a T list -> 'a Exn.result list
   val join: 'a T -> 'a
 end;
 
@@ -212,8 +212,10 @@
 
 (* join: retrieve results *)
 
-fun join_all xs =
+fun join_results xs =
   let
+    val _ = Multithreading.self_critical () andalso
+      error "Cannot join future values within critical section";
     val _ = scheduler_check ();
 
     fun unfinished () =
@@ -238,14 +240,9 @@
       | SOME (task, _) => SYNCHRONIZED "join" (fn () =>
          (change queue (TaskQueue.depend (unfinished ()) task); active_join ())));
 
-    val res = xs |> map (fn Future {result = ref (SOME res), ...} => res);
-  in
-    (case get_first (fn Exn.Exn Interrupt => NONE | Exn.Exn e => SOME e | _ => NONE) res of
-      NONE => map Exn.release res
-    | SOME e => raise e)
-  end;
+  in xs |> map (fn Future {result = ref (SOME res), ...} => res) end;
 
-fun join x = singleton join_all x;
+fun join x = Exn.release (singleton join_results x);
 
 
 (* termination *)