diff options
Diffstat (limited to 'books/workshops/2000/lusk-mccune/lusk-mccune-final')
20 files changed, 5044 insertions, 0 deletions
diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/README b/books/workshops/2000/lusk-mccune/lusk-mccune-final/README new file mode 100644 index 0000000..49a036e --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/README @@ -0,0 +1,56 @@ +ACL2 for Parallel Systems Software + +This directory contains version sim19 of our multiprocess +simulator. It is described in a short paper (paper.ps). + +This represents the early stages of a work in progress. +The simulator doesn't have all the functions we write +about in the paper, it is not well debugged, and it is +slow. The guard proofs are very slow. But it's s start :-) + +Bill McCune mccune@mcs.anl.gov +Rusty Lusk lusk@mcs.anl.gov + +September 1, 2000 + +====================================================== + +Paper: + +paper.tex +paper.ps + +====================================================== + +Books: + +util some utilities +gensym-e generate new symbols +base basic types such as hostname, process-id, file descriptor +expr expressions for the programming language +pstate process state +cstate connection state +lstate listening state +mstate multiprocess state +stepproc0 step functions for for exec, fork, rsh +stepproc1 step functions for send, receive, select, and ordinary stmts +setup support for stepproc2 +stepproc2 step functions for setup-listener, accept, connect +stepprocess bring together all step functions +compile preprocessor for our programs +simulator the simulator + +====================================================== + +Example Multiprocess Programs: + +trace pass a message around a ring +fence a barrier operation + +====================================================== + +Bill McCune mccune@mcs.anl.gov +Rusty Lusk lusk@mcs.anl.gov + +September 1, 2000 + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/base.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/base.lisp new file mode 100644 index 0000000..82e52a1 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/base.lisp @@ -0,0 +1,74 @@ +(in-package "ACL2") + +(include-book "util") + +;;---------------------------------------- +;; +;; mstate: (pstates cstates lstates) ;; multiprocess state +;; pstate: (hpid code cc xstack memory) ;; process state +;; cstate: (connection transitq inboxq) ;; connection state +;; connection: (hpid1 fd1 hpid2 fd2) +;; lstate: ((hpid fd) port requestq) ;; listening state +;; +;;---------------------------------------- + +;; Simple recognizers used by both pstate and cstate + +(defun hostp (x) ;; host name -- symbolp + (declare (xargs :guard t)) + (and (symbolp x) + (not (null x)))) + +(defun pidp (x) ;; process ID -- pos-integer + (declare (xargs :guard t)) + (pos-integerp x)) + +(defun hpidp (x) ;; host/process ID -- (hostp pidp) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 2) + (hostp (first x)) + (pidp (second x)))) + +(defun fdp (x) ;; file descriptor -- natural + (declare (xargs :guard t)) + (naturalp x)) + +(defun fd-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + ((not (fdp (car x))) nil) + (t (fd-listp (cdr x))))) + +(defun portp (x) ;; port name -- pos-integer + (declare (xargs :guard t)) + (pos-integerp x)) + +(defun hpid-fdp (x) ;; hpid-fdp -- (hpidp fpd) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 2) + (hpidp (first x)) + (fdp (second x)))) + +(in-theory (disable hostp pidp hpidp fdp portp hpid-fdp)) + +;; These are for our programming language. + +(defun varp (x) ;; variable -- symbolp + (declare (xargs :guard t)) + (and (symbolp x) + (not (null x)))) + +(defun constp (x) ;; constant -- (quote symbolp) + (declare (xargs :guard t)) + (and (equal (len x) 2) + (equal (first x) 'quote) + (symbolp (second x)) + (not (null (second x))) + (null (cddr x)))) + +(in-theory (disable varp constp)) + + + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/compile.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/compile.lisp new file mode 100644 index 0000000..b3c3d6f --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/compile.lisp @@ -0,0 +1,222 @@ +(in-package "ACL2") + +(include-book "pstate") +(include-book "gensym-e") + +(mutual-recursion + + (defun progstmt (s) + (declare (xargs :guard t)) + (cond ((statementp s) t) + ((and (>= (len s) 3) + (equal (car s) 'if) + (expressionp (second s))) + (proglistelse (cddr s))) + + ((and (>= (len s) 3) + (equal (car s) 'while) + (expressionp (second s))) + (proglist (cddr s))) + (t nil))) + + (defun proglistelse (s) ;; list of progstmts with at most one 'else + (declare (xargs :guard t)) + (cond ((atom s) (null s)) + ((equal (car s) 'else) (proglist (cdr s))) + (t (and (progstmt (car s)) + (proglistelse (cdr s)))))) + + (defun proglist (s) ;; list of progstmts + (declare (xargs :guard t)) + (cond ((atom s) (null s)) + (t (and (progstmt (car s)) + (proglist (cdr s)))))) + ) + +(defun prog-i (flg s) + (declare (xargs :guard t)) + (cond ((equal flg 0) + (cond ((statementp s) 'leaf) + ((and (>= (len s) 3) + (equal (car s) 'if) + (expressionp (second s))) (prog-i 1 (cddr s))) + + ((and (>= (len s) 3) + (equal (car s) 'while) + (expressionp (second s))) (prog-i 2 (cddr s))) + (t 'leaf))) + ((equal flg 1) + (cond ((atom s) 'leaf) + ((equal (car s) 'else) (prog-i 2 (cdr s))) + (t (cons (prog-i 0 (car s)) + (prog-i 1 (cdr s)))))) + (t + (cond ((atom s) 'leaf) + (t (cons (prog-i 0 (car s)) + (prog-i 2 (cdr s)))))) + )) + +(mutual-recursion + + (defun labels-stmt (s) + (declare (xargs :guard (progstmt s) + :verify-guards nil)) + (cond ((statementp s) (if (equal (first s) 'label) + (list (second s)) + nil)) + ((and (>= (len s) 3) + (equal (car s) 'if) + (expressionp (second s))) (labels-list (cddr s))) + + ((and (>= (len s) 3) + (equal (car s) 'while) + (expressionp (second s))) (labels-list (cddr s))) + (t nil))) + + (defun labels-list (s) + (declare (xargs :guard (proglist s))) + (cond ((atom s) nil) + (t (append (labels-stmt (car s)) + (labels-list (cdr s)))))) + ) + +#| +;; To make this section doesn work, i think we'd have to either make +;; the mutual recursion of labels-stmt like that of progstmt, or +;; make a speical induction function for labels-stmt. + +(defthm labels-symbol-listp-flg + (if flg + (symbol-listp (labels-stmt s)) + (symbol-listp (labels-list s))) + :hints (("Goal" + :induct (prog-i flg s))) + :rule-classes nil) + +(defthm labels-stmt-symbol-listp + (symbol-listp (labels-stmt x)) + :hints (("Goal" + :by (:instance labels-symbol-listp-flg (flg t))))) + +(defthm labels-list-symbol-listp + (symbol-listp (labels-list x)) + :hints (("Goal" + :by (:instance labels-symbol-listp-flg (flg nil))))) + +(defthm symbol-list-is-true-list + (implies (symbol-listp x) + (true-listp x))) + +(verify-guards labels-stmt + :otf-flg t) + +|# + +(defun then-part (l) + (declare (xargs :guard (true-listp l))) + (cond ((atom l) nil) + ((equal (car l) 'else) nil) + (t (cons (car l) (then-part (cdr l)))))) + +(defun else-part (l) + (declare (xargs :guard (true-listp l))) + (cond ((atom l) nil) + ((equal (car l) 'else) (cdr l)) + (t (else-part (cdr l))))) + +(mutual-recursion + + (defun compile-stmt (s labs) ;; return a list of statements + (declare (xargs :guard (and (progstmt s) + (symbol-listp labs)) + :verify-guards nil)) + + (cond ((and (>= (len s) 3) + (equal (car s) 'if) + (expressionp (second s))) + + (let ((cond (second s)) + (then (then-part (cddr s))) + (else (else-part (cddr s))) + (else-label (gen-symbol 'else- labs)) + (endif-label (gen-symbol 'endif- labs))) + (let* ((then-seg (compile-list + then + (list* else-label endif-label labs))) + (then-labels (labels-list then-seg))) + + (append (list (list 'branch (list 'not cond) else-label)) + then-seg + (list (list 'goto endif-label)) + (list (list 'label else-label)) + (compile-list + else + (append (list* else-label endif-label labs) + then-labels)) + + (list (list 'label endif-label)))))) + + ((and (>= (len s) 3) + (equal (car s) 'while) + (expressionp (second s))) + + (let ((cond (second s)) + (body (cddr s)) + (start-label (gen-symbol 'startwhile- labs)) + (end-label (gen-symbol 'endwhile- labs))) + (append (list (list 'label start-label)) + (list (list 'branch (list 'not cond) end-label)) + (compile-list body (list* start-label end-label labs)) + (list (list 'goto start-label)) + (list (list 'label end-label))))) + (t (list s)))) + + (defun compile-list (c labs) + (declare (xargs :guard (and (proglist c) + (symbol-listp labs)))) + + (cond ((atom c) nil) + (t (let* ((cc (compile-stmt (car c) labs)) + (cclabs (labels-list cc))) + (append cc + (compile-list (cdr c) (append labs cclabs)))))))) + +;;------------------- + +;; A few things have been omitted. +;; To prove things about compile-stmt/list, I think we need a special +;; induction scheme, because of the label arguments. In particular, +;; 1. to verify guards, +;; 2. to prove that compiling a prog-list gives a statement-listp. + +;; (verify-guards compile-stmt +;; :otf-flg t) + +; for example, + +#| +(compile-list '( + (while p1 (return)) + ) + '(else-6 lkj-9)) + +(compile-list '( + (if c1 + (return) + (if c2 + (return) + (return) + else + (return)) + (return) + else + (return) + (return) + (return)) + (while p1 + (return) + (while c2 (return) (return)) + (return)) + ) + '(else-6 lkj-9)) +|# diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/cstate.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/cstate.lisp new file mode 100644 index 0000000..638e7b5 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/cstate.lisp @@ -0,0 +1,155 @@ +(in-package "ACL2") + +(include-book "expr") + +(defun evaluated-expression-listp (x) ;; move to expr + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + ((not (evaluated-expressionp (car x))) nil) + (t (evaluated-expression-listp (cdr x))))) + +;;---------------------------------------- +;; cstate -- connection state + +(defun connectionp (x) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 4) + (hpidp (first x)) ;; source process + (or (fdp (second x)) ;; source fd if open, nil if closed + (null (second x))) + (hpidp (third x)) ;; destination process + (fdp (fourth x)))) ;; destination fd + +(defun cstatep (x) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 3) + (connectionp (first x)) ;; connection + (evaluated-expression-listp (second x)) ;; transit queue + (evaluated-expression-listp (third x)))) ;; inbox queue + +(defmacro transitq (cs) +;; (declare (xargs :guard (cstatep cs))) + (list 'second cs)) + +(defmacro inboxq (cs) +;; (declare (xargs :guard (cstatep cs))) + (list 'third cs)) + +(defmacro update-transitq (cs tq) +;; (declare (xargs :guard (and (cstatep cs) +;; (evaluated-expression-listp tq)))) + (list 'update-ith cs 2 tq)) + +(defmacro update-inboxq (cs iq) +;; (declare (xargs :guard (and (cstatep cs) +;; (evaluated-expression-listp iq)))) + (list 'update-ith cs 3 iq)) + +;;---------------------------------------- +;; alist of cstates + +(defun cstate-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (cstatep (car x)) + (cstate-listp (cdr x)))))) + +(defthm cstate-list-is-alist + (implies (cstate-listp x) + (alistp x)) + :rule-classes :forward-chaining) + +(defthm cstate-listp-contains-cstates + (implies (and (cstate-listp css) + (assoc-equal conn css)) + (cstatep (assoc-equal conn css))) + :hints (("Goal" + :in-theory (disable cstatep)))) + +;;-------------------------------------- + +(defun message-to-transfer (cs) + (declare (xargs :guard (cstatep cs))) + (consp (transitq cs))) + +(in-theory (enable constp varp)) + +(defun transfer-message (cs) + + ;; Given a cstate with a nonempty transit queue, move the first + ;; message in the transit queue to the end of the inbox queue. + + (declare (xargs :guard (and (cstatep cs) + (message-to-transfer cs)))) + (update-inboxq + (update-transitq cs (cdr (transitq cs))) + (append (inboxq cs) (list (car (transitq cs)))))) + +;; For example, + +#| +(transfer-message '(((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2))) +|# + +(defthm transfer-message-preserves-cstatep + (implies (and (cstatep cs) + (message-to-transfer cs)) + (cstatep (transfer-message cs))) + :otf-flg t) + +(defun active-cstates (css) + ;; Return the number of cstates with messages in transit. + (declare (xargs :guard (cstate-listp css))) + (cond ((atom css) 0) + (t (+ (if (message-to-transfer (car css)) 1 0) + (active-cstates (cdr css)))))) + +(defun ith-active-cstate (n css) ;; This counts from 1. + (declare (xargs :guard (and (pos-integerp n) + (cstate-listp css)))) + (cond ((atom css) nil) + ((message-to-transfer (car css)) + (if (equal n 1) + (car css) + (ith-active-cstate (- n 1) (cdr css)))) + (t (ith-active-cstate n (cdr css))))) + +(defthm cstate-listp-update + (implies (and (cstate-listp css) + (cstatep cs)) + (cstate-listp (update-alist-member x cs css)))) + +(defthm ith-active-cstate-properties + (implies (and (cstate-listp css) + (integerp n) + (> n 0) + (<= n (active-cstates css))) + (and (cstatep (ith-active-cstate n css)) + (member-equal (ith-active-cstate n css) css) + (message-to-transfer (ith-active-cstate n css)) + (consp (cadr (ith-active-cstate n css))))) + :hints (("Goal" + :in-theory (disable cstatep)))) + +(defun make-cstate (conn tq iq) + (declare (xargs :guard (and (connectionp conn) + (evaluated-expression-listp tq) + (evaluated-expression-listp iq)))) + (list conn tq iq)) + +(defun update-cstate (connection cstate cstates) + (declare (xargs :guard (and (connectionp connection) + (cstatep cstate) + (cstate-listp cstates)))) + (update-alist-member connection cstate cstates)) + +(defthm cstate-properties + (implies (cstatep cs) + (and (connectionp (car cs)) + (evaluated-expression-listp (cadr cs)) + (evaluated-expression-listp (caddr cs))))) + +(in-theory (disable constp varp)) + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/expr.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/expr.lisp new file mode 100644 index 0000000..3a789d9 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/expr.lisp @@ -0,0 +1,305 @@ +(in-package "ACL2") + +(include-book "base") + +#| + Expressions: + varp ;; variable + constp ;; constant + integerp + arithmetic ;; +, - + boolean ;; 'true, 'false, and, or, not, =, <, >, <=, >= + list operations ;; append, member, etc. +|# + +(defun bfix (x) ;; If x is not our kind of boolean, make it so. + (declare (xargs :guard t)) + (if (equal x ''false) ''false ''true)) + +(in-theory (disable bfix)) + +(defun lfix (x) + (declare (xargs :guard t)) + (cond ((atom x) nil) + ((constp x) nil) + (t (cons (car x) (lfix (cdr x)))))) + +(defun expressionp (e) + (declare (xargs :guard t)) + (cond ((null e) t) + ((varp e) t) + ((constp e) t) + ((integerp e) t) + ((atom e) nil) + (t (and (expressionp (car e)) + (expressionp (cdr e)))))) + +(defun evaluated-expressionp (e) + (declare (xargs :guard t)) + (cond ((null e) t) + ((constp e) t) + ((integerp e) t) + ((varp e) nil) + ((atom e) nil) + ((equal (len e) 3) + (and (not (member-equal (car e) (list '+ '- '= '< '<= 'equal 'and 'or + 'member 'assoc 'append + 'cons 'ith))) + (evaluated-expressionp (car e)) + (evaluated-expressionp (cdr e)))) + + ((equal (len e) 2) + (and (not (member-equal (car e) (list 'not 'length 'car 'cdr))) + (evaluated-expressionp (car e)) + (evaluated-expressionp (cdr e)))) + + (t (and (evaluated-expressionp (car e)) + (evaluated-expressionp (cdr e)))))) + +(defthm varp-not-cons + (not (varp (cons x y))) + :hints (("Goal" + :in-theory (enable varp)))) + +;;(defthm constp-evaluated-expressionp +;; (implies (constp x) +;; (evaluated-expressionp x))) + +;;-------------------------- +;; variables and memory + +(defun memoryp (x) ;; + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (consp (car x)) + (varp (caar x)) + (evaluated-expressionp (cdar x)) + (memoryp (cdr x)))))) + +(defthm memory-is-alist + (implies (memoryp mem) + (alistp mem)) + :rule-classes :forward-chaining) + +(defthm memory-access-gives-evaluated-expressionp + (implies (and (memoryp mem) + (assoc-equal e mem)) + (evaluated-expressionp (cdr (assoc-equal e mem))))) + +(defun val (var mem) ;; memory access + (declare (xargs :guard (and (varp var) + (memoryp mem)))) + (if (assoc-equal var mem) + (cdr (assoc-equal var mem)) + nil)) + +(in-theory (disable val)) + +(defun asgn (var val mem) + (declare (xargs :guard (and (varp var) + (evaluated-expressionp val) + (memoryp mem)))) + (cond ((atom mem) (list (cons var val))) + ((equal (caar mem) var) (cons (cons var val) (cdr mem))) + (t (cons (car mem) (asgn var val (cdr mem)))))) + +(defthm asgn-gives-memoryp + (implies (and (varp var) + (evaluated-expressionp e) + (memoryp mem)) + (memoryp (asgn var e mem)))) + +(defun myassoc (key lst) ;; + (declare (xargs :guard (true-listp lst))) + (cond ((atom lst) ''false) + ((atom (car lst)) (myassoc key (cdr lst))) + ((equal key (caar lst)) (car lst)) + (t (myassoc key (cdr lst))))) + +(defthm const-cons-expressionp + (implies (not (expressionp x)) + (not (constp (cons x y)))) + :hints (("Goal" + :in-theory (enable constp)))) + +(defthm const-list-expressionp + (implies (not (expressionp y)) + (not (constp (list* x y z)))) + :hints (("Goal" + :in-theory (enable constp varp)))) + +(defun evl2 (e mem) + (declare (xargs :guard (and (expressionp e) + (memoryp mem)))) + (cond + ((integerp e) e) + ((constp e) e) + ((varp e) (val e mem)) ;; undefined variables evaluate to nil; + ((atom e) nil) ;; junk atom evaluates to nil; + ((equal (len e) 3) + (case + (car e) + (+ (+ (rfix (evl2 (second e) mem)) (rfix (evl2 (third e) mem)))) + (- (- (rfix (evl2 (second e) mem)) (rfix (evl2 (third e) mem)))) + + (= (if (equal (rfix (evl2 (second e) mem)) (rfix (evl2 (third e) mem))) + ''true ''false)) + (< (if (< (rfix (evl2 (second e) mem)) (rfix (evl2 (third e) mem))) + ''true ''false)) + (<= (if (<= (rfix (evl2 (second e) mem)) (rfix (evl2 (third e) mem))) + ''true ''false)) + (equal (if (equal (evl2 (second e) mem) (evl2 (third e) mem)) + ''true ''false)) + (and (if (and (equal (bfix (evl2 (second e) mem)) ''true) + (equal (bfix (evl2 (third e) mem)) ''true)) + ''true ''false)) + (or (if (or (equal (bfix (evl2 (second e) mem)) ''true) + (equal (bfix (evl2 (third e) mem)) ''true)) + ''true ''false)) + + (member (if (member-equal (evl2 (second e) mem) + (lfix (evl2 (third e) mem))) + ''true + ''false)) + + (assoc (myassoc (evl2 (second e) mem) + (lfix (evl2 (third e) mem)))) + + (append (append (lfix (evl2 (second e) mem)) + (lfix (evl2 (third e) mem)))) + + (cons (cons (evl2 (second e) mem) + (evl2 (third e) mem))) + + (ith (ith (nfix (evl2 (second e) mem)) (lfix (evl2 (third e) mem)))) + + (otherwise (cons (evl2 (car e) mem) + (evl2 (cdr e) mem))))) + + ((equal (len e) 2) + (case + (car e) + (not (if (equal (bfix (evl2 (second e) mem)) ''false) + ''true ''false)) + (length (length (lfix (evl2 (second e) mem)))) + + (car (if (consp (lfix (evl2 (second e) mem))) + (car (evl2 (second e) mem)) + nil)) + + (cdr (if (consp (lfix (evl2 (second e) mem))) + (cdr (evl2 (second e) mem)) + nil)) + + (otherwise (cons (evl2 (car e) mem) + (evl2 (cdr e) mem))))) + + (t (cons (evl2 (car e) mem) + (evl2 (cdr e) mem))))) + +#| +(evl2 '(append ('a 'b 'c) (1 2 3)) nil) +(evl2 '(member 'b ('a 'b 'c)) nil) +(evl2 '(length (a b c)) nil) +(evl2 '(cons 2 (a b c)) nil) +(evl2 '(car ('a 'b 'c)) nil) +(evl2 '(cdr ('a 'b 'c)) nil) +(evl2 '(ith 2 (a b c)) '((a . 10) (b . 20) (c . 30))) +|# + +(defthm not-constp-cons-cons + (not (constp (cons (cons x y) z))) + :hints (("Goal" + :in-theory (enable constp)))) + +(defthm const-evaluated-myassoc + (implies (constp (cons lst1 lst2)) + (evaluated-expressionp (myassoc key lst2))) + :hints (("goal" + :in-theory (enable constp)))) + +(defthm myassoc-evaluated + (implies (and (evaluated-expressionp key) + (evaluated-expressionp lst)) + (evaluated-expressionp (myassoc key lst))) + :hints (("goal" + :induct (myassoc key lst)))) + +(defthm constp-not-rationalp + (implies (constp x) + (not (rationalp x))) + :hints (("goal" + :in-theory (enable constp)))) + +(defthm evaluated-expressionp-lfix + (implies (evaluated-expressionp lst) + (evaluated-expressionp (lfix lst)))) + +(defthm evaluated-append + (implies (and (evaluated-expressionp a) + (evaluated-expressionp b)) + (evaluated-expressionp (append (lfix a) b)))) + +(defthm evaluated-member + (implies (evaluated-expressionp lst) + (evaluated-expressionp (member-equal x (lfix lst))))) + +(defthm evaluated-ith + (implies (evaluated-expressionp lst) + (evaluated-expressionp (ith x (lfix lst)))) + :hints (("Goal" + :do-not generalize + :induct (ith x lst)))) + +(defthm car-const-expr + (implies (constp c) + (expressionp (car c))) + :hints (("Goal" + :in-theory (enable constp)))) + +(defthm cdr-const-expr + (implies (constp c) + (expressionp (cadr c))) + :hints (("Goal" + :in-theory (enable constp varp)))) + +(defthm integer-or-constp-not-varp + (implies (or (integerp x) + (constp x)) + (not (varp x))) + :hints (("Goal" + :in-theory (enable varp constp)))) + +(defthm sum-not-varp + (not (varp (+ x y))) + :hints (("Goal" + :in-theory (enable varp)))) + +(defthm expressionp-3 + (implies (and (expressionp e) + (equal (len e) 3)) + (and (expressionp (second e)) + (expressionp (third e)))) + :hints (("Goal" + :in-theory (enable constp)))) + +(defthm expressionp-2 + (implies (and (expressionp e) + (equal (len e) 2)) + (expressionp (second e))) + :hints (("Goal" + :in-theory (enable constp)))) + +(defthm evaluated-val + (implies (and (varp v) + (memoryp mem)) + (evaluated-expressionp (val v mem))) + :hints (("Goal" + :in-theory (enable varp val)))) + +(defthm evl2-expressionp + (implies (and (memoryp mem) + (expressionp e)) + (evaluated-expressionp (evl2 e mem)))) + +(in-theory (disable expressionp-2 expressionp-3)) diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/fence b/books/workshops/2000/lusk-mccune/lusk-mccune-final/fence new file mode 100644 index 0000000..6ab22ac --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/fence @@ -0,0 +1,688 @@ +(in-package "ACL2") + +(include-book "simulator") +(include-book "compile") + +(sim + + '( + (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (DELIVER . 7828) + + (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (DELIVER . 7828) + + (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (DELIVER . 7828) + ) + + 0;; step counter + + nil;; trace + + (list ; mstate = multiprocess state with connections + + ;; This program simulates a barrier algorithm implemented by the managers + ;; for the clients. (There are no daemons or consoles.) The three clients + ;; each must call the barrier (send fence-in message) before they can + ;; continue (receive fence-out message). All connections are + ;; pre-established in the initial mstate. + + + (list ; list of pstates, one for each process + + ;;------------------------------------------------------------- manager 0 + + ;; Each manager is connected to its neighbors in the ring and to a client + ;; process. The managers must collectively wait for all the clients to + ;; enter the barrier (send their managers fence-in messages) before they + ;; are allowed to leave (they wait for fence-out messages from their managers.) + + (list ; first manager pstate + + '(host1 1) ; process id for manager 0 + + (compile-list ; main manager program + '( + (asgn select-set (lhs-fd cli-fd)) + (while 'true + (select select-set selected-set) + (if (member lhs-fd selected-set) + (call lhs-handler) + ) + (if (member cli-fd selected-set) + (call cli-handler) + ) + ) + (return) ; end of main manager program + + + (procedure lhs-handler) ; lhs-handler + (receive lhs-fd lhs-message) + (asgn cmd (cdr (assoc 'cmd lhs-message))) + + (if (equal cmd 'man-fence-in) + (call man-fence-in-handler) + ) + (if (equal cmd 'man-fence-out) + (call man-fence-out-handler) + ) + (return) ; end of lhs-handler + + + (procedure cli-handler) ; client handler in manager + (receive cli-fd cli-message) + (asgn cmd (cdr (assoc 'cmd cli-message))) + (if (equal cmd 'cli-fence-in) + (call cli-fence-in-handler) + ) + (if (not (equal cmd 'cli-fence-in)) + (asgn status 'ERROR-unxpected-message-not-fence-in) + ) + (return) ; end of cli-handler + + + ; beginning of specific message handlers + + + (procedure cli-fence-in-handler) ; manager gets fence-in message from client + (asgn client-fenced-in 1) + (if (equal man-id 0) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + (if (not (equal man-id 0)) + (if (equal fence-in-msg-here 1) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + ) + (return) ; end of cli-fence-in handler + + (procedure man-fence-in-handler) ; manager gets fence-in message from lhs + (asgn fence-in-msg-here 1) + (if (equal man-id 0) + (send rhs-fd (('cmd . 'man-fence-out))) + ) + (if (not (equal man-id 0)) + (if (equal client-fenced-in 1) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + ) + (return) ; end of man-fence-in-handler + + (procedure man-fence-out-handler) ; manager gets fence out message from lhs + (send cli-fd (('cmd . 'cli-fence-out))) + (if (not (equal man-id 0)) + (send rhs-fd (('cmd . 'man-fence-out))) + ) + (return) ; end of man-fence-out-handler + + ) ; uncompiled program + nil + ) ; compiled program + 1 ; program counter + nil ; xstack + '((man-id . 0) ; initial memory + (fence-in-msg-here . 0) + (client-fenced-in . 0) + (lhs-fd . 3) + (rhs-fd . 4) + (mpd-fd . 5) + (cli-fd . 6) + ) + ) ; end of pstate + + ;;------------------------------------------------------------- manager 1 + + ;; Same as for manager 0 + + (list ; first manager pstate + + '(host2 1) ; process id for manager 0 + + (compile-list ; main manager program + '( + (asgn select-set (lhs-fd cli-fd)) + (while 'true + (select select-set selected-set) + (if (member lhs-fd selected-set) + (call lhs-handler) + ) + (if (member cli-fd selected-set) + (call cli-handler) + ) + ) + (return) ; end of main manager program + + + (procedure lhs-handler) ; lhs-handler + (receive lhs-fd lhs-message) + (asgn cmd (cdr (assoc 'cmd lhs-message))) + + (if (equal cmd 'man-fence-in) + (call man-fence-in-handler) + ) + (if (equal cmd 'man-fence-out) + (call man-fence-out-handler) + ) + (return) ; end of lhs-handler + + + (procedure cli-handler) ; client handler in manager + (receive cli-fd cli-message) + (asgn cmd (cdr (assoc 'cmd cli-message))) + (if (equal cmd 'cli-fence-in) + (call cli-fence-in-handler) + ) + (if (not (equal cmd 'cli-fence-in)) + (asgn status 'ERROR-unxpected-message-not-fence-in) + ) + (return) ; end of cli-handler + + + ; beginning of specific message handlers + + + (procedure cli-fence-in-handler) ; manager gets fence-in message from client + (asgn client-fenced-in 1) + (if (equal man-id 0) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + (if (not (equal man-id 0)) + (if (equal fence-in-msg-here 1) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + ) + (return) ; end of cli-fence-in handler + + (procedure man-fence-in-handler) ; manager gets fence-in message from lhs + (asgn fence-in-msg-here 1) + (if (equal man-id 0) + (send rhs-fd (('cmd . 'man-fence-out))) + ) + (if (not (equal man-id 0)) + (if (equal client-fenced-in 1) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + ) + (return) ; end of man-fence-in-handler + + (procedure man-fence-out-handler) ; manager gets fence out message from lhs + (send cli-fd (('cmd . 'cli-fence-out))) + (if (not (equal man-id 0)) + (send rhs-fd (('cmd . 'man-fence-out))) + ) + (return) ; end of man-fence-out-handler + + ) ; uncompiled program + nil + ) ; compiled program + 1 ; program counter + nil ; xstack + '((man-id . 1) ; initial memory + (fence-in-msg-here . 0) + (client-fenced-in . 0) + (lhs-fd . 3) + (rhs-fd . 4) + (mpd-fd . 5) + (cli-fd . 6) + ) + ) ; end of pstate + + ;;------------------------------------------------------------- manager 2 + + (list ; first manager pstate + + ;; same as for managers 0 and 1 + + '(host3 1) ; process id for manager 0 + + (compile-list ; main manager program + '( + (asgn select-set (lhs-fd cli-fd)) + (while 'true + (select select-set selected-set) + (if (member lhs-fd selected-set) + (call lhs-handler) + ) + (if (member cli-fd selected-set) + (call cli-handler) + ) + ) + (return) ; end of main manager program + + + (procedure lhs-handler) ; lhs-handler + (receive lhs-fd lhs-message) + (asgn cmd (cdr (assoc 'cmd lhs-message))) + + (if (equal cmd 'man-fence-in) + (call man-fence-in-handler) + ) + (if (equal cmd 'man-fence-out) + (call man-fence-out-handler) + ) + (return) ; end of lhs-handler + + + (procedure cli-handler) ; client handler in manager + (receive cli-fd cli-message) + (asgn cmd (cdr (assoc 'cmd cli-message))) + (if (equal cmd 'cli-fence-in) + (call cli-fence-in-handler) + ) + (if (not (equal cmd 'cli-fence-in)) + (asgn status 'ERROR-unxpected-message-not-fence-in) + ) + (return) ; end of cli-handler + + + ; beginning of specific message handlers + + + (procedure cli-fence-in-handler) ; manager gets fence-in message from client + (asgn client-fenced-in 1) + (if (equal man-id 0) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + (if (not (equal man-id 0)) + (if (equal fence-in-msg-here 1) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + ) + (return) ; end of cli-fence-in handler + + (procedure man-fence-in-handler) ; manager gets fence-in message from lhs + (asgn fence-in-msg-here 1) + (if (equal man-id 0) + (send rhs-fd (('cmd . 'man-fence-out))) + ) + (if (not (equal man-id 0)) + (if (equal client-fenced-in 1) + (send rhs-fd (('cmd . 'man-fence-in))) + ) + ) + (return) ; end of man-fence-in-handler + + (procedure man-fence-out-handler) ; manager gets fence out message from lhs + (send cli-fd (('cmd . 'cli-fence-out))) + (if (not (equal man-id 0)) + (send rhs-fd (('cmd . 'man-fence-out))) + ) + (return) ; end of man-fence-out-handler + + ) ; uncompiled program + nil + ) ; compiled program + 1 ; program counter + nil ; xstack + '((man-id . 2) ; initial memory + (fence-in-msg-here . 0) + (client-fenced-in . 0) + (lhs-fd . 3) + (rhs-fd . 4) + (mpd-fd . 5) + (cli-fd . 6) + ) + ) ; end of pstate + + ;;-------------------------------------------------------- client 0 + + ;; Each client sends its manager a fence-in message and waits for a + ;; fence-out message. + + (list ; client on first host + + '(host1 2) ; process id for first client + + (compile-list ; client doing fence + '( + (send man-fd (('cmd . 'cli-fence-in))) + (receive man-fd man-message) + (asgn cmd (cdr (assoc 'cmd man-message))) + (if (not (equal cmd 'cli-fence-out)) + (asgn status 'ERROR-unexpected-message-not-cli-fence-out) + ) + (return) ; end of client + + ) ; uncompiled program + nil + ) ; compiled program + 1 ; program counter + nil ; xstack + '((man-fd . 1)) ; initial memory + ) ; end of pstate + + ;;-------------------------------------------------------- client 1 + + ;; Same as for client 0 + + (list ; client on first host + + '(host2 2) ; process id for first client + + (compile-list ; client doing fence + '( + (send man-fd (('cmd . 'cli-fence-in))) + (receive man-fd man-message) + (asgn cmd (cdr (assoc 'cmd man-message))) + (if (not (equal cmd 'cli-fence-out)) + (asgn status 'ERROR-unexpected-message-not-cli-fence-out) + ) + (return) ; end of client + + ) ; uncompiled program + nil + ) ; compiled program + 1 ; program counter + nil ; xstack + '((man-fd . 1)) ; initial memory + ) ; end of pstate + + ;;-------------------------------------------------------- client 2 + + ;; Same as for clients 0 and 1 + + (list ; client on first host + + '(host3 2) ; process id for first client + + (compile-list ; client doing fence + '( + (send man-fd (('cmd . 'cli-fence-in))) + (receive man-fd man-message) + (asgn cmd (cdr (assoc 'cmd man-message))) + (if (not (equal cmd 'cli-fence-out)) + (asgn status 'ERROR-unexpected-message-not-cli-fence-out) + ) + (return) ; end of client + + ) ; uncompiled program + nil + ) ; compiled program + 1 ; program counter + nil ; xstack + '((man-fd . 1)) ; initial memory + ) ; end of pstate + + ;;------------------------------------------------------------ + + ) ; end of pstate list + + (list ; connection list + + ;; The managers are connected in a ring and each client is connected to one + ;; manager. + + '(((host1 1) 4 (host2 1) 3) nil nil) + '(((host2 1) 4 (host3 1) 3) nil nil) + '(((host3 1) 4 (host1 1) 3) nil nil) + + '(((host1 1) 6 (host1 2) 1) nil nil) + '(((host2 1) 6 (host2 2) 1) nil nil) + '(((host3 1) 6 (host3 2) 1) nil nil) + + '(((host2 1) 3 (host1 1) 4) nil nil) + '(((host3 1) 3 (host2 1) 4) nil nil) + '(((host1 1) 3 (host3 1) 4) nil nil) + + '(((host1 2) 1 (host1 1) 6) nil nil) + '(((host2 2) 1 (host2 1) 6) nil nil) + '(((host3 2) 1 (host3 1) 6) nil nil) + + ) ; end of connections + + (list ; list of sockets being listened on + + ) ; end of listening list + + nil ; program-list + + ) ; End of multiprocess-state + + ) diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/gensym-e.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/gensym-e.lisp new file mode 100644 index 0000000..4bd6b41 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/gensym-e.lisp @@ -0,0 +1,199 @@ +(in-package "ACL2") + +;; This file deals with generation of a new symbol. I assume that +;; there is a list of symbols whose names are "l...ld...d" where l=letter, +;; d=digit. The string of d's in the symbol name is called an index. +;; If there is something other than a digit to the right of the leftmost +;; digit in the symbol name, that character is ignored. For example, +;; index of v12x3 = 123. +;; +;; How this works: I used Matt Kaufmann's functions. He assumed that +;; we have a list of characters that represents an integer. His functions +;; generate the list of character that represent the successor of that +;; integer. +;; +;; Given a list of symbols, I compute the index that represents the +;; largest integer. Gen-sym produces a symbol whose index is a +;; successor to that integer. + +(defun next-int-char (char) + (declare (xargs :guard t)) + (case char + (#\1 (mv #\2 nil)) + (#\2 (mv #\3 nil)) + (#\3 (mv #\4 nil)) + (#\4 (mv #\5 nil)) + (#\5 (mv #\6 nil)) + (#\6 (mv #\7 nil)) + (#\7 (mv #\8 nil)) + (#\8 (mv #\9 nil)) + (#\9 (mv #\0 t)) + (otherwise ;; treat as #\0 + (mv #\1 nil)))) + +(defun next-int-char-list (chars) + (declare (xargs :guard t)) + (if (atom chars) + (mv nil t) + (mv-let (next-chars carryp1) + (next-int-char-list (cdr chars)) + (if carryp1 + (mv-let (c carryp2) + (next-int-char (car chars)) + (mv (cons c next-chars) carryp2)) + (mv (cons (car chars) next-chars) nil))))) + +(defun int-char-listp (chars) + (declare (xargs :guard t)) + (if (atom chars) + (null chars) + (and (member (car chars) + '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)) + (int-char-listp (cdr chars))))) + +(defthm next-char-list-gives-charlist + (implies (character-listp x) + (character-listp (car (next-int-char-list x))))) + +(defun charlist< (i1 i2) + (declare (xargs :guard (and (character-listp i1) (character-listp i2)))) + (cond ((atom i2) nil) + ((atom i1) t) + ((> (len i1) (len i2)) nil) + ((< (len i1) (len i2)) t) + (t (cond ((char< (car i1) (car i2)) t) + ((char> (car i1) (car i2)) nil) + (t (charlist< (cdr i1) (cdr i2))))))) + +(defun next-int-char-list-actual (chars) + (declare (xargs :guard t)) + (mv-let (next carryp) + (next-int-char-list chars) + (if carryp + (cons #\1 next) + next))) + +(defthm carry-char-list + (implies (character-listp x) + (character-listp (cons #\1 x)))) + +(defthm next-char-list-actual-gives-charlist + (implies (character-listp x) + (character-listp (next-int-char-list-actual x)))) + +(defthm carry-int-char-list + (implies (int-char-listp x) + (int-char-listp (cons #\1 x)))) + +(defthm next-char-list-len + (equal (len (car (next-int-char-list x))) + (len x))) + +(defthm next-char-list-actual-gives-greater-list + (implies (int-char-listp x) + (charlist< x (next-int-char-list-actual x))) + :otf-flg t) + +(defun index (l) + (declare (xargs :guard (character-listp l))) + (cond ((atom l) nil) + ((member (car l) '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)) + (cons (car l) (index (cdr l)))) + (t (index (cdr l))))) + +(defthm index-gives-int-char-list + (int-char-listp (index l))) + +(defthm index-gives-charlist + (character-listp (index l))) + +(defun charlist-max (i1 i2) + (declare (xargs :guard (and (character-listp i1) (character-listp i2)))) + (if (charlist< i1 i2) i2 i1)) + +(defun max-index (l) + (declare (xargs :guard (symbol-listp l))) + (if (atom l) + nil + (charlist-max (index (coerce (symbol-name (car l)) 'list)) + (max-index (cdr l))))) + +(local (defthm greater-index-symbol-not-in-list ;; does 3 inductions + (implies (and (symbolp sym) + (charlist< (max-index l) + (index (coerce (symbol-name sym) 'list)))) + (not (member-equal sym l))))) + +(defun gen-sym (sym l) + (declare (xargs :guard (and (symbolp sym) + (character-listp l)))) + (intern-in-package-of-symbol + (coerce (append (coerce (symbol-name sym) 'list) + (next-int-char-list-actual l)) 'string) + sym)) + +(defthm consp-index-append + (implies (and (character-listp x) + (character-listp y)) + (equal (index (append x y)) + (append (index x) (index y))))) + +(defthm charlist<-append + (implies (and (character-listp prefix) + (character-listp y) + (charlist< x y)) + (charlist< x (append prefix y))) + :hints (("Goal" + :do-not generalize + ;; When we went from ACL2-v2.3 to 2.4, we had to include the + ;; following expand hints. On the plus side, this reduced + ;; the number of inductions from 7 to 1. + :expand ((charlist< x (cons (car prefix) (append (cdr prefix) y))) + (charlist< x (append prefix2 y)) + ) + ))) + +(defthm intchar-list-next-index + (implies (int-char-listp l) + (equal (index (next-int-char-list-actual l)) + (next-int-char-list-actual l)))) + +(defthm max-index-lessthan-gensym-index + (implies (symbolp sym) + (charlist< + (max-index l) + (index (coerce (symbol-name (gen-sym sym (max-index l))) 'list)))) + :hints (("Goal" :do-not generalize + :in-theory (disable next-int-char-list-actual)))) + +;; top-level gensym: make a symbol (with a prefix sym) +;; that does not occur in the given list l + +(defun gen-symbol (sym l) + (declare (xargs :guard (and (symbolp sym) + (symbol-listp l)))) + (gen-sym sym (max-index l))) + +;; Main theorem, gen-symbol really makes a NEW symbol + +(defthm new-symbol-not-in-list + (implies (symbolp sym) + (not (member-equal (gen-symbol sym l) l))) + :hints (("Goal" :in-theory (disable gen-sym)))) + +(in-theory (disable gen-symbol)) + +;; a few examples +;; (gen-symbol 'v nil) ;; => v1 +;; (gen-symbol 'v2- '(x1 v23 y1 x10)) ;; => v2-24 +;; (gen-symbol 'v '(x12 v99)) ;; => v100 +;; (gen-symbol 'v2 '(x1x3 x10)) ;; => v214 + + + + + + + + + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/lstate.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/lstate.lisp new file mode 100644 index 0000000..0403895 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/lstate.lisp @@ -0,0 +1,154 @@ +(in-package "ACL2") + +(include-book "base") + +;;---------------------------------------- +;; lstate -- listening state +;; +;; ((hpid lfd) port requestq) +;; +;; This means that hpid is listening on lfd for connections +;; at the port. When a process p issues a "(connect hpid port)", +;; the pair (p fd) is added to the request queue. When the +;; listening process issues an (accept lfd), the first request is +;; removed from requestq, and a new connection is established. + +(defun request-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (hpid-fdp (car x)) + (request-listp (cdr x)))))) + +(defun lstatep (x) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 3) + (hpid-fdp (first x)) + (portp (second x)) + (request-listp (third x)))) + +(defmacro port (ls) +;; (declare (xargs :guard (lstatep ls))) + (list 'second ls)) + +(defmacro requestq (ls) +;; (declare (xargs :guard (lstatep ls))) + (list 'third ls)) + +(defmacro update-requestq (ls rq) +;; (declare (xargs :guard (and (lstatep ls) +;; (request-listp rq)))) + (list 'update-ith ls 3 rq)) + +(defun lstate-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (lstatep (car x)) + (lstate-listp (cdr x)))))) + +(defthm lstate-list-is-alist + (implies (lstate-listp x) + (alistp x)) + :rule-classes :forward-chaining) + +(defthm lstate-assoc + (implies (and (lstate-listp lss) + (assoc-equal x lss)) + (lstatep (assoc-equal x lss)))) + +;; first-request -- get the first pair (hpid fd) from the request +;; queue, or NIL if the queue is empty. + +(defun first-request (hpid lfd lss) + (declare (xargs :guard (and (hpidp hpid) + (fdp lfd) + (lstate-listp lss)))) + (let ((ls (assoc-equal (list hpid lfd) lss))) + (cond ((not ls) nil) + ((atom (third ls)) nil) + (t (car (third ls)))))) + +(defthm first-request-gets-hpid-fd + (implies (and (lstate-listp lss) + (consp (first-request hpid lfd lss))) + (and (hpidp (first (first-request hpid lfd lss))) + (fdp (second (first-request hpid lfd lss))))) + :hints (("Goal" + :in-theory (enable hpid-fdp)))) + +;; pop-request -- remove the first pair (hpid fd) from the request queue. + +(defun pop-request (hpid lfd lss) + (declare (xargs :guard (and (hpidp hpid) + (fdp lfd) + (lstate-listp lss)))) + (let ((ls (assoc-equal (list hpid lfd) lss))) + (cond ((not ls) lss) + ((not (consp (requestq ls))) lss) + (t (update-alist-member (list hpid lfd) + (update-requestq ls (cdr (requestq ls))) + lss))))) + +#| For example, +(pop-request '(lutra 320) + 14 + '((((gyro 440) 15) 8585 nil) + (((lutra 320) 14) 7483 (((cosmo 354) 16))) + (((donner 320) 17) 3535 (((fire 444) 18))))) +|# + +(defthm pop-request-preserves-lstate-listp + (implies (and (hpidp hpid) + (fdp lfd) + (lstate-listp lss)) + (lstate-listp (pop-request hpid lfd lss)))) + +(include-book "cstate") + +(defun new-connection (hpid1 fd1 hpid2 fd2 css) + (declare (xargs :guard (and (hpidp hpid1) + (fdp fd1) + (hpidp hpid2) + (fdp fd2) + (cstate-listp css)))) + + (list* (list (list hpid1 fd1 hpid2 fd2) nil nil) + (list (list hpid2 fd2 hpid1 fd1) nil nil) + css)) + +(defthm new-connection-preserves-cstate-listp + (implies (and (hpidp hpid1) + (fdp fd1) + (hpidp hpid2) + (fdp fd2) + (cstate-listp css)) + (cstate-listp (new-connection hpid1 fd1 hpid2 fd2 css)))) + +;;-------------------------------------------------------------------- + +(defun listening-pairs (lss) + (declare (xargs :guard (lstate-listp lss))) + (cond ((atom lss) nil) + (t (cons (caar lss) + (listening-pairs (cdr lss)))))) + +(defun connection-pairs (css) + (declare (xargs :guard (cstate-listp css))) + (cond ((atom css) nil) + (t (list* (list (first (caar css)) (second (caar css))) + (list (third (caar css)) (fourth (caar css))) + (connection-pairs (cdr css)))))) + +(in-theory (enable hpid-fdp)) + +(defun fds-in-use (hpid pairs) + (declare (xargs :guard (and (hpidp hpid) + (request-listp pairs)))) + (cond ((atom pairs) nil) + ((equal (first (car pairs)) hpid) + (cons (second (car pairs)) (fds-in-use hpid (cdr pairs)))) + (t (fds-in-use hpid (cdr pairs))))) + +(in-theory (disable hpid-fdp)) + + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/mstate.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/mstate.lisp new file mode 100644 index 0000000..4595205 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/mstate.lisp @@ -0,0 +1,240 @@ +(in-package "ACL2") + +(include-book "cstate") +(include-book "pstate") +(include-book "lstate") + +;; At this point we start associating cstates with pstates (because +;; processes alter connections). + +(defun something-to-receive (hpid fd css) + (declare (xargs :guard (and (hpidp hpid) + (fdp fd) + (cstate-listp css)))) + (cond ((atom css) nil) + ((and (equal hpid (third (first (car css)))) + (equal fd (fourth (first (car css)))) + (consp (inboxq (car css)))) t) + (t (something-to-receive hpid fd (cdr css))))) + +(defun message-to-select (hpid css) + (declare (xargs :guard (and (hpidp hpid) + (cstate-listp css)))) + (cond ((atom css) nil) + ((and (equal hpid (third (first (car css)))) + (consp (inboxq (car css)))) t) + (t (message-to-select hpid (cdr css))))) + +(in-theory (enable hpid-fdp)) + +(defun request-to-select (hpid lss) + (declare (xargs :guard (and (hpidp hpid) + (lstate-listp lss)))) + (cond ((atom lss) nil) + ((and (equal hpid (first (first (car lss)))) + (consp (requestq (car lss)))) t) + (t (request-to-select hpid (cdr lss))))) + +(in-theory (disable hpid-fdp)) + +(in-theory (enable statementp)) + +(defun pstate-status (ps css lss) + (declare (xargs :guard (and (pstatep ps) + (cstate-listp css) + (lstate-listp lss)))) + (let ((stmt (if (zp (cc ps)) nil (ith (cc ps) (code ps))))) + (cond ((atom stmt) 'idle) ;; cc 0 or out of range + ((equal (car stmt) 'receive) + (let ((fd (evl2 (second stmt) (memory ps)))) + (cond ((not (fdp fd)) 'active) ;; handle error elsewhere + (t (if (something-to-receive (car ps) fd css) + 'active 'waiting))))) + ((equal (car stmt) 'select) + (if (or (message-to-select (car ps) css) + (request-to-select (car ps) lss)) + 'active 'waiting)) + ;; We should also check here if the process is waiting for + ;; a connect or waiting for an accept. As it is, the + ;; simulator will attempt these, so it might spin. + (t 'active)))) + +(in-theory (disable statementp)) + +(defun waiting-pstates (pss css lss) + ;; Return the number of processes hanging in receive or select. + (declare (xargs :guard (and (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss)))) + (cond ((atom pss) 0) + (t (+ (if (equal (pstate-status (car pss) css lss) + 'waiting) 1 0) + (waiting-pstates (cdr pss) css lss))))) + +(defun active-pstates (pss css lss) + ;; Return the number of processes with something to do. + (declare (xargs :guard (and (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss)))) + (cond ((atom pss) 0) + (t (+ (if (equal (pstate-status (car pss) css lss) + 'active) 1 0) + (active-pstates (cdr pss) css lss))))) + +(defun ith-active-pstate (n pss css lss) ;; This counts from 1. + (declare (xargs :guard (and (pos-integerp n) + (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss)))) + (cond ((atom pss) nil) + ((equal (pstate-status (car pss) css lss) 'active) + (if (equal n 1) + (car pss) + (ith-active-pstate (- n 1) (cdr pss) css lss))) + (t (ith-active-pstate n (cdr pss) css lss)))) + +(defthm ith-active-pstate-properties + (implies (and (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss) + (integerp n) + (> n 0) + (<= n (active-pstates pss css lss))) + (and (pstatep (ith-active-pstate n pss css lss)) + (member-equal (ith-active-pstate n pss css lss) pss))) + :hints (("Goal" + :in-theory (disable pstatep)))) + +;;---------------------------------------- +;; prog: (program-name program-code) + +(defun progp (x) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 2) + (symbolp (first x)) + (codep (second x)))) + +(defun program-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (progp (car x)) + (program-listp (cdr x)))))) + +(defthm program-listp-is-alistp + (implies (program-listp pgms) + (alistp pgms)) + :rule-classes :forward-chaining) + +;;---------------------------------------- +;; mstate -- multiprocess state + +(defun mstatep (x) + (declare (xargs :guard t)) + (and (equal (len x) 4) + (pstate-listp (first x)) + (cstate-listp (second x)) + (lstate-listp (third x)) + (program-listp (fourth x)))) + +(defun pstates (ms) ;; get the list of pstates from an mstate + (declare (xargs :guard (mstatep ms))) + (first ms)) + +(defun cstates (ms) ;; get the list of cstates from an mstate + (declare (xargs :guard (mstatep ms))) + (second ms)) + +(defun lstates (ms) ;; get the list of lstates from an mstate + (declare (xargs :guard (mstatep ms))) + (third ms)) + +(defun programs (ms) ;; get the list of programs from an mstate + (declare (xargs :guard (mstatep ms))) + (fourth ms)) + +(defun update-pstates (ms pss) + (declare (xargs :guard (and (mstatep ms) + (pstate-listp pss)))) + (update-first ms pss)) + +(defun update-cstates (ms css) + (declare (xargs :guard (and (mstatep ms) + (cstate-listp css)))) + (update-second ms css)) + +(defun update-lstates (ms lss) + (declare (xargs :guard (and (mstatep ms) + (lstate-listp lss)))) + (update-third ms lss)) + + +#| +(mstatep '( + ( ;; pstates: + ((lutra 320) ((asgn z 6)) 13 nil ((x . 4) (y . 6))) + ((gyro 440) ((procedure handle)) 14 nil nil) + ) + + ( ;; cstates: + (((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2)) + ) + ( ;; lstates: + (((gyro 440) 15) 8585 nil) + (((lutra 320) 14) 7483 (((cosmo 354) 16))) + (((donner 320) 17) 3535 (((fire 444) 18))) + ) + nil ;; programs + )) +|# + +(defthm true-listp-append-list + (true-listp (append a (list x)))) + +(defthm evaluated-expression-append + (implies (and (evaluated-expression-listp a) + (evaluated-expressionp x)) + (evaluated-expression-listp (append a (list x))))) + +(defun deliver-message (ms cs) + (declare (xargs :guard (and (mstatep ms) + (cstatep cs) + (member-equal cs (cstates ms)) + (message-to-transfer cs)))) + (update-cstates + ms + (update-alist-member + (car cs) + (transfer-message cs) + (cstates ms)))) + +;; For example, + +#| +(deliver-message '(( + ((lutra 320) ((asgn z 6)) 13 nil ((x . 4) (y . 6))) + ((gyro 440) ((procedure handle)) 14 nil nil) + ) + ( + (((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2)) + ) + nil + ) + + '(((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2))) +|# + +(defthm mstatep-deliver-message + (implies (and (mstatep ms) + (cstatep cs)) + (mstatep (deliver-message ms cs)))) + +;;--------------- + +(defun make-mstate (pstates cstates lstates programs) + (declare (xargs :guard (and (pstate-listp pstates) + (cstate-listp cstates) + (lstate-listp lstates) + (program-listp programs) + ))) + (list pstates cstates lstates programs)) diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/paper.ps.gz b/books/workshops/2000/lusk-mccune/lusk-mccune-final/paper.ps.gz Binary files differnew file mode 100644 index 0000000..d780814 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/paper.ps.gz diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/paper.tex b/books/workshops/2000/lusk-mccune/lusk-mccune-final/paper.tex new file mode 100644 index 0000000..038f304 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/paper.tex @@ -0,0 +1,335 @@ +\documentclass{article} + +\newcommand{\link}[1]{\underline{\bfseries #1}} + +\usepackage{times} % Necessary because Acrobat can't handle fonts properly +\usepackage{epsf} + +% \setlength\textwidth{6.5in} +% \setlength\oddsidemargin{0in} +% \setlength\evensidemargin{0in} +% \setlength\marginparwidth{0.7in} + +\renewcommand{\floatpagefraction}{0.9} + +\begin{document} +\title{\bf ACL2 for Parallel Systems Software:\\A Progress Report\thanks{This +work was supported by the Mathematical, Information, and +Computational Sciences Division subprogram of the Office of +Advanced Scientific Computing Research, U.S.\ Department of Energy, +under Contract W-31-109-Eng-38.}} +\author{\emph{Ewing Lusk and William McCune}\\[0.2in] + Mathematics and Computer Science Division\\ + Argonne National Laboratory\\ + Argonne, IL 60439} +% \date{} +\maketitle +\thispagestyle{empty} + +\section{Introduction} +\label{sec:introduction} + +A significant development in high-performance computing has occurred in recent +years with the proliferation of ``Beowulf'' clusters~\cite{beowulf-95}. +Beowulf clusters are parallel computers assembled from commodity-priced +personal computers and networks. The explosive growth of the personal +computer marketplace, together with rapid technological advances in the +hardware sold there, has driven the price/performance ratio so low for Beowulf +clusters that they have become competitive with traditional tightly integrated +(and thus expensive) supercomputers. + +The current bottleneck is systems software. Small clusters are already +working well in a large variety of situations, as well as large systems +devoted to single applications. To truly compete with highly parallel +supercomputer systems, however, Beowulfs need scalable parallel libraries, +system management tools, job schedulers, process managers, and other systems +software to support a mix of users and applications on systems consisting of +hundreds of network-connected computers. Traditional systems software either is +not scalable or is tied to specific vendor systems. + +The Mathematics and Computer Science Division at Argonne National Laboratory +conducts research and prototype software development in parallel +systems software. The MPICH +implementation~\cite{gropp-lusk-doss-skjellum:mpich} of the MPI standard for +message passing is already widely used in the Beowulf community. A new +project is MPD (for Multi-Purpose Daemon), whose purpose is to explore issues +in scalable process management for parallel jobs on Beowulf clusters. Process +management includes process startup, job control, management of standard I/O +(especially for interactive jobs), security, reliable process shutdown, and +provision of some set of facilities for use by an application-level parallel +library (such as MPICH) to dynamically establish network connections among +processes. The MPD system as a whole consists of dynamically changing network +of processes. A diagram of one possible state of the system is shown in +Figure~\ref{fig:mpds-all}. Details may be found in ~\cite{mpd-short}. +\begin{figure}[htbp] + \centerline{ + \epsfxsize=5.0in + \epsfbox{newmpds.eps} + } + \caption{Daemons with console process, managers, and clients} + \label{fig:mpds-all} +\end{figure} + +The prototype implementation of MPD in C has not been easy. Informal +reasoning about dynamically changing parallel systems is difficult. +Compounding the problem is the fact that the software layer on which MPD is +built is a low-level-one: it is composed of C programs that make Unix system +calls to manage processes ({\tt fork}, {\tt exec} and its variants, {\tt + kill}, {\tt rsh}, etc.) to establish TCP connections ({\tt socket}, {\tt + bind}, {\tt listen}, {\tt accept}, {\tt connect}, etc.), and to communicate +({\tt read} and {\tt write} on sockets)~\cite{linux-man-pages}. + +We decided to bring higher-level tools to bear on the problem and to employ +ACL2~\cite{acl2-approach} in doing so. This paper describes our experiences +so far. + +\section{Goals of the Project} +\label{sec:goals} + +Our abstract goal was to explore the use of high-level tools in the +development of complex software. What attracted us to this particular project +was the fact that the system we wished to apply the tools to, the MPD +process manager, was +\begin{enumerate} +\item complex enough that ACL2-based technology might really hasten its + development and improve its robustness, +\item important enough in the context of Beowulf system software to be worth + an investment in tools, and yet +\item simple enough that we had hope of concrete success. The various MPD + processes themselves have relatively simple structures, in which handlers are + attached to various sockets and invoked when messages arrive to process the + messages. Although there are many types of messages and thus many handlers, + each one is relatively straightforward. +\end{enumerate} + +The core of the project is a simulator. We hoped that the exercise of +defining the relevant states of (Unix) processes and the state of a system of +such processes connected by communication channels with the characteristics of +Unix sockets would lead us to a simple data structure that would abstract the +significant aspects of the system, enabling us to effectively reason about it, +both informally and formally. The {\tt man} pages of the various Unix system +calls would be abstracted into the simple semantics of functions that update +this data structure. + +Our concrete goal was to improve the MPD system as its development +continued, by testing it in a way orthogonal to the traditional +testing procedures. We expect to modify its code to conform closely to the +version expressed in the language used by the simulator to express the +individual programs that the MPD processes execute. + +In the long run we hope to use this phase of the project as a step toward +proving theorems about MPD and similar systems, thus establishing a new level +of reliability for parallel systems software. + +\section{The Multiprocess Model} + +We are modeling a collection of Unix-style processes communicating via +TCP using Unix system calls. That is, our model is a slight, rather than an +extreme, abstraction of the C implementation. + +\subsection{The State of a Multiprocess Computation} + +A \emph{multiprocess-state} (or \emph{m-state}) is a 4-tuple: +\begin{quote} +(\emph{process-states\ \ connection-states\ \ listening-states\ \ program-list}). +\end{quote} +Each \emph{process-state} is a 5-tuple: +\begin{quote} +(\emph{process-id\ \ program-name\ \ program-counter\ \ runtime-stack\ \ memory}). +\end{quote} +The programs that update process states can contain system +calls that update other parts of the multiprocess state, +for example, creating new connections, sending and receiving +messages, and creating new process states. + +Each \emph{connection-state} is a 4-tuple: +\begin{quote} +(\emph{source\ \ destination\ \ transit-queue\ \ inbox-queue}). +\end{quote} +A connection-state represents a one-way communication channel +between a pair of processes. The source and destination are +pairs (\emph{process-id file-descriptor}), because +there can be any number of connections between a pair of +processes (as in Unix). The transit queue represents messages +en route, and the inbox queue represents messages +that have been delivered but not yet received by the destination +process. + +A \emph{listening-state} is a 4-tuple: +\begin{quote} +(\emph{process-id\ \ file-descriptor\ \ port-number\ \ request-queue}). +\end{quote} +Each listening-state represents a process listening for new connections. +As in Unix, the file descriptor is known only to +the local process, and the port number is known globally. +The request queue is a list of (\emph{process-id file-descriptor}) +pairs representing processes that are asking for connections. + +The \emph{program-list} is simply an alist that maps program +names to program code. This is used when starting new processes. + +\subsection{The System Calls} + +The programming language has a set of system calls for +setting up communication channels with other processes, +sending and receiving messages, and creating new processes. +The system calls reflect similar Unix system calls, in +particular, the use of ports and file descriptors. We +have simplified things, however, by omitting error handling. + +\begin{description} +\item{\it file-descriptor \rm = \bf setup-listener(\it port\/\bf).} +This takes the place of the Unix \textbf{socket} and \textbf{bind} +system calls. It modifies a multiprocess state by creating +a new listening state. +\item{\it file-descriptor \rm = \bf connect(\it host, port\/\bf).} +A request to connect to another process inserts an entry into +the request queue of a listening state. +The process waits until the connection is accepted by the remote process. +\item{\it file-descriptor \rm = \bf accept(\it file-descriptor\/\bf).} +Accepting a connection takes a member of the request queue and +creates a new connection state. +If the request queue is empty, the process waits until a request arrives. +\item{\it file-descriptor-list \rm = \bf select().} +Select returns the list of file descriptors that have messages +ready to be received, in particular, nonempty inbox queues in +connection states and nonempty request queues in listening states. +\item{\bf send(\it file-descriptor, message\/\bf).} +Send inserts a message into the transit queue of a connection state. +\item{\it message \rm = \bf receive(\it file-descriptor\/\bf).} +Receive takes a message from the inbox queue of a connection state. +If the inbox queue is empty, the process waits +until a message has been delivered. +\item{\it return-code \rm = \bf fork(\it \/\bf).} +Fork creates a copy of the current process, returning a flag telling +whether the process is the parent or the child. +\item{\bf exec(\it program, arguments\/\bf).} +Exec replaces the current process with a new process. +\item{\bf rsh(\it host, program, arguments\/\bf).} +Rsh creates a new process on a given host. +\end{description} + +\subsection{The Multiprocess Simulator} + +The individual processes are simulated as ordinary state machines, +with an ACL2 function that steps the process by executing one +instruction of the program, updating the process state. When a +simulator executes a system call, the multiprocess state can be +updated as well. + +The multiprocess is simulated by executing two types of step: +(1) stepping an individual process, and +(2) stepping a connection state. +Stepping a connection state is simply +transferring a message from the transit queue to the inbox queue, +that is, delivering a message. An oracle tells the simulator +which kind of step to perform and which process to step or +which connection state to step. + +A deficiency of our multiprocess model is that the {\tt connect}, {\tt accept}, +and {\tt rsh} commands are executed is if they had instantaneous effects +on other processes. The model could be improved by adding another +type of communication channel for system operations; that would +allow delays before the operations are carried out, analogous +to the transit and inbox queues of connection states. + +\subsection{Status of the ACL2 Code} + +We have constructed a prototype multiprocess simulator in ACL2 +(see the file \link{README} of the associated directory +for pointers to the books) +and run it on two simple parallel programs. +The first contains console and daemon programs (see Figure~\ref{fig:mpds-all}) +that cause a message to be sent from the console to a daemon, around the ring +and back to the console. The second is a set of manager and client programs +by which the managers implement a barrier operation for the clients: all +clients must call the barrier before any of them can leave it. The general +case of such a barrier was difficult to get right in the real MPD system; we +wish we had been able to test it first on the simulator, which didn't exist at +the time. + +The programs are available in the files \link{trace} and +\link{fence}, respectively, of the associated directory. + +\section{The Next Steps} + +Aside from verifying guards, we have not proved anything about +the simulator. But we are hopeful. + +In~\cite{moore:multi}, J Moore presents a method for proving +properties of shared-memory multiprocess programs. The key idea of +the method is that a substantial part of the proofs can be done from +the points of view of the individual processes. As an individual +process steps from state to state, an oracle tells the process how the +shared memory is changed by the other processes. The properties of +the uniprocessor view are then related to the global multiprocessor +view. Perhaps we can use a similar method to prove properties of our +(message-passing) multiprocess model by replacing the shared-memory +oracle with an oracle that tells how the rest of the multiprocess +state changes, in particular, how the connection and listening states +change. + +Experience with designing and debugging the C version +of MPD has shown us many areas where formal verification +with ACL2 would be of great value. +In addition to the barrier example above, we have had difficulties in ensuring +that if any client aborts, the entire job is brought down cleanly. These are +cases where even attempting formal proofs would help us get it right and +increase our confidence that we had it right. + +\section{Conclusion} + +This project is still in its early stages. Nonetheless, we have learned a few +things. It is possible to usefully abstract the complex collection of Unix +interprocess communication system calls without trivializing the problems +inherent in real parallel algorithms. Using ACL2 has a steep but climbable +learning curve. Our simulator is slow, but we have hopes of speeding things +up by using single-threaded objects. + +\bibliographystyle{plain} + +% \bibliography{paper,/home/MPI/allbib,/home/gropp/Update/new/gropp,/home/MPI/papers/jumpshot/paper} + +\begin{thebibliography}{1} + +\bibitem{mpd-short} +Ralph Butler, Ewing Lusk, and William Gropp. +\newblock A scalable process-management environment for parallel programs. +\newblock In Peter Kacsuk, editor, {\em Recent Advances in {P}arallel {V}irtual + {M}achine and {M}essage {P}assing {I}nterface, 7th European PVM/MPI Users' + Group Meeting, Balatonfured, Hungary}, Lecture Notes in Computer Science. + Springer Verlag, 2000. +\newblock (to appear). + +\bibitem{gropp-lusk-doss-skjellum:mpich} +William Gropp, Ewing Lusk, Nathan Doss, and Anthony Skjellum. +\newblock A high-performance, portable implementation of the {MPI} + {M}essage-{P}assing {I}nterface standard. +\newblock {\em Parallel Computing}, 22(6):789--828, 1996. + +\bibitem{acl2-approach} +M.~Kaufmann, P.~Manolios, and J~Moore. +\newblock {\em Computer-Aided Reasoning: An Approach}. +\newblock Advances in Formal Methods. Kluwer Academic, 2000. + +\bibitem{linux-man-pages} +Linux {\tt man} pages. + +\bibitem{moore:multi} +J~Moore. +\newblock A {M}echanically {C}hecked {P}roof of a {M}ultiprocessor {R}esult via + a {U}niprocessor {V}iew. +\newblock Tech. report, Department of Computer Sciences, University of Texas, + Austin, August 1998. + +\bibitem{beowulf-95} +T.~Sterling, D.~Savarese, D.~J. Becker, J.~E. Dorband, U.~A. Ranawake, and + C.~V. Packer. +\newblock {BEOWULF}: {A} parallel workstation for scientific computation. +\newblock In {\em International Conference on Parallel Processing, Vol.~1: + Architecture}, pages 11--14, Boca Raton, FL, August 1995. CRC Press. + +\end{thebibliography} + + +\end{document} diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/pstate.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/pstate.lisp new file mode 100644 index 0000000..df46ed6 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/pstate.lisp @@ -0,0 +1,190 @@ +(in-package "ACL2") + +(include-book "expr") + +;;------------------------------------------------------------------------ +;; fdexpressionp -- this is a special kind of expression that +;; is a function call, with side effects, that returns an fd. +;; The functions have to do with establishing connections, +;; and the side effects change the lstates and cstates. + +#| + Statements: + (asgn variable expression) + (branch expression name) + (goto name) + (label name) + (call procedure) ;; what if procedure doesn't exist? + (return) + (noop) + (procedure name) ;; start of procedure + + (send fd expression) ;; what if FD doesn't exist? + (select variable) ;; returns list of active FDs + (receive fd variable) + (fdasgn variable fdexpression) ;; for socket primitives + (fork variable) + (exec program-name arguments) + +|# + +(defun statementp (stmt) + (declare (xargs :guard t)) + (cond ((atom stmt) nil) + (t (case (car stmt) + (asgn (and (equal (len stmt) 3) + (varp (second stmt)) ;; variable + (expressionp (third stmt)))) + (setup-listener (and (equal (len stmt) 3) + (expressionp (second stmt)) ;; port + (varp (third stmt)))) ;; for new FD + (connect (and (equal (len stmt) 4) + (expressionp (second stmt)) ;; host + (expressionp (third stmt)) ;; port + (varp (fourth stmt)))) ;; for new FD + (accept (and (equal (len stmt) 3) + (expressionp (second stmt)) ;; listening FD + (varp (third stmt)))) ;; for new FD + (my-hpid (and (equal (len stmt) 2) + (varp (second stmt)))) ;; for hpid + (branch (and (equal (len stmt) 3) + (expressionp (second stmt)) ;; test + (symbolp (third stmt)))) ;; label + (call (and (equal (len stmt) 2) + (symbolp (second stmt)))) ;; label + (procedure (and (equal (len stmt) 2) + (symbolp (second stmt)))) ;; label + (label (and (equal (len stmt) 2) + (symbolp (second stmt)))) ;; label + (goto (and (equal (len stmt) 2) + (symbolp (second stmt)))) ;; label + (return (and (equal (len stmt) 1))) + (send (and (equal (len stmt) 3) + (expressionp (second stmt)) ;; fd + (expressionp (third stmt)))) ;; message + (select (and (equal (len stmt) 3) + (expressionp (second stmt)) ;; fds of interest + (varp (third stmt)))) ;; receiving var + (receive (and (equal (len stmt) 3) + (expressionp (second stmt)) ;; fd + (varp (third stmt)))) ;; receiving var + (fork (and (equal (len stmt) 2) + (varp (second stmt)))) ;; for return val of fork + (exec (and (equal (len stmt) 3) + (symbolp (second stmt)) ;; program name + (memoryp (third stmt)))) ;; program args + (rsh (and (equal (len stmt) 4) + (hostp (second stmt)) ;; host name + (symbolp (third stmt)) ;; program name + (memoryp (fourth stmt)))) ;; program args + (otherwise nil))))) + +(in-theory (disable statementp)) + +(defthm consp-statement-forward + (implies (statementp stmt) + (consp stmt)) + :hints (("Goal" + :in-theory (enable statementp))) + :rule-classes :forward-chaining) + +;;-------------------------------- +;; pstate -- process state + +(defun codep (code) + (declare (xargs :guard t)) + (cond ((atom code) (null code)) + (t (and (statementp (car code)) + (codep (cdr code)))))) + +(defthm ith-of-code-is-statementp ;; move to pstate + (implies (and (codep code) + (consp (ith n code))) + (statementp (ith n code))) + :hints (("Goal" + :in-theory (enable statementp)))) + +(defun ccp (x) ;; program counter + (declare (xargs :guard t)) + (naturalp x)) + +(defun xstackp (x) ;; execution stack + (declare (xargs :guard t)) + (natural-listp x)) + +(defun pstatep (x) + (declare (xargs :guard t)) + (and (true-listp x) + (equal (len x) 5) + (hpidp (first x)) + (codep (second x)) + (ccp (third x)) + (xstackp (fourth x)) + (memoryp (fifth x)))) + +(defmacro code (ps) + (list 'second ps)) + +(defmacro cc (ps) + (list 'third ps)) + +(defmacro xstack (ps) + (list 'fourth ps)) + +(defmacro memory (ps) + (list 'fifth ps)) + +(defmacro update-cc (ps cc) +;; (declare (xargs :guard (and (pstatep ps) +;; (ccp cc)))) + (list 'update-ith ps 3 cc)) + +(defmacro update-xstack (ps xs) +;; (declare (xargs :guard (and (pstatep ps) +;; (xstackp xs)))) + (list 'update-ith ps 4 xs)) + +(defmacro update-memory (ps mem) +;; (declare (xargs :guard (and (pstatep ps) +;; (memoryp mem)))) + (list 'update-ith ps 5 mem)) + +;;---------------------------------------- +;; alist of pstates + +(defun pstate-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (pstatep (car x)) + (pstate-listp (cdr x)))))) + +(defthm pstate-list-is-alist + (implies (pstate-listp x) + (alistp x)) + :rule-classes :forward-chaining) + +(defthm pstatep-assoc-pstate-listp + (implies (and (pstate-listp pss) + (consp (assoc-equal hpid pss))) + (pstatep (assoc-equal hpid pss)))) + +;;--------------- + +(defun make-pstate (hpid code cc xstack memory) + (declare (xargs :guard (and (hpidp hpid) (codep code) (ccp cc) + (xstackp xstack) (memoryp memory)))) + (list hpid code cc xstack memory)) + +(defun update-pstate (hpid pstate pstates) + (declare (xargs :guard (and (hpidp hpid) + (pstatep pstate) + (pstate-listp pstates)))) + (update-alist-member hpid pstate pstates)) + +(defthm pstate-listp-update-alist-member + (implies (and (pstate-listp pss) + (pstatep ps)) + (pstate-listp (update-alist-member x ps pss)))) + +;;--------------------- + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/setup.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/setup.lisp new file mode 100644 index 0000000..38766c7 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/setup.lisp @@ -0,0 +1,325 @@ +(in-package "ACL2") + +(include-book "mstate") + +(defun connection-pairsx (css) + (declare (xargs :guard (cstate-listp css))) + (cond ((atom css) nil) + ((null (second (caar css))) + (cons (list (third (caar css)) (fourth (caar css))) + (connection-pairsx (cdr css)))) + (t (list* (list (first (caar css)) (second (caar css))) + (list (third (caar css)) (fourth (caar css))) + (connection-pairsx (cdr css)))))) + +(defun newfd (hpid ms) + (declare (xargs :guard (and (hpidp hpid) + (mstatep ms)) + :verify-guards nil)) + (gen-natural (fds-in-use hpid (append (connection-pairsx (cstates ms)) + (listening-pairs (lstates ms)))))) + +(defthm request-listp-connection-pairs + (implies (cstate-listp css) + (request-listp (connection-pairsx css))) + :hints (("Goal" + :in-theory (enable hpid-fdp)))) + +(defthm request-listp-listening-pairs + (implies (lstate-listp lss) + (request-listp (listening-pairs lss)))) + +(defthm request-listp-append + (implies (and (request-listp a) + (request-listp b)) + (request-listp (append a b)))) + +(in-theory (enable fdp hpidp hpid-fdp)) + +(defthm natural-listp-fds-in-use + (implies (request-listp a) + (natural-listp (fds-in-use hpid a)))) + +(verify-guards newfd) + +(defthm newfd-fdp + (fdp (newfd hpid ms))) + +(in-theory (disable fdp hpidp hpid-fdp)) + +(in-theory (disable newfd)) + +;;------------------------------------------------------------------------ +;; accept +;; +;; This takes the first connection-request from the queue, and +;; establishes a new connection. We return a pair (FD MS), where +;; FD is a new (local, server) fd for the connection. As usual, MS is +;; the updated mstate. +;; +;; In addition, a kludgey thing happens: we bump the PC of the +;; connecting (remote, client) process. This, in effect, tells that +;; process to stop waiting. +;; +;; If there is nothing to accept, return (-1 MS). + +(defun accept (hpid lfd ms) + (declare (xargs :guard (and (hpidp hpid) + (fdp lfd) + (mstatep ms)) + :verify-guards nil)) + + (let ((request (first-request hpid lfd (lstates ms))) + (newfd (newfd hpid ms))) + (if (not (consp request)) + (list -1 ms) + (let* ((client-fd (second request)) + (client-hpid (first request)) + (client-ps (assoc-equal client-hpid (pstates ms)))) + + (if (not (consp client-ps)) + (list -1 ms) + (list newfd + (make-mstate (update-pstate client-hpid + (make-pstate client-hpid + (code client-ps) + (+ 1 (cc client-ps)) + (xstack client-ps) + (memory client-ps)) + (pstates ms)) + (new-connection hpid + newfd + client-hpid + client-fd + (cstates ms)) + (pop-request hpid lfd (lstates ms)) + (programs ms)))))))) + +(defthm requestq-properties + (implies (and (lstatep ls) + (consp (third ls))) + (and (hpidp (car (car (third ls)))) + (cdr (car (third ls))) + (consp (cdr (car (third ls)))) + (fdp (second (car (third ls)))))) + :hints (("Goal" + :in-theory (enable hpid-fdp)))) + +(defthm first-request-forward + (implies (and (lstate-listp lss) + (consp (first-request hpid fd lss))) + (consp (cdr (first-request hpid fd lss))))) + +(in-theory (disable first-request)) + +(defthm pstate-listp-assoc-forward + (implies (and (pstate-listp pss) + (consp (assoc-equal hpid pss))) + (and (consp (cdr (assoc-equal hpid pss))) + (consp (cddr (assoc-equal hpid pss))) + (consp (cdddr (assoc-equal hpid pss))) + (consp (cddddr (assoc-equal hpid pss))))) + :rule-classes :forward-chaining) + +(defthm pstatep-second + (implies (pstatep ps) + (codep (second ps)))) + +(defthm pstatep-third + (implies (pstatep ps) + (acl2-numberp (third ps)))) + +(defthm pstatep-third-increment + (implies (pstatep ps) + (ccp (+ 1 (third ps))))) + +(defthm pstatep-fourth + (implies (pstatep ps) + (xstackp (fourth ps)))) + +(defthm pstatep-fourth-again + (implies (pstatep ps) + (natural-listp (fourth ps)))) + +(defthm pstatep-fifth + (implies (pstatep ps) + (memoryp (fifth ps)))) + +;;--------------- + +(verify-guards accept + :hints (("Goal" + :in-theory (disable pop-request statementp)))) + +#| For example, +(accept '(lutra 320) ;; source hpid + 14 ;; listening fd + '( + (((cosmo 354) nil 13 nil nil)) ;; pstates + nil ;; cstates + ((((gyro 440) 15) 8585 nil) + (((lutra 320) 14) 7483 (((cosmo 354) 16))) + (((donner 320) 17) 3535 (((fire 444) 18)))))) +|# + +(defthm accept-preserves-mstatep + (implies (and (hpidp hpid) + (fdp lfd) + (mstatep ms)) + (mstatep (second (accept hpid lfd ms)))) + :hints (("Goal" + :in-theory (disable pop-request statementp)))) + +;;------------------------------------------- + +(in-theory (enable hpidp hpid-fdp)) + +(defun find-ls (host port lss) + (declare (xargs :guard (and (hostp host) + (portp port) + (lstate-listp lss)))) + (cond ((atom lss) nil) + ((and (equal (caaaar lss) host) + (equal (second (car lss)) port)) (car lss)) + (t (find-ls host port (cdr lss))))) + +(in-theory (disable hpidp hpid-fdp)) + +;;------------------------------------------------------------------------ +;; connect +;; +;; This attempts a connection request. If the the remote host is not +;; listening on the specified port, nothing happens. If he is listening, +;; we insert the request into the listening queue of the remote host, +;; and return a new fd for the connecting process. +;; +;; Note that this returns a pair (FD MSTATE). + +(defun connect (source-hpid dest-host dest-port ms) + (declare (xargs :guard (and (hpidp source-hpid) + (hostp dest-host) + (portp dest-port) + (mstatep ms)) + :verify-guards nil)) + (let ((ls (find-ls dest-host dest-port (lstates ms))) + (fd (newfd source-hpid ms))) + (cond ((not (consp ls)) (list -1 ms)) ;; no one is listening + (t (list fd + (make-mstate (pstates ms) + (cstates ms) + (update-alist-member + (car ls) + (update-requestq ls (append + (requestq ls) + (list + (list source-hpid fd)))) + (lstates ms)) + (programs ms))))))) + +#| For example, +(connect '(gyro 440) ;; source hpid + 'lutra ;; destination host + 7483 ;; destination port + '(nil ;; pstates + nil ;; cstates + ((((gyro 440) 15) 8585 nil) + (((lutra 320) 14) 7483 (((cosmo 354) 16))) + (((donner 320) 17) 3535 (((fire 444) 18)))))) +|# + +(defthm lstatep-find-ls + (implies (and (lstate-listp lss) + (consp (find-ls host port lss))) + (lstatep (find-ls host port lss)))) + +(defthm request-listp-append-list + (implies (and (lstatep ls) + (hpidp hpid) + (fdp fd)) + (request-listp (append (third ls) + (list (list hpid fd))))) + :hints (("Goal" + :in-theory (enable hpid-fdp)))) + +;;(defthm request-listp-is-true-listp +;; (implies (request-listp x) +;; (true-listp x))) + +(defthm true-listp-third-lstate + (implies (lstatep ls) + (true-listp (third ls))) + :otf-flg t) + +(defthm lstate-listp-assoc-forward + (implies (and (lstate-listp lss) + (consp (find-ls host post lss))) + (and (consp (cdr (find-ls host post lss))) + (consp (cddr (find-ls host post lss))))) + :rule-classes :forward-chaining) + +(defthm find-ls-true-listp + (implies (and (lstate-listp lss) + (consp (find-ls host port lss))) + (true-listp (find-ls host port lss)))) + +(defthm lstate-listp-update-alist + (implies (and (lstate-listp lss) + (lstatep ls)) + (lstate-listp (update-alist-member x ls lss)))) + +(defthm update-requestq-lstate-listp + (implies (and (lstatep ls) + (hpidp hpid) + (fdp fd) + (lstate-listp lss)) + (lstate-listp (update-alist-member + (car ls) + (update-requestq ls (append (requestq ls) + (list (list hpid fd)))) + lss))) + :hints (("Goal" + :in-theory (enable hpidp)))) + +(defthm consp-update-ith + (implies (consp x) + (consp (update-ith x i y)))) + +(verify-guards connect) + +(defthm connect-preserves-mstatep + (implies (and (hpidp source-hpid) + (hostp dest-host) + (portp dest-port) + (mstatep ms)) + (mstatep (second (connect source-hpid dest-host dest-port ms))))) + +;;------------------------------------------------------------------ +;; setup-listener +;; +;; This allocates a new fd and adds an lstate to the lstates. +;; +;; Note that this returns a pair (FD MS), where FD is +;; the new fd that is used for listening, and MS is the updated +;; mstate. + +(in-theory (enable hpid-fdp)) + +(defun setup-listener (hpid port ms) + (declare (xargs :guard (and (hpidp hpid) + (portp port) + (mstatep ms)))) + (let ((lfd (newfd hpid ms))) + (list lfd + (make-mstate (pstates ms) + (cstates ms) + (cons (list (list hpid lfd) port nil) + (lstates ms)) + (programs ms))))) + +(defthm setup-listener-preserves-mstatep + (implies (and (hpidp hpid) + (portp port) + (mstatep ms)) + (mstatep (second (setup-listener hpid port ms))))) + +(in-theory (disable hpid-fdp)) diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/simulator.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/simulator.lisp new file mode 100644 index 0000000..575e020 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/simulator.lisp @@ -0,0 +1,122 @@ +(in-package "ACL2") + +(include-book "stepprocess") + +;;--------------------------------------------- +;; Here is the simulator + +;; The oracle for the simulator tells what type of operation and +;; which operation of that type to do next. It is a list of +;; pairs in which the cars are a (random) type and the cdrs are +;; (random) nonnegative integers. + +(defun oraclep (o) + (declare (xargs :guard t)) + (cond ((atom o) (null o)) + (t (and (consp (car o)) + (or (equal (caar o) 'step) + (equal (caar o) 'deliver)) + (integerp (cdar o)) + (>= (cdar o) 0) + (oraclep (cdr o)))))) + +;; There is a built-in (mod x y) for rationals, but the version for +;; nonnegative integers in book mod-gcd seems easier to work with. + +(include-book "../../../../arithmetic/mod-gcd") + +;; count -- counts the number of oracle members we go through. +;; trace -- keeps track of what we do. If the oracle says to do +;; something that can't be done, nothing is added to the trace. +;; + +(defun sim (oracle count trace ms) + (declare (xargs :guard (and (oraclep oracle) + (naturalp count) + (true-listp trace) + (mstatep ms)) + :verify-guards nil)) + + (let ((np (active-pstates (pstates ms) (cstates ms) (lstates ms))) + (nc (active-cstates (cstates ms)))) + + (cond ((atom oracle) (list 'timeout count trace ms)) + ((and (equal np 0) + (equal nc 0)) (list (if (> (waiting-pstates (pstates ms) + (cstates ms) + (lstates ms)) + 0) + 'someone-is-waiting + 'nothing-to-do) + 'count count + 'trace trace + 'final-mstate ms)) + + ((and (equal (caar oracle) 'step) + (> np 0)) + (let ((ps (ith-active-pstate + (+ 1 (nonneg-int-mod (cdar oracle) np)) + (pstates ms) + (cstates ms) + (lstates ms)))) + (sim (cdr oracle) (1+ count) (append trace + (list (list 'step (car ps) + (cc ps)))) + (step-process ms ps)))) + + ((and (equal (caar oracle) 'deliver) + (> nc 0)) + (let ((cs (ith-active-cstate + (+ 1 (nonneg-int-mod (cdar oracle) nc)) + (cstates ms)))) + (sim (cdr oracle) (1+ count) (append + trace + (list (list 'deliver (car cs)))) + (deliver-message ms cs )))) + + ;; If there is no operation of the given type to perform, + ;; just go to the next member of the oracle. + + (t (sim (cdr oracle) (1+ count) trace ms))))) + +;;-------------------- +;; lemmas to help verify sim guards + +(defthm mstatep-properties + (implies (mstatep ms) + (and (pstate-listp (car ms)) + (cstate-listp (cadr ms))))) + +(defthm sim-guard-helper-1 + (implies (and (cstate-listp css) + (ith-active-cstate n css)) + (consp (ith-active-cstate n css)))) + +(defthm sim-guard-helper-2 + (implies (and (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss) + (ith-active-pstate n pss css lss)) + (consp (ith-active-pstate n pss css lss)))) + +(defthm sim-guard-helper-3 + (implies (and (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss) + (not (consp (cddr (ith-active-pstate n pss css lss))))) + (not (cddr (ith-active-pstate n pss css lss))))) + +(defthm sim-guard-helper-4 + (implies (and (pstate-listp pss) + (cstate-listp css) + (lstate-listp lss) + (not (consp (cdr (ith-active-pstate n pss css lss))))) + (not (cdr (ith-active-pstate n pss css lss))))) + +(verify-guards sim + :hints (("Goal" + :in-theory (disable deliver-message + step-process + cstatep pstatep + ))) + :otf-flg t) diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc0.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc0.lisp new file mode 100644 index 0000000..f4af32a --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc0.lisp @@ -0,0 +1,260 @@ +(in-package "ACL2") + +(include-book "mstate") + +(in-theory (enable hpidp pidp)) + +(defun pids-in-use (host pss) + (declare (xargs :guard (and (hostp host) + (pstate-listp pss)))) + (cond ((atom pss) nil) + ((equal host (first (caar pss))) (cons (second (caar pss)) + (pids-in-use host (cdr pss)))) + (t (pids-in-use host (cdr pss))))) + +(defun newpid (host pss) + (declare (xargs :guard (and (hostp host) + (pstate-listp pss)))) + (gen-pos-integer (pids-in-use host pss))) + +(defthm newpid-is-pid + (pidp (newpid host pss))) + +(in-theory (disable hpidp pidp)) + +;;====================================================================== +;; When a process forks, we copy all of the connections involving +;; the parent process, updating the hpid to the hpid of the child. + +(defun fork-connections (old-hpid new-hpid css) + (declare (xargs :guard (and (hpidp old-hpid) + (hpidp new-hpid) + (cstate-listp css)))) + (cond ((atom css) nil) + ((and (equal old-hpid (first (caar css))) + (equal old-hpid (third (caar css)))) + (list* (cons (list new-hpid (second (caar css)) + new-hpid (fourth (caar css))) + (cdar css)) + (car css) + (fork-connections old-hpid new-hpid (cdr css)))) + ((equal old-hpid (first (caar css))) + (list* (cons (list new-hpid (second (caar css)) + (third (caar css)) (fourth (caar css))) + (cdar css)) + (car css) + (fork-connections old-hpid new-hpid (cdr css)))) + ((equal old-hpid (third (caar css))) + (list* (cons (list (first (caar css)) (second (caar css)) + new-hpid (fourth (caar css))) + (cdar css)) + (car css) + (fork-connections old-hpid new-hpid (cdr css)))) + (t (cons (car css) + (fork-connections old-hpid new-hpid (cdr css)))))) + +;; For example, + +#| +(fork-connections '(lutra 320) + '(lutra 321) + '( + (((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2)) + (((gyro 440) 6 (lutra 320) 5) ('m3 'm4) ('m1 'm2)) + (((lutra 320) 7 (lutra 320) 8) ('m3 'm4) ('m1 'm2)) + )) +|# + +(defthm fork-connections-preserves-cstate-listp + (implies (and (cstate-listp css) + (hpidp new-hpid)) + (cstate-listp (fork-connections old-hpid new-hpid css)))) + +;;====================================================================== + +(defun exec-fork (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'fork) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + (let ((newpid (newpid (first (car ps)) (pstates ms)))) + + (make-mstate + (cons (make-pstate (list (first (car ps)) newpid);; child process + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (memory ps)) + (update-pstate (car ps) + (make-pstate (car ps);; parent process + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (second stmt) + newpid + (memory ps))) + (pstates ms))) + (fork-connections (car ps) (list (first (car ps)) newpid) (cstates ms)) + (lstates ms) + (programs ms)))) + +;; For example, + +#| +(exec-fork '(fork fpid) + '((lutra 320) ((asgn z 6)) 13 nil ((x . 4) (y . 6))) + '( + (;; pstates: + ((lutra 320) ((asgn z 6)) 13 nil ((x . 4) (y . 6))) + ((gyro 440) ((procedure handle)) 14 nil nil) + ) + + (;; cstates: + (((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2)) + ) + (;; lstates: + (((gyro 440) 15) 8585 nil) + (((lutra 320) 14) 7483 (((cosmo 354) 16))) + (((donner 320) 17) 3535 (((fire 444) 18))) + ) + nil + )) +|# + +(local (in-theory (enable statementp))) + +(verify-guards exec-fork + :hints (("Goal" + :in-theory (enable hpidp pidp hostp)))) + +(defthm exec-fork-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'fork) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-fork stmt ps ms))) + :hints (("Goal" + :in-theory (enable hpidp pidp hostp)))) + +;;=================================================================== + +(defun exec-exec (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'exec) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + (let ((program (assoc-equal (second stmt) (programs ms)))) + + (if program + + ;; all is well---the program exists + + (make-mstate (update-pstate (car ps) + (make-pstate (car ps) + (second program) + 1 + nil + (third stmt)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms)) + ;; error + + (make-mstate (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-prog-name-in-exec + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))))) + +(defthm program-listp-assoc-properties + (implies (and (program-listp pgms) + (assoc-equal name pgms)) + (and (consp (assoc-equal name pgms)) + (consp (cdr (assoc-equal name pgms))) + (codep (second (assoc-equal name pgms)))))) + +(verify-guards exec-exec + :otf-flg t) + +(defthm exec-exec-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'exec) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-exec stmt ps ms)))) + +;;=================================================================== + +(defun exec-rsh (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'rsh) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + (let ((program (assoc-equal (third stmt) (programs ms)))) + (if program + + ;; All is well---the program exists. + ;; Cons the new process onto the updated process list. + + (make-mstate + + (cons (make-pstate (list (second stmt) + (newpid (caar ps) (pstates ms))) + (second program) + 1 + nil + (fourth stmt)) + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (memory ps)) + (pstates ms))) + (cstates ms) + (lstates ms) + (programs ms)) + ;; error + + (make-mstate (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-prog-name-in-rsh + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))))) + +(defthm gen-pos-integer-pidp + (pidp (gen-pos-integer x)) + :hints (("Goal" + :in-theory (enable pidp)))) + +(verify-guards exec-rsh + :hints (("Goal" + :in-theory (enable hpidp)))) + +(defthm exec-rsh-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'rsh) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-rsh stmt ps ms))) + :hints (("Goal" + :in-theory (enable hpidp)))) + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc1.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc1.lisp new file mode 100644 index 0000000..e90afc5 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc1.lisp @@ -0,0 +1,666 @@ +(in-package "ACL2") + +(include-book "mstate") + +;;--------------- + +;; forward chaining rules for kinds of statement + +(in-theory (enable statementp)) + +(defthm statement-my-hpid-forward + (implies (and (statementp stmt) + (equal (car stmt) 'my-hpid)) + (and (consp (cdr stmt)) + (varp (cadr stmt)))) + :rule-classes :forward-chaining) + +(defthm statement-goto-forward + (implies (and (statementp stmt) + (equal (car stmt) 'goto)) + (and (consp (cdr stmt)) + (symbolp (cadr stmt)))) + :rule-classes :forward-chaining) + +(defthm statement-call-forward + (implies (and (statementp stmt) + (equal (car stmt) 'call)) + (and (consp (cdr stmt)) + (symbolp (cadr stmt)))) + :rule-classes :forward-chaining) + +(defthm statement-asgn-forward + (implies (and (statementp stmt) + (equal (car stmt) 'asgn)) + (and (consp (cdr stmt)) + (consp (cddr stmt)) + (varp (second stmt)) + (expressionp (third stmt)) + )) + :rule-classes :forward-chaining) + +(defthm statement-branch-forward + (implies (and (statementp stmt) + (equal (car stmt) 'branch)) + (and (consp (cdr stmt)) + (consp (cddr stmt)) + (expressionp (second stmt)) + (symbolp (third stmt)) + )) + :rule-classes :forward-chaining) + +(defthm statement-send-forward + (implies (and (statementp stmt) + (equal (car stmt) 'send)) + (and (consp (cdr stmt)) + (consp (cddr stmt)) + (expressionp (second stmt)) + (expressionp (third stmt)) + )) + :rule-classes :forward-chaining) + +(defthm statement-receive-forward + (implies (and (statementp stmt) + (equal (car stmt) 'receive)) + (and (consp (cdr stmt)) + (consp (cddr stmt)) + (expressionp (second stmt)) + (varp (third stmt)) + )) + :rule-classes :forward-chaining) + +(defthm statement-select-forward + (implies (and (statementp stmt) + (equal (car stmt) 'select)) + (and (consp (cdr stmt)) + (consp (cddr stmt)) + (expressionp (second stmt)) + (varp (third stmt)) + )) + :rule-classes :forward-chaining) + +(in-theory (disable statementp)) + +;;--------------- +;; index-of-name gets the index of a label statment so that +;; we can set the program counter when we execute goto, call, and +;; branch statements. + +(in-theory (enable statementp)) + +(defun index-of-name (name code i) + (declare (xargs :guard (and (symbolp name) + (codep code) + (pos-integerp i)))) + (cond ((atom code) 0) + ((and (or (equal (caar code) 'procedure) + (equal (caar code) 'label)) + (equal (second (car code)) name)) i) + (t (index-of-name name (cdr code) (+ 1 i))))) + +(in-theory (disable statementp)) + +(defthm index-of-name-is-naturalp + (implies (pos-integerp i) + (naturalp (index-of-name name code i)))) + +;;================== +;; Here are 2 simple operations: return, skip. Define and +;; prove that they preserve mstatep. + +(defun exec-skip (ps ms) ;; just increment the program counter + (declare (xargs :guard (and (mstatep ms) + (pstatep ps)))) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (memory ps)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + +(defthm exec-skip-preserves-mstatep + (implies (and (mstatep ms) + (pstatep ps)) + (mstatep (exec-skip ps ms)))) + +(defun exec-return (ps ms) + (declare (xargs :guard (and (mstatep ms) + (pstatep ps)))) + (if (atom (xstack ps)) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (memory ps)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms)) + + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (car (xstack ps)) + (cdr (xstack ps)) + (memory ps)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms)))) + +(defthm exec-return-preserves-mstatep + (implies (and (mstatep ms) + (pstatep ps)) + (mstatep (exec-return ps ms)))) + +;;--------------------------------------------------- + +(defun exec-goto (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'goto) + (mstatep ms) + (pstatep ps)))) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (index-of-name (second stmt) (code ps) 1) + (xstack ps) + (memory ps)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + +(defthm exec-goto-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'goto) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-goto stmt ps ms)))) + +(defun exec-call (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'call) + (mstatep ms) + (pstatep ps)))) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (index-of-name (second stmt) (code ps) 1) + (cons (+ 1 (cc ps)) (xstack ps)) + (memory ps)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + +(defthm exec-call-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'call) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-call stmt ps ms)))) + +;;====================================================== + +(defun exec-my-hpid (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'my-hpid) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (second stmt) + (list (list 'quote (first (car ps))) + (second (car ps))) + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + +(defthm my-hpid-helper + (implies (hpidp hpid) + (evaluated-expressionp (list (list 'quote (first hpid)) + (second hpid)))) + :hints (("Goal" + :in-theory (enable hostp pidp hpidp constp)))) + +(verify-guards exec-my-hpid + :hints (("Goal" + :in-theory (enable hpidp)))) + +(defthm exec-my-hpid-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'my-hpid) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-my-hpid stmt ps ms))) + :hints (("Goal" + :in-theory (enable hpidp)))) + +;;====================================================== + +(defun exec-asgn (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'asgn) + (mstatep ms) + (pstatep ps)))) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (second stmt) + (evl2 (third stmt) (memory ps)) + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + +(defthm exec-asgn-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'asgn) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-asgn stmt ps ms)))) + +;;=================================================== + +;; The following speeds up exec-branch proofs below. + +(defun branch-destination (stmt mem code cc) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'branch) + (codep code) + (ccp cc) + (memoryp mem)))) + (if (equal (evl2 (second stmt) mem) ''true) + (index-of-name (third stmt) code 1) + (+ 1 cc))) + +(defthm branch-destination-ccp + (implies (ccp cc) + (ccp (branch-destination stmt mem code cc)))) + +(in-theory (disable branch-destination)) + +(defun exec-branch (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'branch) + (mstatep ms) + (pstatep ps)))) + (make-mstate + (update-pstate + (car ps) + (make-pstate (car ps) + (code ps) + (branch-destination stmt (memory ps) (code ps) (cc ps)) + (xstack ps) + (memory ps)) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + +(defthm exec-branch-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'branch) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-branch stmt ps ms)))) + +;;================================================== + +(defthm cstatep-send + (implies (and (cstatep cs) + (evaluated-expressionp e)) + (cstatep (list (car cs) + (append (cadr cs) (list e)) + (caddr cs))))) + +(defthm cstatep-receive + (implies (and (cstatep cs) + (consp (inboxq cs))) + (cstatep (list (first cs) + (second cs) + (cdr (third cs)))))) + +(defun sender-cstate (hpid fd css) + (declare (xargs :guard (and (hpidp hpid) (fdp fd) (cstate-listp css)))) + (cond ((atom css) nil) + ((and (equal hpid (first (caar css))) + (equal fd (second (caar css)))) (car css)) + (t (sender-cstate hpid fd (cdr css))))) + +(defthm sender-cstate-cstatep + (implies (and (cstate-listp css) + (consp (sender-cstate x y css))) + (cstatep (sender-cstate x y css)))) + +(defun receiver-cstate (hpid fd css) + (declare (xargs :guard (and (hpidp hpid) (fdp fd) (cstate-listp css)))) + (cond ((atom css) nil) + ((and (equal hpid (third (caar css))) + (equal fd (fourth (caar css)))) (car css)) + (t (receiver-cstate hpid fd (cdr css))))) + +(defthm receiver-cstate-cstatep + (implies (and (cstate-listp css) + (consp (receiver-cstate x y css))) + (cstatep (receiver-cstate x y css)))) + +;;================================================== + +(defun exec-send (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'send) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + (let* ((fd (evl2 (second stmt) (memory ps))) + (cs (if (fdp fd) + (sender-cstate (car ps) fd (cstates ms)) + nil))) + + (cond ((atom cs) + ;; The FD is bad, so set pc to 0 and set error variable. + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-fd-in-send + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + + ;; all is well + (t (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (memory ps)) + (pstates ms)) + (update-cstate (car cs) + (make-cstate (car cs) + (append (transitq cs) + (list (evl2 (third stmt) + (memory ps)))) + (inboxq cs)) + (cstates ms)) + (lstates ms) + (programs ms)))))) + +(defthm second-of-cstate-is-true-listp + (implies (cstatep cs) + (true-listp (second cs))) + :otf-flg t) + +(defthm cstate-listp-sender-forward + (implies (and (cstate-listp css) + (consp (sender-cstate hpid fd css))) + (and (consp (cdr (sender-cstate hpid fd css))) + (consp (cddr (sender-cstate hpid fd css))))) + :rule-classes :forward-chaining) + +(verify-guards exec-send + :hints (("Goal" + :in-theory (disable connectionp + cstatep + + ;; mstatep + ;; pstatep + ;; xstackp ccp + )))) + +(defthm exec-send-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'send) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-send stmt ps ms)))) + +;;================================================================== + +(defthm evaluated-expressionp-car-inbox + (implies (and (cstatep cs) + (consp (caddr cs))) + (evaluated-expressionp (caaddr cs))) + :hints (("Goal" + :in-theory (enable constp)))) + +(defun exec-receive (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'receive) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + + (let* ((fd (evl2 (second stmt) (memory ps))) + (cs (if (fdp fd) + (receiver-cstate (car ps) fd (cstates ms)) + nil))) + + (cond ((atom cs) + ;; the FD is bad, so halt with error message + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-fd-in-receive + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + + ((atom (inboxq cs)) + ;; no message to receive, so wait (i.e., don't change state) + ms) + + ;; all is well + (t (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (third stmt) + (car (inboxq cs)) + (memory ps))) + (pstates ms)) + (update-cstate (car cs) + (make-cstate (car cs) + (transitq cs) + (cdr (inboxq cs))) + (cstates ms)) + (lstates ms) + (programs ms)))))) + +(defthm cstate-cdr-inbox + (implies (and (cstatep cs) + (consp (caddr cs))) + (evaluated-expression-listp (cdr (caddr cs))))) + +(defthm cstate-listp-receiver-forward + (implies (and (cstate-listp css) + (consp (receiver-cstate hpid fd css))) + (and (consp (cdr (receiver-cstate hpid fd css))) + (consp (cddr (receiver-cstate hpid fd css))))) + :rule-classes :forward-chaining) + +(verify-guards exec-receive + :hints (("Goal" + :in-theory (disable connectionp cstatep)))) + +(defthm exec-receive-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'receive) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-receive stmt ps ms)))) + +;;=========================================================== +;; select - given an hpid, return the list of FDs that have +;; messages or connection-requests available for receiving. +;; This includes both ordinary FSs (from cstates) and listening +;; FDs (from lstates). + +(defun select-ordinary-fds (hpid css) + (declare (xargs :guard (and (hpidp hpid) + (cstate-listp css)))) + (cond ((atom css) nil) + ((and (equal hpid (third (caar css))) + (consp (inboxq (car css)))) + (cons (fourth (caar css)) + (select-ordinary-fds hpid (cdr css)))) + (t (select-ordinary-fds hpid (cdr css))))) + +(in-theory (enable hpid-fdp)) + +(defun select-listening-fds (hpid lss) + (declare (xargs :guard (and (hpidp hpid) + (lstate-listp lss)))) + (cond ((atom lss) nil) + ((and (equal hpid (first (caar lss))) + (consp (requestq (car lss)))) + (cons (second (caar lss)) + (select-listening-fds hpid (cdr lss)))) + (t (select-listening-fds hpid (cdr lss))))) + +(in-theory (disable hpid-fdp)) + +(defun select (hpid fds-of-interest ms) + (declare (xargs :guard (and (hpidp hpid) + (mstatep ms)))) + (intersect-equal (lfix fds-of-interest) + (append (select-ordinary-fds hpid (cstates ms)) + (select-listening-fds hpid (lstates ms))))) + +;; For example, + +#| +(select-ordinary-fds '(gyro 4) '((((a 1) 7 (gyro 4) 1) nil ('m1 'm2 'm3)) + (((b 2) 8 (junk 3) 2) nil ('m4 'm5)) + (((c 3) 9 (gyro 4) 3) nil ('m6)))) + +(select-listening-fds '(gyro 4) '((((gyro 4) 1) 81 (((donner 101) 6))) + (((junk 3) 2) 82 (((juju 102) 7))) + (((gyro 4) 3) 83 (((lutra 103) 8))))) + +(select '(gyro 4) '(1 6 9) '(nil + ((((a 1) 7 (gyro 4) 1) nil ('m1 'm2 'm3)) + (((b 2) 8 (junk 3) 2) nil ('m4 'm5)) + (((c 3) 9 (gyro 4) 3) nil ('m6))) + ((((gyro 4) 4) 81 (((donner 101) 6))) + (((junk 3) 5) 82 (((juju 102) 7))) + (((gyro 4) 6) 83 (((lutra 103) 8)))))) + +|# + +(defthm select-ordinary-fds-gives-fd-listp + (implies (cstate-listp css) + (fd-listp (select-ordinary-fds x css)))) + +(defthm select-listening-fds-gives-fd-listp + (implies (lstate-listp lss) + (fd-listp (select-listening-fds x lss))) + :hints (("Goal" + :in-theory (enable hpid-fdp)))) + +(defthm fd-listp-append + (implies (and (fd-listp a) + (fd-listp b)) + (fd-listp (append a b)))) + +(defthm fd-listp-intersect + (implies (or (fd-listp a) + (fd-listp b)) + (fd-listp (intersect-equal a b)))) + +(defthm select-gives-fd-listp + (implies (mstatep ms) + (fd-listp (select x y ms)))) + +(defthm select-gives-true-listp + (true-listp (select x y ms))) + +(in-theory (disable select)) + +(defthm fdp-is-evaluated-expressionp + (implies (fdp x) + (evaluated-expressionp x)) + :hints (("Goal" + :in-theory (enable fdp)))) + +(defthm fd-listp-is-evaluated-expressionp + (implies (fd-listp fds) + (evaluated-expressionp fds))) + +(defthm select-gives-evaluated-expressionp + (implies (mstatep ms) + (evaluated-expressionp (select x y ms)))) + +;;----------------------------------------------------------------- +;; exec-select +;; +;; If any messages are available, set the variable to the list of FDs. +;; If not, do nothing (i.e., wait). + +(defun exec-select (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'select) + (mstatep ms) + (pstatep ps)))) + (let ((sel (select (car ps) (evl2 (second stmt) (memory ps)) ms))) + (if (null sel) + ms ;; no messages to receive, so wait (i.e., don't change state) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (third stmt) + sel + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))))) + +(defthm exec-select-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'select) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-select stmt ps ms)))) + +;;------------------------------------------------------ diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc2.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc2.lisp new file mode 100644 index 0000000..25637de --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc2.lisp @@ -0,0 +1,294 @@ +(in-package "ACL2") + +(include-book "setup") + +(local (in-theory (enable statementp))) + +;; The following are useful when disabling mstatep + +(defthm mstate-pstate-listp + (implies (mstatep ms) + (pstate-listp (first ms)))) + +(defthm mstate-cstate-listp + (implies (mstatep ms) + (cstate-listp (second ms)))) + +(defthm mstate-lstate-listp + (implies (mstatep ms) + (lstate-listp (third ms)))) + +(defthm mstate-program-listp + (implies (mstatep ms) + (program-listp (fourth ms)))) + +;;-------------------------------- +;; exec-setup-listener + +;; [Jared] adding this because the defun below failed when it was added to ACL2. +(local (in-theory (disable FOLD-CONSTS-IN-+))) + +(defun exec-setup-listener (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'setup-listener) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + + (let ((port (evl2 (second stmt) (memory ps)))) + (if (portp port) + (let* ((x (setup-listener (car ps) port ms)) + (lfd (first x)) + (ms1 (second x))) + + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (third stmt) + lfd + (memory ps))) + (pstates ms1)) + (cstates ms1) + (lstates ms1) + (programs ms))) + + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-port-in-setup-listener + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms)) + ))) + +(defthm evaluated-expressionp-car-setup-listener + (evaluated-expressionp (car (setup-listener hpid port ms)))) + +(verify-guards exec-setup-listener + :hints (("Goal" + :in-theory (disable setup-listener))) + :otf-flg t) + +(defthm exec-setup-listener-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'setup-listener) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-setup-listener stmt ps ms))) + :hints (("Goal" + :in-theory (disable setup-listener)))) + +;;------------------------------------ + +(defthm request-listp-is-alistp + (implies (request-listp rq) + (alistp rq)) + :hints (("Goal" + :in-theory (enable hpid-fdp))) + :rule-classes :forward-chaining) + +(defthm find-ls-alistp + (implies (and (lstate-listp lss) + (consp (find-ls dest-host dest-port lss))) + (alistp (caddr (find-ls dest-host dest-port lss))))) + +(defun connection-status (my-hpid dest-host dest-port ms) + (declare (xargs :guard (and (hpidp my-hpid) + (hostp dest-host) + (portp dest-port) + (mstatep ms)))) + (let ((ls (find-ls dest-host dest-port (lstates ms)))) + (cond ((atom ls) 'not-listening) + ((assoc-equal my-hpid (requestq ls)) 'pending) + (t 'ready)))) + +(defun unkwote (x) + (declare (xargs :guard t)) + (if (and (equal (len x) 2) + (equal (first x) 'quote)) + (second x) + x)) + +(in-theory (disable unkwote)) + +;;------------------------------------------------------------------ +;; exec-connect +;; +;; This executes (or continues to execute) a statement like +;; (FDASGN FD (CONNECT remote-host remote-port)). +;; +;; If the remote-host is not listening on the remote-port, we set +;; the FD to -1 and bump the PC (connection refused). +;; If we have already issued a connect-request, and the remote host +;; has not accepted it, we do nothing. +;; Otherwise, we issue a connect-request. +;; +;; Note that the PC is bumped by the accepting process when the connection +;; is accepted. Perhaps this bit of implicit handshaking should be rethought. + +(defun exec-connect (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'connect) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + + (let ((my-hpid (car ps)) + (dest-host (unkwote (evl2 (second stmt) (memory ps)))) + (dest-port (evl2 (third stmt) (memory ps)))) + (if (or (not (hostp dest-host)) + (not (portp dest-port))) + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-host-or-port-in-connect + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms)) + + (let ((status (connection-status my-hpid dest-host dest-port ms))) + (case status + (pending ms) ;; do nothing + + (not-listening (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (fourth stmt) + -1 + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms))) + + (ready (let* ((x (connect my-hpid dest-host dest-port ms)) + (fd (first x)) + (ms1 (second x))) + + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (cc ps) + (xstack ps) + (asgn (fourth stmt) + fd + (memory ps))) + (pstates ms1)) + (cstates ms1) + (lstates ms1) + (programs ms)))) + + (otherwise ms) + ))))) + +(defthm evaluated-expressionp-car-connect + (evaluated-expressionp (car (connect hpid host port ms)))) + +(defthm conp-cdr-connect + (consp (cdr (connect hpid host port ms)))) + +(defthm cdr-connect + (cdr (connect hpid host port ms))) + +(verify-guards exec-connect + :hints (("Goal" + :in-theory (disable connect mstatep)))) + +(defthm exec-connect-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'connect) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-connect stmt ps ms))) + :hints (("Goal" + :in-theory (disable connect)))) + +;;------------------------------------ +;; exec-accept +;; +;; This executes a statement like (FDASGN FD (ACCEPT LFD)), where +;; LFD is the listening fd. When and if we succeed, FD is given +;; the new fd for the conection. If there are no requests to accept, +;; we do nothing (i.e., we wait). + +(defun exec-accept (stmt ps ms) + (declare (xargs :guard (and (statementp stmt) + (equal (car stmt) 'accept) + (mstatep ms) + (pstatep ps)) + :verify-guards nil)) + + (let ((lfd (evl2 (second stmt) (memory ps)))) + (if (not (fdp lfd)) + ;; The fd is bad, so set pc to 0 and set error variable. + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + 0 + (xstack ps) + (asgn 'error + ''bad-fd-in-accept + (memory ps))) + (pstates ms)) + (cstates ms) + (lstates ms) + (programs ms)) + + ;; The listening FD is ok. Try to accept a connection. + (let* ((x (accept (car ps) lfd ms)) + (fd (first x)) + (ms1 (second x))) + + (if (equal fd -1) + ;; There is nothing to accept, so just wait. + ms + ;; All is well, so accept, bump our PC, and assign fd. + (make-mstate + (update-pstate (car ps) + (make-pstate (car ps) + (code ps) + (+ 1 (cc ps)) + (xstack ps) + (asgn (third stmt) + fd + (memory ps))) + (pstates ms1)) + (cstates ms1) + (lstates ms1) + (programs ms))))))) + +(defthm evaluated-expressionp-car-accept + (evaluated-expressionp (car (accept hpid fd ms)))) + +(verify-guards exec-accept + :hints (("Goal" + :in-theory (disable accept)))) + +(defthm exec-accept-preserves-mstatep + (implies (and (statementp stmt) + (equal (car stmt) 'accept) + (mstatep ms) + (pstatep ps)) + (mstatep (exec-accept stmt ps ms))) + :hints (("Goal" + :in-theory (disable accept)))) diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepprocess.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepprocess.lisp new file mode 100644 index 0000000..7e4f571 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/stepprocess.lisp @@ -0,0 +1,61 @@ +(in-package "ACL2") + +(include-book "stepproc1") +(include-book "stepproc2") +(include-book "stepproc0") + +(defun step-process (ms ps) ;; returns mstate + (declare (xargs :guard (and (mstatep ms) + (pstatep ps)))) + + (let ((stmt (if (zp (cc ps)) nil (ith (cc ps) (code ps))))) + (cond + ((atom stmt) ms) ;; cc out of range + (t (case (car stmt) + (asgn (exec-asgn stmt ps ms)) + (setup-listener (exec-setup-listener stmt ps ms)) + (connect (exec-connect stmt ps ms)) + (accept (exec-accept stmt ps ms)) + (my-hpid (exec-my-hpid stmt ps ms)) + ((label procedure) (exec-skip ps ms)) + (goto (exec-goto stmt ps ms)) + (call (exec-call stmt ps ms)) + (return (exec-return ps ms)) + (branch (exec-branch stmt ps ms)) + (send (exec-send stmt ps ms)) + (select (exec-select stmt ps ms)) + (receive (exec-receive stmt ps ms)) + (fork (exec-fork stmt ps ms)) + (exec (exec-exec stmt ps ms)) + (rsh (exec-rsh stmt ps ms)) + + (otherwise ms)))))) ;; bad statement + +;; Prove that step-process preserves mstatep + +(defthm step-process-mstatep + (implies (and (mstatep ms) + (pstatep ps)) + (mstatep (step-process ms ps))) + :hints (("Goal" + :in-theory (disable exec-asgn + exec-send + exec-select + exec-receive + exec-setup-listener + exec-connect + exec-accept + exec-my-hpid + exec-skip + exec-goto + exec-call + exec-return + exec-branch + exec-fork + exec-exec + exec-rsh + mstatep + pstatep + )))) + + diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/trace b/books/workshops/2000/lusk-mccune/lusk-mccune-final/trace new file mode 100644 index 0000000..e9fc5c2 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/trace @@ -0,0 +1,582 @@ +(in-package "ACL2") + +(include-book "simulator") +(include-book "compile") + +(sim + + ;; First, the oracle. + + '( + (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (DELIVER . 7828) + + (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (DELIVER . 7828) + + (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200) + (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124) + (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229) + (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593) + (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074) + (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518) + (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460) + (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326) + (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137) + (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379) + (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157) + (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482) + (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398) + (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265) + (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958) + (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573) + (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629) + (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772) + (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976) + (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251) + (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840) + (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336) + (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028) + (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392) + (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888) + (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904) + (DELIVER . 7828) + ) + + 0 ;; step counter + + nil ;; trace + + ;;--------------------------------------------------------- mstate + + ;; This mstate contains a console and set of daemons The console sends a + ;; message to the local daemon, which forwards it aroung the ring to the + ;; local daemon, which sends it back to the console. + + (list;; mstate + + (list;; list of pstates + + ;;--------------------------------------------------------- console pstate + + ;; This pstate is for the console. It connects to the local daemon, sends + ;; a message to it, and then waits for a reply. + + (list;; trace pstate + '(host1 9) + + (compile-list;; trace program + '( + (my-hpid myhpid) + (asgn host (car myhpid)) + (connect host 2000 mpd-fd) + (send mpd-fd 'trace) + (asgn eof 'false) + (asgn host-list nil) ;; note that the constant nil is unquoted + (while (not eof) + (receive mpd-fd x) + (if (not (equal x 'end-of-file)) + (asgn host-list (cons x host-list)) + else + (asgn eof 'true) + );; end if + );; end while + (return) + ) + nil + );; end of trace program + + 1;; program counter at first statement + nil;; xstack + nil;; memory + );; end of trace process + + ;;--------------------------------------------------------- daemon 1 pstate + + (list;; first mpd pstate + + ;; All the daemons are the same. They wait for a connection from a console + ;; and accept it, then process commands from it. The trace command handler + ;; forwards the message to the next daemon. The ring connections among the + ;; daemons are pre-established in the connection part of the mstate. A + ;; ring-message handler reads the message and either forwards it around the + ;; ring or (if it is the original daemon that received it from the console, + ;; back to the console. + + '(host1 1) + + (compile-list;; mpd program + '( + (my-hpid myhpid) + (asgn select-set (lhs-fd conl-fd)) + (asgn con-fd -1) + (while 'true + (select select-set selected-set) + (if (member conl-fd selected-set) + (call conl-handler) + );; end if + (if (member lhs-fd selected-set) + (call lhs-handler) + );; end if + (if (member con-fd selected-set) + (call con-handler) + );; end if + );; end while + + (return);; end of main program + + (procedure conl-handler) + (accept conl-fd con-fd) + (asgn select-set (cons con-fd select-set)) + (return) + + (procedure con-handler) + (receive con-fd con-handler-message) + (if (equal con-handler-message 'trace) + (send rhs-fd (('cmd . 'trace-request) ('src . myhpid))) + );; end if + (return) + + (procedure lhs-handler) + (receive lhs-fd lhs-handler-message) + (asgn cmd (cdr (assoc 'cmd lhs-handler-message))) + (asgn src (cdr (assoc 'src lhs-handler-message))) + (if (equal cmd 'trace-request) + (if (equal src myhpid) + (send con-fd myhpid) + (send con-fd 'end-of-file) + else + (send rhs-fd (('src . myhpid) + ('dest . src) + ('cmd . 'trace-ack))) + (send rhs-fd lhs-handler-message) + );; end if + else + (if (equal cmd 'trace-ack) + (asgn dest (cdr (assoc 'dest lhs-handler-message))) + (if (not (equal dest myhpid)) + (send rhs-fd lhs-handler-message) + else + (send con-fd src) + );; end if + );; end if + );; end if + (return) + );; uncompiled program + nil + );; compiled program + + 1;; program counter + nil;; xstack + '((lhs-fd . 3) + (rhs-fd . 4) + (conl-fd . 5)) + );; end of pstate + + ;;--------------------------------------------------------- daemon 2 pstate + + (list;; second mpd pstate + + ;; same as first + + '(host2 2) + + (compile-list;; mpd program + '( + (my-hpid myhpid) + (asgn select-set (lhs-fd conl-fd)) + (asgn con-fd -1) + (while 'true + (select select-set selected-set) + (if (member conl-fd selected-set) + (call conl-handler) + );; end if + (if (member lhs-fd selected-set) + (call lhs-handler) + );; end if + (if (member con-fd selected-set) + (call con-handler) + );; end if + );; end while + + (return);; end of main program + + (procedure conl-handler) + (accept conl-fd con-fd) + (asgn select-set (cons con-fd select-set)) + (return) + + (procedure con-handler) + (receive con-fd con-handler-message) + (if (equal con-handler-message 'trace) + (send rhs-fd (('cmd . 'trace-request) ('src . myhpid))) + );; end if + (return) + + (procedure lhs-handler) + (receive lhs-fd lhs-handler-message) + (asgn cmd (cdr (assoc 'cmd lhs-handler-message))) + (asgn src (cdr (assoc 'src lhs-handler-message))) + (if (equal cmd 'trace-request) + (if (equal src myhpid) + (send con-fd myhpid) + (send con-fd 'end-of-file) + else + (send rhs-fd (('src . myhpid) + ('dest . src) + ('cmd . 'trace-ack))) + (send rhs-fd lhs-handler-message) + );; end if + else + (if (equal cmd 'trace-ack) + (asgn dest (cdr (assoc 'dest lhs-handler-message))) + (if (not (equal dest myhpid)) + (send rhs-fd lhs-handler-message) + else + (send con-fd src) + );; end if + );; end if + );; end if + (return) + );; uncompiled program + nil + );; compiled program + + 1;; program counter + nil;; xstack + '((lhs-fd . 3) + (rhs-fd . 4) + (conl-fd . 5)) + );; end of pstate + + ;;---------------------------------------------------------- daemon 3 pstate + + (list;; third mpd pstate + + ;; same as first and second + + '(host3 3) + + (compile-list;; mpd program + '( + (my-hpid myhpid) + (asgn select-set (lhs-fd conl-fd)) + (asgn con-fd -1) + (while 'true + (select select-set selected-set) + (if (member conl-fd selected-set) + (call conl-handler) + );; end if + (if (member lhs-fd selected-set) + (call lhs-handler) + );; end if + (if (member con-fd selected-set) + (call con-handler) + );; end if + );; end while + + (return);; end of main program + + (procedure conl-handler) + (accept conl-fd con-fd) + (asgn select-set (cons con-fd select-set)) + (return) + + (procedure con-handler) + (receive con-fd con-handler-message) + (if (equal con-handler-message 'trace) + (send rhs-fd (('cmd . 'trace-request) ('src . myhpid))) + );; end if + (return) + + (procedure lhs-handler) + (receive lhs-fd lhs-handler-message) + (asgn cmd (cdr (assoc 'cmd lhs-handler-message))) + (asgn src (cdr (assoc 'src lhs-handler-message))) + (if (equal cmd 'trace-request) + (if (equal src myhpid) + (send con-fd myhpid) + (send con-fd 'end-of-file) + else + (send rhs-fd (('src . myhpid) + ('dest . src) + ('cmd . 'trace-ack))) + (send rhs-fd lhs-handler-message) + );; end if + else + (if (equal cmd 'trace-ack) + (asgn dest (cdr (assoc 'dest lhs-handler-message))) + (if (not (equal dest myhpid)) + (send rhs-fd lhs-handler-message) + else + (send con-fd src) + );; end if + );; end if + );; end if + (return) + );; uncompiled program + nil + );; compiled program + + 1;; program counter + nil;; xstack + '((lhs-fd . 3) + (rhs-fd . 4) + (conl-fd . 5)) + );; end of pstate + + ;;---------------------------------------------------- end of pstates + + );; end of pstate-list + + (list;; connection-list + + ;; The three daemons are bidirectionally connected in a ring. + + '(((host1 1) 4 (host2 2) 3) nil nil) + '(((host2 2) 4 (host3 3) 3) nil nil) + '(((host3 3) 4 (host1 1) 3) nil nil) + + '(((host2 2) 3 (host1 1) 4) nil nil) + '(((host3 3) 3 (host2 2) 4) nil nil) + '(((host1 1) 3 (host3 3) 4) nil nil) + + );; end of connections + + (list;; listener-list + + ;; All daemons are listening for connections from consoles. + + '(((host1 1) 5) 2000 nil) + '(((host2 2) 5) 2000 nil) + '(((host3 3) 5) 2000 nil) + + );; end of lstate-list + + nil;; program-list + + ) + ) + +;;-------------------- diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/util.lisp b/books/workshops/2000/lusk-mccune/lusk-mccune-final/util.lisp new file mode 100644 index 0000000..6739d28 --- /dev/null +++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/util.lisp @@ -0,0 +1,116 @@ +(in-package "ACL2") + +;;---------------------------------------- +;; a few generic utilities + +(defmacro boolp (x) + (list 'or (list 'null x) (list 'equal x 't))) + +(defmacro pos-integerp (x) + (list 'and (list 'integerp x) (list '> x 0))) + +(defmacro naturalp (x) + (list 'and (list 'integerp x) (list '>= x 0))) + +(defun natural-listp (x) + (declare (xargs :guard t)) + (cond ((atom x) (null x)) + (t (and (naturalp (car x)) + (natural-listp (cdr x)))))) + +(defun ith (n lst) ;; counts from 1 + (declare (xargs :guard (naturalp n) + :measure (acl2-count lst))) + (cond ((atom lst) nil) + ((equal n 0) nil) + ((equal n 1) (car lst)) + (t (ith (- n 1) (cdr lst))))) + +(defun update-alist-cdr (key val alist) ;; no-op if the key is not there + (declare (xargs :guard (alistp alist))) + (cond ((atom alist) alist) + ((equal key (caar alist)) (cons (cons key val) (cdr alist))) + (t (cons (car alist) (update-alist-cdr key val (cdr alist)))))) + +(defun update-alist-member (key mem alist) ;; no-op if the key is not there + (declare (xargs :guard (and (alistp alist) + (consp mem)))) + (cond ((atom alist) alist) + ((equal key (caar alist)) (cons mem (cdr alist))) + (t (cons (car alist) (update-alist-member key mem (cdr alist)))))) + +(defmacro update-first (l x) + (list 'cons x (list 'cdr l))) + +(defmacro update-second (l x) + (list 'cons (list 'car l) (list 'cons x (list 'cddr l)))) + +(defmacro update-third (l x) + (list 'cons + (list 'car l) + (list 'cons (list 'cadr l) (list 'cons x (list 'cdddr l))))) + +(defmacro update-fourth (l x) + (list 'cons + (list 'car l) + (list 'cons + (list 'cadr l) + (list 'cons (list 'caddr l) (list 'cons x (list 'cddddr l)))))) + +(defmacro update-fifth (l x) + (list 'cons + (list 'car l) + (list 'cons + (list 'cadr l) + (list 'cons + (list 'caddr l) + (list 'cons + (list 'cadddr l) + (list 'cons x (list 'cddddr (list 'cdr l)))))))) + +(defun update-ith (l i x) ;; this counts from 1 + (declare (xargs :guard (and (true-listp l) + (integerp i)))) + (cond ((atom l) l) + ((equal i 1) (cons x (cdr l))) + (t (cons (car l) (update-ith (cdr l) (- i 1) x))))) + +;;----------------------------------- + +(defun max-in-natural-listp (l) + (declare (xargs :guard (natural-listp l))) + (cond ((atom l) -1) + (t (max (nfix (car l)) (max-in-natural-listp (cdr l)))))) + +(defun gen-natural (l) + (declare (xargs :guard (natural-listp l))) + (+ 1 (max-in-natural-listp l))) + +(defthm gen-natural-naturalp + (naturalp (gen-natural lst))) + +(defun gen-pos-integer (l) + (declare (xargs :guard (natural-listp l))) + (let ((n (+ 1 (max-in-natural-listp l)))) + (if (equal n 0) 1 n))) + +(defthm gen-pos-integer-pos-integerp + (pos-integerp (gen-pos-integer lst))) + +;; We'll probably need to prove something like the following. +;; +;; (defthm gen-natural-not-in-list +;; (implies (natural-listp l) +;; (not (member-equal (gen-natural l) l)))) + +(in-theory (disable gen-natural gen-pos-integer)) + +;;----------------------------------- + +(defun intersect-equal (a b) + (declare (xargs :guard (and (true-listp a) + (true-listp b)))) + (cond ((atom a) nil) + ((member-equal (car a) b) (cons (car a) (intersect-equal (cdr a) b))) + (t (intersect-equal (cdr a) b)))) + |