The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

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.