equal
deleted
inserted
replaced
255 | (alive, dead) => |
255 | (alive, dead) => |
256 (workers := alive; Multithreading.tracing 0 (fn () => |
256 (workers := alive; Multithreading.tracing 0 (fn () => |
257 "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads"))); |
257 "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads"))); |
258 |
258 |
259 val m = if ! do_shutdown then 0 else Multithreading.max_threads_value (); |
259 val m = if ! do_shutdown then 0 else Multithreading.max_threads_value (); |
260 val mm = if m = 9999 then 1 else (m * 3) div 2; |
260 val mm = if m = 9999 then 1 else m * 2; |
261 val l = length (! workers); |
261 val l = length (! workers); |
262 val _ = excessive := l - mm; |
262 val _ = excessive := l - mm; |
263 val _ = |
263 val _ = |
264 if mm > l then |
264 if mm > l then |
265 funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) () |
265 funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) () |