more informative task timing: some dependency tracking;

--- a/src/Pure/Concurrent/future.ML	Tue Feb 01 21:05:22 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 01 22:24:28 2011 +0100
@@ -91,10 +91,10 @@
     NONE => e ()
   | SOME task => Task_Queue.joining task e);
 
-fun worker_waiting e =
+fun worker_waiting deps e =
   (case worker_task () of
     NONE => e ()
-  | SOME task => Task_Queue.waiting task e);
+  | SOME task => Task_Queue.waiting task deps e);
 
 
 (* datatype future *)
@@ -215,8 +215,8 @@
       let
         val s = Task_Queue.str_of_task task;
         fun micros time = string_of_int (Time.toNanoseconds time div 1000);
-        val (run, wait) = pairself micros (Task_Queue.timing_of_task task);
-      in "TASK " ^ s ^ " " ^ run ^ " " ^ wait end);
+        val (run, wait, deps) = Task_Queue.timing_of_task task;
+      in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
@@ -453,7 +453,8 @@
   else
     (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
       (NONE, []) => NONE
-    | (NONE, deps') => (worker_waiting (fn () => worker_wait true work_finished); join_next deps')
+    | (NONE, deps') =>
+        (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps')
     | (SOME work, deps') => SOME (work, deps'));
 
 fun execute_work NONE = ()
@@ -543,7 +544,7 @@
                 Unsynchronized.change_result queue
                   (Task_Queue.dequeue_passive (Thread.self ()) task));
           in if still_passive then execute (task, group, [job]) else () end);
-      val _ = worker_waiting (fn () => Single_Assignment.await result);
+      val _ = worker_waiting [task] (fn () => Single_Assignment.await result);
     in () end;
 
 fun fulfill x res = fulfill_result x (Exn.Result res);

--- a/src/Pure/Concurrent/task_queue.ML	Tue Feb 01 21:05:22 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Feb 01 22:24:28 2011 +0100
@@ -10,10 +10,10 @@
   val dummy_task: task
   val pri_of_task: task -> int
   val str_of_task: task -> string
-  val timing_of_task: task -> Time.time * Time.time
+  val timing_of_task: task -> Time.time * Time.time * string list
   val running: task -> (unit -> 'a) -> 'a
   val joining: task -> (unit -> 'a) -> 'a
-  val waiting: task -> (unit -> 'a) -> 'a
+  val waiting: task -> task list -> (unit -> 'a) -> 'a
   type group
   val new_group: group option -> group
   val group_id: group -> int
@@ -48,10 +48,10 @@
 
 (* timing *)
 
-type timing = Time.time * Time.time;
+type timing = Time.time * Time.time * string list;
 
 fun new_timing () =
-  Synchronized.var "timing" (Time.zeroTime, Time.zeroTime);
+  Synchronized.var "timing" ((Time.zeroTime, Time.zeroTime, []): timing);
 
 fun gen_timing account timing e =
   let
@@ -80,10 +80,15 @@
 
 fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
 
-fun running (Task {timing, ...}) = gen_timing (fn t => fn (a, b) => (Time.+ (a, t), b)) timing;
-fun joining (Task {timing, ...}) = gen_timing (fn t => fn (a, b) => (Time.- (a, t), b)) timing;
-fun waiting (Task {timing, ...}) =
-  gen_timing (fn t => fn (a, b) => (Time.- (a, t), Time.+ (b, t))) timing;
+fun running (Task {timing, ...}) =
+  gen_timing (fn t => fn (a, b, ds) => (Time.+ (a, t), b, ds)) timing;
+
+fun joining (Task {timing, ...}) =
+  gen_timing (fn t => fn (a, b, ds) => (Time.- (a, t), b, ds)) timing;
+
+fun waiting (Task {timing, ...}) deps =
+  timing |> gen_timing (fn t => fn (a, b, ds) =>
+    (Time.- (a, t), Time.+ (b, t), fold (fn Task {name, ...} => insert (op =) name) deps ds));
 
 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));