		Search-engine friendly clone of the ACL2 documentation.

Get-internal-time

Runtime vs. realtime in ACL2 timings

The ACL2 system provides utilities that deal with elapsed time. The most visible of these is in the time summaries printed when completing evaluation of events. For others, see with-prover-time-limit, see read-run-time, see time-tracker, see time-tracker-tau, and see pstack.

By default, these utilities all use an underlying notion of run time provided by the host Common Lisp implementation: specifically, the Common Lisp function get-internal-run-time. However, Common Lisp also provides the function get-internal-real-time, which returns the real time (wall clock time). While the latter is specified to measure elapsed time, the former is left to the implementation, which might well only measure time spent in the Lisp process. Consider the following example, which is a bit arcane but basically sleeps for 2 seconds.

(defttag t) ; to allow sys-call
(make-event
 (prog2$ (sys-call "sleep" '("2"))
         (value '(value-triple nil))))

A typical time summary might be as follows, drastically under-reporting the elapsed time.

Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

However, you can instruct ACL2 to switch to using elapsed time (real time), in summaries and elsewhere, by evaluating the following form.

(assign get-internal-time-as-realtime t)

To return to using runtime:

(assign get-internal-time-as-realtime nil)

While the above example is rather silly, the issue becomes significant in time summaries for proofs that call out to external tools (see sys-call and see clause-processor).

Note that a function get-internal-time is defined in raw Lisp but is not available inside the ACL2 loop. However, the expression (read-run-time state) provides an interface to this function that is available inside the ACL2 loop; see read-run-time.

We are open to changing the default to elapsed wall-clock time (realtime), and may do so in future ACL2 releases.

Implementation note (GCL only): If the host Lisp is Gnu Common Lisp, then get-internal-run-time has a multiple value return, and the first two values (runtime and child runtime) are added together to produce a result for get-internal-time.