Make sure accumulators do not exceed the minor heap (partly fix #11170). #13431
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…1170). Accumulators can grow arbitrarily large, even when well-typed. So, this commit makes sure they are allocated on the major heap when they are too large. If so, fields need to be filled with caml_initialize, in case they point to the minor heap.
silene
added
kind: fix
xavierleroy
approved these changes
Nov 20, 2020
|
Bench running at https://gitlab.com/coq/coq/-/jobs/863754892. |
|
Even with letting my imagination running wild, I cannot see how it could cause any noticeable change to performances. But perhaps someone out there is intensively building accumulators with more than 250 arguments. |
|
Could you please add a test file which used to segfault, but does no more? |
|
It is a bit complicated. We would have to create an accumulator with millions of arguments, as we have to overflow the whole minor heap. We can workaround the issue by severely reducing the size of the minor heap, but I am not quite sure how to do that with the testsuite. That said, with a minimal minor heap (which causes Coq to take ages to execute), I can trigger a buffer overflow with Require Import BinNat.
Fixpoint T n := match n with O => nat | S n => nat -> T n end.
Fixpoint app n : T n -> nat :=
match n with O => fun x => x | S n => fun f => app n (f 0) end.
Definition n := N.to_nat 5000.
Axiom f : T n.
Eval vm_compute in let t := (app n f, 0) in snd t.Unfortunately, the invalid access does not immediately crash Coq. It takes some time before an actual segfault occurs (in |
|
You can write a misc test with a script that sets OCAMLRUNPARAM before invoking coqc. |
ppedrot
reviewed
Nov 20, 2020
test-suite/misc/aux11170.v
Outdated
| @@ -0,0 +1,7 @@ | |||
| Require Import BinNat. | |||
There was a problem hiding this comment.
Since this has a lot of dependencies, it might be better to write a self-contained function that generates a big integer without relying on N.
(Ideally, even redefining nat so as to compile with -noinit.)
|
I have removed the dependency on
|
|
Bench: So, fourcolor does seem to be very mildly affected by the patch. It might be noise, but it's unlikely because it's also reflected in the CPU cycles. |
I just tried. This is actually noise, since Fourcolor does not exercise these code paths. Or rather, the change of code presumably led the compiler to select a different optimization strategy for the whole interpreter. Nothing we can do about it. |
gares
approved these changes
Nov 21, 2020
|
@coqbot merge now |
gares
added a commit
to gares/coq
that referenced
this pull request
Nov 21, 2020
… heap (partly fix coq#11170).
coqbot-app
bot
moved this from Request 8.13+beta1 inclusion
to Shipped in 8.13+beta1
in Coq 8.13
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Accumulators can grow arbitrarily large, even when well-typed. So, this commit makes sure they are allocated on the major heap when they are too large. If so, fields need to be filled with
caml_initialize, in case they point to the minor heap.@xavierleroy