equal
deleted
inserted
replaced
183 val _ = |
183 val _ = |
184 if ok then () |
184 if ok then () |
185 else if Task_Queue.cancel (! queue) group then () |
185 else if Task_Queue.cancel (! queue) group then () |
186 else do_cancel group; |
186 else do_cancel group; |
187 val _ = broadcast work_finished; |
187 val _ = broadcast work_finished; |
188 val _ = if maximal then () else broadcast work_available; |
188 val _ = if maximal then () else signal work_available; |
189 in () end); |
189 in () end); |
190 in () end; |
190 in () end; |
191 |
191 |
192 |
192 |
193 (* worker threads *) |
193 (* worker threads *) |
214 worker_wait false scheduler_event; |
214 worker_wait false scheduler_event; |
215 worker_next false) |
215 worker_next false) |
216 else |
216 else |
217 (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of |
217 (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of |
218 NONE => (worker_wait false work_available; worker_next true) |
218 NONE => (worker_wait false work_available; worker_next true) |
219 | some => some); |
219 | some => (signal work_available; some)); |
220 |
220 |
221 fun worker_loop name = |
221 fun worker_loop name = |
222 (case SYNCHRONIZED name (fn () => worker_next false) of |
222 (case SYNCHRONIZED name (fn () => worker_next false) of |
223 NONE => () |
223 NONE => () |
224 | SOME work => (execute work; worker_loop name)); |
224 | SOME work => (execute work; worker_loop name)); |
279 val _ = max_active := m; |
279 val _ = max_active := m; |
280 |
280 |
281 val mm = |
281 val mm = |
282 if ! do_shutdown then 0 |
282 if ! do_shutdown then 0 |
283 else if m = 9999 then 1 |
283 else if m = 9999 then 1 |
284 else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 2 * m); |
284 else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m); |
285 val _ = |
285 val _ = |
286 if tick andalso mm > ! max_workers then |
286 if tick andalso mm > ! max_workers then |
287 Unsynchronized.change worker_trend (fn w => if w < 0 then 0 else w + 1) |
287 Unsynchronized.change worker_trend (fn w => if w < 0 then 0 else w + 1) |
288 else if tick andalso mm < ! max_workers then |
288 else if tick andalso mm < ! max_workers then |
289 Unsynchronized.change worker_trend (fn w => if w > 0 then 0 else w - 1) |
289 Unsynchronized.change worker_trend (fn w => if w > 0 then 0 else w - 1) |
290 else (); |
290 else (); |
291 val _ = |
291 val _ = |
292 if mm = 0 orelse ! worker_trend > 5 orelse ! worker_trend < ~50 |
292 if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then max_workers := mm |
293 then max_workers := mm |
293 else if ! worker_trend > 5 then max_workers := Int.min (mm, 2 * m) |
294 else (); |
294 else (); |
295 |
295 |
296 val missing = ! max_workers - length (! workers); |
296 val missing = ! max_workers - length (! workers); |
297 val _ = |
297 val _ = |
298 if missing > 0 then |
298 if missing > 0 then |