Heap exhaustion
Giulia Sindoni
Hi everyone,
I’m working my way through a reasonably large theorem. At some point, I need to do some rewriting/expansion of definition. I have found (on smaller cases) that the rule (do-rewrite) works better in terms of time than repeating the rule (expand function-name).
However, when it comes to rewriting a quite large formula, I get an heap exhaustion message, something like:
Heap exhausted during allocation: 129564672 bytes available, 221287376 requested.
I have found a similar issue reported (https://github.com/SRI-CSL/PVS/issues/73) and I tried the solution suggested from the poster (i.e. changing the emacs/pvs-ilips.el) but that doesn’t solve the issue and it also does not seem practical.
Has anyone else dealt with something like this before? I’m sure PVS has been used to prove large theorems before…. I’m wondering whether I am dealing with a memory leak, so I should release memory that is storing stuff that is no longer useful. But I’m not quite sure how to tell PVS to do that (if that’s even the case).
Thanks,
Giulia
Sam Owre
Hi Giulia,
This is (partially) discussed in Section 3.2.3 of the SBCL document
(https://www.sbcl.org/manual/#Saving-a-Core-Image), under
:save-runtime-options. The problem is that --dynamic-space-size and
--control-stack-size can't be changed in a running SBCL image, and if the
image was built using save-lisp-and-die, it will ignore these arguments.
The bottom line is that you need to change this at build time, i.e., in the
Makefile. Look for SBCL_SPACE_SIZE, which is currently set to 6 Gb, and
change it to whatever you want. This is also the place to change the
SBCL_STACK_SIZE if you're running out of stack space.
I tested it by setting it to 30 Gb on my 16 Gb Linux laptop with 2 Gb of
swap, and it started right up. You can see that it's virtual size is 30 Gb,
though it's resident set size is only 149 Mb.
USER PID %CPU %MEM VSZ RSS TTY STAT START TIME COMMAND
owre 1309476 1.6 0.9 30980736 148624 pts/10 Sl+ 14:44 0:00 bin/ix86_64-Linux/runtime/pvs-sbclisp --no-userinit
I'm not exactly sure what the trade-offs are for making it larger by
default, but I'm happy to hear any suggestions. Note that increasing the
stack size will increase your resident set size.
Sam