318 fun future_schedule task_graph = |
318 fun future_schedule task_graph = |
319 let |
319 let |
320 val tasks = Graph.topological_order task_graph |> map_filter (fn name => |
320 val tasks = Graph.topological_order task_graph |> map_filter (fn name => |
321 (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE)); |
321 (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE)); |
322 |
322 |
323 val group = TaskQueue.new_group (); |
|
324 fun future (name, body) tab = |
323 fun future (name, body) tab = |
325 let |
324 let |
|
325 val group = TaskQueue.new_group (); |
326 val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name); |
326 val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name); |
327 val x = Future.future (SOME group) deps true body; |
327 val x = Future.future (SOME group) deps true body; |
328 in (x, Symtab.update (name, Future.task_of x) tab) end; |
328 in (x, Symtab.update (name, Future.task_of x) tab) end; |
329 |
329 in |
330 val exns = #1 (fold_map future tasks Symtab.empty) |
330 #1 (fold_map future tasks Symtab.empty) |
331 |> uninterruptible (fn _ => Future.join_results) |
331 |> uninterruptible (fn _ => Future.join_results) |
332 |> map_filter Exn.get_exn; |
332 |> Exn.release_all |
333 in |
333 |> ignore |
334 if null exns then () |
|
335 else raise Exn.EXCEPTIONS (exns, "") |
|
336 end; |
334 end; |
337 |
335 |
338 local |
336 local |
339 |
337 |
340 fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m)) |
338 fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m)) |
370 if m <= 1 then schedule_seq tasks |
368 if m <= 1 then schedule_seq tasks |
371 else if Multithreading.self_critical () then |
369 else if Multithreading.self_critical () then |
372 (warning (loader_msg "no multithreading within critical section" []); |
370 (warning (loader_msg "no multithreading within critical section" []); |
373 schedule_seq tasks) |
371 schedule_seq tasks) |
374 else if ! future_scheduler then future_schedule tasks |
372 else if ! future_scheduler then future_schedule tasks |
375 else |
373 else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks))) |
376 (case Schedule.schedule (Int.min (m, n)) next_task tasks of |
|
377 [] => () |
|
378 | exns => raise Exn.EXCEPTIONS (exns, "")) |
|
379 end; |
374 end; |
380 |
375 |
381 end; |
376 end; |
382 |
377 |
383 |
378 |