/usr/share/acl2-6.3/books/parallel/fibonacci.lisp is in acl2-books-source 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 | (in-package "ACL2")
; Here we fool the dependency tracker (thus removing a dependency from
; Makefile).
#||
(include-book "matrix-multiplication-parallel")
||#
(include-book "misc/assert" :dir :system)
(set-compile-fns t)
; Serial version of Fibonacci
(defun fib (x)
(declare (xargs :guard (natp x)))
(cond ((mbe :logic (or (zp x) (<= x 0))
:exec (<= x 0))
0)
((= x 1) 1)
(t (let ((a (fib (- x 1)))
(b (fib (- x 2))))
(+ a b)))))
; Parallelized version of Fibonacci, using plet
(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 (> x 30)))
((a (pfib (- x 1)))
(b (pfib (- x 2))))
(+ a b)))))
(assert! (equal (fib 32) (pfib 32)))
; Parallel version of Fibonacci, using pargs
(defun pfib-with-pargs (x)
(declare (xargs :guard (natp x)))
(cond ((mbe :logic (or (zp x) (<= x 0))
:exec (<= x 0))
0)
((= x 1) 1)
(t (pargs (declare (granularity (> x 30)))
(binary-+ (pfib-with-pargs (- x 1))
(pfib-with-pargs (- x 2)))))))
(assert! (equal (fib 32) (pfib-with-pargs 32)))
(defmacro assert-when-parallel (form)
`(assert! (if (and (f-boundp-global 'parallel-evaluation-enabled state)
(f-get-global 'parallel-evaluation-enabled state))
,form
t)))
; About 2.3 seconds on an 8-core Linux machine running
; OpenMCL Version 1.1-r7635:
(assert-when-parallel (equal (time$ (fib 39)) 63245986))
; About 0.7 seconds on an 8-core Linux machine running
; OpenMCL Version 1.1-r7635:
(assert-when-parallel (equal (time$ (pfib 39)) 63245986))
; About 0.8 seconds on an 8-core Linux machine running
; OpenMCL Version 1.1-r7635:
(assert-when-parallel (equal (time$ (pfib-with-pargs 39)) 63245986))
|