Stream: Coq devs & plugin devs

Topic: Coq, TCE, logic_monad.v and ARM

Paolo Giarrusso (Dec 07 2021 at 20:44):

I should expect Coq's logic monad to be properly tail-recursive, right? If that fails on ARM64 and I get a stack overflow, but not on x86, is this an OCaml bug? We're wondering with @Janno, but here's an highlight:

$ fgrep 'camlProofview__anon_fn$5blogic_monad$2eml$3a191$2c15$2d$2d96$5' bt-all.txt|wc -l
  231582
$ fgrep -v 'camlProofview__anon_fn$5blogic_monad$2eml$3a191$2c15$2d$2d96$5' bt-all.txt|wc -l
     202

We're somewhat confident this is arch-specific, since on x86_64 requires take more stack space...

Janno (Dec 07 2021 at 20:46):

To be a bit more specific about the stack space: I can compile the file on my x64 system with 260KB of stack space and it requires somewhere between 8 and 16MB on Paolo's machine.

Paolo Giarrusso (Dec 07 2021 at 20:46):

Here's also the filtered stack trace: https://gist.github.com/Blaisorblade/688e0bce54a7431843e30db64abae664...

Paolo Giarrusso (Dec 07 2021 at 20:47):

Of course, there's plenty of other fun stuff going on in the offending code, but TCO failing on a continuation monad could be a bigger compiler bug (even if it's not yet blocking).

Paolo Giarrusso (Dec 07 2021 at 20:51):

BTW, I got essentially the same symptoms on OCaml 4.13.1 and 4.10.2 (all with flambda), and probably with some intermediate versions as well. The only difference is a known issue (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/PSA.3A.20ARM.20OCaml.20.3C4.2E13.20reports.20stack.20overflows.20as.20SIGSEGV).

Gaëtan Gilbert (Dec 07 2021 at 21:01):

what's the .v source?

Paolo Giarrusso (Dec 07 2021 at 21:02):

we don't have (yet) a minimization we can share :-(, apologies

Gaëtan Gilbert (Dec 07 2021 at 21:09):

Ltac bad := bad.

Lemma foo : False.
  bad.

stack overflows in a couple seconds with my dev coq, but my opam coq doesn't seem to stack overflow
possibly a difference between ocamlopt -opaque vs cross module optimized

Paolo Giarrusso (Dec 07 2021 at 21:29):

Hm, now wondering whether @tailcall be appropriate, and where exactly...

Gaëtan Gilbert (Dec 07 2021 at 22:32):

the backtrace looks like

Error:
Stack overflow.
Raised by primitive operation at file "clib/int.ml", line 22, characters 16-23
Called from file "map.ml", line 123, characters 18-33
Called from file "map.ml", line 127, characters 21-33
Called from file "map.ml", line 130, characters 21-33
Called from file "plugins/ltac/tacinterp.ml", line 1283, characters 18-50
Called from file "engine/logic_monad.ml", line 192, characters 38-43
Called from file "engine/logic_monad.ml", line 260, characters 6-27
Called from file "engine/logic_monad.ml", line 67, characters 36-42
Called from file "engine/logic_monad.ml", line 67, characters 36-42
....

Paolo Giarrusso (Dec 07 2021 at 23:52):

Hmm... our stacktrace seems almost entirely made of the bind operation (line 191) — we never got an OCaml stacktrace.

Paolo Giarrusso (Apr 18 2022 at 14:06):

I've seen another such issue, fixed by OCaml 4.14.0: https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Coq.20Platform.20and.20stack.20overflows.

Paolo Giarrusso (Apr 18 2022 at 14:06):

But let's continue the discussion there.

Last updated: May 28 2023 at 13:30 UTC