The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

If you believe there is a bug in the OCaml runtime, have you reported
an issue on the OCaml bugtracker ( http://caml.inria.fr/mantis/ )? I
haven't found any related issue.

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.

My understanding of Coq's lib/control.ml code (
https://github.com/coq/coq/blob/629fbc7/lib/control.ml ) is that there
are two timeout functions, one for Windows, which spins a separate
timer thread, and one for Linux which uses Unix.alarm. 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.

¹: See for example http://maxim.int.ru/bookshelf/PthreadsProgram/htm/r_40.html
²: In that respect the "Management of signals" paragraph in the OCaml
manual ( http://caml.inria.fr/pub/docs/manual-ocaml/libref/Thread.html
) might be misleading; it talks about synchronous signals, and maybe
it is not clear that alarms are an "external" signal.

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


On Thu, May 3, 2018 at 12:27 PM, Łukasz Czajka 
<lukaszcz AT mimuw.edu.pl>
 wrote:
> Hi.
>
> Our usecase is that Coq's timeout function is broken because of a bug
> in OCaml runtime, and we wrote our own a bit less broken version for
> the CoqHammer plugin.
>
> Best,
> Lukasz
>
>
> On 2 May 2018 at 20:41, Emilio Jesús Gallego Arias 
> <e AT x80.org>
>  wrote:
>> Burak Ekici 
>> <ekcburak AT hotmail.com>
>>  writes:
>>
>>> The latest release of Coq (8.8.0) seems to drop the "set_timeout"
>>> function from "control.ml". How can I simply mimic it? We want to use a
>>> particular timeout function...
>>
>> Umm, that function was pretty internal so I wonder what your use case
>> is. Please open a ticket on GitHub and we will add the interface back
>> for 8.8.1
>>
>> E.