DEFLOCK

define a wrapper macro that provides mutual exclusion in ACL2(p)
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 !>