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