# HG changeset patch # User wenzelm # Date 1297119423 -3600 # Node ID 82339c3fd74ac9bcf47d1e395ac32f3d2825373b # Parent 3422ae5aff3a351a7f7bbc0097400f84cb055413 more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier); diff -r 3422ae5aff3a -r 82339c3fd74a src/Pure/Concurrent/time_limit.ML --- a/src/Pure/Concurrent/time_limit.ML Sat Feb 05 20:38:32 2011 +0100 +++ b/src/Pure/Concurrent/time_limit.ML Mon Feb 07 23:57:03 2011 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/Concurrent/time_limit.ML Author: Makarius -Execution with time limit. +Execution with time limit (considerable overhead due to fork of watchdog thread). *) signature TIME_LIMIT = @@ -15,18 +15,29 @@ exception TimeOut; -fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () => - let - val worker = Thread.self (); - val timeout = Unsynchronized.ref false; - val watchdog = Thread.fork (fn () => - (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []); +fun timeLimit time f x = + Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts => + let + val main = Thread.self (); + val timeout = Unsynchronized.ref false; + val watchdog = Simple_Thread.fork true (fn () => + (OS.Process.sleep time; timeout := true; Thread.interrupt main)); + + val result = Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) (); - val result = Exn.capture (restore_attributes f) x; - val was_timeout = Exn.is_interrupt_exn result andalso ! timeout; + val _ = Thread.interrupt watchdog handle Thread _ => (); + val _ = while Thread.isActive watchdog do OS.Process.sleep (seconds 0.0001); - val _ = Thread.interrupt watchdog handle Thread _ => (); - in if was_timeout then raise TimeOut else Exn.release result end) (); + val test = + Exn.capture (fn () => + Multithreading.with_attributes (Multithreading.sync_interrupts orig_atts) + (fn _ => Thread.testInterrupt ())) (); + in + if ! timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test) + then raise TimeOut + else if Exn.is_interrupt_exn test then Exn.interrupt () + else Exn.release result + end); end;