# HG changeset patch # User wenzelm # Date 1248524306 -7200 # Node ID 4fc7a882b41e7f574362d791ed951feeeee962cd # Parent 4086cdd8dd704a251595ea6500f9a460ffb3b806 enqueue: maintain transitive closure, which simplifies dequeue_towards; diff -r 4086cdd8dd70 -r 4fc7a882b41e src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sat Jul 25 13:15:53 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Sat Jul 25 14:18:26 2009 +0200 @@ -94,9 +94,6 @@ fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task); fun set_job task job (jobs: jobs) = Task_Graph.map_node task (fn (group, _) => (group, job)) jobs; -fun add_job task dep (jobs: jobs) = - Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; - (* queue of grouped jobs *) @@ -150,6 +147,12 @@ (* enqueue *) +fun add_job task dep (jobs: jobs) = + Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; + +fun get_deps (jobs: jobs) task = + Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => []; + fun enqueue group deps pri job (Queue {groups, jobs, cache}) = let val task = new_task pri; @@ -157,7 +160,8 @@ |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group); val jobs' = jobs |> Task_Graph.new_node (task, (group, Job [job])) - |> fold (add_job task) deps; + |> fold (add_job task) deps + |> fold (fold (add_job task) o get_deps jobs) deps; val cache' = (case cache of Result last => @@ -205,20 +209,15 @@ then SOME (task, group, rev list) else NONE | _ => NONE); - val tasks = filter (can (Task_Graph.get_node jobs)) deps; - fun result (res as (task, _, _)) = - let - val jobs' = set_job task (Running (Thread.self ())) jobs; - val cache' = Unknown; - in (SOME (res, tasks), make_queue groups jobs' cache') end; in (case get_first ready tasks of - SOME res => result res - | NONE => - (case get_first ready (Task_Graph.all_preds jobs tasks) of - SOME res => result res - | NONE => (NONE, queue))) + SOME (res as (task, _, _)) => + let + val jobs' = set_job task (Running (Thread.self ())) jobs; + val cache' = Unknown; + in (SOME (res, tasks), make_queue groups jobs' cache') end + | NONE => (NONE, queue)) end;