# HG changeset patch # User wenzelm # Date 1222970340 -7200 # Node ID dcc030b525838319cce8e74e61b97df058a450be # Parent b8f16c92122a91c4e4c3521952647a9399a214af tuned SYNCHRONIZED: outermost Exn.release; tuned tracing; diff -r b8f16c92122a -r dcc030b52583 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Oct 02 19:38:48 2008 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Oct 02 19:59:00 2008 +0200 @@ -101,15 +101,18 @@ val cond = ConditionVar.conditionVar (); in -fun SYNCHRONIZED name e = uninterruptible (fn restore_attributes => fn () => +fun SYNCHRONIZED name e = Exn.release (uninterruptible (fn restore_attributes => fn () => let - val _ = Multithreading.tracing 3 (fn () => name ^ ": locking"); - val _ = Mutex.lock lock; - val _ = Multithreading.tracing 3 (fn () => name ^ ": locked"); + val _ = + if Mutex.trylock lock then Multithreading.tracing 4 (fn () => name ^ ": locked") + else + (Multithreading.tracing 3 (fn () => name ^ ": locking ..."); + Mutex.lock lock; + Multithreading.tracing 3 (fn () => name ^ ": ... locked")); val result = Exn.capture (restore_attributes e) (); val _ = Mutex.unlock lock; - val _ = Multithreading.tracing 3 (fn () => name ^ ": unlocked"); - in Exn.release result end) (); + val _ = Multithreading.tracing 4 (fn () => name ^ ": unlocked"); + in result end) ()); fun wait name = (*requires SYNCHRONIZED*) ConditionVar.wait (cond, lock); @@ -141,9 +144,9 @@ fun execute name (task, group, run) = let val _ = trace_active (); - val _ = Multithreading.tracing 3 (fn () => name ^ ": running"); + val _ = Multithreading.tracing 4 (fn () => name ^ ": running"); val ok = setmp_thread_data (name, task, group) run (); - val _ = Multithreading.tracing 3 (fn () => name ^ ": finished"); + val _ = Multithreading.tracing 4 (fn () => name ^ ": finished"); val _ = SYNCHRONIZED "execute" (fn () => (change queue (TaskQueue.finish task); if ok then () @@ -171,7 +174,7 @@ fun worker_loop name = (case SYNCHRONIZED name (fn () => worker_next name) of - NONE => Multithreading.tracing 3 (fn () => name ^ ": exit") + NONE => Multithreading.tracing 4 (fn () => name ^ ": exit") | SOME work => (execute name work; worker_loop name)); fun worker_start name = (*requires SYNCHRONIZED*) @@ -206,7 +209,7 @@ val _ = if continue then () else scheduler := NONE; val _ = notify_all (); - val _ = wait_timeout "scheduler" (Time.fromSeconds 1); + val _ = wait_timeout "scheduler" (Time.fromSeconds 3); in continue end; fun scheduler_loop () = @@ -216,7 +219,7 @@ fun scheduler_active () = (*requires SYNCHRONIZED*) (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); -fun scheduler_check () = SYNCHRONIZED "scheduler_check" (fn () => +fun scheduler_check name = SYNCHRONIZED name (fn () => if not (scheduler_active ()) then (Multithreading.tracing 3 (fn () => "scheduler: fork"); do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop)) @@ -228,7 +231,7 @@ fun future opt_group deps pri (e: unit -> 'a) = let - val _ = scheduler_check (); + val _ = scheduler_check "future check"; val group = (case opt_group of SOME group => group | NONE => TaskQueue.new_group ()); @@ -253,7 +256,7 @@ fun join_results [] = [] | join_results xs = let - val _ = scheduler_check (); + val _ = scheduler_check "join check"; val _ = Multithreading.self_critical () andalso error "Cannot join future values within critical section"; @@ -290,7 +293,7 @@ (* misc operations *) (*focus: collection of high-priority task*) -fun focus tasks = SYNCHRONIZED "interrupt" (fn () => +fun focus tasks = SYNCHRONIZED "focus" (fn () => change queue (TaskQueue.focus tasks)); (*interrupt: permissive signal, may get ignored*) @@ -299,14 +302,14 @@ (*cancel: present and future group members will be interrupted eventually*) fun cancel x = - (scheduler_check (); + (scheduler_check "cancel check"; SYNCHRONIZED "cancel" (fn () => (change canceled (cons (group_of x)); notify_all ()))); (*global join and shutdown*) fun shutdown () = if Multithreading.available then - (scheduler_check (); + (scheduler_check "shutdown check"; SYNCHRONIZED "shutdown" (fn () => (while not (scheduler_active ()) do wait "shutdown: scheduler inactive"; while not (TaskQueue.is_empty (! queue)) do wait "shutdown: join";