;;;;;;;;;;;;;;;; Tests for presentation on 5/4/05 ;;;;;;;;;;;;;
;;; Jared wrote this script
(include-book "finite-set-theory/osets/sets" :dir :system)
(defun integers (n acc)
(if (zp n)
(reverse acc)
(integers (1- n) (cons n acc))))
(comp 'integers)
;;; For the sets library
;;; Non parallel version
(defun mergesort-exec (x)
(cond ((endp x) nil)
((endp (cdr x)) (insert (car x) nil))
(t (mv-let (part1 part2)
(split-list x)
(union (mergesort-exec part1) (mergesort-exec part2))))))
;;; Parallel version
(defun mergesort-exec (x)
(declare (xargs :guard (true-listp x)))
(cond ((endp x) nil)
((endp (cdr x)) (insert (car x) nil))
(t (mv-let (part1 part2)
(split-list x)
(ACL2::parallelize (union (mergesort-exec part1) (mergesort-exec part2)))))))
;;; Both of these admit, certify, and produce the result expected in Open MCL
;;; up to an integer list of length 50,000 or so. Around this number, Open MCL
;;; bombs as it runs out of stack space.
;;; Timings gathered from ACL2 prompt with below command. With different
;;; numbers, this command runs in both environments. The ACL2 limit is around
;;; 20,000 integers while raw Lisp can handle around 50,000. I did the timings
;;; in raw lisp to get a more accurate reading. These tests were conducted in a
;;; primative terminal to minimize the timing of filling a buffer.
(prog2 (setf *int-list* (integers 100000 nil)) t)
(prog2 (setf *res* (SETS::mergesort-exec *int-list*)) t)
;;; With serial versino of osets: Approximately 1.0 second for 4 runs
;;; With parallel version of osets:
;;; How frustrating to have such a great example and only be able to measure
;;; for 1.5 seconds, because we ran out of stack space!
;;; Experiencing very odd behavior - I would suspect synchronization bugs,
;;; except only one process is ever parallelized at once - see note in code
;;; works non-deterministically
(SETS::mergesort-exec (integers 100 nil))
;;; seems to be correct
(1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 ... 99 100)
(SETS::mergesort-exec (integers 1000 nil))
;;; missing 12, 20, etc
(1 2 3 4 5 6 7 8 9 10 11 13 14 15 16 17 18 19 21 22 23 24 ... 998 999 1000)
;;; missing 1, 5, etc
(2 3 4 6 7 8 10 12 14 16 18 19 20 22 24 26 28 30 32 34 35 36 ... 998 999 1000)
;;;; Timing Results for BAD Comparison
;;; Remember that the parallel case currently DROPS elements, reducing the workload
(prog2 (setf *int-list* (integers 50000 nil)) t)
(time (prog2 (setf *res* (SETS::mergesort-exec *int-list*)) t))
;;; Serial mergesort-exec case: 0.792, 0.686, 0.707, 0.687, 0.724
;;; Parallel mergesort-exec case 50,000: 0.291, 0.302, 0.403, 0.439, 0.536
;;; Parallel mergesort-exec case 100,000: 0.623, 1.143, .560, 1.356, 1.078, 1.427
;;; The parallel 50,000 case dropped 60% of the elements.... What will the
;;; times look like once they're not dropped? What will the times look like
;;; if we can get a larger sample size (> elements 50,000)