[isabelle] Problem with timeLimit
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 () =>
val worker = Thread.self ();
val timeout = ref false;
val watchdog = Thread.fork (fn () =>
(OS.Process.sleep time; timeout := true; Thread.interrupt
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and