#| (DEFPKG "M4" (set-difference-equal (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<) (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)) '(PC PROGRAM PUSH POP REVERSE STEP ++))) ; % v25 < apprentice.script >& apprentice.log & ; Time: 5945.74 seconds (prove: 5661.91, print: 273.01, other: 10.82) ; caerlaverock% ls -l apprentice.log ; -rw-r----- 1 moore prof 61686851 Oct 21 16:18 apprentice.log ; JSM Sep 30, 2000 - 2-thread version ; JSM Oct 7, 2000 - n-thread version ; JSM Oct 21, 2000 - version described in proofs.tex Acknowledgements: I started by working on a two thread version of this theorem with the intention of stopping there. But later I decided to go to an unbounded number of threads. The comments below are about the two thread version. George wrote M4 and the system below. He then made several useful suggestions for simplifying his original code. The most important was to rearrange the code sequence (load job1) (invokevirtual "Job" "start" 0) (load job2) (invokevirtual "Job" "start" 0) to (load job2) (load job1) (invokevirtual "Job" "start" 0) (invokevirtual "Job" "start" 0) In retrospect this is not a big deal and could be easily dealt with. But at the time I was doing the proof I just couldn't stand the idea of carrying more invariants further into the ``pre-*s1*'' state. Pete helped me clarify my thoughts after three days of struggle. He also contributed the idea of using computation to define the invariant. I didn't use his idea as fully here as he thinks it could be used, but I used it to great and beneficial effect in the ``bootstrapping'' proof here, i.e., in proving that the first 25 states are ok. Timesheet: I started on this task on Saturday, Sep 23. I spent two and a half frustrating days before asking Pete and George for some time together. My problem was that I had tried to tackle the good-state invariant without wanting to say everything I actually knew. I should have known better. On Monday night I didn't work on it. On Tuesday I taught and started defining good-state as it exists below. I completed good-state on Wednesday and began exploring ways to control the proof of the good-state invariance through step. The work I did on Wednesday was largely irrelevant because I had not seen the simplicity of doing a case for each of th=0,1,2, and other. I was proving many theorems about parts of good-state. On Thursday and Friday I was with Legato. On Friday night I saw to do the th case split and I also figured out the stage hack. On Saturday Sep 30, I got the proof done, working about 8 hours. I presented the two thread proof to the ACL2 research seminar on Wednesday, Oct 4. At that seminar it became clear that the two thread version could yield to a finite state exploration. In fact, Pete used ACL2 to prove the two thread version within a day or two of when I did, above. At the seminar I realized that an unbounded number of threads would not be significantly harder. Indeed, I had by then gotten a clear view of the big picture. Therefore, on Saturday, Oct 7, I worked several hours on it, while also working on other things. On Sunday, Oct 8, I spent another 6 hours and finished. |# (in-package "M4") (include-book "m4") (include-book "watchlog") ; (acl2::divert) ; uncomment this and you cand do % watchlog foo ; in another shell and watch the progress. But divert isn't ; an embedded event so you can't certify this file with it in it. ; There is a matching undivert at the end. ; In this file we exhibit two M4 initial states. When run, both ; create a new object, called a Container, with a field named ; "counter" initialized to 0. Then both run two threads of class ; "Job" named job1 and job2 (which happen to get those thread numbers) ; and then enter an infinite loop. Each of the two jobs infinitely ; repeats the following loop: get the value of the counter (i.e., push ; the value onto the job's local stack), increment it by one, and ; put it back into the counter field. ; The difference between the two M4 states is that in one the two jobs ; use monitorenter and monitorexit to obtain exclusive rights to the ; counter and in the other they do not. The first state is called the ; ``synchronized state'' and is the value of the constant *a0*. The ; other is the ``non-synchronized state'' and is *ns0*. ; Thus, running with an arbitrary schedule in starting from *a0* we ; will see the counter monotonically increase in value. But there are ; schedules for which *ns0* will make the counter sometimes ; decrease in value. For example, suppose job2 is run until it ; obtains and increments the value of the counter but suppose that ; job1 is then run for a long time and increments the counter many ; times. Then when job2 is scheduled again it will write its now ; out-dated value to the counter, decreasing its value from the high ; created by job1. (defconst *sync-class-table* (make-class-def (list (make-class-decl "Container" '("Object") '("counter") '()) (make-class-decl "Job" '("Thread" "Object") '("x" "objref") '(("incr" () nil (load this) (getfield "Job" "objref") (store temp) (load temp) (monitorenter) (load this) (getfield "Job" "objref") (load this) (getfield "Job" "objref") (getfield "Container" "counter") (push 1) (add) (putfield "Container" "counter") (load temp) (monitorexit) (load this) (xreturn)) ("run" () nil (load this) (invokevirtual "Job" "incr" 0) (goto -1)) ("setref" (r) nil (load this) (load r) (putfield "Job" "objref") (return)) ))))) (defconst *nosync-class-table* (make-class-def (list (make-class-decl "Container" '("Object") '("counter") '()) (make-class-decl "Job" '("Thread" "Object") '("x" "objref") '(("incr" () nil (load this) (getfield "Job" "objref") (load this) (getfield "Job" "objref") (getfield "Container" "counter") (push 1) (add) (putfield "Container" "counter") (load this) (xreturn)) ("run" () nil (load this) (invokevirtual "Job" "incr" 0) (goto -1)) ("setref" (r) nil (load this) (load r) (putfield "Job" "objref") (return)) ))))) (defconst *main* '((new "Container") ;;; 0 (store container) ;;; 1 (new "Job") ;;; 2 (store job) ;;; 3 (load job) ;;; 4 (load container) ;;; 5 (invokevirtual "Job" "setref" 1) ;;; 6 (load job) ;;; 7 (invokevirtual "Job" "start" 0) ;;; 8 (goto -7))) ;;; 9 (defconst *a0* (make-state (make-tt (push (make-frame 0 '((container . nil) (job . nil)) nil *main* 'UNLOCKED) nil)) nil *sync-class-table*)) (defconst *incr* (method-program (assoc-equal "incr" (class-decl-methods (assoc-equal "Job" (class-table *a0*)))))) (defconst *run* (method-program (assoc-equal "run" (class-decl-methods (assoc-equal "Job" (class-table *a0*)))))) (defconst *setref* (method-program (assoc-equal "setref" (class-decl-methods (assoc-equal "Job" (class-table *a0*)))))) (defconst *ns0* (make-state (make-tt (push (make-frame 0 '((container . nil) (job . nil)) nil *main* 'UNLOCKED) nil)) nil *nosync-class-table*)) (defmacro gf (class field i heap) `(binding ,field (binding ,class (binding ,i ,heap)))) (defun counter (s) (gf "Container" "counter" 0 (heap s))) ; So here is a theorem illustrating that the counter value might decrease in ; the *ns0* run. (defun start-two-jobs () ; This is just enough to start two jobs. (ack0 25)) (defun position-job2-to-write-a-1 () ; This schedule (when run after both jobs have been started) leaves ; job2 about to write a 1 to the counter value. That is, it grabs the ; initial counter value, 0, increments it on its local stack, and is ; poised to write it back to the counter field when we stop. (ack2 2 (+ 2 ; to execute the first two instructions in the run method 7 ; to grab counter and increment it locally. ) nil)) (defun let-job1-count-up-to-4 () ; This schedule (when run after the two above) leaves the counter with ; value 4. This is done by running job1 through four calls of incr. (ack1 (+ 2 10 2 10 2 10 2 10))) (defun let-job2-write-its-1 () ; This schedule (when run after the two above) leaves the counter with ; value 4. This is done by running job1 through four calls of incr. '(2)) (defun bad-schedule () (append (start-two-jobs) (position-job2-to-write-a-1) (let-job1-count-up-to-4) (let-job2-write-its-1))) (defun bad-n () (- (len (bad-schedule)) 1)) (defun firstn (n lst) (if (zp n) nil (cons (car lst) (firstn (- n 1) (cdr lst))))) (defun runn (n schedule s) (run (firstn n schedule) s)) (defthm snosync-may-decrease-counter (and (equal (counter (runn (bad-n) (bad-schedule) *ns0*)) 4) (equal (counter (runn (+ (bad-n) 1) (bad-schedule) *ns0*)) 1)) :rule-classes nil) ; The theorem we will prove is shown below. ; (defthm s0-increases-counter-monotonically ; (implies (and (integerp n) ; (<= 0 n) ; (integerp m) ; (<= n m)) ; (<= (counter (runn n any-schedule *a0*)) ; (counter (runn m any-schedule *a0*))))) ; Proof. ; Let alpha be the first n elements of any-schedule. Let beta be ; the next m-n elements. Then the conclusion above is equivalent to ; (<= (counter (run alpha *a0*)) ; (counter (run beta (run alpha *a0*)))) ; Suppose (good-state s) is a predicate with the property that ; [1] (good-state *a0*) ; [2] (good-state s) -> (good-state (step s th)) ; [3] (good-state s) -> (<= (counter s) (counter (step s th))) ; Then it is easy to get ; [4] (good-state (run alpha *a0*)) ; [5] (good-state s) -> (<= (counter s) (counter (run beta s))) ; and thus our main theorem. ; Q.E.D. ; The key is thus the definition of good-state to have properties ; [1]-[3]. The proof of [1] will be by computation. ; The combination of [2] and [3] is the lemma ; (defthm good-state-invariant ; (implies (good-state s) ; (and (good-state (step s th)) ; (<= (counter s) (counter (step s th)))))) ; below. It will be proved in three parts. Lemma0 is ; good-state-invariant for th = 0, where the main program is running. ; Lemma1 is good-state-invariant for a scheduled thread th, 0 < th < ; (len (heap s)). These are the threads running Jobs. Lemma2 is ; good-state-invariant for an unscheduled thread th. Together these ; three lemmas establish good-state-invariant. ; A look at the actual statement of lemma0, lemma1, and lemma2 ; below reveals that they are not quite of the form claimed above. ; Their conclusions are wrapped up in functions which are disabled and ; about which a few lemmas have been proved. This ugly aspect of our ; proof addresses the hardest problem we had to face in mechanically ; checking this proof: how to stage the simplifier so as to control the ; case splitting. Our strategy is: ; (a) expand (good-state s) in the hypothesis so as to develop each of ; the possible cases. ; (b) when that stabilizes for a given case, expand (step s th) to ; symbolically compute the next state for the case in question. ; (c) when the next state is stable, expand the good-state predicate on ; and see that it is t. ; This is just symbolic evaluation, but carefully staged. A typical ; one of these proofs generates over 3000 cases when done this way. ; Unguided expansion just blows up. ; =========================================================================== ; Basic Utilities (include-book "/projects/acl2/v2-5-debian-gnu-linux/books/arithmetic/top-with-meta" ;"/projects/acl2/v2-5/books/arithmetic/top-with-meta" ) (defthm len-bind (implies (alistp alist) (equal (len (bind x v alist)) (if (bound? x alist) (len alist) (+ 1 (len alist)))))) (defthm assoc-equal-bind (equal (assoc-equal x (bind y v alist)) (if (equal x y) (cons x v) (assoc-equal x alist)))) (defthm nth-add1! (implies (and (integerp n) (<= 0 n)) (equal (nth (+ 1 n) lst) (nth n (cdr lst))))) (defthm alistp-bind (implies (alistp alist) (alistp (bind x v alist)))) (defthm do-inst-opener (implies (syntaxp (quotep inst)) (equal (do-inst inst s th) (CASE (OP-CODE INST) (PUSH (EXECUTE-PUSH INST S TH)) (POP (EXECUTE-POP INST S TH)) (LOAD (EXECUTE-LOAD INST S TH)) (STORE (EXECUTE-STORE INST S TH)) (ADD (EXECUTE-ADD INST S TH)) (SUB (EXECUTE-SUB INST S TH)) (MUL (EXECUTE-MUL INST S TH)) (GOTO (EXECUTE-GOTO INST S TH)) (IFEQ (EXECUTE-IFEQ INST S TH)) (IFLT (EXECUTE-IFLT INST S TH)) (IFGT (EXECUTE-IFGT INST S TH)) (INVOKEVIRTUAL (EXECUTE-INVOKEVIRTUAL INST S TH)) (RETURN (EXECUTE-RETURN INST S TH)) (XRETURN (EXECUTE-XRETURN INST S TH)) (NEW (EXECUTE-NEW INST S TH)) (GETFIELD (EXECUTE-GETFIELD INST S TH)) (PUTFIELD (EXECUTE-PUTFIELD INST S TH)) (MONITORENTER (EXECUTE-MONITORENTER INST S TH)) (MONITOREXIT (EXECUTE-MONITOREXIT INST S TH)) (HALT S) (OTHERWISE S)))) :hints (("Goal" :in-theory (disable EXECUTE-PUSH EXECUTE-POP EXECUTE-LOAD EXECUTE-STORE EXECUTE-ADD EXECUTE-SUB EXECUTE-MUL EXECUTE-GOTO EXECUTE-IFEQ EXECUTE-IFLT EXECUTE-IFGT EXECUTE-INVOKEVIRTUAL EXECUTE-RETURN EXECUTE-XRETURN EXECUTE-NEW EXECUTE-GETFIELD EXECUTE-PUTFIELD EXECUTE-MONITORENTER EXECUTE-MONITOREXIT)))) (in-theory (disable do-inst)) (defthm step-opener (implies (syntaxp (and (quotep th) (integerp (cadr th)))) (equal (step s th) (IF (EQUAL (CALL-STACK-STATUS S TH) 'SCHEDULED) (DO-INST (NEXT-INST S TH) S TH) S)))) (in-theory (disable step)) (defthm run-opener (and (implies (endp schedule) (equal (run schedule s) s)) (equal (run (cons th schedule) s) (run schedule (step s th))))) (defthm run-append (equal (run (append a b) s) (run b (run a s)))) (in-theory (disable run)) ; Finally, we develop a basic inductive invariant method of proving ; properties. ; Suppose we can invent a predicate, psi, such that ; psi1: (psi s) -> (psi (step s th) ; and ; psi2: (psi s) -> (counter s) <= (counter (step s th)) ; Then clearly ; (psi s0) -> (counter s0) <= (counter (run schedule s0)) ; Here is an encapsulation of that argument. (encapsulate ((psi (s) t)) (local (defun psi (s) (declare (ignore s)) nil)) (defthm psi1 (implies (psi s) (psi (step s th)))) (defthm psi2 (implies (psi s) (<= (counter s) (counter (step s th)))) :rule-classes :linear)) (defthm psi-run1 (implies (psi s) (psi (run schedule s))) :hints (("Goal" :in-theory (set-difference-theories (enable run) '(counter))))) (defthm psi-run2 (implies (psi s) (<= (counter s) (counter (run schedule s)))) :rule-classes :linear :hints (("Goal" :in-theory (set-difference-theories (enable run) '(counter))))) (defthm psi-main (implies (psi s0) (<= (counter (run alpha s0)) (counter (run beta (run alpha s0))))) :hints (("Goal" :in-theory (disable counter))) :rule-classes nil) ; =========================================================================== ; Now I will define the good states. ; In my original proof I used naked cars and cdrs to access the ; components of frames, stacks, etc. But when I wrote the paper, I ; did not want to write deep car/cdr nests. So I will define the ; concepts as macros so they expand as before (thereby not affecting ; the proof in the slightest) while allowing me to write more ; perspicuously for the cadadar challenged. ; My plan is to start by defining the good threads but without stating ; the constraints on the heap that are implicit in the various pcs. ; Then I will define the good heaps and use the basic case analysis ; developed for the threads. (defun good-setref-frame (i frame) (let ((pc (pc frame)) (locals (locals frame)) (stack (stack frame)) (program (program frame)) (flg (sync-flg frame))) (and (equal program *setref*) (equal locals `((THIS REF ,i) (R REF 0))) (equal flg 'UNLOCKED) (case pc (0 (equal stack nil)) (1 (equal stack `((REF ,i)))) (2 (equal stack `((REF 0) (REF ,i)))) (3 t) (t nil))))) (defun good-main-frame (i frame activep) ; i is the number of the last item in the heap. I won't attempt to ; constrain the heap in this function. (let* ((pc (pc frame)) (locals (locals frame)) (stack (stack frame)) (program (program frame)) (flg (sync-flg frame)) (container (binding 'CONTAINER locals)) (job (binding 'JOB locals))) (and (equal program *main*) (equal flg 'UNLOCKED) (case pc (0 (and activep (equal stack nil))) (1 (and activep (equal stack '((REF 0))))) (2 (and activep (equal stack nil) (equal container '(REF 0)))) (3 (and activep (equal stack `((REF ,i))) (equal container '(REF 0)))) (4 (and activep (equal stack nil) (equal container '(REF 0)) (equal job `(REF ,i)))) (5 (and activep (equal stack `(,job)) (equal container '(REF 0)) (equal job `(REF ,i)))) (6 (and activep (equal stack `((REF 0) ,job)) (equal container '(REF 0)) (equal job `(REF ,i)))) (7 (and (equal stack nil) (equal container '(REF 0)) (equal job `(REF ,i)))) (8 (and activep (equal stack `(,job)) (equal container '(REF 0)) (equal job `(REF ,i)))) (9 (and activep (equal stack nil) (equal container '(REF 0)))) (t nil))))) (defun thread-no (thread) (nth 0 thread)) (defun thread-call-stack (thread) (nth 1 thread)) (defun thread-status (thread) (nth 2 thread)) (defun thread-rref (thread) (nth 3 thread)) (defun frame0 (cs) (first cs)) (defun frame1 (cs) (second cs)) (defun good-thread0 (thread i) (let ((n (thread-no thread)) (cs (thread-call-stack thread)) (status (thread-status thread)) (rref (thread-rref thread))) (and (equal n 0) (equal status 'SCHEDULED) (equal rref nil) (cond ((endp cs) nil) ((equal (program (frame0 cs)) *setref*) (and (good-setref-frame i (frame0 cs)) (not (endp (cdr cs))) (good-main-frame i (frame1 cs) nil))) (t (good-main-frame i (frame0 cs) t)))))) (defun good-objrefs (threads heap-pairs except-last-flg) ; Initially, threads is the cdr of the thread table and heap-pairs is ; the cdr of the heap. We walk down both of them. They must be the ; same length. Let the car of threads be (i call-stack status rref) ; and let the car of heap-pairs be (j . (("Job" ("x" . 0) ("objref" ; . ref0)) ...)). Then we insist that ; * i = j (the thread number is the same as the heap address of the ; object representing the thread in this system) ; * rref = (REF j), and ; * ref0 = (REF 0) (with the exception noted below). ; If except-last-flg is t, then if this is the last item in the heap ; we insist that ref0 = 0, instead of (REF 0) as above. (cond ((endp heap-pairs) (endp threads)) ((endp threads) nil) (t (let* ((threadi (car threads)) (i (thread-no threadi)) (rref (thread-rref threadi)) (j (car (car heap-pairs))) (obj (cdr (car heap-pairs)))) (and (equal i j) (equal rref `(REF ,j)) (equal obj (if (and (endp (cdr heap-pairs)) except-last-flg) '(("Job" ("x" . 0) ("objref" . 0)) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0))) '(("Job" ("x" . 0) ("objref" . (REF 0))) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0))))) (good-objrefs (cdr threads) (cdr heap-pairs) except-last-flg)))))) (defun good-heap (tt heap) ; Tt is the thread table of a state and heap is the heap. We ; determine whether the heap is consistent with the thread table. We ; assume we know that thread 0 is good wrt the length of heap. We do ; not enforce here any of the monitor/mcount invariants on (REF 0) in ; the heap, because they are entirely determined by the details of the ; Job threads. (let* ((thread0 (first tt)) (n0 (thread-no thread0)) (frame0 (frame0 (thread-call-stack thread0)))) (and (alistp heap) (equal n0 0) (cond ((equal (program frame0) *setref*) ; We've executed main down to the setref (so we are at pc 7 in main ; but perhaps have not yet moved (REF 0) into the "objref" field of ; the last thread created. We will have set the "objref" field ; properly if we are at pc 3 in the setref and otherwise the field ; will still be 0. (and (consp heap) (equal (car (car heap)) 0) (consp (cdr heap)) (good-objrefs (cdr tt) (cdr heap) (not (equal (pc frame0) 3))))) ((equal (pc frame0) 0) (equal heap nil)) (t (and (consp heap) (equal (car (car heap)) 0) (case (pc frame0) (1 (equal (cdr heap) nil)) (2 (good-objrefs (cdr tt) (cdr heap) nil)) (3 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) t))) (4 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) t))) (5 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) t))) (6 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) t))) (7 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) nil))) (8 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) nil))) (9 (and (not (endp (cdr heap))) (good-objrefs (cdr tt) (cdr heap) nil))) (t nil)))))))) (defun good-class-table (ct) (equal ct *sync-class-table*)) (defun good-run-frame (th frame activep monitor mcount) (let ((pc (pc frame)) (locals (locals frame)) (stack (stack frame)) (program (program frame)) (flg (sync-flg frame))) (and (equal program *run*) (equal locals `((THIS . (REF ,th)))) (equal flg 'UNLOCKED) (if activep (or (equal mcount 0) (not (equal monitor th))) t) (case pc (0 (and activep (equal stack nil))) (1 (and activep (equal stack `((REF ,th))))) (2 (if activep (equal stack `((REF ,th))) (equal stack nil))) (t nil))))) (defun object-lockedp (th monitor mcount) (and (equal mcount 1) (equal th monitor))) (defun good-incr-frame (th frame counter monitor mcount) ; In this system it happens that the heap address of the THIS object ; of every invocation of the "incr" method is always the same as ; the number of thread, th, in which that method is running. So ; I use th above for both. (let ((pc (pc frame)) (locals (locals frame)) (stack (stack frame)) (program (program frame)) (flg (sync-flg frame)) (self `(REF ,th))) (and (equal program *incr*) (equal flg 'UNLOCKED) (case pc (0 (and (equal locals `((THIS . ,self))) (or (equal mcount 0) (not (equal monitor th))) (equal stack nil))) (1 (and (equal locals `((THIS . ,self))) (or (equal mcount 0) (not (equal monitor th))) (equal stack `(,self)))) (2 (and (equal locals `((THIS . ,self))) (equal stack '((REF 0))) (or (equal mcount 0) (not (equal monitor th))))) (3 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (equal stack nil) (or (equal mcount 0) (not (equal monitor th))))) (4 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (equal stack '((REF 0))) (or (equal mcount 0) (not (equal monitor th))))) (5 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack nil))) (6 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack `(,self)))) (7 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack '((REF 0))))) (8 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack `(,self (REF 0))))) (9 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack '((REF 0) (REF 0))))) (10 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack `(,counter (REF 0))))) (11 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack `(1 ,counter (REF 0))))) (12 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack `(,(+ 1 counter) (REF 0))))) (13 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack nil))) (14 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (object-lockedp th monitor mcount) (equal stack '((REF 0))))) (15 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (or (equal mcount 0) (not (equal monitor th))) (equal stack nil))) (16 (and (equal locals `((THIS . ,self) (TEMP . (REF 0)))) (or (equal mcount 0) (not (equal monitor th))) (equal stack `(,self)))) (t nil))))) (defun good-thread (th scheduled thread counter monitor mcount) (let ((n (thread-no thread)) (cs (thread-call-stack thread)) (status (thread-status thread)) (rref (thread-rref thread))) (and (equal n th) (equal status scheduled) (equal rref `(REF ,th)) (cond ((equal scheduled 'UNSCHEDULED) ; This used to be (equal cs `((0 ((THIS REF ,th)) NIL ,*run* UNLOCKED)))) ; but that doesn't capture the constraints on the monitor and mcount (and (good-run-frame th (frame0 cs) t monitor mcount) (null (cdr cs)))) ((endp cs) nil) ((equal (program (frame0 cs)) *incr*) (and (good-incr-frame th (frame0 cs) counter monitor mcount) (not (endp (frame0 cs))) (good-run-frame th (frame1 cs) nil monitor mcount))) (t (good-run-frame th (frame0 cs) t monitor mcount)))))) (defun good-threads (i threads counter monitor mcount except-last-flg) (declare (xargs :measure (acl2-count threads))) (cond ((endp threads) t) (t (and (good-thread i (if (and (endp (cdr threads)) except-last-flg) 'unscheduled 'scheduled) (car threads) counter monitor mcount) (good-threads (+ 1 i) (cdr threads) counter monitor mcount except-last-flg))))) (defun good-thread-table (tt i counter monitor mcount) (let* ((thread0 (first tt)) (frame0 (frame0 (thread-call-stack thread0)))) (and (alistp tt) (equal (thread-no thread0) 0) (good-thread0 thread0 i) (if (and (equal (program frame0) *main*) ; main pc = 0 or 1 (<= (pc frame0) 1)) ; no other threads to check. (equal (cdr tt) nil) (good-threads 1 (cdr tt) counter monitor mcount (or (equal (program frame0) *setref*) ; main pc = 7 (case (pc frame0) ; main pc (0 nil) (1 nil) (2 nil) (3 t) (4 t) (5 t) (6 t) (7 t) (8 t) (t nil)))))))) ; pc=9 (defun good-state (s) (let ((counter (gf "Container" "counter" 0 (heap s))) (monitor (gf "Object" "monitor" 0 (heap s))) (mcount (gf "Object" "mcount" 0 (heap s)))) (and (good-class-table (class-table s)) (good-thread-table (thread-table s) (- (len (heap s)) 1) counter monitor mcount) (good-heap (thread-table s) (heap s)) ; We must know the monitor is some existing thread, else a thread ; can come into existence owning the lock! (or (equal (heap s) nil) (if (equal mcount 0) (equal monitor 0) (and (equal mcount 1) (< 0 monitor) (< monitor (len (heap s))))))))) ; We wish to prove: ; (implies (good-state s) ; (and (good-state (step s th)) ; (<= (counter s) ; (counter (step s th))))) ; My basic strategy will be to prove three cases: ; th = 0 ; 1 <= th < (len (thread-table s)) ; other ; Consider one of these three theorems, e.g., the one for 0. I wish to ; avoid simplifying (step s 0) twice. I will do this by defining a ; predicate equivalent to the conclusion above, but one which relates ; two states, s0 and s1, and then I will call that predicate on s and ; (step s 0). This exposes the (step s 0) without exposing the ; good-state inside the predicate. Only after the step has simplified ; will I open up the predicate to expose the good-state and the ; counter question. ; I thus have three basic stages of rewriting: ; (a) simplify the hypothsis good-state, splitting out all the cases. ; (b) simplify the (step s 0) ; (c) simplify the concluding good-state and counter question. ; I will stage these phases by disabling step and good-state ; and proving lemmas that open them up at just the right times. ; I'll note the lemmas when I get to them. (defthm equal-len-0 (equal (equal (len x) 0) (endp x))) (defthm assoc-equal-i-cdr-heap (implies (and (good-threads j tt c m mc flg1) (integerp j) (good-objrefs tt heap flg2)) (equal (ASSOC-EQUAL i heap) (if (and (integerp i) (<= j i) (<= i (- (+ j (len heap)) 1))) (if (and flg2 (equal i (- (+ j (len heap)) 1))) (cons i '(("Job" ("x" . 0) ("objref" . 0)) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0)))) (cons i '(("Job" ("x" . 0) ("objref" REF 0)) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0))))) nil))) :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) (defthm good-objrefs-setref-gen (implies (and (consp heap) (integerp j) (good-threads j tt c m mc flg1) (good-objrefs tt heap t)) (good-objrefs tt (bind (- (+ (len heap) j) 1) '(("Job" ("x" . 0) ("objref" REF 0)) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0))) heap) nil)) :rule-classes nil :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) ; This lemma establishes that when setref writes to the "objref" field, ; we can convert the ``except last'' flag of good-objrefs from t to nil. (defthm good-objrefs-setref (implies (and (consp heap) (good-threads 1 tt c m mc flg1) (good-objrefs tt heap t)) (good-objrefs tt (bind (len heap) '(("Job" ("x" . 0) ("objref" REF 0)) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0))) heap) nil)) :hints (("Goal" :use ((:instance good-objrefs-setref-gen (j 1)))))) ; We now prove a symmetric lemma that says when we allocate a new thread ; and a new object in the heap we can convert the flag from nil to t. (defthm good-objrefs-new-thread (implies (and (integerp j) (good-threads j tt c m mc flg1) (good-objrefs tt heap nil)) (good-objrefs (bind (+ j (len heap)) (list cs 'unscheduled (list 'ref (+ j (len heap)))) tt) (bind (+ j (len heap)) '(("Job" ("x" . 0) ("objref" . 0)) ("Thread") ("Object" ("monitor" . 0) ("mcount" . 0) ("wait-set" . 0))) heap) t)) :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) (defthm good-threads-new-thread (implies (and (integerp j) (good-threads j tt c m mc nil) (good-objrefs tt heap flg) (< m (+ j (len heap)))) (good-threads j (bind (+ j (len heap)) (list `((0 ((THIS REF ,(+ j (len heap)))) NIL ,*run* UNLOCKED)) 'unscheduled (list 'ref (+ j (len heap)))) tt) c m mc t)) :hints (("Goal" :in-theory (disable good-incr-frame ;good-run-frame )))) ; If (REF 0) is on top of the stack of frame0 then the top of the ; stack of frame0 is (REF 0). Duh. (defthm little-lemma1 (implies (EQUAL (CADDAR (CADAAR S)) ; stack of frame 0 (LIST '(REF 0) (CDR (ASSOC-EQUAL 'JOB (CADADR (CADAAR S)))))) (equal (CAADDR (CAADAR (CAR S))) '(REF 0)))) (defthm rreftothread-good-threads (implies (and (good-threads j tt c m mc flg1) (integerp j)) (equal (rreftothread ref tt) (if (and (consp ref) (equal (car ref) 'REF) (null (cddr ref))) (let ((i (cadr ref))) (if (and (integerp i) (<= j i) (<= i (- (+ j (len tt)) 1))) i NIL)) nil))) :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) (defthm len-thread-table-len-heap-gen (implies (and (integerp j) (good-threads j tt c m mc flg1) (good-objrefs tt heap flg2)) (equal (len tt) (len heap))) :rule-classes nil :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) ; This looks scary because the len expression is replaced by something ; bigger. But I want to think in terms of the length of the heap, not ; the length of the thread table. (defthm len-thread-table-len-heap (implies (and (good-threads 1 (cdar s) c m mc flg1) (good-objrefs (cdar s) (cdadr s) flg2)) (equal (len (cdar s)) (len (cdadr s)))) :hints (("Goal" :use ((:instance len-thread-table-len-heap-gen (j 1) (tt (cdar s)) (heap (cdadr s))))))) (defthm good-objrefs-new-schedule (implies (and (good-threads j tt c m mc flg1) (integerp j) (good-objrefs tt heap flg2) (integerp th) (<= j th) (<= th (- (+ j (len tt)) 1))) (good-objrefs (bind th (list (cadr (assoc-equal th tt)) 'SCHEDULED (cadddr (assoc-equal th tt))) tt) heap flg2)) :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) (defthm good-threads-new-schedule-gen (implies (and (good-threads j tt c m mc t) (consp heap) (integerp j) (good-objrefs tt heap flg2)) (good-threads j (bind (- (+ (len heap) j) 1) (list (cadr (assoc-equal (- (+ (len heap) j) 1) tt)) 'SCHEDULED (cadddr (assoc-equal (- (+ (len heap) j) 1) tt))) tt) c m mc nil)) :rule-classes nil :hints (("Goal" :in-theory (disable good-incr-frame ; good-run-frame )))) (defthm good-threads-new-schedule (implies (and (good-threads 1 tt c m mc t) (consp heap) (good-objrefs tt heap flg2) (force (equal n (len heap)))) (good-threads 1 (bind n (list (cadr (assoc-equal n tt)) 'SCHEDULED (cadddr (assoc-equal n tt))) tt) c m mc nil)) :hints (("Goal" :use ((:instance good-threads-new-schedule-gen (j 1)))))) (defthm nth-0 (equal (nth 0 x) (car x))) (in-theory (disable nth)) ; (acl2::divert) (in-theory (disable step-opener)) ; The next two defthms stage the opening of step and good-state. ; The hyp of the first lemma is totally irrelevant but causes the ; lemma not to fire until we've gotten certain hypotheses free and ; clear in the goal. (defthm step-opener-x0 (implies (alistp s1) (equal (step s th) (if (equal (call-stack-status s th) 'scheduled) (do-inst (next-inst s th) s th) s))) :hints (("Goal" :use step-opener))) (defthm good-state-opener-x0 (equal (good-state (list (cons (cons 0 thread) tt) heap classt)) (let ((counter (gf "Container" "counter" 0 heap)) (monitor (gf "Object" "monitor" 0 heap)) (mcount (gf "Object" "mcount" 0 heap))) (and (good-class-table classt) (good-thread-table (cons (cons 0 thread) tt) (- (len heap) 1) counter monitor mcount) (good-heap (cons (cons 0 thread) tt) heap) (OR (EQUAL heap NIL) (IF (EQUAL MCOUNT 0) (EQUAL MONITOR 0) (AND (EQUAL MCOUNT 1) (< 0 MONITOR) (< MONITOR (LEN heap)))))))) :hints (("Goal" :in-theory (disable good-class-table good-thread-table good-heap)))) (in-theory (disable good-state)) (defthm lemma0 (implies (good-state s) (and (good-state (step s 0)) (<= (counter s) (counter (step s 0))))) :hints (("Goal" :expand (good-state s) :in-theory (cons 'step-opener-x0 (disable good-incr-frame good-run-frame lookup-method)))) :rule-classes nil) (in-theory (disable step-opener-x0 good-state-opener-x0)) ; (acl2::undivert) ; We next deal with stepping an arbitrary Job, i.e, a thread th such ; that 1<= th < (len (heap s)). ; Suppose we know (good-state s). Now how do we open up (step s th)? ; We need to get ; (good-thread i ; (if (and (endp (cdr tt)) ; except-last-flg) ; 'unscheduled ; 'scheduled) ; (car tt) ; counter monitor mcount) ; appropriately instantiated and into the theorem. Then we need ; to get it splattered open. (defthm good-threads-step (implies (and (case-split (good-thread th 'SCHEDULED (cons th thread) c m mc)) (integerp i) (good-threads i tt c m mc flg) (equal (cadr (binding th tt)) 'SCHEDULED)) (good-threads i (bind th thread tt) c m mc flg)) :hints (("Goal" :in-theory (disable good-run-frame good-incr-frame)))) (defthm good-objrefs-step (implies (and (equal (caddr thread) (cons 'ref (cons th nil))) (assoc-equal th tt) (good-objrefs tt heap flg)) (good-objrefs (bind th thread tt) heap flg))) ; The proof of lemma1 raises the case that (equal th ) and ; because th is a variable, it is replaced everywhere by . I ; don't want that to happen because its harder for me to read. So I ; shut off object-lockedp after proving this little theorem. ; Object-lockedp was invented just to hide the (equal th monitor). (defthm object-lockedp-opener-1 (implies (equal th thmon) (equal (object-lockedp th thmon 1) t))) (defthm object-lockedp-opener-2 (implies (not (equal th thmon)) (equal (object-lockedp th thmon 1) nil))) (defthm object-lockedp-opener-3 (equal (object-lockedp th1 th2 0) nil)) (in-theory (disable object-lockedp)) ; Free-var below prevents frequent tries. (defthm assoc-equal-non-nil (implies (and (equal (car (assoc-equal free-th (cdar s))) th) (syntaxp (equal free-th th)) (equal free-th th) (integerp th)) (assoc-equal th (cdar s)))) (defthm lookup-method-incr (implies (and (equal ct *sync-class-table*) (force (equal class "Job"))) (equal (lookup-method "incr" class ct) '("incr" () nil (LOAD THIS) (GETFIELD "Job" "objref") (STORE TEMP) (LOAD TEMP) (MONITORENTER) (LOAD THIS) (GETFIELD "Job" "objref") (LOAD THIS) (GETFIELD "Job" "objref") (GETFIELD "Container" "counter") (PUSH 1) (ADD) (PUTFIELD "Container" "counter") (LOAD TEMP) (MONITOREXIT) (LOAD THIS) (XRETURN))))) (defthm lookup-method-run (implies (and (equal ct *sync-class-table*) (force (equal class "Job"))) (equal (lookup-method "run" class ct) '("run" () NIL (LOAD THIS) (INVOKEVIRTUAL "Job" "incr" 0) (GOTO -1))))) (in-theory (disable lookup-method)) (defthm good-threads-step-over-monitorenter-lemma1 (implies (and (integerp i) (integerp th) (< th i) (good-threads i tt c 0 0 flg)) (good-threads i tt c th 1 flg)) :hints (("Goal" :in-theory (enable object-lockedp)))) (defthm good-threads-step-over-monitorenter (implies (and (object-lockedp th thmon 1) (case-split (good-thread th 'SCHEDULED (cons th thread) c thmon 1)) (integerp i) (good-threads i tt c 0 0 flg) (equal (cadr (binding th tt)) 'SCHEDULED)) (good-threads i (bind th thread tt) c thmon 1 flg)) :hints (("Goal" :in-theory (enable object-lockedp)))) (defthm good-threads-step-over-monitorexit-lemma1 (implies (and (integerp i) (integerp th) (< th i) (good-threads i tt c th 1 flg)) (good-threads i tt c 0 0 flg)) :hints (("Goal" :in-theory (enable object-lockedp)))) (defthm good-threads-step-over-monitorexit (implies (and (case-split (good-thread th 'SCHEDULED (cons th thread) c 0 0)) (integerp i) (good-threads i tt c th 1 flg) (equal (cadr (binding th tt)) 'SCHEDULED)) (good-threads i (bind th thread tt) c 0 0 flg)) :hints (("Goal" :in-theory (enable object-lockedp)))) ; Now I need to prove that you can step over the putfield. (defthm good-threads-step-over-putfield-lemma1 (implies (and (integerp i) (integerp th) (< th i) (good-threads i tt c th 1 flg)) (good-threads i tt (+ 1 c) th 1 flg)) :hints (("Goal" :in-theory (enable object-lockedp)))) (defthm good-threads-step-over-putfield (implies (and (object-lockedp th thmon 1) (case-split (good-thread th 'SCHEDULED (cons th thread) (+ 1 c) th 1)) (integerp i) (good-threads i tt c thmon 1 flg) (equal (cadr (binding th tt)) 'SCHEDULED)) (good-threads i (bind th thread tt) (+ 1 c) thmon 1 flg)) :hints (("Goal" :in-theory (enable object-lockedp)))) (defthm last-thread-sometimes-unscheduled-gen (implies (and (integerp i) (consp heap) (good-threads i tt c m mc T) (GOOD-OBJREFS tt heap T)) (EQUAL (CADDR (ASSOC-EQUAL (- (+ i (LEN heap)) 1) tt)) 'unscheduled)) :rule-classes nil) (defthm last-thread-sometimes-unscheduled (implies (and (good-threads 1 tt c m mc T) (consp heap) (GOOD-OBJREFS tt heap T)) (EQUAL (CADDR (ASSOC-EQUAL (LEN heap) tt)) 'unscheduled)) :hints (("Goal" :use ((:instance last-thread-sometimes-unscheduled-gen (i 1)))))) ; (acl2::divert) ; Here are the stage lemmas for lemma1. (defthm step-opener-x1 (implies (and (alistp (cdadr s2)) (syntaxp (equal s2 s))) (equal (step s th) (if (equal (call-stack-status s th) 'scheduled) (do-inst (next-inst s th) s th) s))) :hints (("Goal" :use step-opener))) (defthm good-state-opener-x1 (equal (good-state (list (cons pair (bind th thread tt)) heap classt)) (let ((counter (gf "Container" "counter" 0 heap)) (monitor (gf "Object" "monitor" 0 heap)) (mcount (gf "Object" "mcount" 0 heap))) (and (good-class-table classt) (good-thread-table (cons pair (bind th thread tt)) (- (len heap) 1) counter monitor mcount) (good-heap (cons pair (bind th thread tt)) heap) (OR (EQUAL heap NIL) (IF (EQUAL MCOUNT 0) (EQUAL MONITOR 0) (AND (EQUAL MCOUNT 1) (< 0 MONITOR) (< MONITOR (LEN heap)))))))) :hints (("Goal" :in-theory (cons 'good-state (disable good-class-table good-thread-table good-heap))))) (defthm lemma1 (implies (and (good-state s) (integerp th) (<= 1 th) (< th (len (heap s))) (good-thread th 'scheduled (assoc-equal th (thread-table s)) (gf "Container" "counter" 0 (heap s)) (gf "Object" "monitor" 0 (heap s)) (gf "Object" "mcount" 0 (heap s)))) (and (good-state (step s th)) (<= (counter s) (counter (step s th))))) :rule-classes nil :otf-flg t :hints (("Goal" :expand ((good-state s)) :in-theory (disable good-threads)))) (in-theory (disable step-opener-x1 good-state-opener-x1)) ; (acl2::undivert) (defthm lemma2 (implies (and (good-state s) (not (equal (call-stack-status s th) 'scheduled))) (and (good-state (step s th)) (<= (counter s) (counter (step s th))))) :rule-classes nil :otf-flg t :hints (("Goal" :in-theory (enable step)))) (defthm assoc-equal-th-cdr-thread-table (implies (and (alistp tt) (good-threads j tt c m mc flg1) (integerp j)) (equal (consp (ASSOC-EQUAL th tt)) (and (integerp th) (<= j th) (<= th (- (+ (len tt) j) 1))))) :rule-classes nil :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) (defthm cases-on-th (implies (and (good-state s) (not (equal th 0)) (equal (call-stack-status s th) 'scheduled)) (and (integerp th) (<= 1 th) (< th (len (heap s))))) :rule-classes nil :hints (("Goal" :use (:instance assoc-equal-th-cdr-thread-table (tt (cdr (thread-table s))) (j 1) (c (gf "Container" "counter" 0 (heap s))) (m (gf "Object" "monitor" 0 (heap s))) (mc (gf "Object" "mcount" 0 (heap s))) (flg1 (let* ((THREAD0 (CAR (thread-table s))) (FRAME0 (CAR (CADR THREAD0)))) (OR (EQUAL (CADDDR FRAME0) *SETREF*) (CASE (CAR FRAME0) (0 NIL) (1 NIL) (2 NIL) (3 T) (4 T) (5 T) (6 T) (7 T) (8 T) (T NIL)))))) :in-theory (cons 'good-state (disable good-threads))))) (defthm good-threads-all-lemma (implies (and (good-threads j tt c m mc flg1) (integerp th) (<= j th) (<= th (- (+ (len tt) j) 1)) (integerp j)) (good-thread th (if (and flg1 (equal th (- (+ (len tt) j) 1))) 'unscheduled 'scheduled) (assoc-equal th tt) c m mc)) :rule-classes nil :hints (("Goal" :in-theory (disable good-incr-frame good-run-frame)))) (defthm good-threads-all (implies (and (good-state s) (integerp th) (<= 1 th) (< th (len (heap s)))) (good-thread th (if (and (let* ((THREAD0 (CAR (thread-table s))) (FRAME0 (CAR (CADR THREAD0)))) (OR (EQUAL (CADDDR FRAME0) *SETREF*) (CASE (CAR FRAME0) (0 NIL) (1 NIL) (2 NIL) (3 T) (4 T) (5 T) (6 T) (7 T) (8 T) (T NIL)))) (equal th (- (len (heap s)) 1))) 'unscheduled 'scheduled) (assoc-equal th (thread-table s)) (gf "Container" "counter" 0 (heap s)) (gf "Object" "monitor" 0 (heap s)) (gf "Object" "mcount" 0 (heap s)))) :rule-classes nil :hints (("Goal" :use (:instance good-threads-all-lemma (tt (cdr (thread-table s))) (j 1) (c (gf "Container" "counter" 0 (heap s))) (m (gf "Object" "monitor" 0 (heap s))) (mc (gf "Object" "mcount" 0 (heap s))) (flg1 (let* ((THREAD0 (CAR (thread-table s))) (FRAME0 (CAR (CADR THREAD0)))) (OR (EQUAL (CADDDR FRAME0) *SETREF*) (CASE (CAR FRAME0) (0 NIL) (1 NIL) (2 NIL) (3 T) (4 T) (5 T) (6 T) (7 T) (8 T) (T NIL)))))) :in-theory (cons 'good-state (disable good-threads good-thread))))) (defthm good-thread-unscheduled-means-not-scheduled (implies (good-thread th 'unscheduled thread c m mc) (equal (caddr thread) 'unscheduled))) (defthm good-state-invariant (implies (good-state s) (and (good-state (step s th)) (<= (counter s) (counter (step s th))))) :hints (("Goal" :use (lemma0 lemma1 lemma2 cases-on-th good-threads-all) :in-theory (disable good-thread)))) (defthm good-state-main (<= (counter (run alpha *a0*)) (counter (run beta (run alpha *a0*)))) :hints (("Goal" :in-theory (disable good-state step counter (counter)) :use ((:instance (:functional-instance psi-main (psi good-state)) (s0 *a0*)))))) (defthm run-append-bridge (implies (equal append-a-b (append a b)) (equal (run append-a-b s) (run b (run a s))))) (defthm firstn-append-difference (implies (and (integerp n) (<= 0 n) (integerp m) (<= n m)) (equal (firstn m any-schedule) (append (firstn n any-schedule) (firstn (- m n) (nthcdr n any-schedule))))) :rule-classes nil) (defthm apprentice-monotonicity (implies (and (integerp n) (<= 0 n) (integerp m) (<= n m)) (<= (counter (runn n any-schedule *a0*)) (counter (runn m any-schedule *a0*)))) :hints (("Goal" :in-theory '(runn run-append-bridge good-state-main) :use ((:instance firstn-append-difference))))) ; (acl2::undivert)