		Search-engine friendly clone of the ACL2 documentation.

Debugging

Accumulated-persistence

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 summary, (accumulated-persistence t) turns on fresh statistics gathering for rules, (accumulated-persistence nil) turns it off, (show-accumulated-persistence) displays the statistics that were gathered, and (accumulated-persistence-oops) restores the statistics, if any, that were cleared by (accumulated-persistence t) or (accumulated-persistence :all).

In general, if the optional second argument of show-accumulated-persistence is supplied as :list, then instead of the result being displayed a ``pretty'' human-readable format, the result will be displayed as a corresponding list of entries of the form (frames tries xrune).

Note: set-accumulated-persistence is equivalent to accumulated-persistence.

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 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.

Consider a :rewrite rule named rune. For simplicity, let us imagine that 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 rune by 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 tried while 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 rune is 1 — we ``bill'' rune once for its own application attempt. If, on the other hand, we tried 10 rules on behalf of that application of rune, then rune's accumulated persistence would be 11.

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 of function print-useless-runes.)

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 keys:

: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 show-accumulated-persistence, :frames is used.

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'' :frames or :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 ``all''.

: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 (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, (bad x).

--------------------------------
      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-ax as ``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 :frames as ``useful'' or ``useless'' is based on whether they support ``useful'' or ``useless'' :tries.

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 rune1 is reported to have a :ratio of 101, meaning that on the average a hundred and one frames were built each time rune1 was tried. Suppose rune2 has a :ratio of 100. It could be that the attempt to apply rune1 resulted in the attempted application of rune2 and no other rune. Thus, in some sense, rune1 is ``cheap'' and rune2 is the ``culprit'' even though it is reported as costing less than rune1.

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 argument :frames-a or :tries-a.

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 accumulated-persistence the argument :ALL:

(accumulated-persistence :all)

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 works, suppose rn is a rune. Then we prepend the keyword :CONC to rn to form what we call its ``conclusion xrune'', and for its I-th hypothesis we prepend :HYP I to rn to form its I-th ``hypothesis xrune.'' Here, ``xrune'' is pronounced ``ex rune'', and is mnemonic for ``extended rune.'' For example, if (REWRITE FOO) is a rune then (:CONC REWRITE FOO) is its conclusion xrune, and (:HYP 2 REWRITE FOO) is a hypothesis xrune corresponding to the second hypothesis of the corresponding rewrite rule.

With (accumulated-persistence :all), we instruct ACL2 to track not only runes but also xrunes. Then, (show-accumulated-persistence) will display information for all xrunes in a format that we consider to be ``raw'', in the sense that data for xrunes are displayed just as for runes. But a ``merged'' format is also available. Here is a summary of display commands, followed below by further discussion.

(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 counts. Rather, they serve as accumulation sites without contributing their :tries to any accumulation. Consider for example the snippet below, taken from a report created with the :merge option (to be discussed further below), i.e., by evaluating the form (show-accumulated-persistence :frames :merge).

: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 :tries are recorded for the xrune (:HYP 1 :REWRITE PERM-MEM), no :frames are recorded. This is because no stack frames were built for runes while this xrune was on the stack — only for the xrune itself, which as we explained above is not accumulated into the total :frames counts. As it turns out, this lack of stack frames is explained by the fact that the rewrite rule PERM-MEM has a free variable in the first hypothesis.

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 type reasoning, that is not done during rewriting of a hypothesis or the conclusion.

Now suppose we have executed (accumulated-persistence :all) and attempted some proofs, and now we are ready to see statistics. The form (show-accumulated-persistence) displays statistics exactly as described above, treating these extra xrunes just as though they are runes; similarly for the form (show-accumulated-persistence KEY), for any legal KEY. A second optional argument may however be supplied to show-accumulated-persistence. The default for that second argument is t, and a second argument of :raw is treated the same as t; thus, these arguments provide the behavior just described, where data for xrunes are displayed just as for runes. You may restrict output to runes, ignoring hypothesis and conclusion xrunes, by giving a second argument of nil. (This gives the same behavior as if we had started with the command (accumulated-persistence t) instead of the command (accumulated-persistence :all).) You may give a second argument of :merge, in which case output will be sorted and displayed as though only runes were tracked (not the extra xrunes), but each data item for a non-rune xrune will be merged so that it is displayed in suitable order just below its corresponding rune, as in the PERM-MEM example displayed above. Finally, you may give a second argument of :list, which is equivalent to the default second argument of t, except that the results are printed as a list of entries (frames tries xrune).

We close by mentioning two aspects of enhanced statistics display for :CONC xrunes that have potential to be confusing. First consider the following example.

  :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 :CONC xrune. The explanation, however, is simple: the hypothesis never rewrote to true, so the conclusion was never rewritten. This is consistent with the marking as ``useless'' of all :frames and :tries for the rune and the hypothesis xrune. Note by the way, once again, that the hypothesis xrune does not contribute to any :frames count.

Another reason not to see data displayed for a :CONC xrune is that if a rule has no hypotheses, then no such data is collected. This decision was made because in the case of no hypotheses, we expect it to be very rare that information for the :CONC xrune will add any useful insight.

On a final note: (show-accumulated-persistence :runes) may be used simply to see a list of all runes (or xrunes) displayed alphabetically.

Users are encouraged to think about other meters we could install in ACL2 to help diagnose performance problems.

Subtopics

Useless-runes: Speed up proofs by disabling useless runes
Dmr: Dynamically monitor rewrites and other prover activity
Accumulated-persistence-subtleties: Some subtle aspects of the counting done by accumulated-persistence