FLASH Cache Coherence Protocol

A fragment of the FLASH cache coherence protocol description for a single memory address. The actions for different memory lines do not interact

The system consists of a directory node 0 and arbitrary number of nodes p (p>0) with caches in state either invalid, shared, or exclusive

For each processing node p, a single variable, network[p] contains a request/reply/forward message for a transaction initiated by p for the memory line. We wish to prove the following invariants:

(murphi-program

;; constant decls
(constant-decls
 (invalid 0)
 (shared 1)
 (exclusive 2)


 (empty 3)
 (get 4)
 (put 5)
 (getx 6)
 (putx 7)
 (shwb 8)
 (fack 9)
 (nak 10)
 (nakc 11)
)


;; global-state
(global-state
 (directory-sh (array bool))
 (directory-ex rat)
 (directory-data rat)
 (directory-pending bool)

 (network-mess (array rat))
 (network-data (array rat))
 (network-proc (array rat))	;; dst for forwarded get getx messages
				;; faked src for fack and shwb
 (network-wb-src rat)
 (network-wb-data rat)

 (request-flag (array bool))
 (cache-state (array rat))
 (cache-data (array rat))

 (aux-proc rat)
 (pmw rat)
) 



;; initialize
(initialize
 (progn
   (setq directory-pending false)
   (setq directory-sh (mwrite directory-sh pmw true false))
   (setq directory-ex 0)	;; 0 means "none", since pid > 0
   (setq network-mess (mwrite network-mess pmw true empty))
   (setq network-proc (mwrite network-proc pmw true 0))
   (setq network-wb-src 0)	;; 0 means "none", since pid > 0
   (setq request-flag (mwrite request-flag pmw true false))
   (setq cache-state (mwrite cache-state pmw true invalid))))

;; Rules
(ruleset (proc-id)   ;; proc-id > 0

  ;; node proc-id sends a request of shared copy to home
  (==>	(and (not (aref request-flag proc-id))
             (= (aref cache-state proc-id) invalid) (> proc-id 0))
	(progn
	  (setq (aref request-flag proc-id) true)
	  (setq (aref network-mess proc-id) get)
	  (setq (aref network-proc proc-id) 0))
  )

  ;; node proc-id sends a request of exclusive copy to home
  (==>	(and (not (aref request-flag proc-id))
	     (or (= (aref cache-state proc-id) invalid)
		 (= (aref cache-state proc-id) shared)) (> proc-id 0))
	(progn
	  (setq (aref request-flag proc-id) true)
	  (setq (aref network-mess proc-id) getx)
	  (setq (aref network-proc proc-id) 0))
  )

  ;; node proc-id sends a request to write back to the main memory
  (==>	(and (= (aref cache-state proc-id) exclusive) (> proc-id 0))

	(progn
	  (setq (aref cache-state proc-id) invalid)
	  (setq network-wb-src proc-id)
	  (setq network-wb-data (aref cache-data proc-id)))
  )

  ;; home processes a get request to generate a put to proc-id
  (==>	(and (= (aref network-mess proc-id) get) (= directory-ex 0) 
	     (not directory-pending) (> proc-id 0))

	(progn
	  (setq (aref network-mess proc-id) put)
	  (setq (aref network-data proc-id) directory-data)
	  (setq (aref directory-sh proc-id) true))
  )

  ;; home forwards a get request to another remote node directory-ex
  (==>	(and (= (aref network-mess proc-id) get) (/= directory-ex 0) 
	     (not directory-pending) (> proc-id 0))

	(progn
	  (setq (aref network-proc proc-id) directory-ex)
	  (setq aux-proc proc-id)
	  (setq directory-pending true))
  )

  ;; home naks a get request to proc-id
  (==>	(and (= (aref network-mess proc-id) get) 
	     directory-pending (> proc-id 0))

	(progn
	  (setq (aref network-mess proc-id) nak))
  )


  ;; home processes a getx request to generate a putx to proc-id
  (==>	(and (= (aref network-mess proc-id) getx) (= directory-ex 0) 
	     (not directory-pending) (> proc-id 0))

	(progn
	  (setq (aref network-mess proc-id) putx)
	  (setq (aref network-data proc-id) directory-data)
	  (setq directory-ex proc-id))
  )

  ;; home forwards a getx request to another remote node directory-ex
  (==>	(and (= (aref network-mess proc-id) getx) (/= directory-ex 0) 
	     (not directory-pending) (> proc-id 0))

	(progn
	  (setq (aref network-proc proc-id) directory-ex)
	  (setq aux-proc proc-id)
	  (setq directory-pending true))
  )

  ;; home naks a getx request to proc-id
  (==>	(and (= (aref network-mess proc-id) getx)
	     directory-pending (> proc-id 0))

	(progn
	  (setq (aref network-mess proc-id) nak))
  )

  ;; a remote node network-proc[proc-id] processes a forwarded get
  ;; to generate a put to the requesting node proc-id
  (==>  (and (= (aref network-mess proc-id) get) 
	     (> (aref network-proc proc-id) 0) (> proc-id 0) 
	     (= (aref cache-state (aref network-proc proc-id)) exclusive))
	
	(progn
	  (setq (aref cache-state (aref network-proc proc-id)) shared)
	  (setq (aref network-mess proc-id) put)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref network-data proc-id) 
		(aref cache-data (aref network-proc proc-id)))
	  (setq (aref network-mess 0) shwb)
	  (setq (aref network-proc 0) proc-id)	;; faked src
	  (setq (aref network-data 0) 
		(aref cache-data (aref network-proc proc-id))))
  )

  ;; a remote node network-proc[proc-id] naks a forwarded get to
  ;; the requesting node proc-id
  (==>  (and (= (aref network-mess proc-id) get) 
	     (> (aref network-proc proc-id) 0) (> proc-id 0) 
	     (/= (aref cache-state (aref network-proc proc-id)) exclusive))
	
	(progn
	  (setq (aref network-mess proc-id) nak)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref network-mess 0) nakc))
  )

  ;; a remote node network-proc[proc-id] processes a forwarded getx
  ;; to generate a putx to the requesting node proc-id
  (==>  (and (= (aref network-mess proc-id) getx)
	     (> (aref network-proc proc-id) 0) (> proc-id 0) 
	     (= (aref cache-state (aref network-proc proc-id)) exclusive))
	
	(progn
	  (setq (aref cache-state (aref network-proc proc-id)) invalid)
	  (setq (aref network-mess proc-id) putx)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref network-data proc-id) 
		(aref cache-data (aref network-proc proc-id)))
	  (setq (aref network-mess 0) fack)
	  (setq (aref network-proc 0) proc-id))	;; faked src
  )

  ;; a remote node network-proc[proc-id] naks a forwarded get to
  ;; the requesting node proc-id
  (==>  (and (= (aref network-mess proc-id) getx)
	     (> (aref network-proc proc-id) 0) (> proc-id 0) 
	     (/= (aref cache-state (aref network-proc proc-id)) exclusive))
	
	(progn
	  (setq (aref network-mess proc-id) nak)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref network-mess 0) nakc))
  )

  ;; requesting node proc-id processes nak reply
  (==>	(and (= (aref network-mess proc-id) nak) (> proc-id 0))
	
	(progn
	  (setq (aref network-mess proc-id) empty)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref request-flag proc-id) false))
  )

  ;; requesting node proc-id processes put reply
  (==>	(and (= (aref network-mess proc-id) put) (> proc-id 0))
	
	(progn
	  (setq (aref network-mess proc-id) empty)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref request-flag proc-id) false)
	  (setq (aref cache-state proc-id) shared)
	  (setq (aref cache-data proc-id) (aref network-data proc-id)))
  )

  ;; requesting node proc-id processes putx reply
  (==>	(and (= (aref network-mess proc-id) putx) (> proc-id 0))
	
	(progn
	  (setq (aref network-mess proc-id) empty)
	  (setq (aref network-proc proc-id) 0)
	  (setq (aref request-flag proc-id) false)
	  (setq (aref cache-state proc-id) exclusive)
	  (setq (aref cache-data proc-id) (aref network-data proc-id)))
  )

  ;; home processes a write-back request
     ;; if we don't have enough instantiations (other than proc-id),
     ;; we need additional condition (= directory-ex proc-id) i.e., /= p!1
  (==>	(and (= network-wb-src proc-id) (> proc-id 0))
	
	(progn
	  (setq network-wb-src 0)
	  (setq directory-data network-wb-data)
	  (setq directory-ex 0))
  )

  ;; home processes shwb
  (==>  (= (aref network-mess 0) shwb)

	(progn
	  (setq (aref directory-sh directory-ex) true) 
	  (setq (aref directory-sh (aref network-proc 0)) true) 
	  (setq (aref network-mess 0) empty)
	  (setq (aref network-proc 0) 0)
	  (setq directory-pending false)
	  (setq directory-ex 0)
	  (setq directory-data (aref network-data 0)))
  )

  ;; home processes fack
  (==>  (= (aref network-mess 0) fack)

	(progn
	  (setq directory-pending false)
	  (setq directory-ex (aref network-proc 0))
	  (setq (aref network-mess 0) empty)
	  (setq (aref network-proc 0) 0))
  )

  ;; home processes nakc
  (==>  (= (aref network-mess 0) nakc)

	(progn
	  (setq (aref network-mess 0) empty)
	  (setq (aref network-proc 0) 0)
	  (setq directory-pending false))
  )
) ; end of ruleset


