# HG changeset patch
# User wenzelm
# Date 1354119533 -3600
# Node ID d0ec1f0d1d7dadc74ced2a66410ff1799c8dbfbe
# Parent  935ac0ad7e83c3d63266554ae86e21d60f0ee4a5
some support for ML runtime statistics;

diff -r 935ac0ad7e83 -r d0ec1f0d1d7d etc/options
--- a/etc/options	Wed Nov 28 16:09:05 2012 +0100
+++ b/etc/options	Wed Nov 28 17:18:53 2012 +0100
@@ -53,6 +53,8 @@
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_proofs_threshold : int = 100
   -- "threshold for sub-proof parallelization"
+option ML_statistics : bool = false
+  -- "ML runtime statistics of parallel execution environment"
 
 
 section "Detail of Proof Recording"
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -271,6 +271,13 @@
 
 (* scheduler *)
 
+fun ML_statistics () =
+  if ! ML_Statistics.enabled then
+    (case ML_Statistics.get () of
+      [] => ()
+    | stats => Output.protocol_message (Markup.ML_statistics @ stats) "")
+  else ();
+
 val status_ticks = Unsynchronized.ref 0;
 
 val last_round = Unsynchronized.ref Time.zeroTime;
@@ -289,6 +296,7 @@
       if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else ();
     val _ =
       if tick andalso ! status_ticks = 0 then
+       (ML_statistics ();
         Multithreading.tracing 1 (fn () =>
           let
             val {ready, pending, running, passive} = Task_Queue.status (! queue);
@@ -304,7 +312,7 @@
               string_of_int total ^ " workers, " ^
               string_of_int active ^ " active, " ^
               string_of_int waiting ^ " waiting "
-          end)
+          end))
       else ();
 
     val _ =
@@ -392,7 +400,7 @@
     Multithreading.with_attributes
       (Multithreading.sync_interrupts Multithreading.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
-  do (); last_round := Time.zeroTime);
+  do (); last_round := Time.zeroTime; ML_statistics ());
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/ML/ml_statistics_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics_dummy.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -0,0 +1,20 @@
+(*  Title:      Pure/ML/ml_statistics_dummy.ML
+    Author:     Makarius
+
+ML runtime statistics -- dummy version.
+*)
+
+signature ML_STATISTICS =
+sig
+  val enabled: bool Unsynchronized.ref
+  val get: unit -> Properties.T
+end;
+
+structure ML_Statistics: ML_STATISTICS =
+struct
+
+val enabled = Unsynchronized.ref false;
+fun get () = [];
+
+end;
+
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/ML/ml_statistics_polyml-5.5.0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -0,0 +1,61 @@
+(*  Title:      Pure/ML/ml_statistics_polyml-5.5.0.ML
+    Author:     Makarius
+
+ML runtime statistics for Poly/ML 5.5.0.
+*)
+
+signature ML_STATISTICS =
+sig
+  val enabled: bool Unsynchronized.ref
+  val get: unit -> Properties.T
+end;
+
+structure ML_Statistics: ML_STATISTICS =
+struct
+
+val enabled = Unsynchronized.ref false;
+
+fun get () =
+  let
+    val
+     {gcFullGCs,
+      gcPartialGCs,
+      sizeAllocation,
+      sizeAllocationFree,
+      sizeHeap,
+      sizeHeapFreeLastFullGC,
+      sizeHeapFreeLastGC,
+      threadsInML,
+      threadsTotal,
+      threadsWaitCondVar,
+      threadsWaitIO,
+      threadsWaitMutex,
+      threadsWaitSignal,
+      timeGCSystem,
+      timeGCUser,
+      timeNonGCSystem,
+      timeNonGCUser,
+      userCounters = _} = PolyML.Statistics.getLocalStats ()
+  in
+    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+     ("full_GCs", Markup.print_int gcFullGCs),
+     ("partial_GCs", Markup.print_int gcPartialGCs),
+     ("size_allocation", Markup.print_int sizeAllocation),
+     ("size_allocation_free", Markup.print_int sizeAllocationFree),
+     ("size_heap", Markup.print_int sizeHeap),
+     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
+     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
+     ("threads_in_ML", Markup.print_int threadsInML),
+     ("threads_total", Markup.print_int threadsTotal),
+     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
+     ("threads_wait_IO", Markup.print_int threadsWaitIO),
+     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
+     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
+     ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)),
+     ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)),
+     ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)),
+     ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))]
+  end;
+
+end;
+
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -126,6 +126,7 @@
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
+  val ML_statistics: Properties.T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -388,6 +389,8 @@
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
+val ML_statistics = [(functionN, "ML_statistics")];
+
 
 
 (** print mode operations **)
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Nov 28 17:18:53 2012 +0100
@@ -307,6 +307,15 @@
         case _ => None
       }
   }
+
+  object ML_Statistics
+  {
+    def unapply(props: Properties.T): Option[Properties.T] =
+      props match {
+        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
+        case _ => None
+      }
+  }
 }
 
 
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/ROOT	Wed Nov 28 17:18:53 2012 +0100
@@ -140,6 +140,8 @@
     "ML/ml_env.ML"
     "ML/ml_lex.ML"
     "ML/ml_parse.ML"
+    "ML/ml_statistics_dummy.ML"
+    "ML/ml_statistics_polyml-5.5.0.ML"
     "ML/ml_syntax.ML"
     "ML/ml_thms.ML"
     "PIDE/command.ML"
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/ROOT.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -70,6 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
+if ML_System.name = "polyml-5.5.0"
+then use "ML/ml_statistics_polyml-5.5.0.ML"
+else use "ML/ml_statistics_dummy.ML";
+
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/System/build.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -27,6 +27,7 @@
         (Options.int options "parallel_proofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+    |> Unsynchronized.setmp ML_Statistics.enabled (Options.bool options "ML_statistics")
     |> no_document options ? Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -217,6 +217,7 @@
   protocol_command "Isabelle_Process.options"
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
+        ML_Statistics.enabled := Options.bool options "ML_statistics";
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads := Options.int options "threads";
         if Multithreading.max_threads_value () < 2
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/System/session.scala	Wed Nov 28 17:18:53 2012 +0100
@@ -358,6 +358,9 @@
             case None =>
           }
 
+        case Markup.ML_Statistics(stats) if output.is_protocol =>
+          java.lang.System.err.println(stats.toString)  // FIXME
+
         case _ if output.is_init =>
             phase = Session.Ready
 
diff -r 935ac0ad7e83 -r d0ec1f0d1d7d src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Nov 28 17:18:53 2012 +0100
@@ -43,7 +43,7 @@
   private val relevant_options =
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
       "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
-      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
+      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
       "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
       "editor_tracing_limit", "editor_update_delay")