simplified/unified Multithreading.tracing_time;
authorwenzelm
Sat Jul 25 00:13:39 2009 +0200 (2009-07-25)
changeset 32184cfa0ef0c0c5f
parent 32183 678f14c9afb5
child 32185 57ecfab3bcfe
simplified/unified Multithreading.tracing_time;
tuned;
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/simple_thread.ML	Fri Jul 24 23:36:37 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:13:39 2009 +0200
     1.3 @@ -28,13 +28,17 @@
     1.4      val immediate =
     1.5        if Mutex.trylock lock then true
     1.6        else
     1.7 -       (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
     1.8 -        Mutex.lock lock;
     1.9 -        Multithreading.tracing 3 (fn () => name ^ ": locked");
    1.10 -        false);
    1.11 +        let
    1.12 +          val timer = Timer.startRealTimer ();
    1.13 +          val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
    1.14 +          val _ = Mutex.lock lock;
    1.15 +          val time = Timer.checkRealTimer timer;
    1.16 +          val _ = Multithreading.tracing_time time (fn () =>
    1.17 +            name ^ ": locked after " ^ Time.toString time);
    1.18 +        in false end;
    1.19      val result = Exn.capture (restore_attributes e) ();
    1.20      val _ =
    1.21 -      if immediate then () else Multithreading.tracing 3 (fn () => name ^ ": unlocking ...");
    1.22 +      if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
    1.23      val _ = Mutex.unlock lock;
    1.24    in result end) ());
    1.25  
     2.1 --- a/src/Pure/ML-Systems/multithreading.ML	Fri Jul 24 23:36:37 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:13:39 2009 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4    include BASIC_MULTITHREADING
     2.5    val trace: int ref
     2.6    val tracing: int -> (unit -> string) -> unit
     2.7 +  val tracing_time: Time.time -> (unit -> string) -> unit
     2.8    val available: bool
     2.9    val max_threads: int ref
    2.10    val max_threads_value: unit -> int
    2.11 @@ -35,6 +36,7 @@
    2.12  
    2.13  val trace = ref (0: int);
    2.14  fun tracing _ _ = ();
    2.15 +fun tracing_time _ _ = ();
    2.16  
    2.17  val available = false;
    2.18  val max_threads = ref (1: int);
     3.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Jul 24 23:36:37 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
     3.3 @@ -36,6 +36,14 @@
     3.4    else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
     3.5      handle _ (*sic*) => ();
     3.6  
     3.7 +fun tracing_time time =
     3.8 +  tracing
     3.9 +   (if Time.>= (time, Time.fromMilliseconds 1000) then 1
    3.10 +    else if Time.>= (time, Time.fromMilliseconds 100) then 2
    3.11 +    else if Time.>= (time, Time.fromMilliseconds 10) then 3
    3.12 +    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    3.13 +
    3.14 +
    3.15  val available = true;
    3.16  
    3.17  val max_threads = ref 0;
    3.18 @@ -205,7 +213,7 @@
    3.19  fun NAMED_CRITICAL name e =
    3.20    if self_critical () then e ()
    3.21    else
    3.22 -    uninterruptible (fn restore_attributes => fn () =>
    3.23 +    Exn.release (uninterruptible (fn restore_attributes => fn () =>
    3.24        let
    3.25          val name' = ! critical_name;
    3.26          val _ =
    3.27 @@ -213,14 +221,10 @@
    3.28            else
    3.29              let
    3.30                val timer = Timer.startRealTimer ();
    3.31 -              val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    3.32 +              val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    3.33                val _ = Mutex.lock critical_lock;
    3.34                val time = Timer.checkRealTimer timer;
    3.35 -              val trace_time =
    3.36 -                if Time.>= (time, Time.fromMilliseconds 1000) then 1
    3.37 -                else if Time.>= (time, Time.fromMilliseconds 100) then 2
    3.38 -                else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4;
    3.39 -              val _ = tracing trace_time (fn () =>
    3.40 +              val _ = tracing_time time (fn () =>
    3.41                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    3.42              in () end;
    3.43          val _ = critical_thread := SOME (Thread.self ());
    3.44 @@ -229,7 +233,7 @@
    3.45          val _ = critical_name := "";
    3.46          val _ = critical_thread := NONE;
    3.47          val _ = Mutex.unlock critical_lock;
    3.48 -      in Exn.release result end) ();
    3.49 +      in result end) ());
    3.50  
    3.51  fun CRITICAL e = NAMED_CRITICAL "" e;
    3.52