		Search-engine friendly clone of the ACL2 documentation.

Memory-management

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.

Use set-max-mem

You can load the centaur/misc/memory-mgmt book and use the set-max-mem command to indicate how large you would like the Lisp heap to be. For instance,

(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.

Optimize hash-consing 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.

Manage hash-consing and memoization overhead.

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 (maybe-wash-memory n), which frees this memory and triggers a garbage collection only when the amount of free memory is below some threshold n. A good choice for n might be 20% of the set-max-mem threshold.

It can be useful to call ACL2::maybe-wash-memory between proofs, or between the cases of parametrized theorems; see for instance the :run-before-cases argument of def-gl-param-thm.