--- a/src/Pure/Concurrent/future.ML Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Nov 29 10:45:25 2012 +0100
@@ -51,6 +51,7 @@
val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
+ val ML_statistics: bool Unsynchronized.ref
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
@@ -169,6 +170,10 @@
val max_active = Unsynchronized.ref 0;
val worker_trend = Unsynchronized.ref 0;
+val status_ticks = Unsynchronized.ref 0;
+val last_round = Unsynchronized.ref Time.zeroTime;
+val next_round = seconds 0.05;
+
datatype worker_state = Working | Waiting | Sleeping;
val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
@@ -176,6 +181,32 @@
fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
+
+(* status *)
+
+val ML_statistics = Unsynchronized.ref false;
+
+fun report_status () = (*requires SYNCHRONIZED*)
+ if ! ML_statistics then
+ let
+ val {ready, pending, running, passive} = Task_Queue.status (! queue);
+ val total = length (! workers);
+ val active = count_workers Working;
+ val waiting = count_workers Waiting;
+ val stats =
+ [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+ ("tasks_ready", Markup.print_int ready),
+ ("tasks_pending", Markup.print_int pending),
+ ("tasks_running", Markup.print_int running),
+ ("tasks_passive", Markup.print_int passive),
+ ("workers_total", Markup.print_int total),
+ ("workers_active", Markup.print_int active),
+ ("workers_waiting", Markup.print_int waiting)] @
+ ML_Statistics.get ();
+ in Output.protocol_message (Markup.ML_statistics @ stats) "" end
+ else ();
+
+
(* cancellation primitives *)
fun cancel_now group = (*requires SYNCHRONIZED*)
@@ -271,18 +302,6 @@
(* 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;
-val next_round = seconds 0.05;
-
fun scheduler_next () = (*requires SYNCHRONIZED*)
let
val now = Time.now ();
@@ -290,30 +309,12 @@
val _ = if tick then last_round := now else ();
- (* queue and worker status *)
+ (* runtime status *)
val _ =
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);
- val total = length (! workers);
- val active = count_workers Working;
- val waiting = count_workers Waiting;
- in
- "SCHEDULE " ^ Time.toString now ^ ": " ^
- string_of_int ready ^ " ready, " ^
- string_of_int pending ^ " pending, " ^
- string_of_int running ^ " running, " ^
- string_of_int passive ^ " passive; " ^
- string_of_int total ^ " workers, " ^
- string_of_int active ^ " active, " ^
- string_of_int waiting ^ " waiting "
- end))
- else ();
+ if tick andalso ! status_ticks = 0 then report_status () else ();
val _ =
if forall (Thread.isActive o #1) (! workers) then ()
@@ -400,7 +401,7 @@
Multithreading.with_attributes
(Multithreading.sync_interrupts Multithreading.public_interrupts)
(fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
- do (); last_round := Time.zeroTime; ML_statistics ());
+ do (); last_round := Time.zeroTime; report_status ());
fun scheduler_active () = (*requires SYNCHRONIZED*)
(case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
@@ -665,11 +666,6 @@
else ();
-(* queue status *)
-
-fun queue_status () = Task_Queue.status (! queue);
-
-
(*final declarations of this structure!*)
val map = map_future;
--- a/src/Pure/ML/ml_statistics_dummy.ML Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/ML/ml_statistics_dummy.ML Thu Nov 29 10:45:25 2012 +0100
@@ -6,14 +6,12 @@
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;
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Thu Nov 29 10:45:25 2012 +0100
@@ -6,15 +6,12 @@
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
@@ -37,8 +34,7 @@
timeNonGCUser,
userCounters = _} = PolyML.Statistics.getLocalStats ()
in
- [("now", signed_string_of_real (Time.toReal (Time.now ()))),
- ("full_GCs", Markup.print_int gcFullGCs),
+ [("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),
--- a/src/Pure/System/build.ML Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/System/build.ML Thu Nov 29 10:45:25 2012 +0100
@@ -27,7 +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")
+ |> Unsynchronized.setmp Future.ML_statistics (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 19:19:39 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML Thu Nov 29 10:45:25 2012 +0100
@@ -217,7 +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";
+ Future.ML_statistics := 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