future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
authorwenzelm
Fri Mar 20 20:20:09 2009 +0100 (2009-03-20 ago)
changeset 30612cb6421b6a18f
parent 30611 591fefcf184e
child 30613 b22d35d9ef28
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
src/Pure/Concurrent/future.ML
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri Mar 20 20:05:51 2009 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Mar 20 20:20:09 2009 +0100
     1.3 @@ -236,7 +236,7 @@
     1.4  fun future_job group (e: unit -> 'a) =
     1.5    let
     1.6      val result = ref (NONE: 'a Exn.result option);
     1.7 -    val job = Multithreading.with_attributes (Thread.getAttributes ())
     1.8 +    val job = Multithreading.with_attributes Multithreading.restricted_interrupts
     1.9        (fn _ => fn ok =>
    1.10          let
    1.11            val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
     2.1 --- a/src/Pure/ML-Systems/multithreading.ML	Fri Mar 20 20:05:51 2009 +0100
     2.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Fri Mar 20 20:20:09 2009 +0100
     2.3 @@ -21,6 +21,7 @@
     2.4    val enabled: unit -> bool
     2.5    val no_interrupts: Thread.threadAttribute list
     2.6    val regular_interrupts: Thread.threadAttribute list
     2.7 +  val restricted_interrupts: Thread.threadAttribute list
     2.8    val with_attributes: Thread.threadAttribute list ->
     2.9      (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    2.10    val self_critical: unit -> bool
    2.11 @@ -46,6 +47,9 @@
    2.12  val regular_interrupts =
    2.13    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    2.14  
    2.15 +val restricted_interrupts =
    2.16 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
    2.17 +
    2.18  fun with_attributes _ f x = f [] x;
    2.19  
    2.20  
     3.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 20:05:51 2009 +0100
     3.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 20:20:09 2009 +0100
     3.3 @@ -69,6 +69,9 @@
     3.4  val regular_interrupts =
     3.5    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
     3.6  
     3.7 +val restricted_interrupts =
     3.8 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
     3.9 +
    3.10  val safe_interrupts = map
    3.11    (fn Thread.InterruptState Thread.InterruptAsynch =>
    3.12        Thread.InterruptState Thread.InterruptAsynchOnce