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)
|
