# HG changeset patch
# User wenzelm
# Date 1185722937 -7200
# Node ID b643ee118928266d1c385e053408533a6ed13c5b
# Parent  89a5382406a1a97984e3cc4688eeb24a6ca8dd20
critical: improved diagostics;
schedule: proper broadcast on wakeup condition;

diff -r 89a5382406a1 -r b643ee118928 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 17:28:56 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 17:28:57 2007 +0200
@@ -26,6 +26,13 @@
 
 val critical_lock = Mutex.mutex ();
 val critical_thread = ref (NONE: Thread.thread option);
+val critical_name = ref "";
+
+fun add_name "" = ""
+  | add_name name = " " ^ name;
+
+fun add_name' "" = ""
+  | add_name' name = " [" ^ name ^ "]";
 
 in
 
@@ -41,13 +48,19 @@
       val _ =
         if Mutex.trylock critical_lock then ()
         else
-         (tracing (fn () =>
-            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": waiting for lock");
-          Mutex.lock critical_lock;
-          tracing (fn () =>
-            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": obtained lock"));
+          let
+            val timer = Timer.startRealTimer ();
+            val _ = tracing (fn () =>
+              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": waiting for lock");
+            val _ = Mutex.lock critical_lock;
+            val _ = tracing (fn () =>
+              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": obtained lock after " ^
+              Time.toString (Timer.checkRealTimer timer));
+          in () end;
       val _ = critical_thread := SOME (Thread.self ());
+      val _ = critical_name := name;
       val result = Exn.capture e ();
+      val _ = critical_name := "";
       val _ = critical_thread := NONE;
       val _ = Mutex.unlock critical_lock;
     in Exn.release result end;
@@ -86,10 +99,10 @@
     (*worker threads*)
     val running = ref 0;
     val status = ref ([]: exn list);
-    val finished = ConditionVar.conditionVar ();
-    fun wait () = ConditionVar.waitUntil (finished, lock, Time.fromMilliseconds 500);
+    val wakeup = ConditionVar.conditionVar ();
+    fun wait () = ConditionVar.wait (wakeup, lock);
     fun continue cont k =
-      (PROTECTED k (fn () => queue := cont (! queue)); ConditionVar.signal finished; work k ())
+      (PROTECTED k (fn () => queue := cont (! queue)); ConditionVar.broadcast wakeup; work k ())
     and work k () =
       (case dequeue k of
         (Task.Task f, cont) =>
@@ -104,7 +117,7 @@
       | (Task.Finished, _) =>
          (tracing (fn () => "TERMINATING " ^ Int.toString k);
           PROTECTED k (fn () => running := ! running - 1);
-          ConditionVar.signal finished));
+          ConditionVar.broadcast wakeup));
 
     (*main control: fork and wait*)
     fun fork 0 = ()