WITH-OUTPUT-LOCK

Major Section:  PARALLEL-PROGRAMMING

This documentation topic relates to an experimental extension of ACL2, ACL2(p), created initially by David L. Rager. See compiling-acl2p for how to build an executable image that supports parallel execution. Also see community books directory books/parallel/ for examples.

One may wish to perform output while executing code in parallel. If threads are allowed to print concurrently, the output will be interleaved and often unreadable. To avoid this, the user can surround forms that perform output with the with-output-lock macro.

Take the following definition of pfib as an example.

(defun pfib (x)
  (declare (xargs :guard (natp x)))
  (cond ((mbe :logic (or (zp x) (<= x 0))
              :exec (<= x 0))
         0)
        ((= x 1) 1)
        (t (plet (declare (granularity t))
                 ((a (prog2$ (cw "Computing pfib ~x0~%" (- x 1))
                             (pfib (- x 1))))
                  (b (prog2$ (cw "Computing pfib ~x0~%" (- x 2))
                             (pfib (- x 2)))))
                 (+ a b)))))

With parallel-execution enabled, a call of (pfib 5)results in non-deterministically interleaved output, for example as follows.

ACL2 !>(pfib 5)
CComputing pfib 4
omputing pfib 3
ComCpuotmipnugt ipnfgi bp fib3
2
Computing pCfiobm put2i
ng pfib 1
Computing pfib Co1mp
uting pfib 0
CCoommppuuttiinngg  ppffiibb  12

ComCpuotmipnugt ipnfgi bp fib1 
0
CoCmopmuptuitnign gp fpifbi b 1
0
5
ACL2 !>

If the user instead surrounds the calls to cw with the macro with-output-lock, as in the following session, the output will no longer be interleaved.

ACL2 !>
(defun pfib (x)
  (declare (xargs :guard (natp x)))
  (cond ((mbe :logic (or (zp x) (<= x 0))
              :exec (<= x 0))
         0)
        ((= x 1) 1)
        (t (plet (declare (granularity t))
                 ((a (prog2$ (with-output-lock
                              (cw "Computing pfib ~x0~%" (- x 1)))
                             (pfib (- x 1))))
                  (b (prog2$ (with-output-lock
                              (cw "Computing pfib ~x0~%" (- x 2)))
                             (pfib (- x 2)))))
                 (+ a b)))))

<snip>

ACL2 !>(pfib 5)
Computing pfib 4
Computing pfib 3
Computing pfib 3
Computing pfib 2
Computing pfib 2
Computing pfib 1
Computing pfib 2
Computing pfib 1
Computing pfib 1
Computing pfib 0
Computing pfib 1
Computing pfib 0
Computing pfib 1
Computing pfib 0
5
ACL2 !>