← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/system/hons-check/memoize-tests.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/system/hons-check/memoize-tests.lisp
1
1
; Memoize Sanity Checking
2
 
; Copyright (C) 2011 Centaur Technology
 
2
; Copyright (C) 2011-2014 Centaur Technology
3
3
;
4
4
; Contact:
5
5
;   Centaur Technology Formal Verification Group
27
27
;   DEALINGS IN THE SOFTWARE.
28
28
;
29
29
; Original author: Jared Davis <jared@centtech.com>
 
30
;
 
31
; Modified 8/2014 by Matt Kaufmann to make functions tail recursive, to avoid
 
32
; errors in LispWorks and Allegro CL (at least).
30
33
 
31
34
(in-package "ACL2")
32
35
(include-book "misc/assert" :dir :system)
33
36
(include-book "std/lists/flatten" :dir :system)
 
37
(include-book "tools/bstar" :dir :system)
34
38
 
35
39
; cert_param: (hons-only)
36
40
 
42
46
  (declare (xargs :guard t))
43
47
  x)
44
48
 
 
49
(defun f1-list-tailrec (x acc)
 
50
  (declare (xargs :guard (true-listp acc)))
 
51
  (if (atom x)
 
52
      (reverse acc)
 
53
    (f1-list-tailrec (cdr x)
 
54
                     (cons (f1 (car x)) acc))))
 
55
 
45
56
(defun f1-list (x)
46
57
  (declare (xargs :guard t))
47
 
  (if (atom x)
48
 
      nil
49
 
    (cons (f1 (car x))
50
 
          (f1-list (cdr x)))))
 
58
  (f1-list-tailrec x nil))
51
59
 
52
60
 
53
61
(defun f2 (x)
54
62
  (declare (xargs :guard t))
55
63
  (cons x x))
56
64
 
 
65
(defun f2-list-tailrec (x acc)
 
66
  (declare (xargs :guard (true-listp acc)))
 
67
  (if (atom x)
 
68
      (reverse acc)
 
69
    (f2-list-tailrec (cdr x)
 
70
                     (cons (f2 (car x)) acc))))
 
71
 
57
72
(defun f2-list (x)
58
73
  (declare (xargs :guard t))
59
 
  (if (atom x)
60
 
      nil
61
 
    (cons (f2 (car x))
62
 
          (f2-list (cdr x)))))
 
74
  (f2-list-tailrec x nil))
63
75
 
64
76
 
65
77
(defun f3 (x)
66
78
  (declare (xargs :guard t))
67
 
  (mv x (cons x x)))
 
79
  (mv x (cons 1 x)))
 
80
 
 
81
(defun f3-list-tailrec (x acc)
 
82
  (declare (xargs :guard (true-listp acc)))
 
83
  (if (atom x)
 
84
      (reverse acc)
 
85
    (mv-let (a b)
 
86
            (f3 (car x))
 
87
            (f3-list-tailrec (cdr x)
 
88
                             (list* b a acc)))))
 
89
 
68
90
 
69
91
(defun f3-list (x)
70
92
  (declare (xargs :guard t))
71
 
  (if (atom x)
72
 
      nil
73
 
    (mv-let (a b) (f3 (car x))
74
 
      (list* a b (f3-list (cdr x))))))
 
93
  (f3-list-tailrec x nil))
75
94
 
76
95
 
77
96
(defun f4 (x y)
78
97
  (declare (xargs :guard t))
79
 
  (cons x y))
 
98
  (cons 1/2 (cons x y)))
 
99
 
 
100
(defun f4-list-tailrec (x acc)
 
101
  (declare (xargs :guard (true-listp acc)))
 
102
  (if (atom x)
 
103
      (reverse acc)
 
104
    (if (atom (cdr x))
 
105
        (reverse acc)
 
106
      (f4-list-tailrec (cdr x)
 
107
                       (cons (f4 (first x) (second x))
 
108
                             acc)))))
80
109
 
81
110
(defun f4-list (x)
82
111
  (declare (xargs :guard t))
83
 
  (if (atom x)
84
 
      nil
85
 
    (if (atom (cdr x))
86
 
        nil
87
 
      (cons (f4 (first x) (second x))
88
 
            (f4-list (cdr x))))))
 
112
  (f4-list-tailrec x nil))
89
113
 
90
114
 
91
115
(defun f5 (x y)
92
116
  (declare (xargs :guard t))
93
117
  (mv x y))
94
118
 
 
119
(defun f5-list-tailrec (x acc)
 
120
  (declare (xargs :guard (true-listp acc)))
 
121
  (if (atom x)
 
122
      (reverse acc)
 
123
    (if (atom (cdr x))
 
124
        (reverse acc)
 
125
      (mv-let (a b)
 
126
              (f5 (first x) (second x))
 
127
              (f5-list-tailrec (cdr x)
 
128
                               (list* b a acc))))))
 
129
 
95
130
(defun f5-list (x)
96
131
  (declare (xargs :guard t))
97
 
  (if (atom x)
98
 
      nil
99
 
    (if (atom (cdr x))
100
 
        nil
101
 
      (mv-let (a b) (f5 (first x) (second x))
102
 
        (list* a b (f5-list (cdr x)))))))
