		Search-engine friendly clone of the ACL2 documentation.

Time$

Oracle-time

Carry out a computation, returning (not just printing!) how long it took and (on supported Lisps) how many bytes were allocated.

The oracle-time macro allows you to run a form and get the elapsed time and memory allocation back as real ACL2 values.

In most cases, you don't really need to do this. Instead, see time$, which is built into ACL2 and allows you to print the runtime and allocation of a form as a logically invisible side-effect. Since time$ doesn't return the elapsed time or allocation, it is simpler and doesn't need access to state. It also has some nice features for controlling when timing information is printed.

On the other hand, if you want to do things like collect up tables that describe how your functions perform on various inputs, then time$ won't do what you want: it just prints the timing information to the terminal, leaving you with no way to collect and compare the times and allocations. In this case, oracle-time may be able to do what you want. The main limitation is that it does need access to the state.

Basic Example

(oracle-time (fib 35))   ; Simple since it returns a single value
  -->
(mv time                 ; Rational, number of seconds
    bytes                ; Natural, bytes allocated
    ans                  ; Answer from (fib 35)
    state)               ; Updated state

Example with Multiple Return Values

(oracle-time (random$ 100 state)  ; Returns multiple values
   :ret (mv ans state))           ; Explains the return type
  -->
(mv time                          ; Rational, number of seconds
    bytes                         ; Natural, bytes allocated
    ans                           ; The random number produced
    state)                        ; Updated state

See also the community book tools/oracle-time-tests.lisp for some additional tests and working examples.

General Form

(oracle-time form [:ret retspec])

The form can be any arbitrary ACL2 form that you want to execute. If the form returns an ordinary, single value, e.g., as in (fib 35) then the :ret argument is not needed. Otherwise, :ret should explain the return signature of form.

The return value of oracle-time extends the return value of form with multiple values. The basic idea is that oracle-time is going to macroexpand to something like this:

(mv-let retspec
   form
   (b* (((mv & time state) (read-acl2-oracle state))
        ((mv & bytes state) (read-acl2-oracle state)))
     (mv time bytes retspec [state])))

You can see here that the retspec is used to explain how to bind the results of executing the form. It is also, essentially, spliced into the return value of the whole oracle-time call. The only twist is that if retspec mentions state, then we don't add an extra state onto the end of the form.

Subtopics

Oracle-timelimit: Carry out some computation, returning (not just printing!) how long it took and (on supported Lisps) how many bytes were allocated, but aborting the execution if it takes too long.