		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. These are most visibly used in reporting the time summaries when completing evaluation of events. For utilities that return elapsed cpu or run time, see read-run-time, get-cpu-time, and get-real-time. Other time-related utilities include with-prover-time-limit, time-tracker, time-tracker-tau, 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 functions get-internal-run-time for cpu time and get-internal-real-time for real (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 actual elapsed (real, wall clock) 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, and also see get-cpu-time and get-real-time.