added Multithreading.real_time;
authorwenzelm
Sat Jul 25 00:39:05 2009 +0200 (2009-07-25 ago)
changeset 3218557ecfab3bcfe
parent 32184 cfa0ef0c0c5f
child 32186 8026b73cd357
added Multithreading.real_time;
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	Sat Jul 25 00:13:39 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:39:05 2009 +0200
     1.3 @@ -29,12 +29,10 @@
     1.4        if Mutex.trylock lock then true
     1.5        else
     1.6          let
     1.7 -          val timer = Timer.startRealTimer ();
     1.8            val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
     1.9 -          val _ = Mutex.lock lock;
    1.10 -          val time = Timer.checkRealTimer timer;
    1.11 -          val _ = Multithreading.tracing_time time (fn () =>
    1.12 -            name ^ ": locked after " ^ Time.toString time);
    1.13 +          val time = Multithreading.real_time Mutex.lock lock;
    1.14 +          val _ = Multithreading.tracing_time time
    1.15 +            (fn () => name ^ ": locked after " ^ Time.toString time);
    1.16          in false end;
    1.17      val result = Exn.capture (restore_attributes e) ();
    1.18      val _ =
     2.1 --- a/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:13:39 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:39:05 2009 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    val trace: int ref
     2.5    val tracing: int -> (unit -> string) -> unit
     2.6    val tracing_time: Time.time -> (unit -> string) -> unit
     2.7 +  val real_time: ('a -> unit) -> 'a -> Time.time
     2.8    val available: bool
     2.9    val max_threads: int ref
    2.10    val max_threads_value: unit -> int
    2.11 @@ -32,11 +33,15 @@
    2.12  structure Multithreading: MULTITHREADING =
    2.13  struct
    2.14  
    2.15 -(* options *)
    2.16 +(* tracing *)
    2.17  
    2.18  val trace = ref (0: int);
    2.19  fun tracing _ _ = ();
    2.20  fun tracing_time _ _ = ();
    2.21 +fun real_time f x = (f x; Time.zeroTime);
    2.22 +
    2.23 +
    2.24 +(* options *)
    2.25  
    2.26  val available = false;
    2.27  val max_threads = ref (1: int);
     3.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:39:05 2009 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4  structure Multithreading: MULTITHREADING =
     3.5  struct
     3.6  
     3.7 -(* options *)
     3.8 +(* tracing *)
     3.9  
    3.10  val trace = ref 0;
    3.11  
    3.12 @@ -43,6 +43,15 @@
    3.13      else if Time.>= (time, Time.fromMilliseconds 10) then 3
    3.14      else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    3.15  
    3.16 +fun real_time f x =
    3.17 +  let
    3.18 +    val timer = Timer.startRealTimer ();
    3.19 +    val () = f x;
    3.20 +    val time = Timer.checkRealTimer timer;
    3.21 +  in time end;
    3.22 +
    3.23 +
    3.24 +(* options *)
    3.25  
    3.26  val available = true;
    3.27  
    3.28 @@ -220,10 +229,8 @@
    3.29            if Mutex.trylock critical_lock then ()
    3.30            else
    3.31              let
    3.32 -              val timer = Timer.startRealTimer ();
    3.33                val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    3.34 -              val _ = Mutex.lock critical_lock;
    3.35 -              val time = Timer.checkRealTimer timer;
    3.36 +              val time = real_time Mutex.lock critical_lock;
    3.37                val _ = tracing_time time (fn () =>
    3.38                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    3.39              in () end;