src/Pure/ML-Systems/multithreading_polyml.ML
changeset 24214 0482ecc4ef11
parent 24208 f4cafbaa05e4
child 24291 fa72aab966dc
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Aug 10 11:02:09 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Aug 10 14:49:01 2007 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Multithreading in Poly/ML (version 5.1).
     1.8 +Multithreading in Poly/ML 5.1 or later (cf. polyml/basis/Thread.sml).
     1.9  *)
    1.10  
    1.11  open Thread;
    1.12 @@ -10,8 +10,8 @@
    1.13  signature MULTITHREADING =
    1.14  sig
    1.15    include MULTITHREADING
    1.16 -  val uninterruptible: ('a -> 'b) -> 'a -> 'b
    1.17 -  val interruptible: ('a -> 'b) -> 'a -> 'b
    1.18 +  val uninterruptible: (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    1.19 +  val interruptible: (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    1.20  end;
    1.21  
    1.22  structure Multithreading: MULTITHREADING =
    1.23 @@ -44,17 +44,16 @@
    1.24  
    1.25  (* thread attributes *)
    1.26  
    1.27 -local
    1.28 -
    1.29  fun with_attributes new_atts f x =
    1.30    let
    1.31      val orig_atts = Thread.getAttributes ();
    1.32      fun restore () = Thread.setAttributes orig_atts;
    1.33    in
    1.34      Exn.release
    1.35 -     (let
    1.36 +    (*RACE for fully asynchronous interrupts!*)
    1.37 +    (let
    1.38          val _ = Thread.setAttributes new_atts;
    1.39 -        val result = Exn.capture f x;
    1.40 +        val result = Exn.capture (f orig_atts) x;
    1.41          val _ = restore ();
    1.42        in result end
    1.43        handle Interrupt => (restore (); Exn.Exn Interrupt))
    1.44 @@ -62,13 +61,9 @@
    1.45  
    1.46  fun with_interrupt_state state = with_attributes [Thread.InterruptState state];
    1.47  
    1.48 -in
    1.49 -
    1.50  fun uninterruptible f x = with_interrupt_state Thread.InterruptDefer f x;
    1.51  fun interruptible f x = with_interrupt_state Thread.InterruptAsynchOnce f x;
    1.52  
    1.53 -end;
    1.54 -
    1.55  
    1.56  (* critical section -- may be nested within the same thread *)
    1.57  
    1.58 @@ -88,7 +83,7 @@
    1.59  fun NAMED_CRITICAL name e =
    1.60    if self_critical () then e ()
    1.61    else
    1.62 -    uninterruptible (fn () =>
    1.63 +    uninterruptible (fn atts => fn () =>
    1.64        let
    1.65          val name' = ! critical_name;
    1.66          val _ =
    1.67 @@ -104,7 +99,7 @@
    1.68              in () end;
    1.69          val _ = critical_thread := SOME (Thread.self ());
    1.70          val _ = critical_name := name;
    1.71 -        val result = Exn.capture e ();
    1.72 +        val result = Exn.capture (with_attributes atts (fn _ => e)) ();
    1.73          val _ = critical_name := "";
    1.74          val _ = critical_thread := NONE;
    1.75          val _ = Mutex.unlock critical_lock;
    1.76 @@ -126,7 +121,7 @@
    1.77  
    1.78  in
    1.79  
    1.80 -fun schedule n next_task = uninterruptible (fn tasks =>
    1.81 +fun schedule n next_task = uninterruptible (fn _ => fn tasks =>
    1.82    let
    1.83      (*protected execution*)
    1.84      val lock = Mutex.mutex ();
    1.85 @@ -152,7 +147,7 @@
    1.86      fun wakeup_all () = ConditionVar.broadcast wakeup;
    1.87      fun wait () = ConditionVar.wait (wakeup, lock);
    1.88  
    1.89 -    (*the queue of tasks*)
    1.90 +    (*queue of tasks*)
    1.91      val queue = ref tasks;
    1.92      val active = ref 0;
    1.93      fun trace_active () = tracing 1 (fn () => "SCHEDULE: " ^ Int.toString (! active) ^ " active");
    1.94 @@ -183,7 +178,7 @@
    1.95      fun worker () =
    1.96        (case PROTECTED "dequeue" dequeue of
    1.97          Task {body, cont, fail} =>
    1.98 -          (case Exn.capture (interruptible body) () of
    1.99 +          (case Exn.capture (interruptible (fn _ => body)) () of
   1.100              Exn.Result () =>
   1.101                (PROTECTED "cont" (fn () => (change queue cont; wakeup_all ())); worker ())
   1.102            | Exn.Exn exn =>