/usr/share/acl2-6.3/books/parallel/matrix-multiplication-setup.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 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 | (in-package "ACL2")
; This book is shared between our serial and parallel versions of matrix
; multiplication.
(set-compile-fns t)
(defun transpose-fast-aux (matrix)
(if (endp matrix)
(mv nil nil)
(let ((element-to-append (caar matrix))
(new-row (cdar matrix)))
(mv-let (acc new-row-list)
(transpose-fast-aux (cdr matrix))
(mv (cons element-to-append acc)
(cons new-row new-row-list))))))
(defun transpose-fast (matrix)
(if (endp (car matrix))
nil
(mv-let (new-row remaining-matrix)
(transpose-fast-aux matrix)
(cons new-row
(transpose-fast remaining-matrix)))))
(defun dot-product (rowA colB acc)
(if (endp rowA)
acc
(dot-product (cdr rowA)
(cdr colB)
(+ (* (car rowA) (car colB))
acc))))
(defun multiply-matrices-row (rowA B-left)
(if (endp B-left)
nil
(cons (dot-product rowA (car B-left) 0)
(multiply-matrices-row rowA (cdr B-left)))))
;;;;;; Matrix creation functions ;;;;;;;;;
(defun make-matrix-aux (rows cols curr-row curr-col row-acc big-acc 64bit-flag)
(declare (xargs :mode :program))
(cond ((equal curr-row rows)
big-acc)
((equal curr-col cols)
(make-matrix-aux rows cols (1+ curr-row) 0 nil
(cons row-acc big-acc)
64bit-flag))
(t
(make-matrix-aux rows cols curr-row (1+ curr-col)
(cons (mod (+ (* curr-row curr-col)
(* 23 curr-row curr-row)
(* 3 curr-col curr-col))
(if 64bit-flag 3000 300))
row-acc)
big-acc 64bit-flag))))
(defun make-matrix (rows cols 64bit-flag)
(declare (xargs :mode :program))
(make-matrix-aux rows cols 0 0 nil nil 64bit-flag))
(defun identity-matrix-aux (i zerow a)
(cond ((zp i) a)
(t (identity-matrix-aux (- i 1)
zerow
(cons (update-nth (- i 1) 1 zerow) a)))))
(defun identity-matrix (n)
(identity-matrix-aux n
(make-list n :initial-element 0)
nil))
; For testing:
(defmacro assert-when-parallel (form)
`(assert! (if (and (f-boundp-global 'parallel-evaluation-enabled state)
(f-get-global 'parallel-evaluation-enabled state))
,form
t)))
(defconst *a-rows* 1024)
(defconst *a-cols* 1024)
(defconst *b-rows* 1024)
(defconst *b-cols* 1024)
|