|
|
|---|
|
|
|
|---|
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
(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