1.1 --- a/src/Pure/Concurrent/future.ML Mon Jan 31 21:54:49 2011 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Mon Jan 31 22:57:01 2011 +0100
1.3 @@ -44,7 +44,8 @@
1.4 val group_of: 'a future -> group
1.5 val peek: 'a future -> 'a Exn.result option
1.6 val is_finished: 'a future -> bool
1.7 - val bulk: {group: group option, deps: task list, pri: int} -> (unit -> 'a) list -> 'a future list
1.8 + val bulk: {name: string, group: group option, deps: task list, pri: int} ->
1.9 + (unit -> 'a) list -> 'a future list
1.10 val fork_pri: int -> (unit -> 'a) -> 'a future
1.11 val fork: (unit -> 'a) -> 'a future
1.12 val join_results: 'a future list -> 'a Exn.result list
1.13 @@ -399,7 +400,7 @@
1.14
1.15 (* fork *)
1.16
1.17 -fun bulk {group, deps, pri} es =
1.18 +fun bulk {name, group, deps, pri} es =
1.19 let
1.20 val grp =
1.21 (case group of
1.22 @@ -408,7 +409,7 @@
1.23 fun enqueue e (minimal, queue) =
1.24 let
1.25 val (result, job) = future_job grp e;
1.26 - val ((task, minimal'), queue') = Task_Queue.enqueue grp deps pri job queue;
1.27 + val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
1.28 val future = Future {promised = false, task = task, group = grp, result = result};
1.29 in (future, (minimal orelse minimal', queue')) end;
1.30 in
1.31 @@ -423,7 +424,7 @@
1.32 in futures end)
1.33 end;
1.34
1.35 -fun fork_pri pri e = singleton (bulk {group = NONE, deps = [], pri = pri}) e;
1.36 +fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
1.37 fun fork e = fork_pri 0 e;
1.38
1.39
1.40 @@ -499,7 +500,9 @@
1.41 in
1.42 if extended then Future {promised = false, task = task, group = group, result = result}
1.43 else
1.44 - singleton (bulk {group = SOME group, deps = [task], pri = Task_Queue.pri_of_task task})
1.45 + singleton
1.46 + (bulk {name = "Future.map", group = SOME group,
1.47 + deps = [task], pri = Task_Queue.pri_of_task task})
1.48 (fn () => f (join x))
1.49 end;
1.50
2.1 --- a/src/Pure/Concurrent/par_list.ML Mon Jan 31 21:54:49 2011 +0100
2.2 +++ b/src/Pure/Concurrent/par_list.ML Mon Jan 31 22:57:01 2011 +0100
2.3 @@ -26,18 +26,19 @@
2.4 structure Par_List: PAR_LIST =
2.5 struct
2.6
2.7 -fun managed_results f xs =
2.8 +fun managed_results name f xs =
2.9 if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
2.10 let
2.11 val group = Task_Queue.new_group (Future.worker_group ());
2.12 val futures =
2.13 - Future.bulk {group = SOME group, deps = [], pri = 0} (map (fn x => fn () => f x) xs);
2.14 + Future.bulk {name = name, group = SOME group, deps = [], pri = 0}
2.15 + (map (fn x => fn () => f x) xs);
2.16 val results = Future.join_results futures
2.17 handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
2.18 in results end
2.19 else map (Exn.capture f) xs;
2.20
2.21 -fun map f xs = Exn.release_first (managed_results f xs);
2.22 +fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs);
2.23
2.24 fun get_some f xs =
2.25 let
2.26 @@ -45,7 +46,8 @@
2.27 fun found (Exn.Exn (FOUND some)) = some
2.28 | found _ = NONE;
2.29 val results =
2.30 - managed_results (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
2.31 + managed_results "Par_List.get_some"
2.32 + (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
2.33 in
2.34 (case get_first found results of
2.35 SOME y => SOME y
3.1 --- a/src/Pure/Concurrent/task_queue.ML Mon Jan 31 21:54:49 2011 +0100
3.2 +++ b/src/Pure/Concurrent/task_queue.ML Mon Jan 31 22:57:01 2011 +0100
3.3 @@ -28,7 +28,8 @@
3.4 val cancel: queue -> group -> bool
3.5 val cancel_all: queue -> group list
3.6 val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
3.7 - val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
3.8 + val enqueue: string -> group -> task list -> int -> (bool -> bool) ->
3.9 + queue -> (task * bool) * queue
3.10 val extend: task -> (bool -> bool) -> queue -> queue option
3.11 val dequeue_passive: Thread.thread -> task -> queue -> bool * queue
3.12 val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
3.13 @@ -62,21 +63,26 @@
3.14
3.15 (* tasks *)
3.16
3.17 -abstype task = Task of (int option * int) * timing Synchronized.var
3.18 +abstype task = Task of
3.19 + {name: string,
3.20 + id: int,
3.21 + pri: int option,
3.22 + timing: timing Synchronized.var}
3.23 with
3.24
3.25 -val dummy_task = Task ((NONE, ~1), new_timing ());
3.26 -fun new_task pri = Task ((pri, new_id ()), new_timing ());
3.27 +val dummy_task = Task {name = "", id = ~1, pri = NONE, timing = new_timing ()};
3.28 +fun new_task name pri = Task {name = name, id = new_id (), pri = pri, timing = new_timing ()};
3.29
3.30 -fun pri_of_task (Task ((pri, _), _)) = the_default 0 pri;
3.31 -fun str_of_task (Task ((_, i), _)) = string_of_int i;
3.32 +fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
3.33 +fun str_of_task (Task {name, id, ...}) =
3.34 + if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
3.35
3.36 -fun timing_of_task (Task (_, timing)) = Synchronized.value timing;
3.37 -fun running (Task (_, timing)) = gen_timing apfst timing;
3.38 -fun waiting (Task (_, timing)) = gen_timing apsnd timing;
3.39 +fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
3.40 +fun running (Task {timing, ...}) = gen_timing apfst timing;
3.41 +fun waiting (Task {timing, ...}) = gen_timing apsnd timing;
3.42
3.43 -fun task_ord (Task (t1, _), Task (t2, _)) =
3.44 - prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
3.45 +fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
3.46 + prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
3.47
3.48 val eq_task = is_equal o task_ord;
3.49
3.50 @@ -219,15 +225,15 @@
3.51
3.52 fun enqueue_passive group abort (Queue {groups, jobs}) =
3.53 let
3.54 - val task = new_task NONE;
3.55 + val task = new_task "" NONE;
3.56 val groups' = groups
3.57 |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
3.58 val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive abort));
3.59 in (task, make_queue groups' jobs') end;
3.60
3.61 -fun enqueue group deps pri job (Queue {groups, jobs}) =
3.62 +fun enqueue name group deps pri job (Queue {groups, jobs}) =
3.63 let
3.64 - val task = new_task (SOME pri);
3.65 + val task = new_task name (SOME pri);
3.66 val groups' = groups
3.67 |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
3.68 val jobs' = jobs
4.1 --- a/src/Pure/Isar/toplevel.ML Mon Jan 31 21:54:49 2011 +0100
4.2 +++ b/src/Pure/Isar/toplevel.ML Mon Jan 31 22:57:01 2011 +0100
4.3 @@ -663,13 +663,15 @@
4.4
4.5 val future_proof = Proof.global_future_proof
4.6 (fn prf =>
4.7 - Future.fork_pri ~1 (fn () =>
4.8 - let val (states, result_state) =
4.9 - (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
4.10 - => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
4.11 - |> fold_map command_result body_trs
4.12 - ||> command (end_tr |> set_print false);
4.13 - in (states, presentation_context_of result_state) end))
4.14 + singleton
4.15 + (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
4.16 + (fn () =>
4.17 + let val (states, result_state) =
4.18 + (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
4.19 + => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
4.20 + |> fold_map command_result body_trs
4.21 + ||> command (end_tr |> set_print false);
4.22 + in (states, presentation_context_of result_state) end))
4.23 #> (fn (states, ctxt) => States.put (SOME states) ctxt);
4.24
4.25 val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
5.1 --- a/src/Pure/PIDE/document.ML Mon Jan 31 21:54:49 2011 +0100
5.2 +++ b/src/Pure/PIDE/document.ML Mon Jan 31 22:57:01 2011 +0100
5.3 @@ -208,7 +208,9 @@
5.4
5.5 fun async_state tr st =
5.6 ignore
5.7 - (singleton (Future.bulk {group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
5.8 + (singleton
5.9 + (Future.bulk {name = "Document.async_state",
5.10 + group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
5.11 (fn () =>
5.12 Toplevel.setmp_thread_position tr
5.13 (fn () => Toplevel.print_state false st) ()));
5.14 @@ -327,7 +329,7 @@
5.15 (* execute *)
5.16
5.17 fun execute version_id state =
5.18 - state |> map_state (fn (versions, commands, execs, execution) =>
5.19 + state |> map_state (fn (versions, commands, execs, _) =>
5.20 let
5.21 val version = the_version state version_id;
5.22
5.23 @@ -337,14 +339,15 @@
5.24 val _ = cancel state;
5.25
5.26 val execution' = (* FIXME proper node deps *)
5.27 - Future.bulk {group = NONE, deps = [], pri = 1} [fn () =>
5.28 - let
5.29 - val _ = await_cancellation state;
5.30 - val _ =
5.31 - node_names_of version |> List.app (fn name =>
5.32 - fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
5.33 - (get_node version name) ());
5.34 - in () end];
5.35 + Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
5.36 + [fn () =>
5.37 + let
5.38 + val _ = await_cancellation state;
5.39 + val _ =
5.40 + node_names_of version |> List.app (fn name =>
5.41 + fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
5.42 + (get_node version name) ());
5.43 + in () end];
5.44
5.45 val _ = await_cancellation state; (* FIXME async!? *)
5.46
6.1 --- a/src/Pure/Thy/thy_info.ML Mon Jan 31 21:54:49 2011 +0100
6.2 +++ b/src/Pure/Thy/thy_info.ML Mon Jan 31 22:57:01 2011 +0100
6.3 @@ -182,15 +182,17 @@
6.4 let
6.5 val get = the o Symtab.lookup tab;
6.6 val deps = map (`get) (Graph.imm_preds task_graph name);
6.7 + val task_deps = map (Future.task_of o #1) deps;
6.8 fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
6.9
6.10 val future =
6.11 - singleton (Future.bulk {group = NONE, deps = map (Future.task_of o #1) deps, pri = 0})
6.12 - (fn () =>
6.13 - (case map_filter failed deps of
6.14 - [] => body (map (#1 o Future.join o get) parents)
6.15 - | bad => error (loader_msg
6.16 - ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
6.17 + singleton
6.18 + (Future.bulk {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
6.19 + (fn () =>
6.20 + (case map_filter failed deps of
6.21 + [] => body (map (#1 o Future.join o get) parents)
6.22 + | bad => error (loader_msg ("failed to load " ^ quote name ^
6.23 + " (unresolved " ^ commas_quote bad ^ ")") [])));
6.24 in Symtab.update (name, future) tab end
6.25 | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
6.26 val _ =
7.1 --- a/src/Pure/goal.ML Mon Jan 31 21:54:49 2011 +0100
7.2 +++ b/src/Pure/goal.ML Mon Jan 31 22:57:01 2011 +0100
7.3 @@ -106,7 +106,9 @@
7.4
7.5 (* parallel proofs *)
7.6
7.7 -fun fork e = Future.fork_pri ~1 (fn () => Future.status e);
7.8 +fun fork e =
7.9 + singleton (Future.bulk {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
7.10 + (fn () => Future.status e);
7.11
7.12 val parallel_proofs = Unsynchronized.ref 1;
7.13
8.1 --- a/src/Pure/proofterm.ML Mon Jan 31 21:54:49 2011 +0100
8.2 +++ b/src/Pure/proofterm.ML Mon Jan 31 22:57:01 2011 +0100
8.3 @@ -1390,7 +1390,7 @@
8.4 else Future.map postproc body
8.5 | fulfill_proof_future thy promises postproc body =
8.6 singleton
8.7 - (Future.bulk {group = NONE,
8.8 + (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
8.9 deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
8.10 (fn () =>
8.11 postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
8.12 @@ -1446,7 +1446,10 @@
8.13 val body0 =
8.14 if ! proofs <> 2 then Future.value (make_body0 MinProof)
8.15 else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
8.16 - else Future.fork_pri ~1 (make_body0 o full_proof0);
8.17 + else
8.18 + singleton
8.19 + (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
8.20 + (make_body0 o full_proof0);
8.21
8.22 fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
8.23 val (i, body') =