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.
The oracle-timelimit macro is similar to oracle-time
except that besides reporting times, it also allows you impose a limit on how
long the form is allowed to run for and how much memory it is allowed to use.
If execution takes too long or allocates too much memory, execution is
aborted.
Warning. This book is intended to be a practically useful tool, but
it may not be entirely sound. In particular:
- In case of a timeout, execution will (of course) not complete normally. If
the computation you are timing includes, for instance, updates to stobjs
or the state, then the stobjs may have been only partially updated.
This might especially pose a soundness problem for abstract stobjs since the stobj invariant might be ruined
if a sequence of writes is interrupted.
- The internal, core, intermediate part of the computation makes use of a
return-last style macro that will not return the right results when the
computation is timed out. The top-level oracle-timelimit macro accounts
for this, but in principle a malicious user could directly call the internal
macro to easily cause unsoundness.
Basic Example
(oracle-timelimit 1/3 ; Fail if more than 1/3 second is needed
(fib 35)) ; What to execute
-->
(mv successp ; Did the computation complete in time?
seconds ; Time taken (rational number of seconds)
bytes ; Bytes allocated (natural)
ans ; Answer on success, or NIL on timeout
state) ; Adjusted with changes to oracle
Example with Multiple Return Values
(oracle-timelimit 5 ; Fail if more than 5 seconds are needed
(random$ 100 state) ; What to execute
:ret (mv ans state) ; Return signature of the form to execute
:onfail (mv :oops state) ; Alternate values to return on timeout
)
-->
(mv successp ; Did the computation complete in time?
seconds ; Time taken (rational number of seconds)
bytes ; Bytes allocated (natural)
ans ; Answer on success, or :oops on timeout
state) ; Adjusted with changes to the oracle
See also the community book tools/oracle-timelimit-tests.lisp for some
additional tests and working examples.
General Form
(oracle-timelimit
timelimit ; rational valued time limit
form ; what to execute
[:ret retspec] ; return signature for form
[:onfail failspec] ; return values for timeout case
[:maxmem bytes] ; maximum memory allocation to allow (CCL Only)
;; Special option to catch Lisp errors that arise during form
[:suppress-lisp-errors bool]
)
The timelimit should evaluate to a rational number which is interpreted
as some number of seconds.
The form can be any arbitrary ACL2 form that you want to execute. If
this form returns an ordinary, single value, e.g., as in (fib 35), then
the :ret form is not needed. Otherwise, :ret should explain the
return signature of form, as in oracle-time.
(CCL Only) If provided, the :maxmem should specify a memory ceiling in
bytes; the default is nil, in which case no memory ceiling is imposed.
This is a very rough mechanism and its implementation may change in the future.
The memory usage is checked only occasionally (i.e., once per second or
similar). Note that we check the global memory usage of the entire ACL2
process, with no regard to which thread has allocated the memory or how much
memory was allocated before the computation began.
The return value of oracle-timelimit extends the return value of
form with multiple values. The basic idea is that oracle-timelimit
is going to macroexpand to something like the following:
(mv-let retspec
form
(b* (((mv & successp state) (read-acl2-oracle state))
((mv & time state) (read-acl2-oracle state))
((mv & bytes state) (read-acl2-oracle state))
;; Fix time/bytes to sensible values
(time (if (and (rationalp time) (<= 0 time)) time 0))
(bytes (nfix bytes))
((unless successp)
;; execution timed out
(mv nil time bytes failspec [state])))
;; Else, execution succeeded
(mv t 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 values for the success and failure cases. The only twist is that if
retspec mentions state, then we don't add an extra state onto
the end of the form.
By default, if form causes a raw Lisp error such as a type error, stack
overflow, or causes some other non-local exit such as throwing to a tag, the
error will propagate through the oracle-timelimit call. However, if you
set :suppress-lisp-errors t, then any such error will be treated as a
timeout. This may have any number of unsound consequences!
