--- 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"
--- 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 \
--- 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) ();
--- 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;
--- 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 [];
--- 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 =