Time-tracker
Display time spent during specified evaluation
The time-tracker macro is a utility for displaying 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
time-tracker.
Note that by default, the time being tracked is runtime (cpu time); to
switch to realtime (elapsed time), see get-internal-time.
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.
The 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 approximately 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.~|~%")
...)
The first time-tracker call (above) ends any existing time-tracking
for tag :tau. One might have expected it to 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).
The second time-tracker call (above) initiates time-tracking for the
tag, :tau. Moreover, it specifies the effect of the :print?
keyword. 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-clausep is 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 :init form above says
that a message should be printed after 1 second, after 2 seconds, ..., and
after 5 seconds. Thereafter, the specification of :interval 5 in the
:init form 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 :msg keyword 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 :msg string above is what is printed using formatted printing (see
fmt), where the character #\t is 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, :msg can
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-tracker above 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
tag :tau at the end of a proof. The ACL2 function print-summary
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-time says that we are to ignore the :times and
:interval established by the :init call 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 #\t is 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
times, unless that default is changed; see get-internal-time.
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, :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 t or
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
t nor nil.
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 and :start! cause the tag to be
in an active state, while :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
:times, :interval, and :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 to
specify :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 first.)
:End specifies that if the tag is being tracked, then it should stop
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.
:Start! has the same effect as :start, except that it does not
cause an error when the tag is already active. In effect, :start! first
invokes :stop if the tag is already active, and then invokes
start.
:Stop specifies that the tag is to stop being active. It is an error
to specify :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
supplied with :print? as well as those supplied with the :init
option 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 supplied with :print?: :min-time must be a rational
number or nil, and :msg must be either a string, a true-list whose
car is a string, or 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.
When :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 car of
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-nil :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
value of :interval.
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 msg is the value of the :msg keyword supplied with
:print?, if non-nil; else, the value of :msg supplied when most
recently initialization with the :init option, if non-nil; and
otherwise, the string "~st s" (the final ``s'' abbreviating the word
``seconds''). It is convenient to supply :msg as a call (msg str
arg-0 arg-1 ... arg-k), where str is a string and each arg-i is
the value to be associated with #\i upon formatted printing (as with
fmt) of the string str.
