more systematic task statistics;
authorwenzelm
Fri Jan 18 17:51:50 2013 +0100 (2013-01-18)
changeset 5097573ec6ad6700e
parent 50974 55f8bd61b029
child 50976 9efd58e1e07c
more systematic task statistics;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/System/session.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri Jan 18 16:20:09 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Jan 18 17:51:50 2013 +0100
     1.3 @@ -256,12 +256,11 @@
     1.4        Task_Queue.running task (fn () =>
     1.5          setmp_worker_task task (fn () =>
     1.6            fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     1.7 -    val _ = Multithreading.tracing 2 (fn () =>
     1.8 -      let
     1.9 -        val s = Task_Queue.str_of_task_groups task;
    1.10 -        fun micros time = string_of_int (Time.toNanoseconds time div 1000);
    1.11 -        val (run, wait, deps) = Task_Queue.timing_of_task task;
    1.12 -      in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
    1.13 +    val _ =
    1.14 +      if ! Multithreading.trace >= 2 then
    1.15 +        Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
    1.16 +          handle Fail msg => warning msg
    1.17 +      else ();
    1.18      val _ = SYNCHRONIZED "finish" (fn () =>
    1.19        let
    1.20          val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
     2.1 --- a/src/Pure/Concurrent/task_queue.ML	Fri Jan 18 16:20:09 2013 +0100
     2.2 +++ b/src/Pure/Concurrent/task_queue.ML	Fri Jan 18 17:51:50 2013 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4    val pri_of_task: task -> int
     2.5    val str_of_task: task -> string
     2.6    val str_of_task_groups: task -> string
     2.7 -  val timing_of_task: task -> Time.time * Time.time * string list
     2.8 +  val task_statistics: task -> Properties.T
     2.9    val running: task -> (unit -> 'a) -> 'a
    2.10    val joining: task -> (unit -> 'a) -> 'a
    2.11    val waiting: task -> task list -> (unit -> 'a) -> 'a
    2.12 @@ -114,14 +114,17 @@
    2.13    name: string,
    2.14    id: int,
    2.15    pri: int option,
    2.16 -  timing: timing Synchronized.var option}
    2.17 +  timing: timing Synchronized.var option,
    2.18 +  pos: Position.T}
    2.19  with
    2.20  
    2.21  val dummy_task =
    2.22 -  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
    2.23 +  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
    2.24 +    pos = Position.none};
    2.25  
    2.26  fun new_task group name pri =
    2.27 -  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
    2.28 +  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
    2.29 +    pos = Position.thread_data ()};
    2.30  
    2.31  fun group_of_task (Task {group, ...}) = group;
    2.32  fun name_of_task (Task {name, ...}) = name;
    2.33 @@ -132,9 +135,6 @@
    2.34  
    2.35  fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
    2.36  
    2.37 -fun timing_of_task (Task {timing, ...}) =
    2.38 -  (case timing of NONE => timing_start | SOME var => Synchronized.value var);
    2.39 -
    2.40  fun update_timing update (Task {timing, ...}) e =
    2.41    uninterruptible (fn restore_attributes => fn () =>
    2.42      let
    2.43 @@ -147,6 +147,18 @@
    2.44  fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
    2.45    prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
    2.46  
    2.47 +fun task_statistics (Task {name, id, timing, pos, ...}) =
    2.48 +  let
    2.49 +    val (run, wait, wait_deps) =
    2.50 +      (case timing of NONE => timing_start | SOME var => Synchronized.value var);
    2.51 +    fun micros time = string_of_int (Time.toNanoseconds time div 1000);
    2.52 +  in
    2.53 +    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
    2.54 +     ("task_name", name), ("task_id", Markup.print_int id),
    2.55 +     ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
    2.56 +    Position.properties_of pos
    2.57 +  end;
    2.58 +
    2.59  end;
    2.60  
    2.61  structure Tasks = Table(type key = task val ord = task_ord);
     3.1 --- a/src/Pure/PIDE/markup.ML	Fri Jan 18 16:20:09 2013 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Fri Jan 18 17:51:50 2013 +0100
     3.3 @@ -134,6 +134,7 @@
     3.4    val invoke_scala: string -> string -> Properties.T
     3.5    val cancel_scala: string -> Properties.T
     3.6    val ML_statistics: Properties.entry
     3.7 +  val task_statistics: Properties.entry
     3.8    val loading_theory: string -> Properties.T
     3.9    val dest_loading_theory: Properties.T -> string option
    3.10    val no_output: Output.output * Output.output
    3.11 @@ -412,6 +413,8 @@
    3.12  
    3.13  val ML_statistics = (functionN, "ML_statistics");
    3.14  
    3.15 +val task_statistics = (functionN, "task_statistics");
    3.16 +
    3.17  fun loading_theory name = [("function", "loading_theory"), ("name", name)];
    3.18  
    3.19  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
     4.1 --- a/src/Pure/PIDE/markup.scala	Fri Jan 18 16:20:09 2013 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Fri Jan 18 17:51:50 2013 +0100
     4.3 @@ -330,6 +330,15 @@
     4.4          case _ => None
     4.5        }
     4.6    }
     4.7 +
     4.8 +  object Task_Statistics
     4.9 +  {
    4.10 +    def unapply(props: Properties.T): Option[Properties.T] =
    4.11 +      props match {
    4.12 +        case (FUNCTION, "task_statistics") :: stats => Some(stats)
    4.13 +        case _ => None
    4.14 +      }
    4.15 +  }
    4.16  }
    4.17  
    4.18  
     5.1 --- a/src/Pure/System/session.scala	Fri Jan 18 16:20:09 2013 +0100
     5.2 +++ b/src/Pure/System/session.scala	Fri Jan 18 17:51:50 2013 +0100
     5.3 @@ -364,6 +364,9 @@
     5.4          case Markup.ML_Statistics(props) if output.is_protocol =>
     5.5            statistics.event(Session.Statistics(props))
     5.6  
     5.7 +        case Markup.Task_Statistics(props) if output.is_protocol =>
     5.8 +          // FIXME
     5.9 +
    5.10          case _ if output.is_init =>
    5.11            phase = Session.Ready
    5.12  
     6.1 --- a/src/Pure/Tools/build.ML	Fri Jan 18 16:20:09 2013 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Fri Jan 18 17:51:50 2013 +0100
     6.3 @@ -19,13 +19,21 @@
     6.4        else NONE
     6.5    | ML_statistics _ _ = NONE;
     6.6  
     6.7 +fun task_statistics (function :: stats) "" =
     6.8 +      if function = Markup.task_statistics then SOME stats
     6.9 +      else NONE
    6.10 +  | task_statistics _ _ = NONE;
    6.11 +
    6.12  fun protocol_message props output =
    6.13    (case ML_statistics props output of
    6.14      SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
    6.15    | NONE =>
    6.16 -      (case Markup.dest_loading_theory props of
    6.17 -        SOME name => writeln ("\floading_theory = " ^ name)
    6.18 -      | NONE => raise Fail "Undefined Output.protocol_message"));
    6.19 +      (case task_statistics props output of
    6.20 +        SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
    6.21 +      | NONE =>
    6.22 +          (case Markup.dest_loading_theory props of
    6.23 +            SOME name => writeln ("\floading_theory = " ^ name)
    6.24 +          | NONE => raise Fail "Undefined Output.protocol_message")));
    6.25  
    6.26  
    6.27  (* build *)
     7.1 --- a/src/Pure/Tools/build.scala	Fri Jan 18 16:20:09 2013 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Fri Jan 18 17:51:50 2013 +0100
     7.3 @@ -561,14 +561,16 @@
     7.4    private val SESSION_PARENT_PATH = "\fSession.parent_path = "
     7.5  
     7.6  
     7.7 -  sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
     7.8 +  sealed case class Log_Info(
     7.9 +    stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
    7.10  
    7.11    def parse_log(text: String): Log_Info =
    7.12    {
    7.13      val lines = split_lines(text)
    7.14      val stats = Props.parse_lines("\fML_statistics = ", lines)
    7.15 +    val tasks = Props.parse_lines("\ftask_statistics = ", lines)
    7.16      val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    7.17 -    Log_Info(stats, timing)
    7.18 +    Log_Info(stats, tasks, timing)
    7.19    }
    7.20  
    7.21