To get statistics on which runes are being tried
Useful Forms: (accumulated-persistence t) ; Activate statistics gathering. (accumulated-persistence :all) ; As above, ``enhanced'' (see below) (show-accumulated-persistence :frames) ; Display statistics ordered by (show-accumulated-persistence :tries) ; frames built, times tried, (show-accumulated-persistence :ratio) ; or their ratio. (show-accumulated-persistence) ; Same as supplying :frames argument. (accumulated-persistence nil) ; Deactivate. (accumulated-persistence-oops) ; Undo the clearing effect of ; (accumulated-persistence t). 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. (show-accumulated-persistence :runes) ; Just show runes alphabetically. (show-accumulated-persistence :useless) ; Just show useless runes. (show-accumulated-persistence :useless :list) ; Just show useless runes as a list.
In general, if the optional second argument of
See the end of this item for a discussion of ``enhanced statistics gathering,'' which can be useful for more fine-grained proof debugging.
Generally speaking, the more ACL2 knows, the slower it runs. That is because the search space grows with the number of alternative rules. Often, the system tries to apply rules that you have forgotten were even there, if you knew about them in the first place! ``Accumulated-persistence'' is a statistic (originally developed for Nqthm) that helps you identify the rules that are causing ACL2's search space to explode.
For other proof debugging utilities, see break-rewrite, with-brr-data, and dmr.
Accumulated persistence tracking can be turned on or off. It is generally off. When on, proofs may take a little more time than otherwise. (We measured approximately 11% more time in a so-called ``everything'' regression run in May 2020.) 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
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.
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.
We do not claim that tracking of runes for accumulated-persistence is
perfect. In practice, we believe it is quite reliable with the exception of
congruence runes and, in some cases executable-counterpart
runes. (For the latter, details are in a comment in the ACL2 source definition
When the accumulated persistence totals are displayed by the function
:frames - the number of frames built on behalf of the rune :tries - the number of times the rune was tried :ratio - frames built per try
The 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
: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 thm form, ACL2 attempts to rewrite
-------------------------------- 1 1 ( 1.00) (:REWRITE BAD-AX) 0 0 [useful] 1 1 [useless] --------------------------------
Now consider the top-level application of rule
-------------------------------- 3 1 ( 3.00) (:REWRITE HYP-IMPLIES-CONCL) 3 1 [useful] 0 0 [useless] --------------------------------
In summary: categorization of
See useless-runes for a way to speed up proofs by automatically turning off useless rules.
Note that a rune with high accumulated persistence may not actually
be the ``culprit.'' For example, suppose
If a proof is aborted, then in general, show-accumulated-persistence 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
There are other subtleties in how rune applications are tallied, documented elsewhere: see accumulated-persistence-subtleties.
We conclude with a discussion of ``enhanced'' statistics gathering, which
is enabled by supplying
At some additional performance expense (but probably well under a factor of
2 altogether), ACL2 then gathers additional statistics for individual
hypotheses of rules as well as their conclusions. To understand how this
(show-accumulated-persistence :frames t) ; t is optional, i.e., the default ; Display enhanced statistics sorted by frames, in a ``raw'' format. (show-accumulated-persistence :frames :merge) ; Display enhanced statistics sorted by frames, in a ``merged'' format. (show-accumulated-persistence :frames nil) ; Display regular statistics sorted by frames ; (runes only, that is, without the enhancements). (show-accumulated-persistence :frames :merge) ; Display a list of entries (frames tries xrune), sorted by frames ; More generally, the descriptions just above apply for any legal first ; argument: (show-accumulated-persistence KEY t) (show-accumulated-persistence KEY :merge) (show-accumulated-persistence KEY nil) (show-accumulated-persistence KEY :list) ; Note also these alternate forms, equivalent to the first of the two forms ; just above, i.e., the form with second argument of t: (show-accumulated-persistence KEY :raw) (show-accumulated-persistence KEY)
There is a significant difference between how runes are tracked and how
ACL2 tracks hypothesis and conclusion xrunes: unlike regular runes, these
xrunes do not contribute to the accumulated
:frames :tries :ratio rune -------------------------------- 462 211 ( 2.18) (:REWRITE PERM-MEM) 13 6 [useful] 449 205 [useless] ............................. 251 47 ( 5.34) (:HYP 2 :REWRITE PERM-MEM) 6 6 [useful] 245 41 [useless] ............................. 0 211 ( 0.00) (:HYP 1 :REWRITE PERM-MEM) 0 6 [useful] 0 205 [useless] ............................. 0 7 ( 0.00) (:CONC :REWRITE PERM-MEM) 0 6 [useful] 0 1 [useless] --------------------------------
Notice that while
ACL2 !>:pe perm-mem 18 (DEFTHM PERM-MEM (IMPLIES (AND (PERM X Y) (MEM A X)) (MEM A Y)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ONCE))) ACL2 !>
The second hypothesis, however, does cause additional rewriting in order to
rewrite it to true, resulting in 251 stack frames for runes. We see that the
conclusion does not lead to creation of any rune stack frames, which might
seem to suggest that only 251 stack frames for runes were created on behalf of
this rule application — yet, we see that 462 frames were actually
created. The difference is the 211 frames created for the rewrite rule
itself. Even if the total had been a bit more than 462, one need not be
surprised, as there could be some work recorded during application of the
rewrite rule, such as
Now suppose we have executed
We close by mentioning two aspects of enhanced statistics display for
:frames :tries :ratio rune -------------------------------- 14 4 ( 3.50) (:REWRITE DEFAULT-+-2) 0 0 [useful] 14 4 [useless] ............................. 10 4 ( 2.50) (:HYP 1 :REWRITE DEFAULT-+-2) 0 0 [useful] 10 4 [useless] --------------------------------
It may be surprising that no data is displayed for the corresponding
Another reason not to see data displayed for a
On a final note:
Users are encouraged to think about other meters we could install in ACL2 to help diagnose performance problems.