223 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task; |
223 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task; |
224 |
224 |
225 |
225 |
226 (* job status *) |
226 (* job status *) |
227 |
227 |
228 fun ready_job task (Job list, (deps, _)) = |
228 fun ready_job (task, (Job list, (deps, _))) = |
229 if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE |
229 if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE |
230 | ready_job task (Passive abort, (deps, _)) = |
230 | ready_job (task, (Passive abort, (deps, _))) = |
231 if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task) |
231 if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task) |
232 then SOME (task, [fn _ => abort ()]) |
232 then SOME (task, [fn _ => abort ()]) |
233 else NONE |
233 else NONE |
234 | ready_job _ _ = NONE; |
234 | ready_job _ = NONE; |
235 |
235 |
236 fun active_job (_, (Job _, _)) = SOME () |
236 fun active_job (_, (Job _, _)) = SOME () |
237 | active_job (_, (Running _, _)) = SOME () |
237 | active_job (_, (Running _, _)) = SOME () |
238 | active_job (task, (Passive _, _)) = |
238 | active_job (task, (Passive _, _)) = |
239 if is_canceled (group_of_task task) then SOME () else NONE; |
239 if is_canceled (group_of_task task) then SOME () else NONE; |
338 in (SOME true, make_queue groups jobs') end |
338 in (SOME true, make_queue groups jobs') end |
339 | SOME _ => (SOME false, queue) |
339 | SOME _ => (SOME false, queue) |
340 | NONE => (NONE, queue)); |
340 | NONE => (NONE, queue)); |
341 |
341 |
342 fun dequeue thread (queue as Queue {groups, jobs}) = |
342 fun dequeue thread (queue as Queue {groups, jobs}) = |
343 (case Task_Graph.get_first (uncurry ready_job) jobs of |
343 (case Task_Graph.get_first ready_job jobs of |
344 SOME (result as (task, _)) => |
344 SOME (result as (task, _)) => |
345 let val jobs' = set_job task (Running thread) jobs |
345 let val jobs' = set_job task (Running thread) jobs |
346 in (SOME result, make_queue groups jobs') end |
346 in (SOME result, make_queue groups jobs') end |
347 | NONE => (NONE, queue)); |
347 | NONE => (NONE, queue)); |
348 |
348 |
354 fun ready [] rest = (NONE, rev rest) |
354 fun ready [] rest = (NONE, rev rest) |
355 | ready (task :: tasks) rest = |
355 | ready (task :: tasks) rest = |
356 (case try (Task_Graph.get_entry jobs) task of |
356 (case try (Task_Graph.get_entry jobs) task of |
357 NONE => ready tasks rest |
357 NONE => ready tasks rest |
358 | SOME (_, entry) => |
358 | SOME (_, entry) => |
359 (case ready_job task entry of |
359 (case ready_job (task, entry) of |
360 NONE => ready tasks (task :: rest) |
360 NONE => ready tasks (task :: rest) |
361 | some => (some, fold cons rest tasks))); |
361 | some => (some, fold cons rest tasks))); |
362 |
362 |
363 fun ready_dep _ [] = NONE |
363 fun ready_dep _ [] = NONE |
364 | ready_dep seen (task :: tasks) = |
364 | ready_dep seen (task :: tasks) = |
365 if Tasks.defined seen task then ready_dep seen tasks |
365 if Tasks.defined seen task then ready_dep seen tasks |
366 else |
366 else |
367 let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in |
367 let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in |
368 (case ready_job task entry of |
368 (case ready_job (task, entry) of |
369 NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks) |
369 NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks) |
370 | some => some) |
370 | some => some) |
371 end; |
371 end; |
372 |
372 |
373 fun result (res as (task, _)) deps' = |
373 fun result (res as (task, _)) deps' = |