The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

Hi Gabriel,

The OCaml bug in question is the following:

https://caml.inria.fr/mantis/view.php?id=7709

As we discussed and diagnosed the problem at POPL, the problem is that
the timeout system is based on signals, and the OCaml runtime is not
able to masks signals per threads while POSIX is. I plan to work on this
at some point, but I have been too busy in the meantime.

-- 
JH



Le 07/05/2018 à 11:41, Gabriel Scherer a écrit :
> 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.

Attachment: signature.asc
Description: OpenPGP digital signature