Print-cl-cache
Information about the cache supporting apply$
General Form:
(print-cl-cache)
Logically this function always returns NIL but it prints to the
comment window information about the cache that supports the application of
quoted LAMBDA objects by apply$. The name stands for Print
Compiled Lambda Cache.
In general there is a non-empty cache line for each LAMBDA object
used in a defun or seen by verify-guards or by apply$ in the
evaluation theory. But the cache has a maximal size. If a new LAMBDA
object is seen when the cache is full, the least recently used line is
re-used for the new LAMBDA object. By default the maximal cache size is
1000. This can be changed -- with the side-effect of clearing the cache --
by exiting the ACL2 loop with :q and doing (setq *cl-cache* k),
where k is the new maximal size.
When print-cl-cache is called it prints a block about each non-empty
cache line enumerated from 0, and listed in the order that the cache is
searched when a LAMBDA object is apply$d. Each block contains:
- :lambda-object - a fully translated LAMBDA object
- :status - one of four keywords with the following meanings:
- :GOOD - the LAMBDA object is well-formed and Common Lisp
compliant (``guard verified'') in the current world
- :BAD - the LAMBDA object is not well-formed or not Common
Lisp compliant (``guard verified'') in the current world, but
(with high probability) there is a world in which it is well-formed
and compliant
- :UGLY - the LAMBDA object is so ill-formed it can never be
:GOOD in any world, e.g., (LAMBDA (T) (CONS 3 . 4))
- :UNKNOWN - we do not know the status of this object in the
current world and leave it to apply$ to determine the proper
status the next time this object is apply$d.
- :abs-event-no - the absolute event number (in the current world) at
which the LAMBDA object was proved to have status :GOOD, or
NIL if its status is not :GOOD
- :extracts - some parts of the LAMBDA object sufficient to
confirm well-formedness. Well-formedness must be re-confirmed if the
world is retracted to before the object became :GOOD
- :problem - One of the following values.
- NIL - no problem; status is :GOOD
- NOT-WELL-FORMED - the LAMBDA is syntactically plausible but
not well-formed but could, perhaps, become well-formed in a suitable
extension of the current world, e.g., the body calls an undefined
function (but perhaps it can be defined), the body contains a
:program mode function (but perhaps that could be upgraded to
:logic mode), the body contains an unbadged or unwarranted
function symbol (but perhaps defbadge or defwarrant could
resolve the issue), etc.
- (GUARD-USES-NON-COMPLIANT-FNS . fns) - fns is a list of
function symbols used in the guard of the LAMBDA object that
have not yet had their guards verified.
- (BODY-USES-NON-COMPLIANT-FNS . fns) - fns is a list of
function symbols used in the body of the LAMBDA object that
have not yet had their guards verified.
- (UNPROVED-GUARD-CLAUSES . cl-set) - cl-set is the list of
guard conjectures -- written as clauses -- that tau was unable to
prove.
- RE-VALIDATION-INTERRUPTED - an interrupt aborted the updating of
this cache line
- :hits - The number of times apply$ has seen this LAMBDA
object
- :guard-code - NIL or the string ``<code>'' indicating that
the guard has been compiled
- :lambda-code - NIL or the string ``<code>'' indicating that
the LAMBDA object has been compiled
Using This Information to Speed Up LAMBDA Application
Remember: A lot of programmers spend enormous amounts of time and
effort optimizing code that runs adequately fast! Do not make the mistake of
investing your time here unless you really have a critical ACL2 top-level
read-eval-print form that you know runs too slowly!
If you see a LAMBDA object in the cache with :status :BAD then it
is being interpreted. If you believe it can be converted to :GOOD and thus
compiled, and you believe you will apply$ it often enough in the future
to warrant trying to speed it up, then here are some tips.
To be converted from :BAD to :GOOD a LAMBDA has to be both
well-formed and guard verified. The cache doesn't try to verify
objects that are not well-formed. So first make sure your object is
well-formed and then once it is make sure it is guard verified.
If the :problem is NOT-WELL-FORMED the :lambda-object
does not pass the well-formed-lambda-objectp test. That predicate
gives no hint as to why, but if you call :translam on the
:lambda-object it might give you more information. E.g.,
ACL2 !>:translam (lambda (x) (bar x))
ACL2 Error in TRANSLAM: The body of a LAMBDA object or lambda$ term
should be fully badged but BAR is used in (BAR X) and has no badge.
Other typical problems are that a function which was formerly in
:logic mode is now in :program mode because of an undo, or the
LAMBDA object is not tame, as in
ACL2 !>:translam (lambda (x) (apply$ (cons x 'nil) 'sq))
ACL2 Error in TRANSLAM: The body of a LAMBDA object or lambda$ term
must be tame and (APPLY$ (CONS X 'NIL) 'SQ) is not.
Here the LAMBDA is unfixable because the arguments to apply$ are
in the wrong order. Typing the object correctly may fix the problem.
In any case, you may need to extend the world to convert functions to
:logic mode, obtain warrants (or at least badges for
functions that return multiple results), or even use a different LAMBDA
object.
When you think you've got a well-formed LAMBDA object, you can get
the cache to update itself by applying the (new?) object in the (new?)
world,
ACL2 !>(apply$ '(lambda (x) (apply$ 'sq (cons x 'nil))) '(5))
25
ACL2 !>(print-cl-cache)
and see if the status is :GOOD and, if not, what the :problem
is.
If the problem is one of GUARD-USES-NON-COMPLIANT-FNS,
BODY-USES-NON-COMPLIANT-FNS, or UNPROVED-GUARD-CLAUSES, the
LAMBDA object is well-formed but not guard verified. Again, you may
need to further extend the world by calling verify-guards on the
listed function symbols in first two problems or call verify-guard on
the lambda object itself for an opportunity to supply :hints to prove
the guard clauses listed in the third problem.
For example, suppose we define squ with a guard of natp,
(defun$ squ (x)
(declare (type (satisfies natp) x))
(* x x))
And suppose we define nfixer to always return a natural number but
in such a way as its type-prescription is weak.
(defun$ nfixer (x)
(if (equal x (car (cons x x)))
(nfix x)
nil))
Furthermore, let's disable nfixer so the prover has no way of
discovering the proper type.
(in-theory (disable nfixer))
If we then
ACL2 !>(apply$ '(lambda (x) (squ (nfixer x))) '(5))
25
and use print-cl-cache, we see that the :problem is that NFIXER
is not guard verified. So we
ACL2 !>(verify-guards nfixer)
and try the apply$ and the print-cl-cache again. This time the :problem is
(UNPROVED-GUARD-CLAUSES ((NATP (NFIXER X)))). So tau couldn't prove that
NFIXER returns a NATP. We can thus
ACL2 !>(verify-guards (lambda (x) (squ (nfixer x)))
:hints (("Goal" :in-theory (enable nfixer))))
The verify-guards should succeed. Successful calls of
verify-guards on LAMBDA objects updates the cache, so we don't have
to ``trick'' the cache into updating itself by apply$ing the lambda
again. We can now just do (print-cl-cache) and see the :status is
:GOOD.
Whether all this work is worth is depends on how often you're going to execute
this LAMBDA object!
A Single Performance Comparison
Suppose we have defined squ and nfixer, disabled nfixer,
and verified the guards of nfixer as above. Additionally, define the
scion that maps a predicate over a list and checks that the predicate
holds for every element.
(defun$ always$ (pred lst)
(if (endp lst)
t
(and (apply$ pred (list (car lst)))
(always$ pred (cdr lst)))))
and define the function that builds a list of the first n+1 naturals
and use it to define the misleadingly named constant *million* which
contains the first million and one naturals.
(defun nats-ac (n ac)
(if (zp n)
(cons 0 ac)
(nats-ac (- n 1) (cons n ac))))
(defconst *million* (nats-ac 1000000 nil))
Now observe that (lambda (x) (natp (squ (nfixer x)))) suffers the
same problem we witnessed above: tau cannot prove the guard clause because
nfixer is disabled. So we can do an experiment! How long does it take
to run this :BAD lambda object over the list *million*? And then,
how long does it take to do it again after verifying its guards and turning
its status to :GOOD?
ACL2 !>(time$ (always$ '(lambda (x) (natp (squ (nfixer x)))) *million*))
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 4.35 seconds realtime, 4.35 seconds runtime
; (128,000,160 bytes allocated).
T
ACL2 !>(verify-guards (lambda (x) (natp (squ (nfixer x))))
:hints (("Goal" :in-theory (enable nfixer))))
...[successful but output elided]...
ACL2 !>(time$ (always$ '(lambda (x) (natp (squ (nfixer x)))) *million*))
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 0.19 seconds realtime, 0.19 seconds runtime
; (32,000,064 bytes allocated).
T
So we dramatically sped up the computation. But we almost certainly spent
longer than the original 4.35 seconds debugging the problems and converting
the object's status to :GOOD. So unless we're going to be doing this
repeatedly in the future, it probably wasn't worth it!
