future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
authorwenzelm
Tue Jul 21 23:42:29 2009 +0200 (2009-07-21 ago)
changeset 3210747d0da617fcc
parent 32106 d7697e311d81
child 32108 77094a0bbc3e
future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
control combinators: paranoia eta-expansion to ensure proper operational semantics;
src/Pure/Concurrent/future.ML
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 21 20:37:32 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 21 23:42:29 2009 +0200
     1.3 @@ -157,14 +157,19 @@
     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 Multithreading.restricted_interrupts
     1.8 -      (fn _ => fn ok =>
     1.9 -        let
    1.10 -          val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
    1.11 -          val _ = result := SOME res;
    1.12 -          val _ = (case res of Exn.Exn exn => Task_Queue.cancel_group group exn | _ => ());
    1.13 -          val res_ok = is_some (Exn.get_result res);
    1.14 -        in res_ok end);
    1.15 +    fun job ok =
    1.16 +      let
    1.17 +        val res =
    1.18 +          if ok then
    1.19 +            Multithreading.with_attributes Multithreading.restricted_interrupts
    1.20 +              (fn _ => fn () => Exn.capture e ()) ()
    1.21 +          else Exn.Exn Exn.Interrupt;
    1.22 +        val _ = result := SOME res;
    1.23 +      in
    1.24 +        (case res of
    1.25 +          Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
    1.26 +        | Exn.Result _ => true)
    1.27 +      end;
    1.28    in (result, job) end;
    1.29  
    1.30  fun do_cancel group = (*requires SYNCHRONIZED*)
    1.31 @@ -203,7 +208,7 @@
    1.32      | some => some);
    1.33  
    1.34  fun worker_loop name =
    1.35 -  (case SYNCHRONIZED name worker_next of
    1.36 +  (case SYNCHRONIZED name (fn () => worker_next ()) of
    1.37      NONE => ()
    1.38    | SOME work => (execute name work; worker_loop name));
    1.39  
    1.40 @@ -259,7 +264,7 @@
    1.41    in continue end;
    1.42  
    1.43  fun scheduler_loop () =
    1.44 -  while SYNCHRONIZED "scheduler" scheduler_next do ();
    1.45 +  while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ();
    1.46  
    1.47  fun scheduler_active () = (*requires SYNCHRONIZED*)
    1.48    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 21 20:37:32 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 21 23:42:29 2009 +0200
     2.3 @@ -92,10 +92,12 @@
     2.4      val _ = Thread.setAttributes orig_atts;
     2.5    in Exn.release result end;
     2.6  
     2.7 -fun interruptible f = with_attributes regular_interrupts (fn _ => f);
     2.8 +fun interruptible f =
     2.9 +  with_attributes regular_interrupts (fn _ => fn x => f x);
    2.10  
    2.11  fun uninterruptible f =
    2.12 -  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
    2.13 +  with_attributes no_interrupts (fn atts => fn x =>
    2.14 +    f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
    2.15  
    2.16  
    2.17  (* execution with time limit *)