Each client, possibly, has its own cached copy of the memory line. When the client needs to access a line not in its cache, it requests the main memory for shared access or exclusive access depending on whether the client needs to read-only access or read-write access. When done with using it, the client releases the memory.
We have proved that if a client has exclusive access then no other client can have the same line in shared or exclusive mode. This is an important correctness property. The predicates used were manually generated.
(murphi-program (constant-decls ;; Message types (EMPTY 0) (REQ-SHARED 1) (REQ-EXCLUSIVE 2) (INVALIDATE 3) (GRANT-SHARED 4) (GRANT-EXCLUSIVE 5) (INVALIDATE-ACK 6) ;; Cache states (INVALID 7) (SHARED 8) (EXCLUSIVE 9) ;; Abstract Home State (INITIAL 10) (INVALIDATING 11) (RESPONDING 12) (UNDEFINED 13)) (deftype client-type rat) (input (client client-type) (client1 client-type)) (global-state ;; Message channel (channel1 (array rat client-type)) (channel2-4 (array rat client-type)) (channel3 (array rat client-type)) ;; cache state (cache (array rat client-type)) ;; Data structures for home node (home-sharer-list (array bool client-type)) (home-invalidate-list (array bool client-type)) (home-exclusive-granted bool) (home-current-command rat) (home-current-client client-type) ;; Used in the proof (a client-type) (owner client-type) ;; Initialization (empty-array (array rat client-type)) (invalid-array (array rat client-type)) (false-array (array bool client-type)) ;; Phase (phase rat)) (axiom (forall (x client-type) (and (= (aref empty-array x) EMPTY) (= (aref invalid-array x) INVALID) (not (aref false-array x))))) ;; Init rule (initialize (progn (setq channel1 empty-array) (setq channel2-4 empty-array) (setq channel3 empty-array) (setq cache invalid-array) (setq home-sharer-list false-array) (setq home-invalidate-list false-array) (setq home-exclusive-granted false) (setq home-current-command EMPTY) (setq phase INITIAL))) (rules ;; Request shared (==> (and (= (aref cache client) INVALID) (= (aref channel1 client) EMPTY)) (setq (aref channel1 client) REQ-SHARED)) ;; Request exclusive (==> (and (or (= (aref cache client) INVALID) (= (aref cache client) SHARED)) (= (aref channel1 client) EMPTY)) (setq (aref channel1 client) REQ-EXCLUSIVE)) ;; Home node receives request (==> (and (= home-current-command EMPTY) (/= (aref channel1 client) EMPTY) (forall (x client-type) (not (aref home-sharer-list x)))) (progn (setq home-current-command (aref channel1 client)) (setq home-current-client client) (setq home-invalidate-list home-sharer-list) (ite (= (aref channel1 client) REQ-SHARED) (ite home-exclusive-granted (setq phase INVALIDATING) (setq phase RESPONDING)) (ite (= (aref channel1 client) REQ-EXCLUSIVE) (setq phase RESPONDING) (setq phase INITIAL))) (setq (aref channel1 client) EMPTY))) (==> (and (= home-current-command EMPTY) (/= (aref channel1 client) EMPTY) (aref home-sharer-list client1)) (progn (setq home-current-command (aref channel1 client)) (setq home-current-client client) (setq home-invalidate-list home-sharer-list) (ite (= (aref channel1 client) REQ-SHARED) (ite home-exclusive-granted (setq phase INVALIDATING) (setq phase RESPONDING)) (ite (= (aref channel1 client) REQ-EXCLUSIVE) (setq phase INVALIDATING) (setq phase INITIAL))) (setq (aref channel1 client) EMPTY))) ;; Home sends INVALIDATE (==> (and (= (aref channel2-4 client) EMPTY) (aref home-invalidate-list client) (or (= home-current-command REQ-EXCLUSIVE) (and (= home-current-command REQ-SHARED) home-exclusive-granted))) (progn (setq (aref channel2-4 client) INVALIDATE) (setq (aref home-invalidate-list client) false))) ;; Home receives INVALIDATE-ACK and removes node from sharer list (==> (and (/= home-current-command EMPTY) (= (aref channel3 client) INVALIDATE-ACK) (/= client1 client) (aref home-sharer-list client1)) (progn (setq (aref home-sharer-list client) false) (setq home-exclusive-granted false) (setq (aref channel3 client) EMPTY) (ite (= home-current-command REQ-EXCLUSIVE) (setq phase INVALIDATING) (setq phase RESPONDING)))) (==> (and (/= home-current-command EMPTY) (= (aref channel3 client) INVALIDATE-ACK) (forall (x client-type) (=> (/= x client) (not (aref home-sharer-list x))))) (progn (setq (aref home-sharer-list client) false) (setq home-exclusive-granted false) (setq (aref channel3 client) EMPTY) (setq phase RESPONDING))) ;; Client gets INVALIDATE and relinquishes the cache line. Also sends an ;; INVALIDATE-ACK to the home node (==> (and (= (aref channel2-4 client) INVALIDATE) (= (aref channel3 client) EMPTY)) (progn (setq (aref channel2-4 client) EMPTY) (setq (aref channel3 client) INVALIDATE-ACK) (setq (aref cache client) INVALID))) ;; Client gets shared access (==> (= (aref channel2-4 client) GRANT-SHARED) (progn (setq (aref cache client) SHARED) (setq (aref channel2-4 client) EMPTY))) ;; Client gets exclusive access (==> (= (aref channel2-4 client) GRANT-EXCLUSIVE) (progn (setq (aref cache client) EXCLUSIVE) (setq (aref channel2-4 client) EMPTY))) ;; Home gives shared access to client (==> (and (= home-current-command REQ-SHARED) (not home-exclusive-granted) (= (aref channel2-4 home-current-client) EMPTY)) (progn (setq (aref home-sharer-list home-current-client) true) (setq home-current-command EMPTY) (setq (aref channel2-4 home-current-client) GRANT-SHARED) (setq phase INITIAL))) ;; Home gives exclusive access to client (==> (and (= home-current-command REQ-EXCLUSIVE) (= (aref channel2-4 home-current-client) EMPTY) (forall (i client-type) (not (aref home-sharer-list i)))) (progn (setq (aref home-sharer-list home-current-client) true) (setq home-current-command EMPTY) (setq owner home-current-client) (setq home-exclusive-granted true) (setq (aref channel2-4 home-current-client) GRANT-EXCLUSIVE) (setq phase INITIAL)))) ;; The invariant to prove (invariant (=> (= (aref cache a) EXCLUSIVE) (forall (x client-type) (=> (/= x a) (= (aref cache x) INVALID))))) (abstraction (INV0 (forall (x client-type) (or (= (aref channel1 x) EMPTY) (= (aref channel1 x) REQ-SHARED) (= (aref channel1 x) REQ-EXCLUSIVE)))) (INV1 (forall (x client-type) (or (= (aref channel2-4 x) EMPTY) (= (aref channel2-4 x) INVALIDATE) (= (aref channel2-4 x) GRANT-SHARED) (= (aref channel2-4 x) GRANT-EXCLUSIVE)))) (INV2 (forall (x client-type) (or (= (aref channel3 x) EMPTY) (= (aref channel3 x) INVALIDATE-ACK)))) (INV3 (forall (x client-type) (or (= (aref cache x) INVALID) (= (aref cache x) SHARED) (= (aref cache x) EXCLUSIVE)))) ;; Home's view (HOME-EXCL-GRANTED home-exclusive-granted) (HOME-EMP (= home-current-command EMPTY)) (HOME-SHAR (= home-current-command REQ-SHARED)) (HOME-EXCL (= home-current-command REQ-EXCLUSIVE)) (H@INIT (= phase INITIAL)) (H@INVA (= phase INVALIDATING)) (H@RESP (= phase RESPONDING)) ;; (=> H@INIT (and HOME-EMP B0)) (B0 (forall (x client-type) (and (/= (aref channel2-4 x) INVALIDATE) (= (aref channel3 x) EMPTY)))) ;; (=> H@INVA (and B1 (not HOME-EMP) (=> HOME-SHAR HOME-EXCL-GRANTED))) (B1 (forall (x client-type) (and (=> (aref home-invalidate-list x) (aref home-sharer-list x)) (<=> (aref home-invalidate-list x) (and (or (and (/= (aref cache x) INVALID) (/= (aref channel2-4 x) INVALIDATE)) (= (aref channel2-4 x) GRANT-SHARED) (= (aref channel2-4 x) GRANT-EXCLUSIVE)) (= (aref channel3 x) EMPTY)))))) ;; (=> H@RESP (and B2 (not HOME-EMP) (=> HOME-SHAR (not HOME-EXCL-GRANTED)))) (B2 (forall (x client-type) (and (=> (aref home-invalidate-list x) (aref home-sharer-list x)) (/= (aref channel2-4 x) INVALIDATE) (= (aref channel3 x) EMPTY) (=> (= home-current-command REQ-EXCLUSIVE) (not (aref home-sharer-list x)))))) (B3 (forall (x client-type) (= (ite (aref home-sharer-list x) (ite home-exclusive-granted EXCLUSIVE SHARED) INVALID) (ite (= (aref channel3 x) INVALIDATE-ACK) (ite (and (= (aref channel2-4 x) EMPTY) (= (aref cache x) INVALID)) (ite home-exclusive-granted EXCLUSIVE SHARED) UNDEFINED) (ite (= (aref channel2-4 x) EMPTY) (aref cache x) (ite (and (= (aref channel2-4 x) INVALIDATE) (= (aref cache x) SHARED)) SHARED (ite (and (= (aref channel2-4 x) INVALIDATE) (= (aref cache x) EXCLUSIVE)) EXCLUSIVE (ite (and (/= (aref cache x) EXCLUSIVE) (= (aref channel2-4 x) GRANT-SHARED)) SHARED (ite (and (= (aref cache x) INVALID) (= (aref channel2-4 x) GRANT-EXCLUSIVE)) EXCLUSIVE UNDEFINED))))))))) (B31 (=> home-exclusive-granted (and (aref home-sharer-list owner) (forall (x client-type) (=> (/= x owner) (not (aref home-sharer-list x))))))) (B4 (forall (x client-type) (=> (and (= home-current-command EMPTY) (/= (aref channel1 x) EMPTY)) (= phase INITIAL)))) (B5 (forall (x client-type) (=> (or (and (= (aref channel2-4 x) EMPTY) (aref home-invalidate-list x) (or (= home-current-command REQ-EXCLUSIVE) (and (= home-current-command REQ-SHARED) home-exclusive-granted))) (and (/= home-current-command EMPTY) (= (aref channel3 x) INVALIDATE-ACK)) (and (= (aref channel2-4 x) INVALIDATE) (= (aref channel3 x) EMPTY))) (= phase INVALIDATING)))) (B6 (forall (x client-type) (=> (or (and (= home-current-command REQ-SHARED) (not home-exclusive-granted) (= (aref channel2-4 home-current-client) EMPTY)) (and (= home-current-command REQ-EXCLUSIVE) (= (aref channel2-4 home-current-client) EMPTY) (forall (i client-type) (not (aref home-sharer-list i))))) (= phase RESPONDING)))) ))