SBCL Dynamic Memory Allocation

[nmoore771]

Greetings,

While grinding my way through a large theorem, I ran into an issue where SBCL (the Lisp backend that I am using) runs out of memory for garbage collection. This causes a hard crash of the prover environment, kicking me into the Lisp debugger. There's a command line argument for sbcl that increases this limit, and it is possible to insert it by replacing in emacs/pvs-ilips.el

(defun pvs-program () pvs-image)

on lines 145 and 146 with

(defun pvs-program () (format "%s --dynamic-space-size 2048" pvs-image))

This seems like a kludgy way of doing this, and perhaps someone who knows the system (and emacs Lisp) a bit better would be able to come up with a better solution (in particular, giving it a 2GB limit, hard coded, is not going to be a good solution for everyone).

Thanks for your time.

[samowre]

Hi

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

[nmoore771]

Thanks for looking into it!