Read-run-time
Read elapsed runtime
By default, (read-run-time state) returns (mv cpu-time
state), where cpu-time is the elapsed cpu time in seconds since the
start of the current ACL2 session and state is the resulting ACL2 state. Thus, (read-run-time state) is, by default, equivalent to
(get-cpu-time state). But read-run-time can be made to return
elapsed real time (wall clock time) instead, thus making it equivalent to
(get-real-time state). Note that time is returned in seconds in all of
these cases.
To specify that read-run-time shall use cpu time or real time:
(assign get-internal-time-as-realtime t) ; use real time
(assign get-internal-time-as-realtime nil) ; use cpu time
See get-internal-time for more discussion of cpu time vs. real time.
In both cases, the precision depends on the host Common Lisp; for example, in
CCL as of this writing, the result is accurate to the microsecond.
The logical definition probably won't concern many users, but for
completeness, we say a word about it here. That definition uses the function
read-ACL2-oracle, which modifies state by popping the value to
return from its acl2-oracle field.
Function: read-run-time
(defun read-run-time (state-state)
(declare (xargs :guard (state-p1 state-state)))
(mv (cond ((or (null (acl2-oracle state-state))
(not (rationalp (car (acl2-oracle state-state)))))
0)
(t (car (acl2-oracle state-state))))
(update-acl2-oracle (cdr (acl2-oracle state-state))
state-state)))
Note that logically (read-run-time state), (get-real-time state),
and (get-cpu-time state) are all equal (defined using the acl2-oracle),
so for example ACL2 succeeds in the proof of (thm (equal (get-real-time
state) (get-cpu-time state))), even though the first returns elapsed real
time and the second returns elapsed cpu time. However, there is no
contradiction: either way, we are logically just reading the oracle of
state. In the ACL2 loop, successive calls of (get-real-time state)
and (get-cpu-time state) would be operating on different values of
state (because their oracles differ).
Subtopics
- Get-real-time
- Read elapsed real time
- Get-cpu-time
- Read elapsed cpu time
