critical: improved diagostics;
authorwenzelm
Sun Jul 29 17:28:57 2007 +0200 (2007-07-29)
changeset 24060b643ee118928
parent 24059 89a5382406a1
child 24061 68d2b6cf5194
critical: improved diagostics;
schedule: proper broadcast on wakeup condition;
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 17:28:56 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 17:28:57 2007 +0200
     1.3 @@ -26,6 +26,13 @@
     1.4  
     1.5  val critical_lock = Mutex.mutex ();
     1.6  val critical_thread = ref (NONE: Thread.thread option);
     1.7 +val critical_name = ref "";
     1.8 +
     1.9 +fun add_name "" = ""
    1.10 +  | add_name name = " " ^ name;
    1.11 +
    1.12 +fun add_name' "" = ""
    1.13 +  | add_name' name = " [" ^ name ^ "]";
    1.14  
    1.15  in
    1.16  
    1.17 @@ -41,13 +48,19 @@
    1.18        val _ =
    1.19          if Mutex.trylock critical_lock then ()
    1.20          else
    1.21 -         (tracing (fn () =>
    1.22 -            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": waiting for lock");
    1.23 -          Mutex.lock critical_lock;
    1.24 -          tracing (fn () =>
    1.25 -            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": obtained lock"));
    1.26 +          let
    1.27 +            val timer = Timer.startRealTimer ();
    1.28 +            val _ = tracing (fn () =>
    1.29 +              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": waiting for lock");
    1.30 +            val _ = Mutex.lock critical_lock;
    1.31 +            val _ = tracing (fn () =>
    1.32 +              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": obtained lock after " ^
    1.33 +              Time.toString (Timer.checkRealTimer timer));
    1.34 +          in () end;
    1.35        val _ = critical_thread := SOME (Thread.self ());
    1.36 +      val _ = critical_name := name;
    1.37        val result = Exn.capture e ();
    1.38 +      val _ = critical_name := "";
    1.39        val _ = critical_thread := NONE;
    1.40        val _ = Mutex.unlock critical_lock;
    1.41      in Exn.release result end;
    1.42 @@ -86,10 +99,10 @@
    1.43      (*worker threads*)
    1.44      val running = ref 0;
    1.45      val status = ref ([]: exn list);
    1.46 -    val finished = ConditionVar.conditionVar ();
    1.47 -    fun wait () = ConditionVar.waitUntil (finished, lock, Time.fromMilliseconds 500);
    1.48 +    val wakeup = ConditionVar.conditionVar ();
    1.49 +    fun wait () = ConditionVar.wait (wakeup, lock);
    1.50      fun continue cont k =
    1.51 -      (PROTECTED k (fn () => queue := cont (! queue)); ConditionVar.signal finished; work k ())
    1.52 +      (PROTECTED k (fn () => queue := cont (! queue)); ConditionVar.broadcast wakeup; work k ())
    1.53      and work k () =
    1.54        (case dequeue k of
    1.55          (Task.Task f, cont) =>
    1.56 @@ -104,7 +117,7 @@
    1.57        | (Task.Finished, _) =>
    1.58           (tracing (fn () => "TERMINATING " ^ Int.toString k);
    1.59            PROTECTED k (fn () => running := ! running - 1);
    1.60 -          ConditionVar.signal finished));
    1.61 +          ConditionVar.broadcast wakeup));
    1.62  
    1.63      (*main control: fork and wait*)
    1.64      fun fork 0 = ()