Major Section: PROGRAMMING
time-tracker macro is a utility for displaying runtime (cpu time)
spent during specified evaluation. In general, the user provides this
specification. However, ACL2 itself uses this utility for tracking uses of
its tau-system reasoning utility (see time-tracker-tau). We discuss
that use as an example before discussing the general form for calls of
Remark for ACL2(p) users (see parallelism):
time-tracker is merely a
no-op in ACL2(p).
During the development of the tau-system, we were concerned about the
possibility that it would slow down proofs without any indication of how one
might avoid the problem. We wanted a utility that would alert the user in
such situations. However, the tau-system code does not return state, so
we could not track time spent in the state. We developed the
time-tracker utility to track time and print messages, and we did it in a
general way so that others can use it in their own code. Here is an example
of such a message that could be printed during a proof.
TIME-TRACKER-NOTE [:TAU]: Elapsed runtime in tau is 2.58 secs; see :DOC time-tracker-tau.And here is an example of such a message that could be printed at the end of the proof.
TIME-TRACKER-NOTE [:TAU]: For the proof above, the total time spent in the tau system was 20.29 seconds. See :DOC time-tracker-tau.
time-tracker utility tracks computation time spent on behalf of a
user-specified ``tag''. In the case of the tau-system, we chose the tag,
:tau. The first argument of
time-tracker is the tag, which in our
running example is always
:tau. Note that although all arguments of
time-tracker are evaluated, the first argument is typically a keyword and
the second is always a keyword, and such arguments evaluate to themselves.
An ACL2 function invoked at the start of a proof includes the following code.
(progn$ (time-tracker :tau :end) (time-tracker :tau :init :times '(1 2 3 4 5) :interval 5 :msg "Elapsed runtime in tau is ~st secs; see :DOC ~ time-tracker-tau.~|~%") ...)
time-tracker call (above) ends any existing time-tracking for
:tau. One might have expected it be put into code managing the proof
summary, but we decided not to rely on that code being executed, say, in case
of an interrupt. When a given tag is not already being time-tracked, then
:end is a no-op (rather than an error).
time-tracker call (above) initiates time-tracking for the tag,
:tau. Moreover, it specifies the effect of the
Consider the following abbreviated definition from the ACL2 source code.
(defun tau-clausep-lst-rec (clauses ens wrld ans ttree state calist) (cond ((endp clauses) (mv (revappend ans nil) ttree calist)) (t (mv-let (flg1 ttree1 calist) (tau-clausep (car clauses) ens wrld state calist) (prog2$ (time-tracker :tau :print?) (tau-clausep-lst-rec (cdr clauses) ...))))))Notice that
(time-tracker :tau :print?)is executed immediately after
tau-clausepis called. The idea is to check whether the total time elapsed inside the tau-system justifies printing a message to the user. The specification of
:times '(1 2 3 4 5)in the
:initform above says that a message should be printed after 1 second, after 2 seconds, ..., and after 5 seconds. Thereafter, the specification of
:interval 5in the
:initform above says that each time we print, at least 5 additional seconds should have been tracked before
(time-tracker :tau :print?)prints again. Finally, the
:msgkeyword above specifies just what should be printed. If it is omitted, then a reasonable default message is printed (as discussed below), but in this case we wanted to print a custom message. The
:msgstring above is what is printed using formatted printing (see fmt), where the character
#\tis bound to a string giving a decimal representation with two decimal points of the time tracked so far for tag
:tau. (As our general description below points out,
:msgcan also be a ``message'' list rather than a string.)
But when is time actually tracked for
:tau? Consider the following
definition from the ACL2 source code.
(defun tau-clausep-lst (clauses ens wrld ans ttree state calist) (prog2$ (time-tracker :tau :start) (mv-let (clauses ttree calist) (tau-clausep-lst-rec clauses ens wrld ans ttree state calist) (prog2$ (time-tracker :tau :stop) (mv clauses ttree calist)))))The two calls of
time-trackerabove first start, and then stop, time-tracking for the tag,
:tau. Thus, time is tracked during evaluation of the call of
tau-clausep-lst-rec, which is the function (discussed above) that does the tau-system's work.
Finally, as noted earlier above, ACL2 may print a time-tracking message for
:tau at the end of a proof. The ACL2 function
contains essentially the following code.
(time-tracker :tau :print? :min-time 1 :msg "For the proof above, the total runtime ~ spent in the tau system was ~st seconds. ~ See :DOC time-tracker-tau.~|~%")The use of
:min-timesays that we are to ignore the
:intervalestablished by the
:initcall described above, and instead, print a message if and only if at least 1 second (since 1 is the value of keyword
:min-time) has been tracked for tag
:tau. Formatted printing (see fmt) is used for the value of
:msg, where the character
#\tis bound to a decimal string representation of the time in seconds, as described above.
The example above covers all legal values for the second argument of
time-tracker and discusses all the additional legal keyword arguments.
We conclude with a precise discussion of all arguments. Note that all
arguments are evaluated; thus when we refer to an argument, we are discussing
the value of that argument. All times discussed are runtimes, i.e., cpu
General forms: (time-tracker t) ; enable time-tracking (default) (time-tracker nil) ; disable time-tracking (time-tracker tag ; a symbol other than t or nil option ; :init, :end, :start, :stop, or :print? ;; keyword arguments: :times ; non-nil if and only if option is :init :interval ; may only be non-nil with :init option :min-time ; may only be non-nil with :print? option :msg ; may only be non-nil with :init and :print? options
Time-tracking is enabled by default. If the first argument is
nil, then no other arguments are permitted and time-tracking is enabled
or disabled, respectively. When time-tracking is disabled, nothing below
takes place. Thus we assume time-tracking is enabled for the remainder of
this discussion. We also assume below that the first argument is neither
We introduce some basic notions about time-tracking. A given tag, such as
:tau in the example above, might or might not currently be ``tracked'':
:init causes the specified tag to be tracked, while
:end causes the
specified tag not to be tracked. If the tag is being tracked, the tag might
or might not be ``active'':
:start causes the tag to be in an active
:stop causes the tag not to be active. Note that only
tracked tags can be in an active or inactive state. For a tag that is being
tracked, the ``accumulated time'' is the total time spent in an active state
since the time that the tag most recently started being tracked, and the
``checkpoint list'' is a non-empty list of rational numbers specifying when
printing may take place, as described below.
We now consider each legal value for the second argument, or ``option'', for
a call of
time-tracker on a given tag.
:Init specifies that the tag is to be tracked. It also establishes
defaults for the operation of
:print?, as described below, using the
:msg keywords. Of these three, only
:times is required, and its value must be a non-empty list of rational
numbers specifying the initial checkpoint list for the tag. It is an error
:init if the tag is already being tracked. (So if you don't
care whether or not the tag is already being tracked and you want to initiate
tracking for that tag, use
:End specifies that if the tag is being tracked, then it should nstop
being tracked. If the tag is not being tracked, then
:end has no effect.
:Start specifies that the tag is to be active. It is an error to specify
:start if the tag is not being tracked or is already active.
:Stop specifies that the tag is to stop being active. It is an error to
:stop if the tag is not being tracked or is not active.
:Print? specifies that if the tag is being tracked (not necessarily
active), then a message should be printed if a suitable condition is met.
The nature of that message and that condition depend on the keyword options
:print? as well as those supplied with the
that most recently initiated tracking.
:Print? has no effect if the tag
is not being tracked, except that if certain keyword values are checked if
:min-time must be a rational number or
:msg must be either a string, a true-list whose
car is a
nil. The remainder of this documentation describes the
:print? option in detail under the assumption that the tag is being
tracked: first, giving the conditions under which it causes a message to be
printed, and second, explaining what is printed.
:print? is supplied a non-
nil value of
:min-time, that value
must be a rational number, in which case a message is printed if the
accumulated time for the tag is at least that value. Otherwise a message is
printed if the accumulated time is greater than or equal to the
the checkpoint list for the tag. In that case, the tracking state for the
tag is updated in the following two ways. First, the checkpoint list is
scanned from the front and as long as the accumulated time is greater than or
equal to the
car of the remaining checkpoint list, that
car is popped
off the checkpoint list. Second, if the checkpoint list has been completely
emptied and a non-
:interval was supplied when tracking was most
recently initiated with the
:init option, then the checkpoint list is set
to contain a single element, namely the sum of the accumulated time with that
Finally, suppose the above criteria are met, so that
:print? results in
printing of a message. We describe below the message,
msg, that is
printed. Here is how it is printed (see fmt), where
seconds-as-decimal-string is a string denoting the number of seconds of
accumulated time for the tag, with two digits after the decimal point.
(fms "TIME-TRACKER-NOTE [~x0]: ~@1~|" (list (cons #0 tag) (cons #1 msg) (cons #t seconds-as-decimal-string)) (proofs-co state) state nil)The value of
msgis the value of the
:msgkeyword supplied with
:print?, if non-
nil; else, the value of
:msgsupplied when most recently initialization with the
:initoption, if non-
nil; and otherwise, the string
"~st s"(the final ``s'' abbreviating the word ``seconds''). It is convenient to supply
:msgas a call
(msg str arg-0 arg-1 ... arg-k), where
stris a string and each
arg-iis the value to be associated with
#\iupon formatted printing (as with
fmt) of the string