# HG changeset patch # User wenzelm # Date 1596636997 -7200 # Node ID 41e1e2395a67e9ab01a23d428d91fc02dc2481a6 # Parent 3afd6b1c7ab5aba8f744ebef52c7bf5376faba54 avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node; diff -r 3afd6b1c7ab5 -r 41e1e2395a67 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Aug 05 12:42:43 2020 +0200 +++ b/src/Pure/Concurrent/future.ML Wed Aug 05 16:16:37 2020 +0200 @@ -320,11 +320,14 @@ val max_active0 = ! max_active; val max_workers0 = ! max_workers; + val workers_waiting = count_workers Waiting; + val m = if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0 else Multithreading.max_threads (); val _ = max_active := m; - val _ = max_workers := 2 * m; + val _ = max_workers := + Int.max (2 * m, if workers_waiting > 0 then workers_waiting + 1 else 0); val missing = ! max_workers - length (! workers); val _ =