Major Section: PARALLEL-PROGRAMMING
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.)
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 !>
