support named tasks, for improved tracing;
authorwenzelm
Mon Jan 31 22:57:01 2011 +0100 (2011-01-31 ago)
changeset 416731c191a39549f
parent 41672 2f70b1ddd09f
child 41674 7da257539a8d
support named tasks, for improved tracing;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/goal.ML
src/Pure/proofterm.ML
     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') =