coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] set_timeout in 8.8.0

From: Xavier Leroy <Xavier.Leroy AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] set_timeout in 8.8.0
Date: Thu, 10 May 2018 12:02:45 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xavier.leroy AT gmail.com; spf=Pass smtp.mailfrom=xavier.leroy AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f181.google.com
Ironport-phdr: 9a23:kzbNaBx+3lJJE3LXCy+O+j09IxM/srCxBDY+r6Qd1O4WIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRR/zlSkJKTA5/mHUhMJ+gq1UrxCuqABwzYPPfIGYNuBzcr/Bcd4UR2dMWNtaWSxbAoO7aosCF+sOMvxGr4n8uVQOtwa1Cw+yC+P1zT9JhmL90Ko73Os7DwHG3RIvH8gUvHrSstr1LqASUOCuwanJyzXDdfJW1i3n5IjGaBAsuPeBVq9zf8rJ0UQjCR/Jg1GKpYHmPz6ZzPkBv3aY4uZ6SO6iiHMrpxlyrzSx3MsglIfEi4APxl3G6Cl12ps5KNmlREN9fNWqCoFftzuAOItzWs4iQ39nuCI9yrAevJ60ZikKyJA+yx/RcfyLb5GE4hz+WOuSPDt0nn1leLW4hxa99Uiv1PfwWdWz0FZPtiZFk9/MuW4R1xHL9MSLVv9w8l2i1DuPzQzf9/9ILEMumabGKJMt36Y8lp8JvkTCGi/2ll/2jKiTdkg89emn8frnYrT4qZ+GLYN0jh/xMr4pms2/Guk4PQ0OUHKa+eS4zrHs4Ur5QLBSgv0sjqbZqIzaJdgcpqOhHwBV1Z8j5w+jADeizdQXhmIKLElFeRKCl4jmIUvCIPH+DfelglSjii1nx/7cPu6pPpKYJX/a1bzlYLxV6khGyQN1w8oMyYhTD+QxKezyV1W5kNHCCQ5xZzy93efqEpNZ25kZSEqOBLWYOeXcqwnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCO10NgEGGYO+AE5Sb6z0QHQYXtof3+3GpkEyHQjEov/VNXMQ4mshPqK2yLpRsQLNFADMUiFFDLTT6vBW/oIb3jMcMpokzhBSqL5DoF4hUjouwj9xL5qaOHT/39AuA==

On 05/09/2018 04:25 PM, Gabriel Scherer wrote:
> Contrarily to what I believed, there seems to be a bug in the OCaml runtime
> (MPR#7709, reported on the OCaml bugtracker by Jacques-Henri) that affects
> the Coq-side implement of the runtime function.

Yes, Thread.sigmask is broken in OCaml. However, even if it was working as
intended I'm not sure it would be enough for Coq to reliably implement its
timeout tactic.

The original sin is that POSIX 1003.1c gives no system call to deliver a
"time is up" signal to the calling thread. Instead, the signal is delivered
to any thread that does not block it. Blocking the signal from all threads
except the one that can handle it is standard practice but doesn't extend to
the case where two threads or more want independent timeouts...

I'm so pessimistic about this whole business that I'd recommend Coq to remove
the timeout tactic and Coq users to learn to live without it.

- Xavier Leroy

[Coq-Club] set_timeout in 8.8.0, Burak Ekici, 05/02/2018
- Re: [Coq-Club] set_timeout in 8.8.0, Emilio Jesús Gallego Arias, 05/02/2018
  - Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/03/2018
    - Re: [Coq-Club] set_timeout in 8.8.0, Gabriel Scherer, 05/07/2018
      - Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/07/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/07/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Gabriel Scherer, 05/09/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Xavier Leroy, 05/10/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Tej Chajed, 05/07/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/07/2018
      - Re: [Coq-Club] set_timeout in 8.8.0, Jacques-Henri Jourdan, 05/07/2018