Set-max-mem
An enhanced memory management scheme. (CCL only; requires
a trust tag)
Typical usage:
(include-book "centaur/misc/memory-mgmt" :dir :system) ;; adds ttag
(value-triple (set-max-mem (* 4 (expt 2 30)))) ;; 4 GB
Logically (set-max-mem n) just returns nil.
Under the hood, loading the centaur/misc/memory-mgmt book adds some
special garbage collection hooks into CCL, and set-max-mem influences the
behavior of these hooks.
Roughly speaking, (set-max-mem n) means: try to use no more than
n bytes of heap memory. You should think of this as a soft cap.
Generally the limit will grow by increments of 1 GB as you start to run out of
memory.
Note that this only influences the heap memory. To avoid swapping death,
you should typically pick an n that leaves space for the stacks and other
processes on your system. For instance, if your machine has only 8 GB of
physical memory, you may wish to reserve no more than about 6 GB for the
heap.
The build::cert.pl build system scans for calls of set-max-mem
and uses them to infer how much memory a book will need. This information may
be useful for scheduling jobs when carrying out distributed builds on a
cluster.
Note that this parsing is done by a simple Perl script, so you can't just
use an arbitrary Lisp expression here. Explicitly supported expressions
are:
Using set-max-mem in Pure ACL2 Books
To make it possible to embed calls of set-max-mem into ordinary,
trust-tag free ACL2 code, the logical definition of set-max-mem is found
in the book:
(include-book "centaur/misc/memory-mgmt-logic" :dir :system)
Note that if you load only this -logic book, without also loading the
raw book, then set-max-mem will do nothing except print a message
saying it is doing nothing.
