Email Gateway (Aug 18 2022 at 17:49): Email Gateway (Aug 18 2022 at 17:49):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
Hi,
when using timeLimit I sometimes observe that the code executed after
the timeLimit raises an Interrupt exception.
I had a look at the definition of timeLimit:
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
let
val worker = Thread.self ();
val timeout = ref false;
val watchdog = Thread.fork (fn () =>
(OS.Process.sleep time; timeout := true; Thread.interrupt
worker), []);
val result = Exn.capture (restore_attributes f) x;
val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
val _ = Thread.interrupt watchdog handle Thread _ => ();
in if was_timeout then raise TimeOut else Exn.release result end) ();
When evaluating "timeLimit time f x", I suspect that the "watchdog"
sometimes interrupts the current thread after the evaluation of
"(restore_attributes f) x"; the interrupt is then delayed (thanks to
uninterruptible) until after the evaluation of "timeLimit time f x".
Do you agree with that explanation?
It may be important to mention that I used timeLimit to limit the
execution of auto and force. The problem arised only with force. When
the problem arised, force consumed a lot of memory and much more run
time than specified by the timeout.
-Matthias
Email Gateway (Aug 18 2022 at 17:49):From: Makarius <makarius@sketis.net>
Yes, I had seen this before. Just after the Isabelle2011 release I've
spent some time on it again, including in-depth discussion with David
Matthews to understand the exact Poly/ML runtime behaviour here.
This resulted in the following changes
http://isabelle.in.tum.de/repos/isabelle/log/2b92a6943915/src/Pure/Concurrent/time_limit.ML
It probably requires some fiddling to port this back to Isabelle2011.
You can also try Poly/ML 5.4.1-SVN, although it is still in flux. IIRC,
David had some clarification there in his code as well, that demands less
adjustment as I did for the official Poly/ML versions.
Makarius
Email Gateway (Aug 18 2022 at 17:49):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
Thanks. Good to know that the problem is fixed. The current situation is
quite acceptable for me. If the bug causes more problems, I will
consider porting the fix to Isabelle2011.
-Matthias
Last updated: Apr 20 2024 at 12:26 UTC