(in-package "ACL2")

(include-book "utilities")

; Here is the function that builds a cache system state from a list of
; named caches and a memory:

(defun csys (caches mem)
 (list caches mem))

; And here are the "accessor" functions that decompose such a state into
; its two components.

(defun caches (csys) (car csys))
(defun mem (csys) (cadr csys))

(defthm caches-csys (equal (caches (csys caches mem))
                                 caches))
(defthm mem-csys (equal (mem (csys caches mem)) mem))
                                                           
(in-theory (disable caches mem csys))

(defun good-csysp (csys)
  (and (unique-keysp (caches csys))
       (every-cache-unique-keysp (caches csys))
       (every-cache-okp (caches csys) (mem csys))))

; There are two actions, (READ addr) and (WRITE addr val).

; The Model of a Cache System

; ACL2 requires that we develop functions in a bottom up way.  But to
; see where I'm going, look at run-csys below.

; Do-action takes an action, a cache and a memory.  It does the action
; to the cache and produces three results:
; * the "response" -- the value read or written
; * the new cache
; * a "message" to be sent on the "bus" to memory.  The other caches
;   will snoop this bus.  A message is nil (meaning no message sent),
;   or an action as above.

; Roughly speaking, if the action is READ and we have a valid cache
; line for the addr, we just return the associated val.  If we do not
; have a valid cache line, we get the value from memory and set up a
; valid cache line.  We also send a READ message to memory.  If the
; action is WRITE we return the written value, set up a valid cache
; line, and send the WRITE to memory.

(defun do-action (action cache mem)
  (let ((op (car action))
        (addr (cadr action))
        (val (caddr action)))
    (case op
      (READ
       (let* ((line (fetch addr cache))
              (oldval (car line))
              (validp  (cadr line)))
         (cond
          ((and line validp) (mv oldval cache nil))
          (t (let ((memval (fetch addr mem)))
               (mv memval
                   (deposit addr (list memval t) cache)
                   (list 'READ addr)))))))
      (otherwise ; WRITE
       (mv val
           (deposit addr (list val t) cache)
           (list 'WRITE addr val)))))) 
                 
; To snoop we use the following function, which takes a msg (implicitly
; on the bus) and a cache and computes the cache's new configuration.
; Snooped READs do not change the cache.  Snooped WRITEs invalidate
; previously valid cache lines in the cache.  The nil message is a noop.

(defun snoop (msg cache)
  (cond
   ((null msg) cache)
   (t (let ((op (car msg))
            (addr (cadr msg)))
        (case op
          (READ cache)
          (otherwise ; WRITE
           (let* ((line (fetch addr cache))
                  (val (car line))
                  (validp (cadr line)))
             (cond ((and line validp)
                    (deposit addr (list val nil) cache))
                   (t cache)))))))))

; The next function is a "driver" that just applies the snoop function
; to every cache other than the one that generated the message.  The
; function returns a "copy" of caches with all the other caches
; in their "post-snoop" states.  The cache responsible for the message
; is not changed.

(defun snoop-others (p msg caches)
  (cond ((endp caches) nil)
        ((equal p (caar caches))
         (cons (car caches)
               (snoop-others p msg (cdr caches))))
        (t (cons (cons (car (car caches))
                       (snoop msg (cdr (car caches))))
                 (snoop-others p msg (cdr caches))))))
         
; Here is how memory changes when it gets a message.  READ and nil are
; noops.  WRITE does the appropriate deposit.
 
(defun new-mem (msg mem)
  (cond ((null msg) mem)
        (t
         (let ((op (car msg))
               (addr (cadr msg))
               (val (caddr msg)))
           (case op
             (READ mem)
             (otherwise ; WRITE
              (deposit addr val mem)))))))

; So here is the single stepper.  P is the name of the cache to which
; action is to be done.  Csys is the current cache state.  We 
; * Do the action to the named cache, generating a response, a new
;   cache and a bus message.
; * Let the other caches snoop the message and change themselves
;   accordingly.
; * Add the changed caches to the cache generated by the action.
; * Change memory according to the message.
; * Package up the changed caches and memory into a new csys.
; * Return two results:  the response to the action and the new csys.

(defun step-csys (p action csys)
  (cond
   ((bound p (caches csys))
    (let ((cache (fetch p (caches csys))))
      (mv-let (response cache^ msg)
              (do-action action cache (mem csys))
              (mv response
                  (csys (deposit p
                                 cache^
                                 (snoop-others p
                                               msg
                                               (caches csys)))
                        (new-mem msg (mem csys)))))))
   (t (mv nil csys))))
      
; And to run a sequence of events through a cache system, we step the
; system for the first event and then step the rest.  We return a
; sequence of the generated responses, paired with the names of the
; agent processors (cache's) responding.

(defun run-csys (events csys)
  (cond ((endp events) nil)
        (t (let ((p (car (car events)))
                 (action (cadr (car events))))
             (mv-let (response csys^)
                     (step-csys p action csys)
                     (cons (cons p response)
                           (run-csys (cdr events) csys^)))))))

(in-theory (disable mv-nth))

; The numbers in the comments below indicate the order in which I
; submitted these events.  When a command has more than one number, I
; submitted it multiple times and all but the last one failed.

; 3
(defthm bound-snoop-others
  (iff (bound q (snoop-others p msg caches))
       (bound q caches)))

; 2, 4
(defthm unique-keysp-snoop-others
  (implies (unique-keysp caches)
           (unique-keysp (snoop-others p msg caches))))

; 6
(defthm every-cache-unique-keysp-snoop-others
  (implies (every-cache-unique-keysp caches)
           (every-cache-unique-keysp (snoop-others p msg caches))))

; 8
(defthm every-other-cache-okp-snoop-others-write
  (implies (and (every-cache-unique-keysp caches)
                (every-cache-okp caches mem))
           (every-other-cache-okp p
                                  (snoop-others p
                                                (list 'write addr val)
                                                caches)
                                  (deposit addr val mem))))

; 9
(defthm every-other-cache-okp-snoop-others-read
  (implies (every-cache-okp caches mem)
           (every-other-cache-okp p
                                  (snoop-others p
                                                (list 'read addr)
                                                caches)
                                  mem)))

; 10
(defthm every-other-cache-okp-snoop-others-nil
  (implies (every-cache-okp caches mem)
           (every-other-cache-okp p
                                  (snoop-others p
                                                nil
                                                caches)
                                  mem)))

; Here is the first invariant.
; 1, 5, 7, 11
(defthm good-csysp-preserved-by-step-csys
  (implies (good-csysp csys)
           (good-csysp (mv-nth 1 (step-csys p action csys)))))

; 13
(defthm appropriate-eventsp-snoop-others
  (implies (appropriate-eventsp events caches)
           (appropriate-eventsp events (snoop-others p msg caches))))

; Here is the second invariant.
; 12, 14
(defthm appropriate-eventsp-preserved-by-step-csys
  (implies (appropriate-eventsp events
                                (caches csys))
           (appropriate-eventsp events
                                (caches
                                 (mv-nth 1 (step-csys p action csys))))))