HONS-NOTE

notes about HONS, especially pertaining to expensive resizing operations 
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-resize command 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 commands like (hons-summary) and, defined in community book books/centaur/misc/memory-mgmt-logic.lisp, (hons-analyze-memory nil). 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 hons-summary at the end of a book, to get an idea of how many honses you should ask for in your hons-resize command).