# HG changeset patch # User wenzelm # Date 1222983044 -7200 # Node ID 7c80ab57f56df895a57f584f290de5d6ddb1d640 # Parent c8336c42668e8cdc34fa3b94052f2d347ef8d382 more tuning of tracing messages; diff -r c8336c42668e -r 7c80ab57f56d src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Oct 02 22:09:22 2008 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Oct 02 23:30:44 2008 +0200 @@ -87,6 +87,7 @@ (* global state *) val queue = ref TaskQueue.empty; +val next = ref 0; val workers = ref ([]: (Thread.thread * bool) list); val scheduler = ref (NONE: Thread.thread option); val excessive = ref 0; @@ -104,21 +105,25 @@ fun SYNCHRONIZED name e = Exn.release (uninterruptible (fn restore_attributes => fn () => let val _ = - if Mutex.trylock lock then Multithreading.tracing 4 (fn () => name ^ ": locked") + if Mutex.trylock lock then Multithreading.tracing 3 (fn () => name ^ ": locked") else - (Multithreading.tracing 3 (fn () => name ^ ": locking ..."); + (Multithreading.tracing 2 (fn () => name ^ ": locking ..."); Mutex.lock lock; - Multithreading.tracing 3 (fn () => name ^ ": ... locked")); + Multithreading.tracing 2 (fn () => name ^ ": ... locked")); val result = Exn.capture (restore_attributes e) (); val _ = Mutex.unlock lock; - val _ = Multithreading.tracing 4 (fn () => name ^ ": unlocked"); + val _ = Multithreading.tracing 3 (fn () => name ^ ": unlocked"); in result end) ()); fun wait name = (*requires SYNCHRONIZED*) + (Multithreading.tracing 3 (fn () => name ^ ": wait ..."); ConditionVar.wait (cond, lock); + Multithreading.tracing 3 (fn () => name ^ ": ... continue")); fun wait_timeout name timeout = (*requires SYNCHRONIZED*) + (Multithreading.tracing 3 (fn () => name ^ ": wait ..."); ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout)); + Multithreading.tracing 3 (fn () => name ^ ": ... continue")); fun notify_all () = (*requires SYNCHRONIZED*) ConditionVar.broadcast cond; @@ -144,9 +149,9 @@ fun execute name (task, group, run) = let val _ = trace_active (); - val _ = Multithreading.tracing 4 (fn () => name ^ ": running"); + val _ = Multithreading.tracing 3 (fn () => name ^ ": running"); val ok = setmp_thread_data (name, task, group) run (); - val _ = Multithreading.tracing 4 (fn () => name ^ ": finished"); + val _ = Multithreading.tracing 3 (fn () => name ^ ": finished"); val _ = SYNCHRONIZED "execute" (fn () => (change queue (TaskQueue.finish task); if ok then () @@ -174,7 +179,7 @@ fun worker_loop name = (case SYNCHRONIZED name (fn () => worker_next name) of - NONE => Multithreading.tracing 4 (fn () => name ^ ": exit") + NONE => Multithreading.tracing 3 (fn () => name ^ ": exit") | SOME work => (execute name work; worker_loop name)); fun worker_start name = (*requires SYNCHRONIZED*) @@ -198,7 +203,7 @@ val l = length (! workers); val _ = excessive := l - m; val _ = - if m > l then funpow (m - l) (fn () => worker_start ("worker " ^ serial_string ())) () + if m > l then funpow (m - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) () else (); (*canceled groups*) @@ -214,14 +219,14 @@ fun scheduler_loop () = (while SYNCHRONIZED "scheduler" scheduler_next do (); - Multithreading.tracing 3 (fn () => "scheduler: exit")); + Multithreading.tracing 2 (fn () => "scheduler: exit")); fun scheduler_active () = (*requires SYNCHRONIZED*) (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); fun scheduler_check name = SYNCHRONIZED name (fn () => if not (scheduler_active ()) then - (Multithreading.tracing 3 (fn () => "scheduler: fork"); + (Multithreading.tracing 2 (fn () => "scheduler: fork"); do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop)) else if ! do_shutdown then error "Scheduler shutdown in progress" else ());