some support for ML runtime statistics;
authorwenzelm
Wed Nov 28 17:18:53 2012 +0100 (2012-11-28)
changeset 50255d0ec1f0d1d7d
parent 50254 935ac0ad7e83
child 50279 902ccccf2efa
some support for ML runtime statistics;
etc/options
src/Pure/Concurrent/future.ML
src/Pure/ML/ml_statistics_dummy.ML
src/Pure/ML/ml_statistics_polyml-5.5.0.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/build.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/session.scala
src/Tools/jEdit/src/isabelle_options.scala
     1.1 --- a/etc/options	Wed Nov 28 16:09:05 2012 +0100
     1.2 +++ b/etc/options	Wed Nov 28 17:18:53 2012 +0100
     1.3 @@ -53,6 +53,8 @@
     1.4    -- "level of parallel proof checking: 0, 1, 2"
     1.5  option parallel_proofs_threshold : int = 100
     1.6    -- "threshold for sub-proof parallelization"
     1.7 +option ML_statistics : bool = false
     1.8 +  -- "ML runtime statistics of parallel execution environment"
     1.9  
    1.10  
    1.11  section "Detail of Proof Recording"
     2.1 --- a/src/Pure/Concurrent/future.ML	Wed Nov 28 16:09:05 2012 +0100
     2.2 +++ b/src/Pure/Concurrent/future.ML	Wed Nov 28 17:18:53 2012 +0100
     2.3 @@ -271,6 +271,13 @@
     2.4  
     2.5  (* scheduler *)
     2.6  
     2.7 +fun ML_statistics () =
     2.8 +  if ! ML_Statistics.enabled then
     2.9 +    (case ML_Statistics.get () of
    2.10 +      [] => ()
    2.11 +    | stats => Output.protocol_message (Markup.ML_statistics @ stats) "")
    2.12 +  else ();
    2.13 +
    2.14  val status_ticks = Unsynchronized.ref 0;
    2.15  
    2.16  val last_round = Unsynchronized.ref Time.zeroTime;
    2.17 @@ -289,6 +296,7 @@
    2.18        if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else ();
    2.19      val _ =
    2.20        if tick andalso ! status_ticks = 0 then
    2.21 +       (ML_statistics ();
    2.22          Multithreading.tracing 1 (fn () =>
    2.23            let
    2.24              val {ready, pending, running, passive} = Task_Queue.status (! queue);
    2.25 @@ -304,7 +312,7 @@
    2.26                string_of_int total ^ " workers, " ^
    2.27                string_of_int active ^ " active, " ^
    2.28                string_of_int waiting ^ " waiting "
    2.29 -          end)
    2.30 +          end))
    2.31        else ();
    2.32  
    2.33      val _ =
    2.34 @@ -392,7 +400,7 @@
    2.35      Multithreading.with_attributes
    2.36        (Multithreading.sync_interrupts Multithreading.public_interrupts)
    2.37        (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
    2.38 -  do (); last_round := Time.zeroTime);
    2.39 +  do (); last_round := Time.zeroTime; ML_statistics ());
    2.40  
    2.41  fun scheduler_active () = (*requires SYNCHRONIZED*)
    2.42    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML/ml_statistics_dummy.ML	Wed Nov 28 17:18:53 2012 +0100
     3.3 @@ -0,0 +1,20 @@
     3.4 +(*  Title:      Pure/ML/ml_statistics_dummy.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +ML runtime statistics -- dummy version.
     3.8 +*)
     3.9 +
    3.10 +signature ML_STATISTICS =
    3.11 +sig
    3.12 +  val enabled: bool Unsynchronized.ref
    3.13 +  val get: unit -> Properties.T
    3.14 +end;
    3.15 +
    3.16 +structure ML_Statistics: ML_STATISTICS =
    3.17 +struct
    3.18 +
    3.19 +val enabled = Unsynchronized.ref false;
    3.20 +fun get () = [];
    3.21 +
    3.22 +end;
    3.23 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Wed Nov 28 17:18:53 2012 +0100
     4.3 @@ -0,0 +1,61 @@
     4.4 +(*  Title:      Pure/ML/ml_statistics_polyml-5.5.0.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +ML runtime statistics for Poly/ML 5.5.0.
     4.8 +*)
     4.9 +
    4.10 +signature ML_STATISTICS =
    4.11 +sig
    4.12 +  val enabled: bool Unsynchronized.ref
    4.13 +  val get: unit -> Properties.T
    4.14 +end;
    4.15 +
    4.16 +structure ML_Statistics: ML_STATISTICS =
    4.17 +struct
    4.18 +
    4.19 +val enabled = Unsynchronized.ref false;
    4.20 +
    4.21 +fun get () =
    4.22 +  let
    4.23 +    val
    4.24 +     {gcFullGCs,
    4.25 +      gcPartialGCs,
    4.26 +      sizeAllocation,
    4.27 +      sizeAllocationFree,
    4.28 +      sizeHeap,
    4.29 +      sizeHeapFreeLastFullGC,
    4.30 +      sizeHeapFreeLastGC,
    4.31 +      threadsInML,
    4.32 +      threadsTotal,
    4.33 +      threadsWaitCondVar,
    4.34 +      threadsWaitIO,
    4.35 +      threadsWaitMutex,
    4.36 +      threadsWaitSignal,
    4.37 +      timeGCSystem,
    4.38 +      timeGCUser,
    4.39 +      timeNonGCSystem,
    4.40 +      timeNonGCUser,
    4.41 +      userCounters = _} = PolyML.Statistics.getLocalStats ()
    4.42 +  in
    4.43 +    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
    4.44 +     ("full_GCs", Markup.print_int gcFullGCs),
    4.45 +     ("partial_GCs", Markup.print_int gcPartialGCs),
    4.46 +     ("size_allocation", Markup.print_int sizeAllocation),
    4.47 +     ("size_allocation_free", Markup.print_int sizeAllocationFree),
    4.48 +     ("size_heap", Markup.print_int sizeHeap),
    4.49 +     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
    4.50 +     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
    4.51 +     ("threads_in_ML", Markup.print_int threadsInML),
    4.52 +     ("threads_total", Markup.print_int threadsTotal),
    4.53 +     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
    4.54 +     ("threads_wait_IO", Markup.print_int threadsWaitIO),
    4.55 +     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
    4.56 +     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
    4.57 +     ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)),
    4.58 +     ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)),
    4.59 +     ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)),
    4.60 +     ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))]
    4.61 +  end;
    4.62 +
    4.63 +end;
    4.64 +
     5.1 --- a/src/Pure/PIDE/markup.ML	Wed Nov 28 16:09:05 2012 +0100
     5.2 +++ b/src/Pure/PIDE/markup.ML	Wed Nov 28 17:18:53 2012 +0100
     5.3 @@ -126,6 +126,7 @@
     5.4    val removed_versions: Properties.T
     5.5    val invoke_scala: string -> string -> Properties.T
     5.6    val cancel_scala: string -> Properties.T
     5.7 +  val ML_statistics: Properties.T
     5.8    val no_output: Output.output * Output.output
     5.9    val default_output: T -> Output.output * Output.output
    5.10    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    5.11 @@ -388,6 +389,8 @@
    5.12  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    5.13  fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
    5.14  
    5.15 +val ML_statistics = [(functionN, "ML_statistics")];
    5.16 +
    5.17  
    5.18  
    5.19  (** print mode operations **)
     6.1 --- a/src/Pure/PIDE/markup.scala	Wed Nov 28 16:09:05 2012 +0100
     6.2 +++ b/src/Pure/PIDE/markup.scala	Wed Nov 28 17:18:53 2012 +0100
     6.3 @@ -307,6 +307,15 @@
     6.4          case _ => None
     6.5        }
     6.6    }
     6.7 +
     6.8 +  object ML_Statistics
     6.9 +  {
    6.10 +    def unapply(props: Properties.T): Option[Properties.T] =
    6.11 +      props match {
    6.12 +        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
    6.13 +        case _ => None
    6.14 +      }
    6.15 +  }
    6.16  }
    6.17  
    6.18  
     7.1 --- a/src/Pure/ROOT	Wed Nov 28 16:09:05 2012 +0100
     7.2 +++ b/src/Pure/ROOT	Wed Nov 28 17:18:53 2012 +0100
     7.3 @@ -140,6 +140,8 @@
     7.4      "ML/ml_env.ML"
     7.5      "ML/ml_lex.ML"
     7.6      "ML/ml_parse.ML"
     7.7 +    "ML/ml_statistics_dummy.ML"
     7.8 +    "ML/ml_statistics_polyml-5.5.0.ML"
     7.9      "ML/ml_syntax.ML"
    7.10      "ML/ml_thms.ML"
    7.11      "PIDE/command.ML"
     8.1 --- a/src/Pure/ROOT.ML	Wed Nov 28 16:09:05 2012 +0100
     8.2 +++ b/src/Pure/ROOT.ML	Wed Nov 28 17:18:53 2012 +0100
     8.3 @@ -70,6 +70,10 @@
     8.4  
     8.5  (* concurrency within the ML runtime *)
     8.6  
     8.7 +if ML_System.name = "polyml-5.5.0"
     8.8 +then use "ML/ml_statistics_polyml-5.5.0.ML"
     8.9 +else use "ML/ml_statistics_dummy.ML";
    8.10 +
    8.11  use "Concurrent/single_assignment.ML";
    8.12  if Multithreading.available then ()
    8.13  else use "Concurrent/single_assignment_sequential.ML";
     9.1 --- a/src/Pure/System/build.ML	Wed Nov 28 16:09:05 2012 +0100
     9.2 +++ b/src/Pure/System/build.ML	Wed Nov 28 17:18:53 2012 +0100
     9.3 @@ -27,6 +27,7 @@
     9.4          (Options.int options "parallel_proofs_threshold")
     9.5      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     9.6      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     9.7 +    |> Unsynchronized.setmp ML_Statistics.enabled (Options.bool options "ML_statistics")
     9.8      |> no_document options ? Present.no_document
     9.9      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    9.10      |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    10.1 --- a/src/Pure/System/isabelle_process.ML	Wed Nov 28 16:09:05 2012 +0100
    10.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Nov 28 17:18:53 2012 +0100
    10.3 @@ -217,6 +217,7 @@
    10.4    protocol_command "Isabelle_Process.options"
    10.5      (fn [options_yxml] =>
    10.6        let val options = Options.decode (YXML.parse_body options_yxml) in
    10.7 +        ML_Statistics.enabled := Options.bool options "ML_statistics";
    10.8          Multithreading.trace := Options.int options "threads_trace";
    10.9          Multithreading.max_threads := Options.int options "threads";
   10.10          if Multithreading.max_threads_value () < 2
    11.1 --- a/src/Pure/System/session.scala	Wed Nov 28 16:09:05 2012 +0100
    11.2 +++ b/src/Pure/System/session.scala	Wed Nov 28 17:18:53 2012 +0100
    11.3 @@ -358,6 +358,9 @@
    11.4              case None =>
    11.5            }
    11.6  
    11.7 +        case Markup.ML_Statistics(stats) if output.is_protocol =>
    11.8 +          java.lang.System.err.println(stats.toString)  // FIXME
    11.9 +
   11.10          case _ if output.is_init =>
   11.11              phase = Session.Ready
   11.12  
    12.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Nov 28 16:09:05 2012 +0100
    12.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Nov 28 17:18:53 2012 +0100
    12.3 @@ -43,7 +43,7 @@
    12.4    private val relevant_options =
    12.5      Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
    12.6        "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
    12.7 -      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
    12.8 +      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
    12.9        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
   12.10        "editor_tracing_limit", "editor_update_delay")
   12.11