Major Section: OTHER
Useful Forms: (accumulated-persistence t) ; Activate statistics gathering.
(show-accumulated-persistence :frames) ; Display statistics ordered by (show-accumulated-persistence :tries) ; frames built, times tried, (show-accumulated-persistence :ratio) ; or their ratio.
(accumulated-persistence nil) ; Deactivate.
Advanced forms: (show-accumulated-persistence :frames-s) ; The `s', `f', and `a' suffixes (show-accumulated-persistence :frames-f) ; stand for `success' (`useful'), (show-accumulated-persistence :frames-a) ; `failure' (`useless'), and `all', (show-accumulated-persistence :tries-s) ; respectively. The only effect of (show-accumulated-persistence :tries-f) ; the `s' and `f' versions is to (show-accumulated-persistence :tries-a) ; sort first by useful or useless ; applications, respectively (see ; below). The `a' versions avoid ; showing the useful/useless ; breakdown.
For other proof debugging utilities, see break-rewrite and see dmr.
Accumulated persistence tracking can be turned on or off. It is generally off. When on, proofs may take perhaps 50% more time than otherwise! But some useful numbers are collected. When it is turned on, by
ACL2 !>(accumulated-persistence t)an accumulation site is initialized and henceforth data about which rules are being tried is accumulated into that site. That accumulated data can be displayed with
show-accumulated-persistence, as described in detail below. When accumulated persistence is turned off, with
(accumulated-persistence nil), the accumulation site is wiped out and the data in it is lost.
The ``accumulated persistence'' of a rune is the number of runes the system has attempted to apply (since accumulated persistence was last activated) while the given rune was being tried.
rewrite rule named
rune. For simplicity, let us
rune is tried only once in the period during which
accumulated persistence is being monitored. Recall that to apply a
rewrite rule we must match the left-hand side of the conclusion to some term
we are trying to rewrite, establish the hypotheses of
rewriting, and, if successful, then rewrite the right-hand side of the
conclusion. We say
rune is ``being tried'' from the time we have
matched its left-hand side to the time we have either abandoned the attempt
or finished rewriting its right-hand side. (By ``match'' we mean to include
any loop-stopper requirement; see loop-stopper.) During that period of time
other rules might be tried, e.g., to establish the hypotheses. The rules
rune is being tried are ``billed'' to
rune in the
sense that they are being considered here only because of the demands of
rune. Thus, if no other rules are tried during that period, the
accumulated persistence of
1 -- we ``bill''
once for its own application attempt. If, on the other hand, we tried
rules on behalf of that application of
accumulated persistence would be
One way to envision accumulated persistence is to imagine that every time a rune is tried it is pushed onto a stack. The rules tried on behalf of a given application of a rune are thus pushed and popped on the stack above that rune. A lot of work might be done on its behalf -- the stack above the rune grows and shrinks repeatedly as the search continues for a way to use the rune. All the while, the rune itself ``persists'' in the stack, until we finish with the attempt to apply it, at which time we pop it off. The accumulated persistence of a rune application is thus the number of stack frames built while that rune was on the stack.
Note that accumulated persistence is tallied whether or not the attempt to apply a rune is successful. Each of the rules tried on its behalf might have failed and the attempt to apply the rune might have also failed. The ACL2 proof script would make no mention of the rune or the rules tried on its behalf because they did not contribute to the proof. But time was spent pursuing the possible application of the rune and accumulated persistence is a measure of that time.
A high accumulated persistence might come about in two extreme ways. One is that the rule causes a great deal of work every time it is tried. The other is that the rule is ``cheap'' but is tried very often. We therefore keep track of the number of times each rule is tried as well as its persistence. The ratio between the two is the average amount of work done on behalf of the rule each time it is tried.
When the accumulated persistence totals are displayed by the function
show-accumulated-persistence we sort them so that the most expensive
runes are shown first. We can sort according to one of three basic
:frames - the number of frames built on behalf of the rune :tries - the number of times the rune was tried :ratio - frames built per tryThe key simply determines the order in which the information is presented. If no argument is supplied to
The display breaks each total into ``useful'' and ``useless'' subtotals. A
``useful'' rule try is one that is viewed as contributing to the progress of
the proof, and the rest are ``useless'' rule applications. For example, if a
rewrite rule is tried but its hypotheses are not successfully
relieved, then that rule application and all work done on behalf of those
hypotheses is ``useless'' work. In general, an attempt to apply a rune
is viewed as ``useful'' unless the attempt fails or the attempt is on the
stack (as described above) for a rune application that ultimately fails.
A large number of ``useless''
:tries along with
correspondingly small ``useful'' counts may suggest runes to consider
disabling (see disable and see in-theory). Thus, here is a more complete
list of the arguments that may be supplied to
show-accumulated-persistence. Suffixes ``s'', ``f'', and ``a'' are
intended to suggest ``success'' (``useful''), ``failure'' (``useless''), and
:frames - sort by the number of frames built on behalf of the rune :frames-s - as above, but sort by useful applications :frames-f - as above, but sort by useless applications :frames-a - as above, but inhibit display of ``useful'' and ``useless'' subtotals :tries - sort by the number of times the rune was tried :tries-s - as above, but sort by useful applications :tries-f - as above, but sort by useless applications :tries-a - as above, but inhibit display of ``useful'' and ``useless'' subtotals :ratio - sort by frames built per try :useless - show only the runes tried whose tries were all ``useless''
For a given line of the report, every frame credited to a ``useful'' (respectively, ``useless'') rule application is considered ``useful'' (respectively, ``useless''). We illustrate with the following example.
(progn (defstub hyp (x) t) (defstub concl (x) t) (defstub bad (x) t) (defstub good (x) t) (defaxiom good-ax (implies (good x) (hyp x))) (defaxiom bad-ax (implies (bad x) (hyp x))) (defaxiom hyp-implies-concl (implies (hyp x) (concl x))) ) (accumulated-persistence t) (thm (implies (good x) (concl x))) (show-accumulated-persistence)To prove the
thmform, ACL2 attempts to rewrite
(concl x)to true by applying rule
hyp-implies-concl. It then attempts to establish
(hyp x)first by trying rule
bad-ax, which fails, and second by trying rule
good-ax, which succeeds. As expected, the report labels as ``useless'' the failure of the attempt to establish the hypothesis,
-------------------------------- 1 1 ( 1.00) (:REWRITE BAD-AX) 0 0 [useful] 1 1 [useless] --------------------------------Now consider the top-level application of rule
hyp-implies-concl. Even though the above report shows the application of
bad-axas ``useless'', note that this rule was applied on behalf of the successful (``useful'') application of
hyp-implies-concl, and hence is incorporated into the ``useful'' line for
hyp-implies-concl, as follows.
-------------------------------- 3 1 ( 3.00) (:REWRITE HYP-IMPLIES-CONCL) 3 1 [useful] 0 0 [useless] --------------------------------In summary: categorization of
:framesas ``useful'' or ``useless'' is based on whether they support ``useful'' or ``useless''
Note that a rune with high accumulated persistence may not actually be
the ``culprit.'' For example, suppose
rune1 is reported to have a
101, meaning that on the average a hundred and one frames
were built each time
rune1 was tried. Suppose
rune2 has a
100. It could be that the attempt to apply
rune1 resulted in the
attempted application of
rune2 and no other rune. Thus, in some
rune1 is ``cheap'' and
rune2 is the ``culprit'' even though it
costs less than
If a proof is aborted, then in general,
will only display totals for runes whose attempted application is complete:
that is, if the rewriter was in the process of relieving hypotheses for a
rule, then information for that rule will not be included in the tally. We
say ``in general'' because, as indicated near the top of the output from
show-accumulated-persistence when such incomplete information is
omitted, you can get this information by using argument
There are other subtleties in how rune applications are tallied, documented elsewhere: see accumulated-persistence-subtleties.
Users are encouraged to think about other meters we could install in ACL2 to
help diagnose performance problems.