103
 
 
 
132
  (f5-list-tailrec x nil))
104
133
 
105
134
 
106
135
(defun f6 (x y z)
107
136
  (declare (xargs :guard t))
108
137
  (list x y z))
109
138
 
 
139
(defun f6-list-tailrec (x acc)
 
140
  (declare (xargs :guard (true-listp acc)))
 
141
  (if (atom x)
 
142
      (reverse acc)
 
143
    (if (atom (cdr x))
 
144
        (reverse acc)
 
145
      (if (atom (cddr x))
 
146
          (reverse acc)
 
147
        (f6-list-tailrec (cdr x)
 
148
                         (cons (f6 (first x) (second x) (third x))
 
149
                               acc))))))
 
150
 
110
151
(defun f6-list (x)
111
152
  (declare (xargs :guard t))
112
 
  (if (atom x)
113
 
      nil
114
 
    (if (atom (cdr x))
115
 
        nil
116
 
      (if (atom (cddr x))
117
 
          nil
118
 
        (cons (f6 (first x) (second x) (third x))
119
 
              (f6-list (cdr x)))))))
120
 
 
 
153
  (f6-list-tailrec x nil))
121
154
 
122
155
 
123
156
(defconst *stuff*
147
180
                   (hons-copy (make-list 1000 :initial-element *stuff*)))))
148
181
 
149
182
 
150
 
; Matt K., 7/31/2014: Commenting out the remainder of this file until after the
151
 
; ACL2 Version 6.5 release, because both Allegro CL and LispWorks hang on the
152
 
; next form.  Probably it will be simple to solve this by making f1-list
153
 
; etc. be tail-recursive.
154
 
