tuned tracing;
authorwenzelm
Sat Jul 25 00:53:47 2009 +0200 (2009-07-25 ago)
changeset 321868026b73cd357
parent 32185 57ecfab3bcfe
child 32187 cca43ca13f4f
tuned tracing;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/simple_thread.ML
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Sat Jul 25 00:39:05 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Jul 25 00:53:47 2009 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4  fun count_active ws =
     1.5    fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0;
     1.6  
     1.7 -fun trace_active () = Multithreading.tracing 1 (fn () =>
     1.8 +fun trace_active () = Multithreading.tracing 6 (fn () =>
     1.9    let
    1.10      val ws = ! workers;
    1.11      val m = string_of_int (length ws);
    1.12 @@ -222,7 +222,7 @@
    1.13  fun scheduler_next () = (*requires SYNCHRONIZED*)
    1.14    let
    1.15      (*queue status*)
    1.16 -    val _ = Multithreading.tracing 1 (fn () =>
    1.17 +    val _ = Multithreading.tracing 6 (fn () =>
    1.18        let val {ready, pending, running} = Task_Queue.status (! queue) in
    1.19          "SCHEDULE: " ^
    1.20            string_of_int ready ^ " ready, " ^
    1.21 @@ -338,8 +338,12 @@
    1.22          if SYNCHRONIZED "join_wait" (fn () =>
    1.23            is_finished x orelse (if worker then worker_wait () else wait (); false))
    1.24          then () else join_wait x;
    1.25 -      val _ = List.app join_wait xs;
    1.26  
    1.27 +      val _ = xs |> List.app (fn x =>
    1.28 +        let val time = Multithreading.real_time join_wait x in
    1.29 +          Multithreading.tracing_time true time
    1.30 +            (fn () => "joined after " ^ Time.toString time)
    1.31 +        end);
    1.32      in map get_result xs end) ();
    1.33  
    1.34  end;
     2.1 --- a/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:39:05 2009 +0200
     2.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:53:47 2009 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4          let
     2.5            val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
     2.6            val time = Multithreading.real_time Mutex.lock lock;
     2.7 -          val _ = Multithreading.tracing_time time
     2.8 +          val _ = Multithreading.tracing_time true time
     2.9              (fn () => name ^ ": locked after " ^ Time.toString time);
    2.10          in false end;
    2.11      val result = Exn.capture (restore_attributes e) ();
     3.1 --- a/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:39:05 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:53:47 2009 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4    include BASIC_MULTITHREADING
     3.5    val trace: int ref
     3.6    val tracing: int -> (unit -> string) -> unit
     3.7 -  val tracing_time: Time.time -> (unit -> string) -> unit
     3.8 +  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
     3.9    val real_time: ('a -> unit) -> 'a -> Time.time
    3.10    val available: bool
    3.11    val max_threads: int ref
    3.12 @@ -37,7 +37,7 @@
    3.13  
    3.14  val trace = ref (0: int);
    3.15  fun tracing _ _ = ();
    3.16 -fun tracing_time _ _ = ();
    3.17 +fun tracing_time _ _ _ = ();
    3.18  fun real_time f x = (f x; Time.zeroTime);
    3.19  
    3.20  
     4.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:39:05 2009 +0200
     4.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:53:47 2009 +0200
     4.3 @@ -36,9 +36,10 @@
     4.4    else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
     4.5      handle _ (*sic*) => ();
     4.6  
     4.7 -fun tracing_time time =
     4.8 +fun tracing_time detailed time =
     4.9    tracing
    4.10 -   (if Time.>= (time, Time.fromMilliseconds 1000) then 1
    4.11 +   (if not detailed then 5
    4.12 +    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
    4.13      else if Time.>= (time, Time.fromMilliseconds 100) then 2
    4.14      else if Time.>= (time, Time.fromMilliseconds 10) then 3
    4.15      else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    4.16 @@ -231,7 +232,7 @@
    4.17              let
    4.18                val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    4.19                val time = real_time Mutex.lock critical_lock;
    4.20 -              val _ = tracing_time time (fn () =>
    4.21 +              val _ = tracing_time true time (fn () =>
    4.22                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    4.23              in () end;
    4.24          val _ = critical_thread := SOME (Thread.self ());