1.1 --- a/src/Pure/Concurrent/future.ML	Wed Nov 28 19:19:39 2012 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Nov 29 10:45:25 2012 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val task_of: 'a future -> task
     1.5    val peek: 'a future -> 'a Exn.result option
     1.6    val is_finished: 'a future -> bool
     1.7 +  val ML_statistics: bool Unsynchronized.ref
     1.8    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.9    val cancel_group: group -> unit
    1.10    val cancel: 'a future -> unit
    1.11 @@ -169,6 +170,10 @@
    1.12  val max_active = Unsynchronized.ref 0;
    1.13  val worker_trend = Unsynchronized.ref 0;
    1.14  
    1.15 +val status_ticks = Unsynchronized.ref 0;
    1.16 +val last_round = Unsynchronized.ref Time.zeroTime;
    1.17 +val next_round = seconds 0.05;
    1.18 +
    1.19  datatype worker_state = Working | Waiting | Sleeping;
    1.20  val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
    1.21  
    1.22 @@ -176,6 +181,32 @@
    1.23    fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
    1.24  
    1.25  
    1.26 +
    1.27 +(* status *)
    1.28 +
    1.29 +val ML_statistics = Unsynchronized.ref false;
    1.30 +
    1.31 +fun report_status () = (*requires SYNCHRONIZED*)
    1.32 +  if ! ML_statistics then
    1.33 +    let
    1.34 +      val {ready, pending, running, passive} = Task_Queue.status (! queue);
    1.35 +      val total = length (! workers);
    1.36 +      val active = count_workers Working;
    1.37 +      val waiting = count_workers Waiting;
    1.38 +      val stats =
    1.39 +       [("now", signed_string_of_real (Time.toReal (Time.now ()))),
    1.40 +        ("tasks_ready", Markup.print_int ready),
    1.41 +        ("tasks_pending", Markup.print_int pending),
    1.42 +        ("tasks_running", Markup.print_int running),
    1.43 +        ("tasks_passive", Markup.print_int passive),
    1.44 +        ("workers_total", Markup.print_int total),
    1.45 +        ("workers_active", Markup.print_int active),
    1.46 +        ("workers_waiting", Markup.print_int waiting)] @
    1.47 +        ML_Statistics.get ();
    1.48 +    in Output.protocol_message (Markup.ML_statistics @ stats) "" end
    1.49 +  else ();
    1.50 +
    1.51 +
    1.52  (* cancellation primitives *)
    1.53  
    1.54  fun cancel_now group = (*requires SYNCHRONIZED*)
    1.55 @@ -271,18 +302,6 @@
    1.56  
    1.57  (* scheduler *)
    1.58  
    1.59 -fun ML_statistics () =
    1.60 -  if ! ML_Statistics.enabled then
    1.61 -    (case ML_Statistics.get () of
    1.62 -      [] => ()
    1.63 -    | stats => Output.protocol_message (Markup.ML_statistics @ stats) "")
    1.64 -  else ();
    1.65 -
    1.66 -val status_ticks = Unsynchronized.ref 0;
    1.67 -
    1.68 -val last_round = Unsynchronized.ref Time.zeroTime;
    1.69 -val next_round = seconds 0.05;
    1.70 -
    1.71  fun scheduler_next () = (*requires SYNCHRONIZED*)
    1.72    let
    1.73      val now = Time.now ();
    1.74 @@ -290,30 +309,12 @@
    1.75      val _ = if tick then last_round := now else ();
    1.76  
    1.77  
    1.78 -    (* queue and worker status *)
    1.79 +    (* runtime status *)
    1.80  
    1.81      val _ =
    1.82        if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else ();
    1.83      val _ =
    1.84 -      if tick andalso ! status_ticks = 0 then
    1.85 -       (ML_statistics ();
    1.86 -        Multithreading.tracing 1 (fn () =>
    1.87 -          let
    1.88 -            val {ready, pending, running, passive} = Task_Queue.status (! queue);
    1.89 -            val total = length (! workers);
    1.90 -            val active = count_workers Working;
    1.91 -            val waiting = count_workers Waiting;
    1.92 -          in
    1.93 -            "SCHEDULE " ^ Time.toString now ^ ": " ^
    1.94 -              string_of_int ready ^ " ready, " ^
    1.95 -              string_of_int pending ^ " pending, " ^
    1.96 -              string_of_int running ^ " running, " ^
    1.97 -              string_of_int passive ^ " passive; " ^
    1.98 -              string_of_int total ^ " workers, " ^
    1.99 -              string_of_int active ^ " active, " ^
   1.100 -              string_of_int waiting ^ " waiting "
   1.101 -          end))
   1.102 -      else ();
   1.103 +      if tick andalso ! status_ticks = 0 then report_status () else ();
   1.104  
   1.105      val _ =
   1.106        if forall (Thread.isActive o #1) (! workers) then ()
   1.107 @@ -400,7 +401,7 @@
   1.108      Multithreading.with_attributes
   1.109        (Multithreading.sync_interrupts Multithreading.public_interrupts)
   1.110        (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
   1.111 -  do (); last_round := Time.zeroTime; ML_statistics ());
   1.112 +  do (); last_round := Time.zeroTime; report_status ());
   1.113  
   1.114  fun scheduler_active () = (*requires SYNCHRONIZED*)
   1.115    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
   1.116 @@ -665,11 +666,6 @@
   1.117    else ();
   1.118  
   1.119  
   1.120 -(* queue status *)
   1.121 -
   1.122 -fun queue_status () = Task_Queue.status (! queue);
   1.123 -
   1.124 -
   1.125  (*final declarations of this structure!*)
   1.126  val map = map_future;
   1.127