# HG changeset patch # User wenzelm # Date 1296511021 -3600 # Node ID 1c191a39549f144f15c1d0a0f8422ac7c063d9f0 # Parent 2f70b1ddd09fe2cb7d34307bc366665e8acfdc09 support named tasks, for improved tracing; diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/Concurrent/future.ML Mon Jan 31 22:57:01 2011 +0100 @@ -44,7 +44,8 @@ val group_of: 'a future -> group val peek: 'a future -> 'a Exn.result option val is_finished: 'a future -> bool - val bulk: {group: group option, deps: task list, pri: int} -> (unit -> 'a) list -> 'a future list + val bulk: {name: string, group: group option, deps: task list, pri: int} -> + (unit -> 'a) list -> 'a future list val fork_pri: int -> (unit -> 'a) -> 'a future val fork: (unit -> 'a) -> 'a future val join_results: 'a future list -> 'a Exn.result list @@ -399,7 +400,7 @@ (* fork *) -fun bulk {group, deps, pri} es = +fun bulk {name, group, deps, pri} es = let val grp = (case group of @@ -408,7 +409,7 @@ fun enqueue e (minimal, queue) = let val (result, job) = future_job grp e; - val ((task, minimal'), queue') = Task_Queue.enqueue grp deps pri job queue; + val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue; val future = Future {promised = false, task = task, group = grp, result = result}; in (future, (minimal orelse minimal', queue')) end; in @@ -423,7 +424,7 @@ in futures end) end; -fun fork_pri pri e = singleton (bulk {group = NONE, deps = [], pri = pri}) e; +fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e; fun fork e = fork_pri 0 e; @@ -499,7 +500,9 @@ in if extended then Future {promised = false, task = task, group = group, result = result} else - singleton (bulk {group = SOME group, deps = [task], pri = Task_Queue.pri_of_task task}) + singleton + (bulk {name = "Future.map", group = SOME group, + deps = [task], pri = Task_Queue.pri_of_task task}) (fn () => f (join x)) end; diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/Concurrent/par_list.ML Mon Jan 31 22:57:01 2011 +0100 @@ -26,18 +26,19 @@ structure Par_List: PAR_LIST = struct -fun managed_results f xs = +fun managed_results name f xs = if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then let val group = Task_Queue.new_group (Future.worker_group ()); val futures = - Future.bulk {group = SOME group, deps = [], pri = 0} (map (fn x => fn () => f x) xs); + Future.bulk {name = name, group = SOME group, deps = [], pri = 0} + (map (fn x => fn () => f x) xs); val results = Future.join_results futures handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn); in results end else map (Exn.capture f) xs; -fun map f xs = Exn.release_first (managed_results f xs); +fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs); fun get_some f xs = let @@ -45,7 +46,8 @@ fun found (Exn.Exn (FOUND some)) = some | found _ = NONE; val results = - managed_results (fn x => (case f x of NONE => () | some => raise FOUND some)) xs; + managed_results "Par_List.get_some" + (fn x => (case f x of NONE => () | some => raise FOUND some)) xs; in (case get_first found results of SOME y => SOME y diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/Concurrent/task_queue.ML Mon Jan 31 22:57:01 2011 +0100 @@ -28,7 +28,8 @@ val cancel: queue -> group -> bool val cancel_all: queue -> group list val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue - val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue + val enqueue: string -> group -> task list -> int -> (bool -> bool) -> + queue -> (task * bool) * queue val extend: task -> (bool -> bool) -> queue -> queue option val dequeue_passive: Thread.thread -> task -> queue -> bool * queue val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue @@ -62,21 +63,26 @@ (* tasks *) -abstype task = Task of (int option * int) * timing Synchronized.var +abstype task = Task of + {name: string, + id: int, + pri: int option, + timing: timing Synchronized.var} with -val dummy_task = Task ((NONE, ~1), new_timing ()); -fun new_task pri = Task ((pri, new_id ()), new_timing ()); +val dummy_task = Task {name = "", id = ~1, pri = NONE, timing = new_timing ()}; +fun new_task name pri = Task {name = name, id = new_id (), pri = pri, timing = new_timing ()}; -fun pri_of_task (Task ((pri, _), _)) = the_default 0 pri; -fun str_of_task (Task ((_, i), _)) = string_of_int i; +fun pri_of_task (Task {pri, ...}) = the_default 0 pri; +fun str_of_task (Task {name, id, ...}) = + if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")"; -fun timing_of_task (Task (_, timing)) = Synchronized.value timing; -fun running (Task (_, timing)) = gen_timing apfst timing; -fun waiting (Task (_, timing)) = gen_timing apsnd timing; +fun timing_of_task (Task {timing, ...}) = Synchronized.value timing; +fun running (Task {timing, ...}) = gen_timing apfst timing; +fun waiting (Task {timing, ...}) = gen_timing apsnd timing; -fun task_ord (Task (t1, _), Task (t2, _)) = - prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2); +fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) = + prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2)); val eq_task = is_equal o task_ord; @@ -219,15 +225,15 @@ fun enqueue_passive group abort (Queue {groups, jobs}) = let - val task = new_task NONE; + val task = new_task "" NONE; val groups' = groups |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group); val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive abort)); in (task, make_queue groups' jobs') end; -fun enqueue group deps pri job (Queue {groups, jobs}) = +fun enqueue name group deps pri job (Queue {groups, jobs}) = let - val task = new_task (SOME pri); + val task = new_task name (SOME pri); val groups' = groups |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group); val jobs' = jobs diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Mon Jan 31 22:57:01 2011 +0100 @@ -663,13 +663,15 @@ val future_proof = Proof.global_future_proof (fn prf => - Future.fork_pri ~1 (fn () => - let val (states, result_state) = - (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) - => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) - |> fold_map command_result body_trs - ||> command (end_tr |> set_print false); - in (states, presentation_context_of result_state) end)) + singleton + (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1}) + (fn () => + let val (states, result_state) = + (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) + => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) + |> fold_map command_result body_trs + ||> command (end_tr |> set_print false); + in (states, presentation_context_of result_state) end)) #> (fn (states, ctxt) => States.put (SOME states) ctxt); val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof)); diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/PIDE/document.ML Mon Jan 31 22:57:01 2011 +0100 @@ -208,7 +208,9 @@ fun async_state tr st = ignore - (singleton (Future.bulk {group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0}) + (singleton + (Future.bulk {name = "Document.async_state", + group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0}) (fn () => Toplevel.setmp_thread_position tr (fn () => Toplevel.print_state false st) ())); @@ -327,7 +329,7 @@ (* execute *) fun execute version_id state = - state |> map_state (fn (versions, commands, execs, execution) => + state |> map_state (fn (versions, commands, execs, _) => let val version = the_version state version_id; @@ -337,14 +339,15 @@ val _ = cancel state; val execution' = (* FIXME proper node deps *) - Future.bulk {group = NONE, deps = [], pri = 1} [fn () => - let - val _ = await_cancellation state; - val _ = - node_names_of version |> List.app (fn name => - fold_entries NONE (fn (_, exec) => fn () => force_exec exec) - (get_node version name) ()); - in () end]; + Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1} + [fn () => + let + val _ = await_cancellation state; + val _ = + node_names_of version |> List.app (fn name => + fold_entries NONE (fn (_, exec) => fn () => force_exec exec) + (get_node version name) ()); + in () end]; val _ = await_cancellation state; (* FIXME async!? *) diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/Thy/thy_info.ML Mon Jan 31 22:57:01 2011 +0100 @@ -182,15 +182,17 @@ let val get = the o Symtab.lookup tab; val deps = map (`get) (Graph.imm_preds task_graph name); + val task_deps = map (Future.task_of o #1) deps; fun failed (future, parent) = if can Future.join future then NONE else SOME parent; val future = - singleton (Future.bulk {group = NONE, deps = map (Future.task_of o #1) deps, pri = 0}) - (fn () => - (case map_filter failed deps of - [] => body (map (#1 o Future.join o get) parents) - | bad => error (loader_msg - ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") []))); + singleton + (Future.bulk {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0}) + (fn () => + (case map_filter failed deps of + [] => body (map (#1 o Future.join o get) parents) + | bad => error (loader_msg ("failed to load " ^ quote name ^ + " (unresolved " ^ commas_quote bad ^ ")") []))); in Symtab.update (name, future) tab end | Finished thy => Symtab.update (name, Future.value (thy, I)) tab)); val _ = diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/goal.ML --- a/src/Pure/goal.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/goal.ML Mon Jan 31 22:57:01 2011 +0100 @@ -106,7 +106,9 @@ (* parallel proofs *) -fun fork e = Future.fork_pri ~1 (fn () => Future.status e); +fun fork e = + singleton (Future.bulk {name = "Goal.fork", group = NONE, deps = [], pri = ~1}) + (fn () => Future.status e); val parallel_proofs = Unsynchronized.ref 1; diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/proofterm.ML Mon Jan 31 22:57:01 2011 +0100 @@ -1390,7 +1390,7 @@ else Future.map postproc body | fulfill_proof_future thy promises postproc body = singleton - (Future.bulk {group = NONE, + (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE, deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0}) (fn () => postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body))); @@ -1446,7 +1446,10 @@ val body0 = if ! proofs <> 2 then Future.value (make_body0 MinProof) else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ())) - else Future.fork_pri ~1 (make_body0 o full_proof0); + else + singleton + (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1}) + (make_body0 o full_proof0); fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); val (i, body') =