more robust scheduler shutdown, notably for spurious crashes;
authorwenzelm
Wed Jul 29 14:23:19 2020 +0200 (2 weeks ago)
changeset 72078b8d0b8659e0a
parent 72077 1d6c3cba47fe
child 72079 8c355e2dd7db
child 72089 8348bba699e6
more robust scheduler shutdown, notably for spurious crashes;
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jul 27 15:58:43 2020 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Jul 29 14:23:19 2020 +0200
     1.3 @@ -285,6 +285,9 @@
     1.4  
     1.5  (* scheduler *)
     1.6  
     1.7 +fun scheduler_end () = (*requires SYNCHRONIZED*)
     1.8 +  (report_status (); scheduler := NONE);
     1.9 +
    1.10  fun scheduler_next () = (*requires SYNCHRONIZED*)
    1.11    let
    1.12      val now = Time.now ();
    1.13 @@ -354,16 +357,18 @@
    1.14      (* shutdown *)
    1.15  
    1.16      val continue = not (! do_shutdown andalso null (! workers));
    1.17 -    val _ = if continue then () else (report_status (); scheduler := NONE);
    1.18 +    val _ = if continue then () else scheduler_end ();
    1.19  
    1.20      val _ = broadcast scheduler_event;
    1.21    in continue end
    1.22    handle exn =>
    1.23 +   (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
    1.24      if Exn.is_interrupt exn then
    1.25 -     (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
    1.26 -      List.app cancel_later (cancel_all ());
    1.27 +     (List.app cancel_later (cancel_all ());
    1.28        signal work_available; true)
    1.29 -    else Exn.reraise exn;
    1.30 +    else
    1.31 +     (scheduler_end ();
    1.32 +      Exn.reraise exn));
    1.33  
    1.34  fun scheduler_loop () =
    1.35   (while
    1.36 @@ -705,7 +710,7 @@
    1.37        while scheduler_active () do
    1.38         (do_shutdown := true;
    1.39          Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
    1.40 -        wait scheduler_event));
    1.41 +        wait_timeout next_round scheduler_event));
    1.42  
    1.43  
    1.44  (*final declarations of this structure!*)