Useless-runes
Speed up proofs by disabling useless runes
This topic documents the :useless-runes keyword argument of
certify-book and ld, which makes it possible to speed up
repeated running of a book's events. This option is ignored in
ACL2(r) (see real) and, when waterfall-parallelism is active, in
ACL2(p) (see parallelism).
Introduction
For a given event, the so-called ``useless'' rules are those that do
not contribute to the progress of any proof supporting that event. For more
background see accumulated-persistence, which is typically used for
finding rules (or more precisely, runes) to disable during
proofs. The feature described in the present topic provides automation for
the discovery and effective disabling of useless rules.
Below, we focus first on the use of :useless-runes for certify-book rather than for ld. The main time to use this option
with ld may be when developing a book that is to be certified
eventually with a :useless-runes option. We return to discuss ld
later in this topic (in Section ``Modifications for ld'').
To use the :useless-runes option of certify-book, first
certify your book — say, foo.lisp — by supplying option
:useless-runes :write. This creates a file in the subdirectory .sys
of the book's directory, creating that directory if it does not already exist.
This new file, .sys/foo@useless-runes.lsp, associates names of defthm, defun, and verify-guards events with sets of
``useless'' runes'': rule names (``runes'') not contributing to
the progress of the proof. Then, future certifications can use option
:useless-runes :read — or some limited variations of :read
using numeric values, as discussed below) — which, during evaluation of
an event, will effectively disable rules associated with that event in
file foo@useless-runes.lsp.
Environment variable ACL2_USELESS_RUNES can take the value
"write" or "read" to be used in place of the :useless-runes
option :read or :write (respectively) of certify-book.
ACL2_USELESS_RUNES can also have value "nil" (case-insensitive) or
a string representing a legal numeric value for the :useless-runes option
of certify-book. This is all discussed below.
By default, certification of the community-books, when using either
make (as described elsewhere; see books-certification) or build::cert.pl, is performed with environment variable
ACL2_USELESS_RUNES set to "-25". This setting, for each book
foo.lisp, causes part of the corresponding file
.sys/foo@useless-runes.lsp, if it exists, to be consulted as described
below. However, useless runes are entirely ignored (both their use and for
writing to .sys/foo@useless-runes.lsp files) both in ACL2(r) (see real) and, when waterfall-parallelism is active, in ACL2(p) (see parallelism).
Detailed Documentation
Again, the :useless-runes option provides a way to automate discovery
and, in subsequent uses, disabling of useless runes that can speed up proofs.
Information about useless runes is communicated using a file, which we call
the ``@useless-runes.lsp file'' (or, sometimes, ``useless-runes file''), whose
name is obtained by adding the suffix "@useless-runes.lsp" to the book
name, and which is placed in the .sys subdirectory of the book's
directory, after creating that subdirectory if it does not already exist. For
example, if the book's filename is "foo.lisp" then the corresponding
@useless-runes.lsp has filename ".sys/foo@useless-runes.lsp".
The following table summarizes the legal values for the option
:useless-runes; further explanation follows.
:write ; Write the @useless-runes.lsp file to speed up future proofs.
:read or ; Read the @useless-runes.lsp file to speed up proofs;
:read? ; file must exist for :read, but need not exist for :read?.
N, -N ; N is a positive integer not exceeding 100. Then |N|% of the rules
; indicated by the @useless-runes.lsp file are to be kept disabled.
; The @useless-runes.lsp file needs to exist for N but not for -N.
nil ; Do not read or write the @useless-runes.lsp file.
Notice in particular that :useless-runes 100 is equivalent to
:useless-runes :read, while :useless-runes -100 is equivalent to
:useless-runes :read?.
The option :useless-runes :write directs that a corresponding
@useless-runes.lsp file is to be written. Each top-level entry of this file
that is non-trivial (see below) has the form
(name
(frames-1 tries-1 rune-1)
(frames-2 tries-2 rune-2)
...
(frames-k tries-k rune-k)
)
where name is the name of a defthm, defun, or verify-guards event, and each tuple (frames-i tries-i rune-i) indicates
the number of frames and tries for rune-i recorded for the proofs done on
behalf of that event. ACL2 claims that none of the indicated rules
contributed to the progress of the proof. See accumulated-persistence,
but also see accumulated-persistence-subtleties for some limitations.
These top-level entries are listed in order of event in the book, from top to
bottom. Because of local events, the same name may appear more
than once; we say more about this in the ``Subtleties'' section, below.
Note that ``trivial'' entries are possible, where there are no tuples; in
that case, just (name) is printed, on a single line. Otherwise printing
uses the format shown above, where the first line contains a left parenthesis
on the left margin followed by the name, and each tuple is on a single line
starting in column 1 (i.e., after a single space), as is the final right
parenthesis.
The option :useless-runes :read or :useless-runes :read? directs
use of the corresponding @useless-runes.lsp file, if it exists. If that file
does not exist, an error is caused when the option value is :read but the
option is simply ignored when the option value is :read?.
The value of :useless-runes may also be a non-zero integer between
-100 and 100, inclusive. The absolute value of this number is the percentage
of the runes associated with the current event that are to be effectively kept
disabled, starting with the useless rune with the highest number of
frames built (see accumulated-persistence). For example, if the value
is 20 then 1/5 of the runes associated with the current event in the
@useless-runes.lsp file are to be kept disabled; so if the relevant top-level
form in that file is
(name
(frames-1 tries-1 rune-1)
(frames-2 tries-2 rune-2)
(frames-3 tries-3 rune-3)
(frames-4 tries-4 rune-4)
(frames-5 tries-5 rune-5)
(frames-6 tries-6 rune-6)
(frames-7 tries-7 rune-7)
)
then 1/5 of the 7 runes are to be disabled, so since the first integer
greater than or equal to 7/5 is 2, the runes rune-1 and rune-2 will
be kept disabled. Note again that the value 100 for :useless-runes
gives the same behavior as the value :read, and the value -100 gives
the same behavior as the value :read?.
The :useless-runes option need not be given explicitly to certify-book. Suppose that the environment variable ACL2_USELESS_RUNES
has a non-empty value. Then that value implicitly invokes the
:useless-runes option as indicated by the following table, which shows
how that environment variable value corresponds to a value for the
:useless-runes option.
ACL2_USELESS_RUNES value :useless-runes value
------------------------ --------------------
WRITE (case insensitive) :write
READ (case insensitive) :read
READ? (case insensitive) :read?
i, ij, -i, -ij, 100, -100 corresponding integer, which cannot be 0
(i and j are base-10 digits)
Important. An explicitly supplied :useless-runes value
normally takes priority over the value of environment variable
ACL2_USELESS_RUNES. However, for certify-book the environment
variable takes priority if its (case insensitive) value is "WRITE"
provided :useless-runes nil is not supplied explicitly. This feature
supports the use of the environment variable when using make to update
@useless-runes.lsp files for the community books.
If you want certification to avoid reading the book's @useless-runes.lsp
file even when this environment variable has a non-empty value that specifies
reading, use option :useless-runes nil.
A reason for allowing integer values, rather than only :read and
:read?, is that the disabling of useless runes can cause a proof to fail.
Although this is probably uncommon, it can happen, for example because an
otherwise useless rule rewrites the hypothesis of rule R to something that can
not be proved by rewriting, thus blocking the use of rule R; but with the
useless rule disabled, R is successfully applied, sending the proof in a
direction that leads to failure. This problem may disappear when using only a
portion of the useless rules. See also accumulated-persistence-subtleties.
Note that when using the @useless-runes.lsp file for a given event's
proofs, then the appropriate rules are effectively disabled not only at
the top level, but also whenever hints are supplied. So if an
:in-theory hint specifies a theory that includes rule R,
but rule R is specified for disabling for the current event by the
@useless-runes.lsp file, then R will be removed from the theory before
installing that hint. In particular, even the hint :in-theory (enable
R) will not enable R in this case.
Finally, we remark that the @useless-runes.lsp file is somewhat robust in
the following sense. Suppose that rule R is specified in that file, but at
the time the @useless-runes.lsp is read, rule R has been removed from one's
books. Then the inclusion of R as a useless rule will simply be ignored,
rather than causing an error.
Subtleties
The @useless-runes.lsp files do not contain any :executable-counterpart runes, because there are many places that ACL2 does
not track such runes for accumulated-persistence.
(Details are in a comment in the ACL2 source definition of function
print-useless-runes.)
On rare occasions, when using the :read option or related values that
specify reading from an appropriate @useless-runes.lsp file, the package of a rune's name might not be known to ACL2 at read time. In that
case, that rune will be ignored.
Because of local events, more than one event may be
associated with a name in a given @useless-runes.lsp file. When using the
:read option or related values that specify reading from an appropriate
@useless-runes.lsp file, ACL2 considers entries for a given name from top to
bottom in the @useless-runes.lsp file, attempting to match them to defthm, defun, and verify-guards events from top to bottom in
the book.
As suggested by discussions above, a @useless-runes.lsp file is intended
not to cause proof failures, even if it is older than the corresponding book
or even older than other books containing runes that are listed in that
@useless-runes.lsp file. That said, an out-of-date @useless-runes.lsp might
cause proofs to fail. In particular, imagine that there are several lemmas in
the corresponding book all with the same name (and thus all local to an
encapsulate event except perhaps the last), and one of those lemmas
other than the last is deleted from the book. Then references to the later
such lemmas will be wrong in the @useless-runes.lsp file. If you run into
this problem, then either regenerate the @useless-runes.lsp file (e.g., using
certify-book with environment variable ACL2_USELESS_RUNES set to
"write"), or give distinct names to your book's lemmas, or even
consider adding a line like the following to a suitable .acl2 file (see
build::custom-certify-book-commands).
; cert-flags: ? t :useless-runes nil
Adaptations for ld
The :useless-runes keyword argument was originally developed for
certify-book, and that is probably still where it is most useful. But
when developing or updating a book "BK", it may be convenient to
evaluate the book's events using (ld "BK.lisp" .. :useless-runes
..). In that case, it is probably a good idea to run that ld command
in the same certification world (i.e., the world with the same sequence
of portcullis commands) as will be encountered when certifying the
book, so that the accesses to the @useless-runes.lsp will match up between the
ld call and a corresponding certify-book call. The following
observations may help in that respect.
- If "BK.lisp" has previously been certified, there should be a file
"BK.port". By executing (ld "BK.port"), you will put yourself
in the appropriate certification world (unless the book's portcullis
commands have changed since the time it was certified).
- If your ld of the book ends prematurely in an error, then before you
call ld again with a :useless-runes argument, it would very likely
be best to back up (using :ubt) so that you are once again in the
intended certification world.
Here are a few differences between ld and certify-book with
respect to useless-runes. For purposes of this discussion, let's say a call
of ld is ``a book-like call'' if the first argument is a string ending
with ".lisp".
- Just as how certify-book consults environment variable
ACL2_USELESS_RUNES for an implicit value of omitted keyword argument
:useless-runes, a book-like call of ld consults environment variable
ACL2_USELESS_RUNES_LD. For example, if environment variable
ACL2_USELESS_RUNES_LD has value "50", then the call (ld
"foo.lisp") will be treated as though it were the call (ld
"foo.lisp" :useless-runes 50).
- If environment variable ACL2_USELESS_RUNES_LD takes on the special
value "cert", case-insensitive, then ld will consult environment
variable ACL2_USELESS_RUNES just as certify-book does.
- It is an error for a call of ld that is not book-like to have a
non-nil :useless-runes argument. For a call of ld without a
:useless-runes argument, environment variables supply a useless-runes
value (as described above) only if it is a book-like call.
- The value of keyword argument :useless-runes in a call of
certify-book or ld does not persist to a subsidiary call of
certify-book or ld. If you want a useless-runes value to persist,
use environment variables.
- Recall that for certify-book, the environment variable takes priority
if its (case insensitive) value is "write" provided the
:useless-runes nil keyword argument is not supplied. But for ld, an
explicit value of the :useless-runes keyword argument always takes
priority; environment variables, even with value "write", do not
override any such value.
Performance
In ``everything'' testing of all of the community-books during
(not quite complete) development of this capability, we found that writing the
@useless-runes.lsp files (by setting the environment variable
ACL2_USELESS_RUNES to "write") caused an 11% slowdown from the
normal time, but a fresh such test when reading the @useless-runes.lsp files
by setting the environment variable ACL2_USELESS_RUNES to "25" cut
24% from the normal time. Books varied considerably, however. For example,
after finding a specific time reduction that was particularly significant, we
re-certified on standalone runs (i.e., on an otherwise unloaded machine) and
found that the time was reduced from 17 minutes and 1.9 seconds down to 34.93
seconds, thus eliminating 96.6% of the time.
Subtopics
- Useless-runes-failures
- Failures caused by useless-runes
