The Coq mailing list

[Łukasz Czajka <lukaszcz AT mimuw.edu.pl>]

This issue becomes noticable in the CoqHammer plugin, which uses the
timeout internally many times during proof reconstruction to find a
tactic that works. It's still rare, but no longer very rare, and it
comes up during normal usage with some regularity.


On 7 May 2018 at 16:51, Tej Chajed 
<tchajed AT mit.edu>
 wrote:
> I’ve already reported a bug that sounds like this issue (the timeout tactic
> sometimes doesn’t work): https://github.com/coq/coq/issues/7430. I didn’t
> include a good test but it seems like the Timeout vernacular doesn’t
> completely solve the problem.
>
> I didn’t need to enable any multi-threading or asynchronous options to
> trigger this bug (not sure exactly what happens by default, though).
>
>
> On Mon, May 7, 2018 at 9:03 AM Łukasz Czajka 
> <lukaszcz AT mimuw.edu.pl>
>  wrote:
>>
>> >
>> > After looking at this out of curiosity, I don't think that "Coq's
>> > timeout function is broken because of a bug in the OCaml runtime" is a
>> > fair description of the situation.
>> >
>>
>> From the point of view of the Coq user, it is possible that you invoke
>> "timeout N tac" and sometimes this doesn't fail after N seconds but
>> runs forever. This is rare and random. This is definitely a bug.
>>
>> > It seems generally well-known¹ that, following POSIX, "alarm" is
>> > process-level
>> > and may deliver the SIGALRM signal to any thread² that does not
>> > explicity block it -- I don't think the OCaml runtime is supposed to
>> > give any stronger guarantees than POSIX on these system calls.
>> >
>>
>> This may be the case, I'm not an expert here. I talked about the
>> problem with some Coq developers when I was at POPL this year, they
>> diagnosed what the problem was, and as far as I remember they said
>> it's a problem with OCaml's runtime and they can't do anything about
>> it. I didn't try to dig deeper and file a bug report. My description
>> of the problem as a "bug" in OCaml might have been inaccurate, because
>> I don't really know how the OCaml runtime is supposed to behave with
>> respect to the ALARM signal. But I believe it's definitely a bug as
>> far as the timeout tactical in Coq is concerned.
>>
>> > My non-expert understanding would thus be that Coq's signal-based
>> > timeout implementation is not actually reliable for multi-threaded
>> > usage, and that maybe the Coq developers could consider using the
>> > thread-based implementation (currently Windows-only) more often. Does
>> > it impact the performance in an important way? (It may also be
>> > possible to use a signal-based implementation by ensuring that all
>> > threads block the SIGALRM signal by default, and only unblocking the
>> > signal before calling "timeout"; this requires using a mutex to
>> > protect "timeout" calls, although it is possible to revert to the
>> > thread-based implementation when the mutex is held by another thread
>> > instead of blocking.)
>>
>> My experience with the Windows version of the timeout function is that
>> it doesn't work at all by itself.