Major Section: HONS-AND-MEMOIZATION
This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.
Certain ``Hons-Notes'' are printed to the terminal to report
implementation-level information about the management of HONS structures.
Some of these may be low-level and of interest mainly to system developers.
But below we discuss what users can learn from a particular hons-note,
``ADDR-LIMIT reached''. In short: If you are seeing a lot of such hons-notes,
then you may be using a lot of memory. (Maybe you can reduce that memory; for
certain BDD operations, for example (as defined in community books
books/centaur/ubdds/), variable ordering can make a big difference.)
By way of background:
The ADDR-HT is the main hash table that lets us look up normed conses, i.e., honses. It is an ordinary Common Lisp hash table, so when it starts to get too full the Lisp will grow it. It can get really big. (It has been seen to take more than 10 GB of memory just for the hash table's array, not to mention the actual conses!)
Hons-Notes may be printed when the ADDR-HT is getting really full. This growth can be expensive and can lead to memory problems. Think about what it takes to resize a hash table:
(1) allocate a new, bigger array
(2) rehash elements, copying them into the new array
(3) free the old array
Until you reach step (3) and a garbage collection takes place, you have to have enough memory to have both the old and new arrays allocated. If the old array was 10 GB and we want to allocate a new one that's 15 GB, this can get pretty bad. Also, rehashing the elements is expensive time-wise when there are lots of elements.
Since resizing a hash table is expensive, we want to avoid it. There's a
hons-resizecommand for this. You may want your books to start with something like the following.
(value-triple (set-max-mem (* 30 (expt 2 30)))) ; 30 GB heap (value-triple (hons-resize :addr-ht #u_100_000_000)) ; 100M honses
Basically, if you roughly know how many honses your book will need, you can just get them up front and then never to resize.
The Hons-Notes about ``ADDR-LIMIT reached'' are basically there to warn you
that the ADDR-HT is being resized. This can help you realize that your
hons-resize command had too small of an ADDR-HT size, or might suggest
that your book should have a
hons-resize command. There are also
) and, defined in community book
These can show you how many honses you currently have, how much space they are
taking, and that sort of thing. (A nice trick is to call
the end of a book, to get an idea of how many honses you should ask for in your