alists with hidden hash tables for faster execution

This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.

The implementation of fast alists is, in many ways, similar to that of ACL2 arrays. Logically, hons-acons is just like acons, and hons-get is similar to assoc-equal. But under the hood, hash tables are associated with these alists, and, when a certain discipline is followed, these functions execute with hash table speeds.

What is this discipline? Each hons-acons operation "steals" the hash table associated with the alist that is being extended. Because of this, one must be very conscious of which object is the most recent extension of an alist and use that extension exclusively.

The only penalty for a failure to keep track of the most recent extension is a loss of execution speed, not of correctness, and perhaps the annoyance of some slow-alist-warnings.

Maintaining discipline may require careful passing of a fast alist up and down through function calls, as with any single threaded object in an applicative setting, but there is no syntactic enforcement that insists you only use the most recent extension of an alist as there is for single threaded objects (stobjs). Also, even with perfectly proper code, discipline can sometimes be lost due to user interrupts and aborts.

Performance Notes

The keys of fast alists are always normed. Why? In Common Lisp, equal-based hashing is relatively slow, so to allow the use of eql-based hash tables, hons-acons and hons-get always hons-copy the keys involved.

Since alist keys are frequently atoms, this norming activity may often be so fast that you do not need to think about it. But if you are going to use large structures as the keys for your fast alist, this overhead can be significant, and you may want to ensure that your keys are normed ahead of time.

There is no automatic mechanism for reclaiming the hash tables that are associated with alists. Because of this, to avoid memory leaks, you should call fast-alist-free to remove the hash table associated with alists that will no longer be used.