# HG changeset patch # User wenzelm # Date 1248476027 -7200 # Node ID 8026b73cd3570abc5a5655b89cebfa0376da8bde # Parent 57ecfab3bcfe9502babe8fb3573ccb2ac301bfa4 tuned tracing; diff -r 57ecfab3bcfe -r 8026b73cd357 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sat Jul 25 00:39:05 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Sat Jul 25 00:53:47 2009 +0200 @@ -138,7 +138,7 @@ fun count_active ws = fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0; -fun trace_active () = Multithreading.tracing 1 (fn () => +fun trace_active () = Multithreading.tracing 6 (fn () => let val ws = ! workers; val m = string_of_int (length ws); @@ -222,7 +222,7 @@ fun scheduler_next () = (*requires SYNCHRONIZED*) let (*queue status*) - val _ = Multithreading.tracing 1 (fn () => + val _ = Multithreading.tracing 6 (fn () => let val {ready, pending, running} = Task_Queue.status (! queue) in "SCHEDULE: " ^ string_of_int ready ^ " ready, " ^ @@ -338,8 +338,12 @@ if SYNCHRONIZED "join_wait" (fn () => is_finished x orelse (if worker then worker_wait () else wait (); false)) then () else join_wait x; - val _ = List.app join_wait xs; + val _ = xs |> List.app (fn x => + let val time = Multithreading.real_time join_wait x in + Multithreading.tracing_time true time + (fn () => "joined after " ^ Time.toString time) + end); in map get_result xs end) (); end; diff -r 57ecfab3bcfe -r 8026b73cd357 src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Sat Jul 25 00:39:05 2009 +0200 +++ b/src/Pure/Concurrent/simple_thread.ML Sat Jul 25 00:53:47 2009 +0200 @@ -31,7 +31,7 @@ let val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ..."); val time = Multithreading.real_time Mutex.lock lock; - val _ = Multithreading.tracing_time time + val _ = Multithreading.tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); in false end; val result = Exn.capture (restore_attributes e) (); diff -r 57ecfab3bcfe -r 8026b73cd357 src/Pure/ML-Systems/multithreading.ML --- a/src/Pure/ML-Systems/multithreading.ML Sat Jul 25 00:39:05 2009 +0200 +++ b/src/Pure/ML-Systems/multithreading.ML Sat Jul 25 00:53:47 2009 +0200 @@ -15,7 +15,7 @@ include BASIC_MULTITHREADING val trace: int ref val tracing: int -> (unit -> string) -> unit - val tracing_time: Time.time -> (unit -> string) -> unit + val tracing_time: bool -> Time.time -> (unit -> string) -> unit val real_time: ('a -> unit) -> 'a -> Time.time val available: bool val max_threads: int ref @@ -37,7 +37,7 @@ val trace = ref (0: int); fun tracing _ _ = (); -fun tracing_time _ _ = (); +fun tracing_time _ _ _ = (); fun real_time f x = (f x; Time.zeroTime); diff -r 57ecfab3bcfe -r 8026b73cd357 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Jul 25 00:39:05 2009 +0200 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Jul 25 00:53:47 2009 +0200 @@ -36,9 +36,10 @@ else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) handle _ (*sic*) => (); -fun tracing_time time = +fun tracing_time detailed time = tracing - (if Time.>= (time, Time.fromMilliseconds 1000) then 1 + (if not detailed then 5 + else if Time.>= (time, Time.fromMilliseconds 1000) then 1 else if Time.>= (time, Time.fromMilliseconds 100) then 2 else if Time.>= (time, Time.fromMilliseconds 10) then 3 else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5); @@ -231,7 +232,7 @@ let val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting"); val time = real_time Mutex.lock critical_lock; - val _ = tracing_time time (fn () => + val _ = tracing_time true time (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time); in () end; val _ = critical_thread := SOME (Thread.self ());