--- 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"
--- 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);
--- /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;
+
--- /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;
+
--- 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 **)
--- 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
+ }
+ }
}
--- 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"
--- 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";
--- 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")
--- 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
--- 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
--- 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")