		Search-engine friendly clone of the ACL2 documentation.

Time$

Time the evaluation of a given form

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

Note: Some of the functionality below is available only for certain host Common Lisp implementations.

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

where form is processed as usual except that the host Common Lisp times its evaluation.

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

The following apply only when the host Lisp is GCL. The two system times will likely be nil unless the GCL version is 2.6.10 or later. Note the upper-case characters for child times.

~sC — the child run time (cpu time) taken, in seconds

~ss — the system time taken, in seconds

~sS — the child system 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)))))

The following log shows a sample execution of the function defined just above.

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.

Subtopics

Time-tracker: Display time spent during specified evaluation
Oracle-time: Carry out a computation, returning (not just printing!) how long it took and (on supported Lisps) how many bytes were allocated.
Profile-all: profile essentially all functions
Profile-ACL2: profile essentially all ACL2 functions