1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 22:42:02 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 23:27:40 2007 +0200
     1.3 @@ -10,6 +10,9 @@
     1.4  structure Multithreading: MULTITHREADING =
     1.5  struct
     1.6  
     1.7 +
     1.8 +(* flags *)
     1.9 +
    1.10  val trace = ref false;
    1.11  fun tracing msg =
    1.12    if ! trace
    1.13 @@ -20,16 +23,22 @@
    1.14  val max_threads = ref 1;
    1.15  
    1.16  
    1.17 +(* misc utils *)
    1.18 +
    1.19 +fun show "" = ""
    1.20 +  | show name = " " ^ name;
    1.21 +
    1.22 +fun show' "" = ""
    1.23 +  | show' name = " [" ^ name ^ "]";
    1.24 +
    1.25 +fun inc i = (i := ! i + 1; ! i);
    1.26 +fun dec i = (i := ! i - 1; ! i);
    1.27 +
    1.28 +
    1.29  (* critical section -- may be nested within the same thread *)
    1.30  
    1.31  local
    1.32  
    1.33 -fun add_name "" = ""
    1.34 -  | add_name name = " " ^ name;
    1.35 -
    1.36 -fun add_name' "" = ""
    1.37 -  | add_name' name = " [" ^ name ^ "]";
    1.38 -
    1.39  val critical_lock = Mutex.mutex ();
    1.40  val critical_thread = ref (NONE: Thread.thread option);
    1.41  val critical_name = ref "";
    1.42 @@ -51,10 +60,10 @@
    1.43            let
    1.44              val timer = Timer.startRealTimer ();
    1.45              val _ = tracing (fn () =>
    1.46 -              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": waiting for lock");
    1.47 +              "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": waiting");
    1.48              val _ = Mutex.lock critical_lock;
    1.49              val _ = tracing (fn () =>
    1.50 -              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": obtained lock after " ^
    1.51 +              "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^
    1.52                Time.toString (Timer.checkRealTimer timer));
    1.53            in () end;
    1.54        val _ = critical_thread := SOME (Thread.self ());
    1.55 @@ -72,8 +81,11 @@
    1.56  
    1.57  (* scheduling -- non-interruptible threads working on a queue of tasks *)
    1.58  
    1.59 -fun inc i = (i := ! i + 1; ! i);
    1.60 -fun dec i = (i := ! i - 1; ! i);
    1.61 +local
    1.62 +
    1.63 +val protected_name = ref "";
    1.64 +
    1.65 +in
    1.66  
    1.67  fun schedule n next_task tasks =
    1.68    let
    1.69 @@ -84,10 +96,12 @@
    1.70          val _ =
    1.71            if Mutex.trylock lock then ()
    1.72            else
    1.73 -           (tracing (fn () => "PROTECTED " ^ name ^ ": waiting for lock");
    1.74 +           (tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting");
    1.75              Mutex.lock lock;
    1.76 -            tracing (fn () => "PROTECTED " ^ name ^ ": obtained lock"));
    1.77 +            tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed"));
    1.78 +        val _ = protected_name := name;
    1.79          val res = Exn.capture e ();
    1.80 +        val _ = protected_name := "";
    1.81          val _ = Mutex.unlock lock;
    1.82        in Exn.release res end;
    1.83  
    1.84 @@ -140,5 +154,7 @@
    1.85  
    1.86  end;
    1.87  
    1.88 +end;
    1.89 +
    1.90  val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.91  val CRITICAL = Multithreading.CRITICAL;