[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 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.