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