		Search-engine friendly clone of the ACL2 documentation.

Fast-alists

Slow-alist-warning

Warnings/errors issued when fast-alists are used inefficiently

Obtaining hash-table performance from hons-get requires one to follow a certain discipline. If this discipline is violated, you may see the following message, which by default is followed by a Lisp break. (The Lisp break may be ignored by continuing in the host Common Lisp, for example using :go if the host Lisp is CCL. Or, it may be aborted, often using :q, again depending on the host Lisp.)

*****************************************************************
Fast alist discipline violated in HONS-ACONS.
See :DOC slow-alist-warning to suppress or break on this warning.
*****************************************************************

This warning means that the alist you are extending or accessing does not have a valid hash table associated with it, and hence any accesses must be carried out with hons-assoc-equal instead of gethash.

You can control whether or not you get a warning and, if so, whether or not a break (again: an error from which you can continue) ensues. For instance:

(set-slow-alist-action :break)    ; warn and also call break$ (default)
(set-slow-alist-action :warning)  ; warn on slow access
(set-slow-alist-action nil)       ; do not warn or break

The above forms expand to table events, so they can be embedded in encapsulates and books, wrapped in local, and so on.

We conclude by showing how slow alist warnings can occur naturally, together with a couple of possible solutions. First consider the rather trivial example; the labels A1, A2, etc. are explained later.

; (A1) Create a hash-table HT1 and associate it with the resulting alist.
(assign a (hons-acons 'fn1 1 nil))

; (A2) Create a hash-table HT2 and associate it with the resulting alist.
; (Minor observation: HT1 is no longer accessible.)
(assign a (hons-acons 'fn1 1 nil))

; (B1) Update HT2 and associate it with the resulting alist.  Thus, H2 is
; no longer associated with (@ a).
(assign b (hons-acons 'fn2 2 (@ a)))

; (B2) Fast alist warning (with a Lisp break, by default): discipline is
; violated because (@ a) no longer has a backing hash-table.
(assign b (hons-acons 'fn2 2 (@ a)))

; (C1) Fast alist warning/break: discipline is violated because (@ b) does not
; have a backing hash-table.
(assign c (hons-acons 'fn3 3 (@ b)))

; (C2) Fast alist warning/break: discipline is violated because (@ b) does not
; have a backing hash-table.
(assign c (hons-acons 'fn3 3 (@ b)))

Now consider the following related example (in a fresh session), involving three encapsulate events labeled A, B, and C.

(encapsulate nil (defconst *a* (hons-acons 'fn1 1 nil))) ; (A)
(encapsulate nil (defconst *b* (hons-acons 'fn2 2 *a*))) ; (B)
(encapsulate nil (defconst *c* (hons-acons 'fn3 3 *b*))) ; (C)

Each of these encapsulate events generates two calls of hons-acons: one in the first pass of the encapsulate and one in the second pass. With a little reflection you can see the connection between the two sequences of events above: encapsulate A makes assignments analogous to A1 (in its first pass) and A2 (in its second pass); similarly for B, B1, B2 and for C, C1, C2. Thus, we get a slow alist warning/break on the second pass of B and on both passes of C.

The simplest way to fix this problem is to call make-fast-alist, which is essentially a no-op when its argument is already a fast alist.

(encapsulate nil (defconst *a* (make-fast-alist (hons-acons 'fn1 1 nil))))
(encapsulate nil (defconst *b* (make-fast-alist (hons-acons 'fn2 2 *a*))))
(encapsulate nil (defconst *c* (make-fast-alist (hons-acons 'fn3 3 *b*))))

We still see the warning/break in pass 2 of the second and third encapsulates, created by calls of hons-acons exactly as before. However, the results of those two calls are converted to fast alists by make-fast-alist; so after each encapsulate, the value of the defined constant is indeed a fast alist. A problem still persists: the second and third defconst event each steal the fast-alist value of the previous defconst. That's a problem that we won't try to solve here; we will just focus on how to ensure that the value of *c* is a fast alist.

The following alternate solution has the advantage of avoiding the expense of reconstituting the fast alist during pass 2 of each of the defconst events. (We continue to use encapsulate since otherwise the issue at hand dissolves.)

(encapsulate nil (make-event `(defconst *a* ',(hons-acons 'fn1 1 nil))))
(encapsulate nil (make-event `(defconst *b* ',(hons-acons 'fn2 2 *a*))))
(encapsulate nil (make-event `(defconst *c* ',(hons-acons 'fn3 3 *b*))))

These uses of make-event cause each fast alist from pass 1 to be saved and then reused in pass 2. There are no fast-alist warnings, and we avoid the expense of make-fast-alist.