;; The invariant
;(invariant
;   (forall (pid) 
;	(and (or (/= (aref cache-state pid) exclusive)
;	         (/= (aref network-mess pid) putx))
;	     (=> (or (= (aref cache-state pid) exclusive)
;	             (= (aref network-mess pid) putx))
;		 (= pid (ite (= (aref network-mess 0) fack)
;		 	     (aref network-proc 0) directory-ex)))))
;)


(invariant 
  (and 	(or Pending No3HopRep2Home)
        (=> DirectoryNoEx NoEx)
        01Ex1  01Ex2 
        01Fwd
        WB
        ReqFlag
  )
)

(abstraction
   (Pending directory-pending)
   (Fack2Home  (= (aref network-mess 0) fack))
   (ShWB2Home  (= (aref network-mess 0) shwb))
   (NoFackShWB2Home (= (aref network-proc 0) 0))
   (No3HopRep2Home (= (aref network-mess 0) empty))

   (DirectoryNoEx (= directory-ex 0))
   
   (NoEx (forall (pid) (and (/= (aref cache-state pid) exclusive)
			    (/= (aref network-mess pid) putx))))

   (NoFwdReq (forall (pid)
             (not (and (> pid 0) 
                       (or (= (aref network-mess pid) get)
			   (= (aref network-mess pid) getx))
                       (> (aref network-proc pid) 0)))))

   (NoFwd (forall (pid) (not (and (> pid 0) (> (aref network-proc pid) 0)))))

   (01Fwd (forall (pid) (=> (and (> pid 0) (> (aref network-proc pid) 0))
			   (= pid aux-proc))))

   (01Ex1 (forall (pid) 
  	     (or (/= (aref cache-state pid) exclusive)
	         (/= (aref network-mess pid) putx))))
   (01Ex2 (forall (pid)
	     (=> (or (= (aref cache-state pid) exclusive)
	             (= (aref network-mess pid) putx))
		 (= pid (ite (= (aref network-mess 0) fack)
		 	     (aref network-proc 0) directory-ex)))))

   (ReqFlag (forall (pid) (=> (> pid 0) 
				  (or (aref request-flag pid)
				      (= (aref network-mess pid) empty)))))

   (WB (forall (pid) (=> (or (= (aref cache-state pid) exclusive)
			     (= (aref network-mess pid) putx)
			     (= (aref network-mess 0) shwb)
			     (= directory-ex 0))
			 (= network-wb-src 0))))

) ;; end of abstraction

(partition
  (Pending No3HopRep2Home DirectoryNoEx NoFackShWB2Home Fack2Home ShWB2Home
   NoEx NoFwd NoFwdReq 01Fwd 01Ex1 01Ex2 ReqFlag WB))

) ;; end of murphi-program

Satyaki Das
Last modified: Wed May 7 15:30:21 PDT 2003