Deflock
Define a wrapper macro that provides mutual exclusion in ACL2(p)
This documentation topic relates to the experimental
extension of ACL2 supporting parallel evaluation and proof; see parallelism.
Example Form:
(deflock *my-lock*)
General Form:
(deflock *symbol*)
where *symbol* is a symbol whose first and last characters are both
the character #\*.
A call of this macro generates a definition of another macro, named
with-<modified-lock-symbol>, where <modified-lock-symbol> is the
given symbol with the leading and trailing * characters removed. This
newly defined macro will guarantee mutually exclusive execution when called in
the body of the raw Lisp definition of a function, as is typically the case
for guard-verified functions, for :program mode functions,
and for calls of macro top-level. (See guard-evaluation-table
for details of how raw Lisp code might not be invoked when guard-checking (see
set-guard-checking) has value :none or :all.) Note that this
macro is also simply the identity when invoked directly in the top-level loop;
see top-level for a way to avoid this issue, and see parallelism-at-the-top-level for a general discussion of this issue for calls
of parallelism primitives.
To see how mutual exclusion is guaranteed, consider the raw Lisp code
generated for the macro, with-<modified-lock-symbol>, that is introduced
by a call of deflock. This code uses a lock (with the given
*symbol* as its name), which guarantees that for any two forms that are
each in the scope of a call of with-<modified-lock-symbol>, the forms do
not execute concurrently.
Note that a call of deflock expands into the application of progn
to two events, as illustrated below.
ACL2 !>:trans1 (deflock *my-cw-lock*)
(PROGN (TABLE LOCK-TABLE '*MY-CW-LOCK* T)
(DEFMACRO WITH-MY-CW-LOCK (&REST ARGS)
(LIST* 'WITH-LOCK '*MY-CW-LOCK* ARGS)))
ACL2 !>
Thus, deflock forms are legal embedded event forms (see embedded-event-form) for books as well as encapsulate and
progn events.
The following log shows a lock in action. Recall that locks work as
expected in guard-verified and :program mode functions;
they do not, however, work in :logic mode functions that have not
been guard-verified, as illustrated below.
ACL2 !>(deflock *my-cw-lock*)
[[.. output omitted ..]]
WITH-MY-CW-LOCK
ACL2 !>(defun foo (n)
(declare (xargs :guard (natp n) :verify-guards nil))
(plet ((x1 (with-my-cw-lock (cw "~x0" (make-list n))))
(x2 (with-my-cw-lock (cw "~x0" (make-list n)))))
(and (null x1) (null x2))))
[[.. output omitted ..]]
FOO
ACL2 !>(foo 20)
(NIL NIL NIL NIL( NIL NIL NIL NIL NIL NILNIL NIL NILNIL NIL NILNIL
NIL NILNIL NIL NIL NILNIL NIL NIL
NIL NILNIL NIL NILNIL )
NIL NIL NIL NIL NIL NIL NIL NIL)
T
ACL2 !>(verify-guards foo)
[[.. output omitted ..]]
FOO
ACL2 !>(foo 20)
(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)
(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)
T
ACL2 !>
