Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] set_timeout in 8.8.0

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] set_timeout in 8.8.0


Chronological Thread 
  • From: Łukasz Czajka <lukaszcz AT mimuw.edu.pl>
  • To: Coq Club <coq-club AT inria.fr>
  • Cc: Gabriel Scherer <gabriel.scherer AT gmail.com>, Burak Ekici <ekcburak AT hotmail.com>, tchajed AT mit.edu
  • Subject: Re: [Coq-Club] set_timeout in 8.8.0
  • Date: Mon, 7 May 2018 17:01:26 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lukaszczz AT gmail.com; spf=Pass smtp.mailfrom=lukaszczz AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f44.google.com
  • Ironport-phdr: 9a23:Umz77hbGa9VHsHt/CcET2tj/LSx+4OfEezUN459isYplN5qZoMS9bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVSNBDIOyYYUMAeQcI+hXs4bzqkASrRunHwSgGP/jxiNKi3LwwKY00/4hEQbD3AE4GdwOrXfUo8/uNKYTSe+40qjJwi/Bb/NVwzj29Y/FchQ8ofGPR71wasvQxlUuFg7ei1WQqInlPy6b1+gXrWeU8vdgWfi3i24jsgx8pCWkyMkrionMnI0Vy1bE+D12wIY0Od24SFN7bsW+HJRMsCGaMo17Sd4hTWFwoCs21KEKtJqhcCUJyJkr3QDTZ+GIfoSS7R/uW+CcKipiin1/YrKwnROy/FCgyuLiUsm0105Hri9fndnNsnABzh3T6tSbRvdk8Ees1jmC2xrc6uFDJkA0mq7bJIA7zrEskZoTtFzPHi7wmErokK+bblso9vSs5uj9YbjrpoWQO5FphgzxKKgjlcOyDfw9MgcUXmib/eq81Kfk/U38WLhKiuA2kqrDv5DBJMUUuq+4Ag5O34Ys7hawFTam0NACkXYbK1JFfQqLj5L1NFHWPPD4EfC/jkywnzds3vDKJ6HuApHQLnfYi7rhZrZ860tEyAUp19xf5pRUCqsAIP3pQEPxusbYXVcFNFmfxP+vI9Fg3MtKUmWWR6SdLan6sFmS5+tpLfPaN6EPvzOoD+Um7uX8ulQrkF0edOH92YYUYWuqFeZOJkScfGWqj9scV38O6FltBNf2gUGPBGYAL025WLgxs3RiUNr/XNXzA7u1ibnE5x+VW5hfZ2RIEFeJSC66eICNWvNKYyWXcJY4zm40EIO5Qopk7imA8RfgwuM+fOXR8ywc85nk0YotvrCBpVQJ7TVxSv+l/SSNQmVzxD5aQjY32OV+vRQ4xAvfl6d/hPNcGJpY4PYbCgo=

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.



Archive powered by MHonArc 2.6.18.

Top of Page