Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
authorwenzelm
Thu, 23 Jun 2011 23:12:00 +0200
changeset 43538 de5c79682b56
parent 43537 80803078552e
child 43539 c49d8f40ba51
child 43543 eb8b4851b039
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
src/Pure/Concurrent/future.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Concurrent/future.ML	Thu Jun 23 23:05:38 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Jun 23 23:12:00 2011 +0200
@@ -454,7 +454,8 @@
 fun execute_work NONE = ()
   | execute_work (SOME (work, deps')) = (worker_joining (fn () => execute work); join_work deps')
 and join_work deps =
-  execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
+  Multithreading.with_attributes Multithreading.no_interrupts
+    (fn _ => execute_work (SYNCHRONIZED "join" (fn () => join_next deps)));
 
 in
isabelle