TIME-TRACKER

display time spent during specified evaluation 
Major Section:  PROGRAMMING

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 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, :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 causes the tag to be in an active state, whie :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 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 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.