Hons-wash
(hons-wash) is like gc$ but can also garbage collect
normed objects (CCL and GCL Only).
Logically, hons-wash just returns nil; we leave it enabled and
would think it odd to ever prove a theorem about it.
Under the hood, in CCL and GCL, hons-wash runs a garbage collection
after taking special measures to allow normed conses to be collected. In
Lisps other than CCL, hons-wash does nothing. This is because the
efficient implementation of hons-wash is specific to the "static
honsing" scheme which requires CCL-specific features.
Why is this function needed? Ordinarily, it is not possible to garbage
collect any normed conses. This is because the Hons Space includes pointers
to any normed conses, and hence Lisp's garbage collector thinks these objects
are live. To correct for this, hons-wash (1) clears out these pointers,
(2) runs a garbage collection, then (3) re-norms any previously-normed conses
which have survived the garbage collection.
Notes.
- It is not recommended to interrupt this function. Doing so may cause
persistently normed conses and fast alist keys to become un-normed, which
might lead to less efficient re-norming and/or violations of the fast-alist
discipline.
- (For ACL2(p) users only; see parallelism) If parallel execution is
enabled (see set-parallel-execution), as it is by default in ACL2(p),
then hons-wash may be a no-op (other than to print a warning), in order
to avoid thread-unsafe behavior. (However, In CCL you are unlikely to see
this restriction unless you are running more than one thread.) To get around
this restriction, you can instead use hons-wash!, which however
requires a trust-tag.
Function: hons-wash
(defun hons-wash nil (declare (xargs :guard t))
nil)