#||
155
 
 
156
183
(defconst *f1-test* (f1-list *data*))
157
184
(defconst *f2-test* (f2-list *data*))
158
185
(defconst *f3-test* (f3-list *data*))
206
233
(unmemoize 'f5)
207
234
(unmemoize 'f6)
208
235
 
209
 
||#
 
236
 
 
237
;; (defun show-me-default-hons-space (from)
 
238
;;   (declare (xargs :guard t)
 
239
;;            (ignorable from))
 
240
;;   (er hard? 'show-me-default-hons-space
 
241
;;       "Raw lisp definition not installed"))
 
242
;; (defttag :show-me-default-hons-space)
 
243
;; (progn!
 
244
;;  (set-raw-mode t)
 
245
;;  (defun show-me-default-hons-space (from)
 
246
;;    (format t "~S: Default-hs is ~S~%"
 
247
;;            from
 
248
;;            (funcall (intern "%ADDRESS-OF" "CCL") *default-hs*))
 
249
;;    nil))
 
250
 
 
251
(defun test-simultaneously-acons ()
 
252
; We may need to verify guards to execute the raw Lisp (parallelized) version
 
253
; of pand.
 
254
  (declare (xargs :verify-guards t))
 
255
  (pand (progn$
 
256
         ;; (show-me-default-hons-space 'thread-1-pre)
 
257
         ;; (hons-summary)
 
258
         (hons-acons 1 2 nil)
 
259
         ;; (show-me-default-hons-space 'thread-1-post)
 
260
         ;; (hons-summary)
 
261
         t)
 
262
        (progn$
 
263
         ;; (show-me-default-hons-space 'thread-2-pre)
 
264
         ;; (hons-summary)
 
265
         (hons-acons 2 3 nil)
 
266
         ;; (show-me-default-hons-space 'thread-2-post)
 
267
         ;; (hons-summary)
 
268
         t)))
 
269
 
 
270
(assert! (test-simultaneously-acons))
 
271
 
 
272
(defun test-simultaneously-acons-with-spec-mv-let ()
 
273
; We must verify guards to execute the raw Lisp (parallelized) version of
 
274
; spec-mv-let.
 
275
  (declare (xargs :verify-guards t))
 
276
  (spec-mv-let (x)
 
277
    (hons-acons 1 2 nil)
 
278
    (mv-let (y z)
 
279
      (mv (hons-acons 3 4 nil)
 
280
          6)
 
281
      (if t
 
282
          (+ (caar x) (cdar x) (caar y) (cdar y) z)
 
283
        (+ (caar y) (cadr y) z)))))
 
284
 
 
285
(assert! (test-simultaneously-acons-with-spec-mv-let))
 
286
 
 
287
(defun test-simultaneously-hons ()
 
288
; We may need to verify guards to execute the raw Lisp (parallelized) version
 
289
; of pand.
 
290
  (declare (xargs :verify-guards t))
 
291
  (pand (hons 1 2)
 
292
        (hons 3 4)))
 
293
 
 
294
(assert! (test-simultaneously-hons))
 
295
 
 
296
(defun test-simultaneously-hons-with-spec-mv-let ()
 
297
; We must verify guards to execute the raw Lisp (parallelized) version of
 
298
; spec-mv-let.
 
299
  (declare (xargs :verify-guards t))
 
300
  (spec-mv-let (x)
 
301
    (hons 7 8)
 
302
    (mv-let (y z)
 
303
      (mv (hons 9 10) 11)
 
304
      (if t
 
305
          (+ (car x) (cdr x) (car y) (cdr y) z)
 
306
        (+ (car y) (cdr y) z)))))
 
307
 
 
308
(assert! (test-simultaneously-hons-with-spec-mv-let))
 
309
 
 
310
 
 
311
 
 
312
(defun make-memoized-alist (x)
 
313
  (declare (xargs :guard t))
 
314
  (make-fast-alist (cons (cons 'x x)
 
315
                         '(("a" . 1)
 
316
                           (b . 2)
 
317
                           (c . 3)))))
 
318
 
 
319
(memoize 'make-memoized-alist)
 
320
 
 
321
(defun do-stuff-to-fast-alist (n alist)
 
322
  (declare (xargs :guard (natp n)))
 
323
  (b* (((when (zp n))
 
324
        alist)
 
325
       (?a (hons-get 'a alist))
 
326
       (?b (hons-get 'b alist))
 
327
       (?c (hons-get 'c alist))
 
328
       (alist (hons-acons n n alist)))
 
329
    (do-stuff-to-fast-alist (- n 1) alist)))
 
330
 
 
331
(comp t)
 
332
 
 
333
(defconst *spec* (do-stuff-to-fast-alist 1000 (make-memoized-alist 5)))
 
334
 
 
335
(defun check-both-with-pand (n)
 
336
  (declare (xargs :guard (natp n)))
 
337
  (pand (equal (do-stuff-to-fast-alist n (make-fast-alist (make-memoized-alist 5))) *spec*)
 
338
        (equal (do-stuff-to-fast-alist n (make-fast-alist (make-memoized-alist 5))) *spec*)))
 
339
 
 
340
(assert! (check-both-with-pand 1000))
 
341
 
 
342
 
 
343
 
 
344
 
 
345
;; Basic check to try to see if threads will interfere with one another
 
346
 
 
347
(defun add-some-honses (x acc)
 
348
  (declare (xargs :guard t))
 
349
  (if (atom x)
 
350
      acc
 
351
    (add-some-honses (cdr x)
 
352
                     (list* (hons-copy (car x))
 
353
                            (hons (car x) (car x))
 
354
                            acc))))
 
355
(defun thread1 (x)
 
356
  (declare (xargs :guard t))
 
357
  (let ((x (add-some-honses x x)))
 
358
    (list (f1-list x)
 
359
          (f2-list x)
 
360
          (f3-list x)
 
361
          (f4-list x)
 
362
          (f5-list x)
 
363
          (f6-list x))))
 
364
 
 
365
(defun thread2 (x)
 
366
  (declare (xargs :guard t))
 
367
  (let ((x (add-some-honses x x)))
 
368
    (list (f2-list x)
 
369
          (f4-list x)
 
370
          (f6-list x)
 
371
          (f1-list x)
 
372
          (f3-list x)
 
373
          (f5-list x))))
 
374
 
 
375
(comp t) ;; so gcl will compile add-some-honses instead of stack overflowing
 
376
 
 
377
(defconst *thread1-spec* (thread1 *data*))
 
378
(defconst *thread2-spec* (thread2 *data*))
 
379
 
 
380
(defun check-thread1 (n)
 
381
  (declare (xargs :guard (natp n)))
 
382
  (if (zp n)
 
383
      t
 
384
    (and (equal *thread1-spec* (thread1 *data*))
 
385
         (check-thread1 (- n 1)))))
 
386
 
 
387
(defun check-thread2 (n)
 
388
  (declare (xargs :guard (natp n)))
 
389
  (if (zp n)
 
390
      t
 
391
    (and (equal *thread2-spec* (thread2 *data*))
 
392
         (check-thread2 (- n 1)))))
 
393
 
 
394
(defun check-both (n)
 
395
  (declare (xargs :guard (natp n)))
 
396
  (pand (check-thread1 n)
 
397
        (check-thread2 n)))
 
398
 
 
399
;; Timings on compute-1-1:
 
400
;;  - ACL2(hp): no memoization: 12.33 seconds (many GC messages)
 
401
;;  - ACL2(h):  no memoization: 15.54 seconds (many GC messages)
 
402
 
 
403
(assert! (time$ (check-both 100)))
 
404
 
 
405
(value-triple (clear-memoize-tables))
 
406
 
 
407
(memoize 'f1)
 
408
(memoize 'f2 :condition '(not (equal x -1/3)))
 
409
(memoize 'f3)
 
410
(memoize 'f4 :condition '(not (equal x -1/3)))
 
411
(memoize 'f5)
 
412
(memoize 'f6 :condition '(not (equal x -1/3)))
 
413
 
 
414
;; Timings on compute-1-1:
 
415
;;  - ACL2(hp): memoization, lock contention:     242 seconds (many gc messages)
 
416
;;  - ACL2(h):  memoization, no lock contention:   61 seconds (many gc messages)
 
417
(assert! (time$ (check-both 100)))
 
418
 
 
419
 
 
420