# HG changeset patch # User haftmann # Date 1244963511 -7200 # Node ID bc2de379575670ea67d9ba532814249b08e23926 # Parent 924f3169ed62bf4e7e641fc9ad769eabed26619b# Parent fe35b72b9ef02ed9afcb053b490f9491868f3c8c merged diff -r fe35b72b9ef0 -r bc2de3795756 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Sat Jun 13 16:32:38 2009 +0200 +++ b/Admin/isatest/isatest-makedist Sun Jun 14 09:11:51 2009 +0200 @@ -106,11 +106,11 @@ sleep 15 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly" sleep 15 -$SSH macbroy2 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para; $MAKEALL $HOME/settings/mac-poly-M8" +$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8" sleep 15 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly" sleep 15 -$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly-M4" +$SSH macbroy6 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para" sleep 15 $SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly" diff -r fe35b72b9ef0 -r bc2de3795756 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Sat Jun 13 16:32:38 2009 +0200 +++ b/Admin/isatest/isatest-stats Sun Jun 14 09:11:51 2009 +0200 @@ -6,7 +6,7 @@ THIS=$(cd "$(dirname "$0")"; pwd -P) -PLATFORMS="at-poly at64-poly at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev" +PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev" ISABELLE_SESSIONS="\ HOL-Plain \ diff -r fe35b72b9ef0 -r bc2de3795756 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sat Jun 13 16:32:38 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Sun Jun 14 09:11:51 2009 +0200 @@ -276,17 +276,21 @@ fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x); -fun join_next pending = (*requires SYNCHRONIZED*) - if forall is_finished pending then NONE +fun join_wait x = + while not (is_finished x) + do SYNCHRONIZED "join_wait" (fn () => wait ()); + +fun join_next x = (*requires SYNCHRONIZED*) + if is_finished x then NONE else (case change_result queue Task_Queue.dequeue of - NONE => (worker_wait (); join_next pending) + NONE => (worker_wait (); join_next x) | some => some); -fun join_loop name pending = - (case SYNCHRONIZED name (fn () => join_next pending) of +fun join_loop x = + (case SYNCHRONIZED "join" (fn () => join_next x) of NONE => () - | SOME work => (execute name work; join_loop name pending)); + | SOME work => (execute "join" work; join_loop x)); in @@ -298,28 +302,16 @@ val _ = Multithreading.self_critical () andalso error "Cannot join future values within critical section"; - fun join_deps _ [] = () - | join_deps name deps = - (case SYNCHRONIZED name (fn () => - change_result queue (Task_Queue.dequeue_towards deps)) of - NONE => () - | SOME (work, deps') => (execute name work; join_deps name deps')); - val _ = (case thread_data () of - NONE => - (*alien thread -- refrain from contending for resources*) - while not (forall is_finished xs) - do SYNCHRONIZED "join_thread" (fn () => wait ()) - | SOME (name, task) => - (*proper task -- actively work towards results*) + NONE => List.app join_wait xs (*alien thread -- refrain from contending for resources*) + | SOME (name, task) => (*proper task -- continue work*) let val pending = filter_out is_finished xs; val deps = map task_of pending; val _ = SYNCHRONIZED "join" (fn () => (change queue (Task_Queue.depend deps task); notify_all ())); - val _ = join_deps ("join_deps: " ^ name) deps; - val _ = join_loop ("join_loop: " ^ name) (filter_out is_finished pending); + val _ = List.app join_loop pending; in () end); in map get_result xs end) (); diff -r fe35b72b9ef0 -r bc2de3795756 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sat Jun 13 16:32:38 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Sun Jun 14 09:11:51 2009 +0200 @@ -23,8 +23,6 @@ val extend: task -> (bool -> bool) -> queue -> queue option val depend: task list -> task -> queue -> queue val dequeue: queue -> (task * group * (bool -> bool) list) option * queue - val dequeue_towards: task list -> queue -> - (((task * group * (bool -> bool) list) * task list) option * queue) val interrupt: queue -> task -> unit val interrupt_external: queue -> string -> unit val cancel: queue -> group -> bool @@ -82,69 +80,59 @@ (* queue of grouped jobs *) +datatype result = Unknown | Result of task | No_Result; + datatype queue = Queue of {groups: task list Inttab.table, (*groups with presently active members*) - jobs: jobs}; (*job dependency graph*) + jobs: jobs, (*job dependency graph*) + cache: result}; (*last dequeue result*) -fun make_queue groups jobs = Queue {groups = groups, jobs = jobs}; +fun make_queue groups jobs cache = Queue {groups = groups, jobs = jobs, cache = cache}; -val empty = make_queue Inttab.empty Task_Graph.empty; +val empty = make_queue Inttab.empty Task_Graph.empty No_Result; fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs; (* enqueue *) -fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs}) = +fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, ...}) = let val task = new_task pri; val groups' = Inttab.cons_list (gid, task) groups; val jobs' = jobs |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps; - in (task, make_queue groups' jobs') end; + in (task, make_queue groups' jobs' Unknown) end; -fun extend task job (Queue {groups, jobs}) = +fun extend task job (Queue {groups, jobs, cache}) = (case try (get_job jobs) task of - SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs)) + SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) cache) | _ => NONE); -fun depend deps task (Queue {groups, jobs}) = - make_queue groups (fold (add_job_acyclic task) deps jobs); +fun depend deps task (Queue {groups, jobs, ...}) = + make_queue groups (fold (add_job_acyclic task) deps jobs) Unknown; (* dequeue *) -local - -fun dequeue_result NONE queue = (NONE, queue) - | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs}) = - (SOME result, make_queue groups (set_job task (Running (Thread.self ())) jobs)); - -in - -fun dequeue (queue as Queue {jobs, ...}) = +fun dequeue (queue as Queue {groups, jobs, cache}) = let fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list) | ready _ = NONE; - in dequeue_result (Task_Graph.get_first ready jobs) queue end; - -fun dequeue_towards tasks (queue as Queue {jobs, ...}) = - let - val tasks' = filter (can (Task_Graph.get_node jobs)) tasks; - - fun ready task = - (case Task_Graph.get_node jobs task of - (group, Job list) => - if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list) - else NONE - | _ => NONE); + fun deq boundary = + (case Task_Graph.get_first boundary ready jobs of + NONE => (NONE, make_queue groups jobs No_Result) + | SOME (result as (task, _, _)) => + let + val jobs' = set_job task (Running (Thread.self ())) jobs; + val cache' = Result task; + in (SOME result, make_queue groups jobs' cache') end); in - (case dequeue_result (get_first ready (Task_Graph.all_preds jobs tasks')) queue of - (NONE, queue') => (NONE, queue') - | (SOME work, queue') => (SOME (work, tasks'), queue')) + (case cache of + Unknown => deq NONE + | Result last => deq (SOME last) + | No_Result => (NONE, queue)) end; -end; - (* sporadic interrupts *) @@ -154,7 +142,7 @@ fun interrupt_external (queue as Queue {jobs, ...}) str = (case Int.fromString str of SOME i => - (case Task_Graph.get_first + (case Task_Graph.get_first NONE (fn (task as Task (_, j), _) => if i = j then SOME task else NONE) jobs of SOME task => interrupt queue task | NONE => ()) | NONE => ()); @@ -180,11 +168,11 @@ val _ = List.app SimpleThread.interrupt running; in groups end; -fun finish task (Queue {groups, jobs}) = +fun finish task (Queue {groups, jobs, ...}) = let val Group (gid, _) = get_group jobs task; val groups' = Inttab.remove_list (op =) (gid, task) groups; val jobs' = Task_Graph.del_node task jobs; - in make_queue groups' jobs' end; + in make_queue groups' jobs' Unknown end; end; diff -r fe35b72b9ef0 -r bc2de3795756 src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Sat Jun 13 16:32:38 2009 +0200 +++ b/src/Pure/General/graph.ML Sun Jun 14 09:11:51 2009 +0200 @@ -15,7 +15,8 @@ val is_empty: 'a T -> bool val keys: 'a T -> key list val dest: 'a T -> (key * key list) list - val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option + val get_first: key option -> (key * ('a * (key list * key list)) -> 'b option) -> + 'a T -> 'b option val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b val minimals: 'a T -> key list val maximals: 'a T -> key list @@ -88,7 +89,7 @@ fun keys (Graph tab) = Table.keys tab; fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab); -fun get_first f (Graph tab) = Table.get_first f tab; +fun get_first b f (Graph tab) = Table.get_first b f tab; fun fold_graph f (Graph tab) = Table.fold f tab; fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G []; diff -r fe35b72b9ef0 -r bc2de3795756 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Sat Jun 13 16:32:38 2009 +0200 +++ b/src/Pure/General/table.ML Sun Jun 14 09:11:51 2009 +0200 @@ -26,13 +26,13 @@ val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list + val min_key: 'a table -> key option + val max_key: 'a table -> key option + val get_first: key option -> (key * 'a -> 'b option) -> 'a table -> 'b option val exists: (key * 'a -> bool) -> 'a table -> bool val forall: (key * 'a -> bool) -> 'a table -> bool - val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option - val min_key: 'a table -> key option - val max_key: 'a table -> key option + val lookup: 'a table -> key -> 'a option val defined: 'a table -> key -> bool - val lookup: 'a table -> key -> 'a option val update: key * 'a -> 'a table -> 'a table val update_new: key * 'a -> 'a table -> 'a table (*exception DUP*) val default: key * 'a -> 'a table -> 'a table @@ -114,17 +114,6 @@ fun dest tab = fold_rev_table cons tab []; fun keys tab = fold_rev_table (cons o #1) tab []; -fun get_first f tab = - let - exception FOUND of 'b option; - fun get entry () = (case f entry of NONE => () | some => raise FOUND some); - in (fold_table get tab (); NONE) handle FOUND res => res end; - -fun exists pred = - is_some o get_first (fn entry => if pred entry then SOME () else NONE); - -fun forall pred = not o exists (not o pred); - (* min/max keys *) @@ -141,6 +130,45 @@ | max_key (Branch3 (_, _, _, _, right)) = max_key right; +(* get_first *) + +fun get_first boundary f tab = + let + val check = + (case boundary of + NONE => K true + | SOME b => (fn k => Key.ord (b, k) = LESS)); + fun apply (k, x) = if check k then f (k, x) else NONE; + fun get_bounded tb k = if check k then get tb else NONE + and get Empty = NONE + | get (Branch2 (left, (k, x), right)) = + (case get_bounded left k of + NONE => + (case apply (k, x) of + NONE => get right + | some => some) + | some => some) + | get (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = + (case get_bounded left k1 of + NONE => + (case apply (k1, x1) of + NONE => + (case get_bounded mid k2 of + NONE => + (case apply (k2, x2) of + NONE => get right + | some => some) + | some => some) + | some => some) + | some => some); + in get tab end; + +fun exists pred = + is_some o get_first NONE (fn entry => if pred entry then SOME () else NONE); + +fun forall pred = not o exists (not o pred); + + (* lookup *) fun lookup tab key =