src/Pure/Concurrent/future.ML
changeset 28470 409fedeece30
parent 28468 7c80ab57f56d
child 28471 00046e3b46b5
     1.1 --- a/src/Pure/Concurrent/future.ML	Thu Oct 02 23:52:10 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Oct 02 23:52:12 2008 +0200
     1.3 @@ -188,6 +188,11 @@
     1.4  
     1.5  (* scheduler *)
     1.6  
     1.7 +fun heartbeat name =
     1.8 + (Multithreading.tracing 1 (fn () => name);
     1.9 +  OS.Process.sleep (Time.fromMilliseconds 100);
    1.10 +  if ! do_shutdown then () else heartbeat name);
    1.11 +
    1.12  fun scheduler_next () = (*requires SYNCHRONIZED*)
    1.13    let
    1.14      (*worker threads*)
    1.15 @@ -227,7 +232,8 @@
    1.16  fun scheduler_check name = SYNCHRONIZED name (fn () =>
    1.17    if not (scheduler_active ()) then
    1.18      (Multithreading.tracing 2 (fn () => "scheduler: fork");
    1.19 -     do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
    1.20 +     do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop);
    1.21 +     SimpleThread.fork false (fn () => heartbeat ("heartbeat " ^ string_of_int (inc next))); ())
    1.22    else if ! do_shutdown then error "Scheduler shutdown in progress"
    1.23    else ());
    1.24  
    1.25 @@ -321,7 +327,8 @@
    1.26        do_shutdown := true;
    1.27        notify_all ();
    1.28        while not (null (! workers)) do wait "shutdown: workers";
    1.29 -      while scheduler_active () do wait "shutdown: scheduler still active")))
    1.30 +      while scheduler_active () do wait "shutdown: scheduler still active";
    1.31 +      OS.Process.sleep (Time.fromMilliseconds 300))))
    1.32    else ();
    1.33  
    1.34  end;