TIME$

Major Section:  ACL2-BUILT-INS

Semantically, (time$ x ...) equals x. However, its evaluation may write timing output to the trace output (which is usually the terminal), as explained further below.

Examples:

; Basic examples:

(time$ (foo 3 4))
(time$ (mini-proveall))
(defun bar (x) (time$ (f x)))

; Custom examples, which use a custom timing message rather than a built-in
; message from Lisp:

; Report only if real time is at least 1/2 second (two equivalent forms).
(time$ (foo) :mintime 1/2)
(time$ (foo) :real-mintime 1/2)

; Report only if allocation is at least 1000 bytes (and if the Lisp supports
; :minalloc).
(time$ (foo) :minalloc 1000)

; Report only if real time is at least 1/2 second and (if the Lisp supports
; :minalloc) allocation is at least 931 bytes.
(time$ (foo) :real-mintime 1/2 :minalloc 931)

; Print "Hello Moon, Goodbye World" instead of any timing data.
(time$ (foo)
       :msg "Hello ~s0, ~s1 World."
       :args (list "Moon" "Goodbye"))

; Print default custom timing message (same as omitting :mintime 0):
(time$ (foo)
       :mintime 0)

; Print supplied custom timing message.
(let ((bar ...))
  (time$ (foo)
         :msg "The execution of ~xf took ~st seconds of real ~
               time and ~sc seconds of run time (cpu time), and ~
               allocated ~sa bytes.  In an unrelated note, bar ~
               currently has the value ~x0.~%"
         :args (list bar)))

General Forms:
(time$ form)
(time$ form ; arguments below are optional
       :real-mintime  <rational number of seconds>
       :run-mintime   <rational number of seconds>
       :minalloc      <number of bytes>
       :msg           <fmt string>
       :args          <list of arguments for msg>
       )
; Note: :real-mintime can be replaced by :mintime

The simplest form is (time$ x), which will call the time utility in the underlying Lisp, and will print a small default message. If you want to see a message printed by the host Lisp, use (time$ x :mintime nil) instead, which may provide detailed, implementation-specific data such as the amounts of time spent in user and system mode, the gc time, the number of page faults encountered, and so on. Of you can create a custom message, configured using the :msg and :args parameters. Time$ can also be made to report timing information only conditionally: the :real-mintime (or equivalently, :mintime), :run-mintime, and :minalloc arguments can be used to avoid reporting timing information for computations that take a small amount of time (perhaps as might be expected in ordinary cases), but to draw the user's attention to computations that take longer or allocate more memory than expected.

We next document the keyword arguments in some detail.

Keyword arguments :real-mintime (or :mintime) and :run-mintime can be used to specify a minimum time threshold for time reporting. That is, no timing information will be printed if the execution of form takes less than the specified number of seconds of real (total) time or run (cpu) time, respectively. Note that rational numbers like 1/2 may be used to specify a fractional amount of seconds. It is an error to specify both :real-mintime and its synonym, :mintime.

Keyword argument :minalloc is not supported on all Lisps. When it is not supported, it is ignored. But on supported Lisps, :minalloc can be used to specify a minimum memory allocation threshold. If form results in fewer than this many bytes being allocated, then no timing information will be reported.

Keyword argument :msg, when provided, should be a string accepted by the fmt family of functions (see fmt), and it may refer to the elements of :args by their positions, just as for cw (see cw).

The following directives allow you to report timing information using the :msg string. The examples at the top of this documentation topic illustrate the use of these directives.

~xf -- the form that was executed

~sa -- the amount of memory allocated, in bytes (in supported Lisps)

~st -- the real time taken, in seconds

~sc -- the run time (cpu time) taken, in seconds

We turn now to an example that illustrates how time$ can be called in function bodies. Consider the following definition of the Fibonacci function, followed by the definition of a function that times k calls of this function.

(defun fib (n)
  (if (zp n)
      1
    (if (= n 1)
        1
      (+ (fib (- n 1))
         (fib (- n 2))))))

(defun time-fib (k)
  (if (zp k)
      nil
    (prog2$
     (time$ (fib k)
            :mintime 1/2
            :msg "(fib ~x0) took ~st seconds, ~sa bytes allocated.~%"
            :args (list k))
     (time-fib (1- k)))))

ACL2 !>(time-fib 36)
(fib 36) took 3.19 seconds, 1280 bytes allocated.
(fib 35) took 1.97 seconds, 1280 bytes allocated.
(fib 34) took 1.21 seconds, 1280 bytes allocated.
(fib 33) took 0.75 seconds, 1280 bytes allocated.
NIL
ACL2 !>

Notes:

(1) Common Lisp specifies that the time utility prints to ``trace output'', and time$ follows this convention. Thus, if you have opened a trace file (see open-trace-file), then you can expect to find the time$ output there.

(2) Unless the :msg argument is supplied, an explicit call of time$ in the top-level loop will show that the form being timed is a call of the ACL2 evaluator function ev-rec. This is normal; the curious are invited, at their own risk, to see return-last for an explanation.