Re: [Caml-list] [IMPORTANT] Intel Skylake / Kaby Lake hardware bug affects OCaml programs

[e@x80.org (Emilio Jesús Gallego Arias)]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> Here is my list of affected OCaml projects known so far (it seems
> surprisingly less rare than I thought at first):
>
> - an (unnamed) industrial user noticed the issue in Spring 2016, as
> reported by Xavier on the bugtracker:
>   https://caml.inria.fr/mantis/view.php?id=7452#c17109
>
> - ahrefs noticed issues in late 2016, as reported by Joris
> Giovannangeli on the bugtracker issue or his longer piece
>   https://tech.ahrefs.com/skylake-bug-a-detective-story-ab1ad2beddcd
>
> - Lwt users were also affected (first report from Sebastien Mondet in
> February 2017):
>   https://github.com/ocsigen/lwt/issues/315
>
> - Julia Lawall reported segfaults from a downstream user on the caml-list,
>   that seem extreley likely to be related to this issue (they
> disappear with hyperthreading disabled)
>   https://sympa.inria.fr/sympa/arc/caml-list/2017-06/msg00115.html

Here is the only Coq bug that I know of:

https://coq.inria.fr/bugs/show_bug.cgi?id=5517

but as Maxime pointed out, the problem was observed by other people
internally.

E.