Memory management can play a significant role in symbolic execution performance. In some cases GL may use too much memory, leading to swapping and slow performance. In other cases, garbage collection may run too frequently or may not reclaim much space. We have several recommendations for managing memory in large-scale GL proofs. Some of these suggestions are specific to Clozure Common Lisp.
You can load the
(set-max-mem (* 8 (expt 2 30)))
says to allocate 8 GB of memory. To avoid swapping, you should use somewhat less than your available physical memory. This book disables ephemeral garbage collection and configures the garbage collector to run only when the threshold set above is exceeded, which can boost performance.
GL's representations of BDDs and AIGs use hons for structure-sharing. The hons-summary command can be used at any time to see how many honses are currently in use, and hash-consing performance can be improved by pre-allocating space for these honses with hons-resize.
Symbolic execution can use a lot of hash conses and can populate the memoization tables for various functions. The memory used for these purposes is not automatically freed during garbage collection, so it may sometimes be necessary to manually reclaim it.
A useful function is
It can be useful to call ACL2::maybe-wash-memory between proofs, or
between the cases of parametrized theorems; see for instance the