IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, VOL. 13, NO. 6,
`%(cid:31)(cid:31)(cid:31) 01(cid:30)2(cid:1)(cid:30)(cid:21)0%32(cid:1) 32 (cid:23)(cid:30)1(cid:30)44(cid:31)4 (cid:30)2(cid:24) (cid:24)%(cid:1)01%(cid:14)50(cid:31)(cid:24) (cid:1)6(cid:1)0(cid:31)(cid:18)(cid:1)(cid:27) (cid:12)34(cid:26) 78(cid:27) 23(cid:26) ,(cid:27)
`
`JUNE 2002
`(cid:25)52(cid:31) 9::9
`
`1
`
`1
`7
`
`(cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:7)(cid:5)(cid:8)(cid:9) (cid:10)(cid:8)(cid:11) (cid:12)(cid:3)(cid:13)(cid:5)(cid:6)(cid:7)(cid:5)(cid:8)(cid:9) (cid:10) (cid:14)(cid:13)(cid:15)(cid:10)(cid:11)(cid:4)(cid:10)(cid:16)(cid:17) (cid:10)(cid:8)(cid:11) (cid:10)
`Specifying and Verifying a Broadcast and a
`(cid:18)(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17) (cid:1)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) (cid:21)(cid:10)(cid:4)(cid:22)(cid:3) (cid:21)(cid:15)(cid:22)(cid:3)(cid:13)(cid:3)(cid:8)(cid:4)(cid:3) (cid:23)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20)
`Multicast Snooping Cache Coherence Protocol
`
`(cid:24)(cid:10)(cid:8)(cid:5)(cid:3)(cid:20) (cid:25)(cid:26) (cid:1)(cid:15)(cid:13)(cid:5)(cid:8)(cid:27) (cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:2) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:18)(cid:10)(cid:8)(cid:15)(cid:28) (cid:23)(cid:20)(cid:10)(cid:29)(cid:10)(cid:20)(cid:27) (cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:2) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:30)(cid:8)(cid:8)(cid:3) (cid:31)(cid:26) (cid:21)(cid:15)(cid:8)(cid:11)(cid:15)(cid:8)(cid:27)
`Daniel J. Sorin, Student Member, IEEE, Manoj Plakal, Student Member, IEEE, Anne E. Condon,
`(cid:18)(cid:10)(cid:13)(cid:29) (cid:24)(cid:26) (cid:5)(cid:20)(cid:20)(cid:27) (cid:13)(cid:5)(cid:14)(cid:14)(cid:15)(cid:16)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:18)(cid:5)(cid:20)(cid:15) (cid:18)(cid:26)!(cid:26) (cid:18)(cid:10)(cid:13)(cid:17)(cid:5)(cid:8)(cid:27) (cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:2) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:10)(cid:8)(cid:11)
`Mark D. Hill, Fellow, IEEE, Milo M.K. Martin, Student Member, IEEE, and
`(cid:24)(cid:10)"(cid:5)(cid:11) (cid:30)(cid:26) #(cid:15)(cid:15)(cid:11)(cid:27) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)
`David A. Wood, Member, IEEE
`
`Abstract—In this paper, we develop a specification methodology that documents and specifies a cache coherence protocol in eight
`(cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:7)(cid:4)$%(cid:8) (cid:17)(cid:22)(cid:5)(cid:16) (cid:2)(cid:10)(cid:2)(cid:3)(cid:13)(cid:27) &(cid:3) (cid:11)(cid:3)"(cid:3)(cid:20)(cid:15)(cid:2) (cid:10) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) ’(cid:3)(cid:17)(cid:22)(cid:15)(cid:11)(cid:15)(cid:20)(cid:15)(cid:9)(cid:7) (cid:17)(cid:22)(cid:10)(cid:17) (cid:11)(cid:15)(cid:4)(cid:19)’(cid:3)(cid:8)(cid:17)(cid:16) (cid:10)(cid:8)(cid:11) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:3)(cid:16) (cid:10) (cid:4)(cid:10)(cid:4)(cid:22)(cid:3) (cid:4)(cid:15)(cid:22)(cid:3)(cid:13)(cid:3)(cid:8)(cid:4)(cid:3) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) (cid:5)(cid:8) (cid:3)(cid:5)(cid:9)(cid:22)(cid:17)
`tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a
`(cid:17)(cid:10)((cid:20)(cid:3)(cid:16)) (cid:17)(cid:22)(cid:3) (cid:16)(cid:17)(cid:10)(cid:17)(cid:3)(cid:16)(cid:27) (cid:3)"(cid:3)(cid:8)(cid:17)(cid:16)(cid:27) (cid:10)(cid:4)(cid:17)(cid:5)(cid:15)(cid:8)(cid:16)(cid:27) (cid:10)(cid:8)(cid:11) (cid:17)(cid:13)(cid:10)(cid:8)(cid:16)(cid:5)(cid:17)(cid:5)(cid:15)(cid:8)(cid:16) (cid:15)(cid:6) (cid:17)(cid:22)(cid:3) (cid:4)(cid:10)(cid:4)(cid:22)(cid:3) (cid:10)(cid:8)(cid:11) ’(cid:3)’(cid:15)(cid:13)(cid:7) (cid:4)(cid:15)(cid:8)(cid:17)(cid:13)(cid:15)(cid:20)(cid:20)(cid:3)(cid:13)(cid:16)(cid:26) #(cid:3) (cid:17)(cid:22)(cid:3)(cid:8) (cid:19)(cid:16)(cid:3) (cid:17)(cid:22)(cid:5)(cid:16) ’(cid:3)(cid:17)(cid:22)(cid:15)(cid:11)(cid:15)(cid:20)(cid:15)(cid:9)(cid:7) (cid:17)(cid:15) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:7) (cid:10)
`detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows
`(cid:11)(cid:3)(cid:17)(cid:10)(cid:5)(cid:20)(cid:3)(cid:11)(cid:27) ’(cid:15)(cid:11)(cid:3)(cid:13)(cid:8) (cid:17)(cid:22)(cid:13)(cid:3)(cid:3)*(cid:16)(cid:17)(cid:10)(cid:17)(cid:3) ((cid:13)(cid:15)(cid:10)(cid:11)(cid:4)(cid:10)(cid:16)(cid:17) (cid:16)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) &(cid:5)(cid:17)(cid:22) (cid:10)(cid:8) (cid:19)(cid:8)(cid:15)(cid:13)(cid:11)(cid:3)(cid:13)(cid:3)(cid:11) (cid:11)(cid:10)(cid:17)(cid:10) (cid:8)(cid:3)(cid:17)&(cid:15)(cid:13)(cid:29) (cid:10)(cid:8)(cid:11) (cid:10)(cid:8) (cid:15)(cid:13)(cid:11)(cid:3)(cid:13)(cid:3)(cid:11) (cid:10)(cid:11)(cid:11)(cid:13)(cid:3)(cid:16)(cid:16) (cid:8)(cid:3)(cid:17)&(cid:15)(cid:13)(cid:29) (cid:17)(cid:22)(cid:10)(cid:17) (cid:10)(cid:20)(cid:20)(cid:15)&(cid:16)
`arbitrary skew. We also present a detailed specification of a new protocol called Multicast Snooping [6] and, in doing so, we better
`(cid:10)(cid:13)((cid:5)(cid:17)(cid:13)(cid:10)(cid:13)(cid:7) (cid:16)(cid:29)(cid:3)&(cid:26) #(cid:3) (cid:10)(cid:20)(cid:16)(cid:15) (cid:2)(cid:13)(cid:3)(cid:16)(cid:3)(cid:8)(cid:17) (cid:10) (cid:11)(cid:3)(cid:17)(cid:10)(cid:5)(cid:20)(cid:3)(cid:11) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) (cid:15)(cid:6) (cid:10) (cid:8)(cid:3)& (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) (cid:4)(cid:10)(cid:20)(cid:20)(cid:3)(cid:11) (cid:18)(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17) (cid:1)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) +,- (cid:10)(cid:8)(cid:11)(cid:27) (cid:5)(cid:8) (cid:11)(cid:15)(cid:5)(cid:8)(cid:9) (cid:16)(cid:15)(cid:27) &(cid:3) ((cid:3)(cid:17)(cid:17)(cid:3)(cid:13)
`illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the Multicast
`(cid:5)(cid:20)(cid:20)(cid:19)(cid:16)(cid:17)(cid:13)(cid:10)(cid:17)(cid:3) (cid:17)(cid:22)(cid:3) (cid:19)(cid:17)(cid:5)(cid:20)(cid:5)(cid:17)(cid:7) (cid:15)(cid:6) (cid:17)(cid:22)(cid:3) (cid:17)(cid:10)((cid:20)(cid:3)*((cid:10)(cid:16)(cid:3)(cid:11) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) ’(cid:3)(cid:17)(cid:22)(cid:15)(cid:11)(cid:15)(cid:20)(cid:15)(cid:9)(cid:7)(cid:26) .(cid:5)(cid:8)(cid:10)(cid:20)(cid:20)(cid:7)(cid:27) &(cid:3) (cid:11)(cid:3)’(cid:15)(cid:8)(cid:16)(cid:17)(cid:13)(cid:10)(cid:17)(cid:3) (cid:10) (cid:17)(cid:3)(cid:4)(cid:22)(cid:8)(cid:5)/(cid:19)(cid:3) (cid:6)(cid:15)(cid:13) "(cid:3)(cid:13)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) (cid:15)(cid:6) (cid:17)(cid:22)(cid:3) (cid:18)(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17)
`Snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model.
`(cid:1)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20)(cid:27) (cid:17)(cid:22)(cid:13)(cid:15)(cid:19)(cid:9)(cid:22) (cid:17)(cid:22)(cid:3) (cid:16)(cid:29)(cid:3)(cid:17)(cid:4)(cid:22) (cid:15)(cid:6) (cid:10) ’(cid:10)(cid:8)(cid:19)(cid:10)(cid:20) (cid:2)(cid:13)(cid:15)(cid:15)(cid:6) (cid:17)(cid:22)(cid:10)(cid:17) (cid:17)(cid:22)(cid:3) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) (cid:16)(cid:10)(cid:17)(cid:5)(cid:16)(cid:6)(cid:5)(cid:3)(cid:16) (cid:10) (cid:16)(cid:3)/(cid:19)(cid:3)(cid:8)(cid:17)(cid:5)(cid:10)(cid:20)(cid:20)(cid:7) (cid:4)(cid:15)(cid:8)(cid:16)(cid:5)(cid:16)(cid:17)(cid:3)(cid:8)(cid:17) ’(cid:3)’(cid:15)(cid:13)(cid:7) ’(cid:15)(cid:11)(cid:3)(cid:20)(cid:26)
`
`Index Terms—Cache coherence, protocol specification, protocol verification, memory consistency, multicast snooping.
`(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:13)(cid:11)(cid:5)(cid:14)(cid:3)$(cid:21)(cid:10)(cid:4)(cid:22)(cid:3) (cid:4)(cid:15)(cid:22)(cid:3)(cid:13)(cid:3)(cid:8)(cid:4)(cid:3)(cid:27) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8)(cid:27) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) "(cid:3)(cid:13)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8)(cid:27) ’(cid:3)’(cid:15)(cid:13)(cid:7) (cid:4)(cid:15)(cid:8)(cid:16)(cid:5)(cid:16)(cid:17)(cid:3)(cid:8)(cid:4)(cid:7)(cid:27) ’(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17) (cid:16)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9)(cid:26)
`
`(cid:1)
`
`1
`INTRODUCTION
`(cid:15) (cid:8)(cid:16)(cid:13)(cid:17)(cid:18)(cid:19)(cid:20)(cid:21)(cid:13)(cid:8)(cid:18)(cid:16)
`(cid:1) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11) (cid:12)(cid:13) (cid:3) (cid:13)(cid:2)(cid:4)(cid:5)(cid:14)(cid:5) (cid:15)(cid:6)(cid:7) (cid:2)(cid:6)(cid:6)(cid:7)(cid:16)(cid:12)(cid:8)(cid:3)(cid:10)(cid:12)(cid:8)(cid:17)
`A cache coherence protocol is a scheme for coordinating
`access to shared blocks of memory. Processors and
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:13)(cid:4)(cid:3)(cid:7)(cid:5)(cid:16) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13) (cid:6)(cid:15) (cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20)(cid:21) (cid:22)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:3)(cid:8)(cid:16)
`memories exchange messages to share data and to
`(cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:12)(cid:5)(cid:13) (cid:5)(cid:23)(cid:2)(cid:4)(cid:3)(cid:8)(cid:17)(cid:5) (cid:14)(cid:5)(cid:13)(cid:13)(cid:3)(cid:17)(cid:5)(cid:13) (cid:10)(cid:6) (cid:13)(cid:4)(cid:3)(cid:7)(cid:5) (cid:16)(cid:3)(cid:10)(cid:3) (cid:3)(cid:8)(cid:16) (cid:10)(cid:6)
`determine which processors have read-only or read-write
`(cid:16)(cid:5)(cid:10)(cid:5)(cid:7)(cid:14)(cid:12)(cid:8)(cid:5) (cid:24)(cid:4)(cid:12)(cid:2)(cid:4) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:4)(cid:3)(cid:25)(cid:5) (cid:7)(cid:5)(cid:3)(cid:16)(cid:26)(cid:6)(cid:8)(cid:11)(cid:20) (cid:6)(cid:7) (cid:7)(cid:5)(cid:3)(cid:16)(cid:26)(cid:24)(cid:7)(cid:12)(cid:10)(cid:5)
`access to data blocks that are in their caches. A processor’s
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:16)(cid:3)(cid:10)(cid:3) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3)(cid:7)(cid:5) (cid:12)(cid:8) (cid:10)(cid:4)(cid:5)(cid:12)(cid:7) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5)(cid:13)(cid:21) (cid:1) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:27)(cid:13)
`access to a cache block is determined by the state of that
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:12)(cid:13) (cid:16)(cid:5)(cid:10)(cid:5)(cid:7)(cid:14)(cid:12)(cid:8)(cid:5)(cid:16) (cid:18)(cid:20) (cid:10)(cid:4)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) (cid:6)(cid:15) (cid:10)(cid:4)(cid:3)(cid:10)
`block in its cache, and this state is generally one of the five
`(cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:12)(cid:8) (cid:12)(cid:10)(cid:13) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5)(cid:28) (cid:3)(cid:8)(cid:16) (cid:10)(cid:4)(cid:12)(cid:13) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) (cid:12)(cid:13) (cid:17)(cid:5)(cid:8)(cid:5)(cid:7)(cid:3)(cid:11)(cid:11)(cid:20) (cid:6)(cid:8)(cid:5) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5) (cid:15)(cid:12)(cid:25)(cid:5)
`MOESI
`(Modified, Owned, Exclusive, Shared, Invalid)
`(cid:29)(cid:30)(cid:31) !
`"(cid:29)(cid:6)(cid:16)(cid:12)(cid:15)(cid:12)(cid:5)(cid:16)(cid:28) (cid:30)(cid:24)(cid:8)(cid:5)(cid:16)(cid:28) (cid:31)(cid:23)(cid:2)(cid:11)#(cid:13)(cid:12)(cid:25)(cid:5)(cid:28) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16)(cid:28)
`!(cid:8)(cid:25)(cid:3)(cid:11)(cid:12)(cid:16)$
`states [32]. Processors issue requests, such as Get Exclusive
`(cid:13)(cid:10)(cid:3)(cid:10)(cid:5)(cid:13) %&’((cid:21) (cid:22)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:12)(cid:13)(cid:13)#(cid:5) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)(cid:13)(cid:28) (cid:13)#(cid:2)(cid:4) (cid:3)(cid:13) *(cid:5)(cid:10) (cid:31)(cid:23)(cid:2)(cid:11)#(cid:13)(cid:12)(cid:25)(cid:5)
`or Get-Shared, to gain access to blocks. They can also lose
`(cid:6)(cid:7) *(cid:5)(cid:10)(cid:26) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16)(cid:28) (cid:10)(cid:6) (cid:17)(cid:3)(cid:12)(cid:8) (cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13)(cid:21) +(cid:4)(cid:5)(cid:20) (cid:2)(cid:3)(cid:8) (cid:3)(cid:11)(cid:13)(cid:6) (cid:11)(cid:6)(cid:13)(cid:5)
`access to blocks, either by choice (e.g., a cache replacement)
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13)(cid:28) (cid:5)(cid:12)(cid:10)(cid:4)(cid:5)(cid:7) (cid:18)(cid:20) (cid:2)(cid:4)(cid:6)(cid:12)(cid:2)(cid:5) "(cid:5)(cid:21)(cid:17)(cid:21)(cid:28) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:7)(cid:5)(cid:9)(cid:11)(cid:3)(cid:2)(cid:5)(cid:14)(cid:5)(cid:8)(cid:10)$
`or when another processor’s request steals a block away.
`(cid:6)(cid:7) (cid:24)(cid:4)(cid:5)(cid:8) (cid:3)(cid:8)(cid:6)(cid:10)(cid:4)(cid:5)(cid:7) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:27)(cid:13) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10) (cid:13)(cid:10)(cid:5)(cid:3)(cid:11)(cid:13) (cid:3) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:3)(cid:24)(cid:3)(cid:20)(cid:21)
`Many invalidate protocols maintain the invariant that there
`(cid:29)(cid:3)(cid:8)(cid:20) (cid:12)(cid:8)(cid:25)(cid:3)(cid:11)(cid:12)(cid:16)(cid:3)(cid:10)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:14)(cid:3)(cid:12)(cid:8)(cid:10)(cid:3)(cid:12)(cid:8) (cid:10)(cid:4)(cid:5) (cid:12)(cid:8)(cid:25)(cid:3)(cid:7)(cid:12)(cid:3)(cid:8)(cid:10) (cid:10)(cid:4)(cid:3)(cid:10) (cid:10)(cid:4)(cid:5)(cid:7)(cid:5)
`can either be one writer and no readers or no writer and any
`(cid:2)(cid:3)(cid:8) (cid:5)(cid:12)(cid:10)(cid:4)(cid:5)(cid:7) (cid:18)(cid:5) (cid:6)(cid:8)(cid:5) (cid:24)(cid:7)(cid:12)(cid:10)(cid:5)(cid:7) (cid:3)(cid:8)(cid:16) (cid:8)(cid:6) (cid:7)(cid:5)(cid:3)(cid:16)(cid:5)(cid:7)(cid:13) (cid:6)(cid:7) (cid:8)(cid:6) (cid:24)(cid:7)(cid:12)(cid:10)(cid:5)(cid:7) (cid:3)(cid:8)(cid:16) (cid:3)(cid:8)(cid:20)
`number of readers.
`(cid:8)#(cid:14)(cid:18)(cid:5)(cid:7) (cid:6)(cid:15) (cid:7)(cid:5)(cid:3)(cid:16)(cid:5)(cid:7)(cid:13)(cid:21)
`What is protocol specification? Cache coherence proto-
`(cid:1)(cid:2)(cid:3)(cid:4) (cid:5)(cid:6) (cid:7)(cid:8)(cid:9)(cid:4)(cid:9)(cid:10)(cid:9)(cid:11) (cid:6)(cid:7)(cid:12)(cid:10)(cid:5)(cid:13)(cid:5)(cid:10)(cid:3)(cid:4)(cid:5)(cid:9)(cid:14)(cid:15) ,(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:26)
`cols for shared memory multiprocessors are implemented
`(cid:2)(cid:6)(cid:11)(cid:13) (cid:15)(cid:6)(cid:7) (cid:13)(cid:4)(cid:3)(cid:7)(cid:5)(cid:16) (cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20) (cid:14)#(cid:11)(cid:10)(cid:12)(cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:3)(cid:7)(cid:5) (cid:12)(cid:14)(cid:9)(cid:11)(cid:5)(cid:14)(cid:5)(cid:8)(cid:10)(cid:5)(cid:16)
`via the actions of numerous system components and the
`(cid:25)(cid:12)(cid:3) (cid:10)(cid:4)(cid:5) (cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:6)(cid:15) (cid:8)#(cid:14)(cid:5)(cid:7)(cid:6)#(cid:13) (cid:13)(cid:20)(cid:13)(cid:10)(cid:5)(cid:14) (cid:2)(cid:6)(cid:14)(cid:9)(cid:6)(cid:8)(cid:5)(cid:8)(cid:10)(cid:13) (cid:3)(cid:8)(cid:16) (cid:10)(cid:4)(cid:5)
`interactions between them. These components include
`(cid:12)(cid:8)(cid:10)(cid:5)(cid:7)(cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:18)(cid:5)(cid:10)(cid:24)(cid:5)(cid:5)(cid:8) (cid:10)(cid:4)(cid:5)(cid:14)(cid:21) +(cid:4)(cid:5)(cid:13)(cid:5) (cid:2)(cid:6)(cid:14)(cid:9)(cid:6)(cid:8)(cid:5)(cid:8)(cid:10)(cid:13) (cid:12)(cid:8)(cid:2)(cid:11)#(cid:16)(cid:5)
`cache controllers, directory controllers, and networks,
`(cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7)(cid:13)(cid:28) (cid:16)(cid:12)(cid:7)(cid:5)(cid:2)(cid:10)(cid:6)(cid:7)(cid:20) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7)(cid:13)(cid:28) (cid:3)(cid:8)(cid:16) (cid:8)(cid:5)(cid:10)(cid:24)(cid:6)(cid:7)(cid:19)(cid:13)(cid:28)
`among others. The specification of a cache coherence
`(cid:3)(cid:14)(cid:6)(cid:8)(cid:17) (cid:6)(cid:10)(cid:4)(cid:5)(cid:7)(cid:13)(cid:21) +(cid:4)(cid:5) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5)
`protocol must detail the actions of each of these components
`(cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11) (cid:14)#(cid:13)(cid:10) (cid:16)(cid:5)(cid:10)(cid:3)(cid:12)(cid:11) (cid:10)(cid:4)(cid:5) (cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:6)(cid:15) (cid:5)(cid:3)(cid:2)(cid:4) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5)(cid:13)(cid:5) (cid:2)(cid:6)(cid:14)(cid:9)(cid:6)(cid:8)(cid:5)(cid:8)(cid:10)(cid:13)
`for every combination of state it could be in and event that
`(cid:15)(cid:6)(cid:7) (cid:5)(cid:25)(cid:5)(cid:7)(cid:20) (cid:2)(cid:6)(cid:14)(cid:18)(cid:12)(cid:8)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) (cid:12)(cid:10) (cid:2)(cid:6)#(cid:11)(cid:16) (cid:18)(cid:5) (cid:12)(cid:8) (cid:3)(cid:8)(cid:16) (cid:5)(cid:25)(cid:5)(cid:8)(cid:10) (cid:10)(cid:4)(cid:3)(cid:10)
`could happen. For example,
`it must specify the actions
`(cid:2)(cid:6)#(cid:11)(cid:16) (cid:4)(cid:3)(cid:9)(cid:9)(cid:5)(cid:8)(cid:21) -(cid:6)(cid:7) (cid:5)(cid:23)(cid:3)(cid:14)(cid:9)(cid:11)(cid:5)(cid:28) (cid:12)(cid:10) (cid:14)#(cid:13)(cid:10) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:20) (cid:10)(cid:4)(cid:5) (cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13)
`performed by a cache controller that has Exclusive access to
`(cid:9)(cid:5)(cid:7)(cid:15)(cid:6)(cid:7)(cid:14)(cid:5)(cid:16) (cid:18)(cid:20) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7) (cid:10)(cid:4)(cid:3)(cid:10) (cid:4)(cid:3)(cid:13) (cid:31)(cid:23)(cid:2)(cid:11)#(cid:13)(cid:12)(cid:25)(cid:5) (cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6)
`a cache block when a Get-Shared request for that block
`(cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:24)(cid:4)(cid:5)(cid:8) (cid:3) *(cid:5)(cid:10)(cid:26) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10) (cid:15)(cid:6)(cid:7) (cid:10)(cid:4)(cid:3)(cid:10) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)
`arrives from another node, and it must specify the new state
`(cid:3)(cid:7)(cid:7)(cid:12)(cid:25)(cid:5)(cid:13) (cid:15)(cid:7)(cid:6)(cid:14) (cid:3)(cid:8)(cid:6)(cid:10)(cid:4)(cid:5)(cid:7) (cid:8)(cid:6)(cid:16)(cid:5)(cid:28) (cid:3)(cid:8)(cid:16) (cid:12)(cid:10) (cid:14)#(cid:13)(cid:10) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:20) (cid:10)(cid:4)(cid:5) (cid:8)(cid:5)(cid:24) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5)
`that the cache controller enters.
`(cid:10)(cid:4)(cid:3)(cid:10) (cid:10)(cid:4)(cid:5) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7) (cid:5)(cid:8)(cid:10)(cid:5)(cid:7)(cid:13)(cid:21)
`
`What is protocol verification? Verification of a cache
`(cid:1)(cid:2)(cid:3)(cid:4) (cid:5)(cid:6) (cid:7)(cid:8)(cid:9)(cid:4)(cid:9)(cid:10)(cid:9)(cid:11) (cid:16)(cid:12)(cid:8)(cid:5)(cid:13)(cid:5)(cid:10)(cid:3)(cid:4)(cid:5)(cid:9)(cid:14)(cid:15) .(cid:5)(cid:7)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5)
`coherence protocol
`involves proving that a protocol
`(cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)
`(cid:12)(cid:8)(cid:25)(cid:6)(cid:11)(cid:25)(cid:5)(cid:13) (cid:9)(cid:7)(cid:6)(cid:25)(cid:12)(cid:8)(cid:17) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)
`specification obeys a desired memory consistency model,
`(cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:18)(cid:5)(cid:20)(cid:13) (cid:3) (cid:16)(cid:5)(cid:13)(cid:12)(cid:7)(cid:5)(cid:16) (cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20) (cid:2)(cid:6)(cid:8)(cid:13)(cid:12)(cid:13)(cid:10)(cid:5)(cid:8)(cid:2)(cid:20) (cid:14)(cid:6)(cid:16)(cid:5)(cid:11)(cid:28)
`such as sequential consistency (SC) [21]. To verify that a
`(cid:13)#(cid:2)(cid:4) (cid:3)(cid:13) (cid:13)(cid:5))#(cid:5)(cid:8)(cid:10)(cid:12)(cid:3)(cid:11) (cid:2)(cid:6)(cid:8)(cid:13)(cid:12)(cid:13)(cid:10)(cid:5)(cid:8)(cid:2)(cid:20) " ,$ %’/((cid:21) +(cid:6) (cid:25)(cid:5)(cid:7)(cid:12)(cid:15)(cid:20) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3)
`protocol satisfies a consistency model requires proving that
`(cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11) (cid:13)(cid:3)(cid:10)(cid:12)(cid:13)(cid:15)(cid:12)(cid:5)(cid:13) (cid:3) (cid:2)(cid:6)(cid:8)(cid:13)(cid:12)(cid:13)(cid:10)(cid:5)(cid:8)(cid:2)(cid:20) (cid:14)(cid:6)(cid:16)(cid:5)(cid:11) (cid:7)(cid:5))#(cid:12)(cid:7)(cid:5)(cid:13) (cid:9)(cid:7)(cid:6)(cid:25)(cid:12)(cid:8)(cid:17) (cid:10)(cid:4)(cid:3)(cid:10)
`it obeys certain invariants about what value a load from
`(cid:12)(cid:10) (cid:6)(cid:18)(cid:5)(cid:20)(cid:13) (cid:2)(cid:5)(cid:7)(cid:10)(cid:3)(cid:12)(cid:8) (cid:12)(cid:8)(cid:25)(cid:3)(cid:7)(cid:12)(cid:3)(cid:8)(cid:10)(cid:13) (cid:3)(cid:18)(cid:6)#(cid:10) (cid:24)(cid:4)(cid:3)(cid:10) (cid:25)(cid:3)(cid:11)#(cid:5) (cid:3) (cid:11)(cid:6)(cid:3)(cid:16) (cid:15)(cid:7)(cid:6)(cid:14)
`memory can return. For example, to satisfy SC, the loads
`(cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20) (cid:2)(cid:3)(cid:8) (cid:7)(cid:5)(cid:10)#(cid:7)(cid:8)(cid:21) -(cid:6)(cid:7) (cid:5)(cid:23)(cid:3)(cid:14)(cid:9)(cid:11)(cid:5)(cid:28) (cid:10)(cid:6) (cid:13)(cid:3)(cid:10)(cid:12)(cid:13)(cid:15)(cid:20) ,(cid:28) (cid:10)(cid:4)(cid:5) (cid:11)(cid:6)(cid:3)(cid:16)(cid:13)
`and stores from the different processors must appear to the
`(cid:3)(cid:8)(cid:16) (cid:13)(cid:10)(cid:6)(cid:7)(cid:5)(cid:13) (cid:15)(cid:7)(cid:6)(cid:14) (cid:10)(cid:4)(cid:5) (cid:16)(cid:12)(cid:15)(cid:15)(cid:5)(cid:7)(cid:5)(cid:8)(cid:10) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:14)#(cid:13)(cid:10) (cid:3)(cid:9)(cid:9)(cid:5)(cid:3)(cid:7) (cid:10)(cid:6) (cid:10)(cid:4)(cid:5)
`programmer to be in some total order where 1) the value of
`(cid:9)(cid:7)(cid:6)(cid:17)(cid:7)(cid:3)(cid:14)(cid:14)(cid:5)(cid:7) (cid:10)(cid:6) (cid:18)(cid:5) (cid:12)(cid:8) (cid:13)(cid:6)(cid:14)(cid:5) (cid:10)(cid:6)(cid:10)(cid:3)(cid:11) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7) (cid:24)(cid:4)(cid:5)(cid:7)(cid:5) /$ (cid:10)(cid:4)(cid:5) (cid:25)(cid:3)(cid:11)#(cid:5) (cid:6)(cid:15)
`a load equals the value of the most recent store to the same
`(cid:3) (cid:11)(cid:6)(cid:3)(cid:16) (cid:5))#(cid:3)(cid:11)(cid:13) (cid:10)(cid:4)(cid:5) (cid:25)(cid:3)(cid:11)#(cid:5) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5) (cid:14)(cid:6)(cid:13)(cid:10) (cid:7)(cid:5)(cid:2)(cid:5)(cid:8)(cid:10) (cid:13)(cid:10)(cid:6)(cid:7)(cid:5) (cid:10)(cid:6) (cid:10)(cid:4)(cid:5) (cid:13)(cid:3)(cid:14)(cid:5)
`address in the total order, and 2) the total order respects the
`(cid:3)(cid:16)(cid:16)(cid:7)(cid:5)(cid:13)(cid:13) (cid:12)(cid:8) (cid:10)(cid:4)(cid:5) (cid:10)(cid:6)(cid:10)(cid:3)(cid:11) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7)(cid:28) (cid:3)(cid:8)(cid:16) ’$ (cid:10)(cid:4)(cid:5) (cid:10)(cid:6)(cid:10)(cid:3)(cid:11) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7) (cid:7)(cid:5)(cid:13)(cid:9)(cid:5)(cid:2)(cid:10)(cid:13) (cid:10)(cid:4)(cid:5)
`program order at each of the processors.
`(cid:9)(cid:7)(cid:6)(cid:17)(cid:7)(cid:3)(cid:14) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7) (cid:3)(cid:10) (cid:5)(cid:3)(cid:2)(cid:4) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13)(cid:21)
`Why is verification difficult? At a high level, protocols
`(cid:1)(cid:2)(cid:17) (cid:5)(cid:6) (cid:16)(cid:12)(cid:8)(cid:5)(cid:13)(cid:5)(cid:10)(cid:3)(cid:4)(cid:5)(cid:9)(cid:14) (cid:18)(cid:5)(cid:13)(cid:13)(cid:5)(cid:10)(cid:19)(cid:11)(cid:4)(cid:15) (cid:1)(cid:10) (cid:3) (cid:4)(cid:12)(cid:17)(cid:4) (cid:11)(cid:5)(cid:25)(cid:5)(cid:11)(cid:28) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13)
`can be represented as in Fig. 1, which illustrates the
`(cid:2)(cid:3)(cid:8) (cid:18)(cid:5) (cid:7)(cid:5)(cid:9)(cid:7)(cid:5)(cid:13)(cid:5)(cid:8)(cid:10)(cid:5)(cid:16) (cid:3)(cid:13) (cid:12)(cid:8) -(cid:12)(cid:17)(cid:21) /(cid:28) (cid:24)(cid:4)(cid:12)(cid:2)(cid:4) (cid:12)(cid:11)(cid:11)#(cid:13)(cid:10)(cid:7)(cid:3)(cid:10)(cid:5)(cid:13) (cid:10)(cid:4)(cid:5)
`specification of a cache controller for a three state (Mod-
`(cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7) (cid:15)(cid:6)(cid:7) (cid:3) (cid:10)(cid:4)(cid:7)(cid:5)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) "(cid:29)(cid:6)(cid:16)(cid:26)
`ified, Shared, Invalid) protocol. There are a handful of
`(cid:12)(cid:15)(cid:12)(cid:5)(cid:16)(cid:28) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16)(cid:28) !(cid:8)(cid:25)(cid:3)(cid:11)(cid:12)(cid:16)$ (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:21) +(cid:4)(cid:5)(cid:7)(cid:5) (cid:3)(cid:7)(cid:5) (cid:3) (cid:4)(cid:3)(cid:8)(cid:16)(cid:15)#(cid:11) (cid:6)(cid:15)
`states, with atomic transitions between them.
`(cid:13)(cid:10)(cid:3)(cid:10)(cid:5)(cid:13)(cid:28) (cid:24)(cid:12)(cid:10)(cid:4) (cid:3)(cid:10)(cid:6)(cid:14)(cid:12)(cid:2) (cid:10)(cid:7)(cid:3)(cid:8)(cid:13)(cid:12)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:18)(cid:5)(cid:10)(cid:24)(cid:5)(cid:5)(cid:8) (cid:10)(cid:4)(cid:5)(cid:14)(cid:21)
`Since cache coherence protocols are simply finite state
` (cid:12)(cid:8)(cid:2)(cid:5) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:3)(cid:7)(cid:5) (cid:13)(cid:12)(cid:14)(cid:9)(cid:11)(cid:20) (cid:15)(cid:12)(cid:8)(cid:12)(cid:10)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5)
`machines, it would appear at first glance that it would be
`(cid:14)(cid:3)(cid:2)(cid:4)(cid:12)(cid:8)(cid:5)(cid:13)(cid:28) (cid:12)(cid:10) (cid:24)(cid:6)#(cid:11)(cid:16) (cid:3)(cid:9)(cid:9)(cid:5)(cid:3)(cid:7) (cid:3)(cid:10) (cid:15)(cid:12)(cid:7)(cid:13)(cid:10) (cid:17)(cid:11)(cid:3)(cid:8)(cid:2)(cid:5) (cid:10)(cid:4)(cid:3)(cid:10) (cid:12)(cid:10) (cid:24)(cid:6)#(cid:11)(cid:16) (cid:18)(cid:5)
`easy to specify and verify a common three state (MSI)
`(cid:5)(cid:3)(cid:13)(cid:20) (cid:10)(cid:6) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:20) (cid:3)(cid:8)(cid:16) (cid:25)(cid:5)(cid:7)(cid:12)(cid:15)(cid:20) (cid:3) (cid:2)(cid:6)(cid:14)(cid:14)(cid:6)(cid:8) (cid:10)(cid:4)(cid:7)(cid:5)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) "(cid:29) !$
`broadcast snooping protocol. Unfortunately, at the level of
`(cid:18)(cid:7)(cid:6)(cid:3)(cid:16)(cid:2)(cid:3)(cid:13)(cid:10) (cid:13)(cid:8)(cid:6)(cid:6)(cid:9)(cid:12)(cid:8)(cid:17) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:21) 0(cid:8)(cid:15)(cid:6)(cid:7)(cid:10)#(cid:8)(cid:3)(cid:10)(cid:5)(cid:11)(cid:20)(cid:28) (cid:3)(cid:10) (cid:10)(cid:4)(cid:5) (cid:11)(cid:5)(cid:25)(cid:5)(cid:11) (cid:6)(cid:15)
`detail required for an actual implementation, even see-
`(cid:16)(cid:5)(cid:10)(cid:3)(cid:12)(cid:11) (cid:7)(cid:5))#(cid:12)(cid:7)(cid:5)(cid:16) (cid:15)(cid:6)(cid:7) (cid:3)(cid:8) (cid:3)(cid:2)(cid:10)#(cid:3)(cid:11) (cid:12)(cid:14)(cid:9)(cid:11)(cid:5)(cid:14)(cid:5)(cid:8)(cid:10)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8)(cid:28) (cid:5)(cid:25)(cid:5)(cid:8) (cid:13)(cid:5)(cid:5)(cid:26)
`mingly straightforward protocols have numerous transient
`(cid:14)(cid:12)(cid:8)(cid:17)(cid:11)(cid:20) (cid:13)(cid:10)(cid:7)(cid:3)(cid:12)(cid:17)(cid:4)(cid:10)(cid:15)(cid:6)(cid:7)(cid:24)(cid:3)(cid:7)(cid:16) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:4)(cid:3)(cid:25)(cid:5) (cid:8)#(cid:14)(cid:5)(cid:7)(cid:6)#(cid:13) (cid:10)(cid:7)(cid:3)(cid:8)(cid:13)(cid:12)(cid:5)(cid:8)(cid:10)
`states and possible race conditions that complicate the tasks
`(cid:13)(cid:10)(cid:3)(cid:10)(cid:5)(cid:13) (cid:3)(cid:8)(cid:16) (cid:9)(cid:6)(cid:13)(cid:13)(cid:12)(cid:18)(cid:11)(cid:5) (cid:7)(cid:3)(cid:2)(cid:5) (cid:2)(cid:6)(cid:8)(cid:16)(cid:12)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:10)(cid:4)(cid:3)(cid:10) (cid:2)(cid:6)(cid:14)(cid:9)(cid:11)(cid:12)(cid:2)(cid:3)(cid:10)(cid:5) (cid:10)(cid:4)(cid:5) (cid:10)(cid:3)(cid:13)(cid:19)(cid:13)
`of specification and verification. While older protocols only
`(cid:6)(cid:15) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:3)(cid:8)(cid:16) (cid:25)(cid:5)(cid:7)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8)(cid:21) 1(cid:4)(cid:12)(cid:11)(cid:5) (cid:6)(cid:11)(cid:16)(cid:5)(cid:7) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:6)(cid:8)(cid:11)(cid:20)
`permitted one outstanding miss and required that a request
`(cid:9)(cid:5)(cid:7)(cid:14)(cid:12)(cid:10)(cid:10)(cid:5)(cid:16) (cid:6)(cid:8)(cid:5) (cid:6)#(cid:10)(cid:13)(cid:10)(cid:3)(cid:8)(cid:16)(cid:12)(cid:8)(cid:17) (cid:14)(cid:12)(cid:13)(cid:13) (cid:3)(cid:8)(cid:16) (cid:7)(cid:5))#(cid:12)(cid:7)(cid:5)(cid:16) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)
`and its responses were atomic, current protocols allow
`(cid:3)(cid:8)(cid:16) (cid:12)(cid:10)(cid:13) (cid:7)(cid:5)(cid:13)(cid:9)(cid:6)(cid:8)(cid:13)(cid:5)(cid:13) (cid:24)(cid:5)(cid:7)(cid:5) (cid:3)(cid:10)(cid:6)(cid:14)(cid:12)(cid:2)(cid:28) (cid:2)#(cid:7)(cid:7)(cid:5)(cid:8)(cid:10) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:3)(cid:11)(cid:11)(cid:6)(cid:24)
`transactions to be split and allow multiple outstanding
`(cid:10)(cid:7)(cid:3)(cid:8)(cid:13)(cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:10)(cid:6) (cid:18)(cid:5) (cid:13)(cid:9)(cid:11)(cid:12)(cid:10) (cid:3)(cid:8)(cid:16) (cid:3)(cid:11)(cid:11)(cid:6)(cid:24) (cid:14)#(cid:11)(cid:10)(cid:12)(cid:9)(cid:11)(cid:5) (cid:6)#(cid:10)(cid:13)(cid:10)(cid:3)(cid:8)(cid:16)(cid:12)(cid:8)(cid:17)
`requests. Thus, other requests and responses can be
`(cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)(cid:13)(cid:21) +(cid:4)#(cid:13)(cid:28) (cid:6)(cid:10)(cid:4)(cid:5)(cid:7) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)(cid:13) (cid:3)(cid:8)(cid:16) (cid:7)(cid:5)(cid:13)(cid:9)(cid:6)(cid:8)(cid:13)(cid:5)(cid:13) (cid:2)(cid:3)(cid:8) (cid:18)(cid:5)
`o The authors are with the Computer Sciences Department, University of
`(cid:1) (cid:1)(cid:2)(cid:3) (cid:4)(cid:5)(cid:6)(cid:2)(cid:7)(cid:8)(cid:9) (cid:4)(cid:8)(cid:3) (cid:10)(cid:11)(cid:6)(cid:2) (cid:6)(cid:2)(cid:3) (cid:12)(cid:7)(cid:13)(cid:14)(cid:5)(cid:6)(cid:3)(cid:8) (cid:15)(cid:16)(cid:11)(cid:3)(cid:17)(cid:16)(cid:3)(cid:9) (cid:18)(cid:3)(cid:14)(cid:4)(cid:8)(cid:6)(cid:13)(cid:3)(cid:17)(cid:6)(cid:19) (cid:20)(cid:17)(cid:11)(cid:21)(cid:3)(cid:8)(cid:9)(cid:11)(cid:6)(cid:22) (cid:7)(cid:23)
`interleaved between a request and its response. This
`(cid:12)(cid:8)(cid:10)(cid:5)(cid:7)(ci
`%(cid:31)(cid:31)(cid:31) 01(cid:30)2(cid:1)(cid:30)(cid:21)0%32(cid:1) 32 (cid:23)(cid:30)1(cid:30)44(cid:31)4 (cid:30)2(cid:24) (cid:24)%(cid:1)01%(cid:14)50(cid:31)(cid:24) (cid:1)6(cid:1)0(cid:31)(cid:18)(cid:1)(cid:27) (cid:12)34(cid:26) 78(cid:27) 23(cid:26) ,(cid:27)
`
`JUNE 2002
`(cid:25)52(cid:31) 9::9
`
`1
`
`1
`7
`
`(cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:7)(cid:5)(cid:8)(cid:9) (cid:10)(cid:8)(cid:11) (cid:12)(cid:3)(cid:13)(cid:5)(cid:6)(cid:7)(cid:5)(cid:8)(cid:9) (cid:10) (cid:14)(cid:13)(cid:15)(cid:10)(cid:11)(cid:4)(cid:10)(cid:16)(cid:17) (cid:10)(cid:8)(cid:11) (cid:10)
`Specifying and Verifying a Broadcast and a
`(cid:18)(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17) (cid:1)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) (cid:21)(cid:10)(cid:4)(cid:22)(cid:3) (cid:21)(cid:15)(cid:22)(cid:3)(cid:13)(cid:3)(cid:8)(cid:4)(cid:3) (cid:23)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20)
`Multicast Snooping Cache Coherence Protocol
`
`(cid:24)(cid:10)(cid:8)(cid:5)(cid:3)(cid:20) (cid:25)(cid:26) (cid:1)(cid:15)(cid:13)(cid:5)(cid:8)(cid:27) (cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:2) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:18)(cid:10)(cid:8)(cid:15)(cid:28) (cid:23)(cid:20)(cid:10)(cid:29)(cid:10)(cid:20)(cid:27) (cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:2) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:30)(cid:8)(cid:8)(cid:3) (cid:31)(cid:26) (cid:21)(cid:15)(cid:8)(cid:11)(cid:15)(cid:8)(cid:27)
`Daniel J. Sorin, Student Member, IEEE, Manoj Plakal, Student Member, IEEE, Anne E. Condon,
`(cid:18)(cid:10)(cid:13)(cid:29) (cid:24)(cid:26) (cid:5)(cid:20)(cid:20)(cid:27) (cid:13)(cid:5)(cid:14)(cid:14)(cid:15)(cid:16)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:18)(cid:5)(cid:20)(cid:15) (cid:18)(cid:26)!(cid:26) (cid:18)(cid:10)(cid:13)(cid:17)(cid:5)(cid:8)(cid:27) (cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:2) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)(cid:27) (cid:10)(cid:8)(cid:11)
`Mark D. Hill, Fellow, IEEE, Milo M.K. Martin, Student Member, IEEE, and
`(cid:24)(cid:10)"(cid:5)(cid:11) (cid:30)(cid:26) #(cid:15)(cid:15)(cid:11)(cid:27) (cid:7)(cid:5)(cid:8)(cid:9)(cid:5)(cid:10)(cid:27) (cid:11)(cid:12)(cid:12)(cid:12)
`David A. Wood, Member, IEEE
`
`Abstract—In this paper, we develop a specification methodology that documents and specifies a cache coherence protocol in eight
`(cid:1)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:7)(cid:4)$%(cid:8) (cid:17)(cid:22)(cid:5)(cid:16) (cid:2)(cid:10)(cid:2)(cid:3)(cid:13)(cid:27) &(cid:3) (cid:11)(cid:3)"(cid:3)(cid:20)(cid:15)(cid:2) (cid:10) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) ’(cid:3)(cid:17)(cid:22)(cid:15)(cid:11)(cid:15)(cid:20)(cid:15)(cid:9)(cid:7) (cid:17)(cid:22)(cid:10)(cid:17) (cid:11)(cid:15)(cid:4)(cid:19)’(cid:3)(cid:8)(cid:17)(cid:16) (cid:10)(cid:8)(cid:11) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:3)(cid:16) (cid:10) (cid:4)(cid:10)(cid:4)(cid:22)(cid:3) (cid:4)(cid:15)(cid:22)(cid:3)(cid:13)(cid:3)(cid:8)(cid:4)(cid:3) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) (cid:5)(cid:8) (cid:3)(cid:5)(cid:9)(cid:22)(cid:17)
`tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a
`(cid:17)(cid:10)((cid:20)(cid:3)(cid:16)) (cid:17)(cid:22)(cid:3) (cid:16)(cid:17)(cid:10)(cid:17)(cid:3)(cid:16)(cid:27) (cid:3)"(cid:3)(cid:8)(cid:17)(cid:16)(cid:27) (cid:10)(cid:4)(cid:17)(cid:5)(cid:15)(cid:8)(cid:16)(cid:27) (cid:10)(cid:8)(cid:11) (cid:17)(cid:13)(cid:10)(cid:8)(cid:16)(cid:5)(cid:17)(cid:5)(cid:15)(cid:8)(cid:16) (cid:15)(cid:6) (cid:17)(cid:22)(cid:3) (cid:4)(cid:10)(cid:4)(cid:22)(cid:3) (cid:10)(cid:8)(cid:11) ’(cid:3)’(cid:15)(cid:13)(cid:7) (cid:4)(cid:15)(cid:8)(cid:17)(cid:13)(cid:15)(cid:20)(cid:20)(cid:3)(cid:13)(cid:16)(cid:26) #(cid:3) (cid:17)(cid:22)(cid:3)(cid:8) (cid:19)(cid:16)(cid:3) (cid:17)(cid:22)(cid:5)(cid:16) ’(cid:3)(cid:17)(cid:22)(cid:15)(cid:11)(cid:15)(cid:20)(cid:15)(cid:9)(cid:7) (cid:17)(cid:15) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:7) (cid:10)
`detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows
`(cid:11)(cid:3)(cid:17)(cid:10)(cid:5)(cid:20)(cid:3)(cid:11)(cid:27) ’(cid:15)(cid:11)(cid:3)(cid:13)(cid:8) (cid:17)(cid:22)(cid:13)(cid:3)(cid:3)*(cid:16)(cid:17)(cid:10)(cid:17)(cid:3) ((cid:13)(cid:15)(cid:10)(cid:11)(cid:4)(cid:10)(cid:16)(cid:17) (cid:16)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) &(cid:5)(cid:17)(cid:22) (cid:10)(cid:8) (cid:19)(cid:8)(cid:15)(cid:13)(cid:11)(cid:3)(cid:13)(cid:3)(cid:11) (cid:11)(cid:10)(cid:17)(cid:10) (cid:8)(cid:3)(cid:17)&(cid:15)(cid:13)(cid:29) (cid:10)(cid:8)(cid:11) (cid:10)(cid:8) (cid:15)(cid:13)(cid:11)(cid:3)(cid:13)(cid:3)(cid:11) (cid:10)(cid:11)(cid:11)(cid:13)(cid:3)(cid:16)(cid:16) (cid:8)(cid:3)(cid:17)&(cid:15)(cid:13)(cid:29) (cid:17)(cid:22)(cid:10)(cid:17) (cid:10)(cid:20)(cid:20)(cid:15)&(cid:16)
`arbitrary skew. We also present a detailed specification of a new protocol called Multicast Snooping [6] and, in doing so, we better
`(cid:10)(cid:13)((cid:5)(cid:17)(cid:13)(cid:10)(cid:13)(cid:7) (cid:16)(cid:29)(cid:3)&(cid:26) #(cid:3) (cid:10)(cid:20)(cid:16)(cid:15) (cid:2)(cid:13)(cid:3)(cid:16)(cid:3)(cid:8)(cid:17) (cid:10) (cid:11)(cid:3)(cid:17)(cid:10)(cid:5)(cid:20)(cid:3)(cid:11) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) (cid:15)(cid:6) (cid:10) (cid:8)(cid:3)& (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) (cid:4)(cid:10)(cid:20)(cid:20)(cid:3)(cid:11) (cid:18)(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17) (cid:1)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) +,- (cid:10)(cid:8)(cid:11)(cid:27) (cid:5)(cid:8) (cid:11)(cid:15)(cid:5)(cid:8)(cid:9) (cid:16)(cid:15)(cid:27) &(cid:3) ((cid:3)(cid:17)(cid:17)(cid:3)(cid:13)
`illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the Multicast
`(cid:5)(cid:20)(cid:20)(cid:19)(cid:16)(cid:17)(cid:13)(cid:10)(cid:17)(cid:3) (cid:17)(cid:22)(cid:3) (cid:19)(cid:17)(cid:5)(cid:20)(cid:5)(cid:17)(cid:7) (cid:15)(cid:6) (cid:17)(cid:22)(cid:3) (cid:17)(cid:10)((cid:20)(cid:3)*((cid:10)(cid:16)(cid:3)(cid:11) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) ’(cid:3)(cid:17)(cid:22)(cid:15)(cid:11)(cid:15)(cid:20)(cid:15)(cid:9)(cid:7)(cid:26) .(cid:5)(cid:8)(cid:10)(cid:20)(cid:20)(cid:7)(cid:27) &(cid:3) (cid:11)(cid:3)’(cid:15)(cid:8)(cid:16)(cid:17)(cid:13)(cid:10)(cid:17)(cid:3) (cid:10) (cid:17)(cid:3)(cid:4)(cid:22)(cid:8)(cid:5)/(cid:19)(cid:3) (cid:6)(cid:15)(cid:13) "(cid:3)(cid:13)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) (cid:15)(cid:6) (cid:17)(cid:22)(cid:3) (cid:18)(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17)
`Snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model.
`(cid:1)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20)(cid:27) (cid:17)(cid:22)(cid:13)(cid:15)(cid:19)(cid:9)(cid:22) (cid:17)(cid:22)(cid:3) (cid:16)(cid:29)(cid:3)(cid:17)(cid:4)(cid:22) (cid:15)(cid:6) (cid:10) ’(cid:10)(cid:8)(cid:19)(cid:10)(cid:20) (cid:2)(cid:13)(cid:15)(cid:15)(cid:6) (cid:17)(cid:22)(cid:10)(cid:17) (cid:17)(cid:22)(cid:3) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8) (cid:16)(cid:10)(cid:17)(cid:5)(cid:16)(cid:6)(cid:5)(cid:3)(cid:16) (cid:10) (cid:16)(cid:3)/(cid:19)(cid:3)(cid:8)(cid:17)(cid:5)(cid:10)(cid:20)(cid:20)(cid:7) (cid:4)(cid:15)(cid:8)(cid:16)(cid:5)(cid:16)(cid:17)(cid:3)(cid:8)(cid:17) ’(cid:3)’(cid:15)(cid:13)(cid:7) ’(cid:15)(cid:11)(cid:3)(cid:20)(cid:26)
`
`Index Terms—Cache coherence, protocol specification, protocol verification, memory consistency, multicast snooping.
`(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:13)(cid:11)(cid:5)(cid:14)(cid:3)$(cid:21)(cid:10)(cid:4)(cid:22)(cid:3) (cid:4)(cid:15)(cid:22)(cid:3)(cid:13)(cid:3)(cid:8)(cid:4)(cid:3)(cid:27) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) (cid:16)(cid:2)(cid:3)(cid:4)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8)(cid:27) (cid:2)(cid:13)(cid:15)(cid:17)(cid:15)(cid:4)(cid:15)(cid:20) "(cid:3)(cid:13)(cid:5)(cid:6)(cid:5)(cid:4)(cid:10)(cid:17)(cid:5)(cid:15)(cid:8)(cid:27) ’(cid:3)’(cid:15)(cid:13)(cid:7) (cid:4)(cid:15)(cid:8)(cid:16)(cid:5)(cid:16)(cid:17)(cid:3)(cid:8)(cid:4)(cid:7)(cid:27) ’(cid:19)(cid:20)(cid:17)(cid:5)(cid:4)(cid:10)(cid:16)(cid:17) (cid:16)(cid:8)(cid:15)(cid:15)(cid:2)(cid:5)(cid:8)(cid:9)(cid:26)
`
`(cid:1)
`
`1
`INTRODUCTION
`(cid:15) (cid:8)(cid:16)(cid:13)(cid:17)(cid:18)(cid:19)(cid:20)(cid:21)(cid:13)(cid:8)(cid:18)(cid:16)
`(cid:1) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11) (cid:12)(cid:13) (cid:3) (cid:13)(cid:2)(cid:4)(cid:5)(cid:14)(cid:5) (cid:15)(cid:6)(cid:7) (cid:2)(cid:6)(cid:6)(cid:7)(cid:16)(cid:12)(cid:8)(cid:3)(cid:10)(cid:12)(cid:8)(cid:17)
`A cache coherence protocol is a scheme for coordinating
`access to shared blocks of memory. Processors and
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:13)(cid:4)(cid:3)(cid:7)(cid:5)(cid:16) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13) (cid:6)(cid:15) (cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20)(cid:21) (cid:22)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:3)(cid:8)(cid:16)
`memories exchange messages to share data and to
`(cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:12)(cid:5)(cid:13) (cid:5)(cid:23)(cid:2)(cid:4)(cid:3)(cid:8)(cid:17)(cid:5) (cid:14)(cid:5)(cid:13)(cid:13)(cid:3)(cid:17)(cid:5)(cid:13) (cid:10)(cid:6) (cid:13)(cid:4)(cid:3)(cid:7)(cid:5) (cid:16)(cid:3)(cid:10)(cid:3) (cid:3)(cid:8)(cid:16) (cid:10)(cid:6)
`determine which processors have read-only or read-write
`(cid:16)(cid:5)(cid:10)(cid:5)(cid:7)(cid:14)(cid:12)(cid:8)(cid:5) (cid:24)(cid:4)(cid:12)(cid:2)(cid:4) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:4)(cid:3)(cid:25)(cid:5) (cid:7)(cid:5)(cid:3)(cid:16)(cid:26)(cid:6)(cid:8)(cid:11)(cid:20) (cid:6)(cid:7) (cid:7)(cid:5)(cid:3)(cid:16)(cid:26)(cid:24)(cid:7)(cid:12)(cid:10)(cid:5)
`access to data blocks that are in their caches. A processor’s
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:16)(cid:3)(cid:10)(cid:3) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3)(cid:7)(cid:5) (cid:12)(cid:8) (cid:10)(cid:4)(cid:5)(cid:12)(cid:7) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5)(cid:13)(cid:21) (cid:1) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:27)(cid:13)
`access to a cache block is determined by the state of that
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:12)(cid:13) (cid:16)(cid:5)(cid:10)(cid:5)(cid:7)(cid:14)(cid:12)(cid:8)(cid:5)(cid:16) (cid:18)(cid:20) (cid:10)(cid:4)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) (cid:6)(cid:15) (cid:10)(cid:4)(cid:3)(cid:10)
`block in its cache, and this state is generally one of the five
`(cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:12)(cid:8) (cid:12)(cid:10)(cid:13) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5)(cid:28) (cid:3)(cid:8)(cid:16) (cid:10)(cid:4)(cid:12)(cid:13) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) (cid:12)(cid:13) (cid:17)(cid:5)(cid:8)(cid:5)(cid:7)(cid:3)(cid:11)(cid:11)(cid:20) (cid:6)(cid:8)(cid:5) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5) (cid:15)(cid:12)(cid:25)(cid:5)
`MOESI
`(Modified, Owned, Exclusive, Shared, Invalid)
`(cid:29)(cid:30)(cid:31) !
`"(cid:29)(cid:6)(cid:16)(cid:12)(cid:15)(cid:12)(cid:5)(cid:16)(cid:28) (cid:30)(cid:24)(cid:8)(cid:5)(cid:16)(cid:28) (cid:31)(cid:23)(cid:2)(cid:11)#(cid:13)(cid:12)(cid:25)(cid:5)(cid:28) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16)(cid:28)
`!(cid:8)(cid:25)(cid:3)(cid:11)(cid:12)(cid:16)$
`states [32]. Processors issue requests, such as Get Exclusive
`(cid:13)(cid:10)(cid:3)(cid:10)(cid:5)(cid:13) %&’((cid:21) (cid:22)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:12)(cid:13)(cid:13)#(cid:5) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)(cid:13)(cid:28) (cid:13)#(cid:2)(cid:4) (cid:3)(cid:13) *(cid:5)(cid:10) (cid:31)(cid:23)(cid:2)(cid:11)#(cid:13)(cid:12)(cid:25)(cid:5)
`or Get-Shared, to gain access to blocks. They can also lose
`(cid:6)(cid:7) *(cid:5)(cid:10)(cid:26) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16)(cid:28) (cid:10)(cid:6) (cid:17)(cid:3)(cid:12)(cid:8) (cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13)(cid:21) +(cid:4)(cid:5)(cid:20) (cid:2)(cid:3)(cid:8) (cid:3)(cid:11)(cid:13)(cid:6) (cid:11)(cid:6)(cid:13)(cid:5)
`access to blocks, either by choice (e.g., a cache replacement)
`(cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)(cid:13)(cid:28) (cid:5)(cid:12)(cid:10)(cid:4)(cid:5)(cid:7) (cid:18)(cid:20) (cid:2)(cid:4)(cid:6)(cid:12)(cid:2)(cid:5) "(cid:5)(cid:21)(cid:17)(cid:21)(cid:28) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:7)(cid:5)(cid:9)(cid:11)(cid:3)(cid:2)(cid:5)(cid:14)(cid:5)(cid:8)(cid:10)$
`or when another processor’s request steals a block away.
`(cid:6)(cid:7) (cid:24)(cid:4)(cid:5)(cid:8) (cid:3)(cid:8)(cid:6)(cid:10)(cid:4)(cid:5)(cid:7) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:27)(cid:13) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10) (cid:13)(cid:10)(cid:5)(cid:3)(cid:11)(cid:13) (cid:3) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:3)(cid:24)(cid:3)(cid:20)(cid:21)
`Many invalidate protocols maintain the invariant that there
`(cid:29)(cid:3)(cid:8)(cid:20) (cid:12)(cid:8)(cid:25)(cid:3)(cid:11)(cid:12)(cid:16)(cid:3)(cid:10)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:14)(cid:3)(cid:12)(cid:8)(cid:10)(cid:3)(cid:12)(cid:8) (cid:10)(cid:4)(cid:5) (cid:12)(cid:8)(cid:25)(cid:3)(cid:7)(cid:12)(cid:3)(cid:8)(cid:10) (cid:10)(cid:4)(cid:3)(cid:10) (cid:10)(cid:4)(cid:5)(cid:7)(cid:5)
`can either be one writer and no readers or no writer and any
`(cid:2)(cid:3)(cid:8) (cid:5)(cid:12)(cid:10)(cid:4)(cid:5)(cid:7) (cid:18)(cid:5) (cid:6)(cid:8)(cid:5) (cid:24)(cid:7)(cid:12)(cid:10)(cid:5)(cid:7) (cid:3)(cid:8)(cid:16) (cid:8)(cid:6) (cid:7)(cid:5)(cid:3)(cid:16)(cid:5)(cid:7)(cid:13) (cid:6)(cid:7) (cid:8)(cid:6) (cid:24)(cid:7)(cid:12)(cid:10)(cid:5)(cid:7) (cid:3)(cid:8)(cid:16) (cid:3)(cid:8)(cid:20)
`number of readers.
`(cid:8)#(cid:14)(cid:18)(cid:5)(cid:7) (cid:6)(cid:15) (cid:7)(cid:5)(cid:3)(cid:16)(cid:5)(cid:7)(cid:13)(cid:21)
`What is protocol specification? Cache coherence proto-
`(cid:1)(cid:2)(cid:3)(cid:4) (cid:5)(cid:6) (cid:7)(cid:8)(cid:9)(cid:4)(cid:9)(cid:10)(cid:9)(cid:11) (cid:6)(cid:7)(cid:12)(cid:10)(cid:5)(cid:13)(cid:5)(cid:10)(cid:3)(cid:4)(cid:5)(cid:9)(cid:14)(cid:15) ,(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:26)
`cols for shared memory multiprocessors are implemented
`(cid:2)(cid:6)(cid:11)(cid:13) (cid:15)(cid:6)(cid:7) (cid:13)(cid:4)(cid:3)(cid:7)(cid:5)(cid:16) (cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20) (cid:14)#(cid:11)(cid:10)(cid:12)(cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:3)(cid:7)(cid:5) (cid:12)(cid:14)(cid:9)(cid:11)(cid:5)(cid:14)(cid:5)(cid:8)(cid:10)(cid:5)(cid:16)
`via the actions of numerous system components and the
`(cid:25)(cid:12)(cid:3) (cid:10)(cid:4)(cid:5) (cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:6)(cid:15) (cid:8)#(cid:14)(cid:5)(cid:7)(cid:6)#(cid:13) (cid:13)(cid:20)(cid:13)(cid:10)(cid:5)(cid:14) (cid:2)(cid:6)(cid:14)(cid:9)(cid:6)(cid:8)(cid:5)(cid:8)(cid:10)(cid:13) (cid:3)(cid:8)(cid:16) (cid:10)(cid:4)(cid:5)
`interactions between them. These components include
`(cid:12)(cid:8)(cid:10)(cid:5)(cid:7)(cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:18)(cid:5)(cid:10)(cid:24)(cid:5)(cid:5)(cid:8) (cid:10)(cid:4)(cid:5)(cid:14)(cid:21) +(cid:4)(cid:5)(cid:13)(cid:5) (cid:2)(cid:6)(cid:14)(cid:9)(cid:6)(cid:8)(cid:5)(cid:8)(cid:10)(cid:13) (cid:12)(cid:8)(cid:2)(cid:11)#(cid:16)(cid:5)
`cache controllers, directory controllers, and networks,
`(cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7)(cid:13)(cid:28) (cid:16)(cid:12)(cid:7)(cid:5)(cid:2)(cid:10)(cid:6)(cid:7)(cid:20) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7)(cid:13)(cid:28) (cid:3)(cid:8)(cid:16) (cid:8)(cid:5)(cid:10)(cid:24)(cid:6)(cid:7)(cid:19)(cid:13)(cid:28)
`among others. The specification of a cache coherence
`(cid:3)(cid:14)(cid:6)(cid:8)(cid:17) (cid:6)(cid:10)(cid:4)(cid:5)(cid:7)(cid:13)(cid:21) +(cid:4)(cid:5) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5)
`protocol must detail the actions of each of these components
`(cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11) (cid:14)#(cid:13)(cid:10) (cid:16)(cid:5)(cid:10)(cid:3)(cid:12)(cid:11) (cid:10)(cid:4)(cid:5) (cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:6)(cid:15) (cid:5)(cid:3)(cid:2)(cid:4) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5)(cid:13)(cid:5) (cid:2)(cid:6)(cid:14)(cid:9)(cid:6)(cid:8)(cid:5)(cid:8)(cid:10)(cid:13)
`for every combination of state it could be in and event that
`(cid:15)(cid:6)(cid:7) (cid:5)(cid:25)(cid:5)(cid:7)(cid:20) (cid:2)(cid:6)(cid:14)(cid:18)(cid:12)(cid:8)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) (cid:12)(cid:10) (cid:2)(cid:6)#(cid:11)(cid:16) (cid:18)(cid:5) (cid:12)(cid:8) (cid:3)(cid:8)(cid:16) (cid:5)(cid:25)(cid:5)(cid:8)(cid:10) (cid:10)(cid:4)(cid:3)(cid:10)
`could happen. For example,
`it must specify the actions
`(cid:2)(cid:6)#(cid:11)(cid:16) (cid:4)(cid:3)(cid:9)(cid:9)(cid:5)(cid:8)(cid:21) -(cid:6)(cid:7) (cid:5)(cid:23)(cid:3)(cid:14)(cid:9)(cid:11)(cid:5)(cid:28) (cid:12)(cid:10) (cid:14)#(cid:13)(cid:10) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:20) (cid:10)(cid:4)(cid:5) (cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13)
`performed by a cache controller that has Exclusive access to
`(cid:9)(cid:5)(cid:7)(cid:15)(cid:6)(cid:7)(cid:14)(cid:5)(cid:16) (cid:18)(cid:20) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7) (cid:10)(cid:4)(cid:3)(cid:10) (cid:4)(cid:3)(cid:13) (cid:31)(cid:23)(cid:2)(cid:11)#(cid:13)(cid:12)(cid:25)(cid:5) (cid:3)(cid:2)(cid:2)(cid:5)(cid:13)(cid:13) (cid:10)(cid:6)
`a cache block when a Get-Shared request for that block
`(cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19) (cid:24)(cid:4)(cid:5)(cid:8) (cid:3) *(cid:5)(cid:10)(cid:26) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10) (cid:15)(cid:6)(cid:7) (cid:10)(cid:4)(cid:3)(cid:10) (cid:18)(cid:11)(cid:6)(cid:2)(cid:19)
`arrives from another node, and it must specify the new state
`(cid:3)(cid:7)(cid:7)(cid:12)(cid:25)(cid:5)(cid:13) (cid:15)(cid:7)(cid:6)(cid:14) (cid:3)(cid:8)(cid:6)(cid:10)(cid:4)(cid:5)(cid:7) (cid:8)(cid:6)(cid:16)(cid:5)(cid:28) (cid:3)(cid:8)(cid:16) (cid:12)(cid:10) (cid:14)#(cid:13)(cid:10) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:20) (cid:10)(cid:4)(cid:5) (cid:8)(cid:5)(cid:24) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5)
`that the cache controller enters.
`(cid:10)(cid:4)(cid:3)(cid:10) (cid:10)(cid:4)(cid:5) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7) (cid:5)(cid:8)(cid:10)(cid:5)(cid:7)(cid:13)(cid:21)
`
`What is protocol verification? Verification of a cache
`(cid:1)(cid:2)(cid:3)(cid:4) (cid:5)(cid:6) (cid:7)(cid:8)(cid:9)(cid:4)(cid:9)(cid:10)(cid:9)(cid:11) (cid:16)(cid:12)(cid:8)(cid:5)(cid:13)(cid:5)(cid:10)(cid:3)(cid:4)(cid:5)(cid:9)(cid:14)(cid:15) .(cid:5)(cid:7)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5)
`coherence protocol
`involves proving that a protocol
`(cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)
`(cid:12)(cid:8)(cid:25)(cid:6)(cid:11)(cid:25)(cid:5)(cid:13) (cid:9)(cid:7)(cid:6)(cid:25)(cid:12)(cid:8)(cid:17) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)
`specification obeys a desired memory consistency model,
`(cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:18)(cid:5)(cid:20)(cid:13) (cid:3) (cid:16)(cid:5)(cid:13)(cid:12)(cid:7)(cid:5)(cid:16) (cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20) (cid:2)(cid:6)(cid:8)(cid:13)(cid:12)(cid:13)(cid:10)(cid:5)(cid:8)(cid:2)(cid:20) (cid:14)(cid:6)(cid:16)(cid:5)(cid:11)(cid:28)
`such as sequential consistency (SC) [21]. To verify that a
`(cid:13)#(cid:2)(cid:4) (cid:3)(cid:13) (cid:13)(cid:5))#(cid:5)(cid:8)(cid:10)(cid:12)(cid:3)(cid:11) (cid:2)(cid:6)(cid:8)(cid:13)(cid:12)(cid:13)(cid:10)(cid:5)(cid:8)(cid:2)(cid:20) " ,$ %’/((cid:21) +(cid:6) (cid:25)(cid:5)(cid:7)(cid:12)(cid:15)(cid:20) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3)
`protocol satisfies a consistency model requires proving that
`(cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11) (cid:13)(cid:3)(cid:10)(cid:12)(cid:13)(cid:15)(cid:12)(cid:5)(cid:13) (cid:3) (cid:2)(cid:6)(cid:8)(cid:13)(cid:12)(cid:13)(cid:10)(cid:5)(cid:8)(cid:2)(cid:20) (cid:14)(cid:6)(cid:16)(cid:5)(cid:11) (cid:7)(cid:5))#(cid:12)(cid:7)(cid:5)(cid:13) (cid:9)(cid:7)(cid:6)(cid:25)(cid:12)(cid:8)(cid:17) (cid:10)(cid:4)(cid:3)(cid:10)
`it obeys certain invariants about what value a load from
`(cid:12)(cid:10) (cid:6)(cid:18)(cid:5)(cid:20)(cid:13) (cid:2)(cid:5)(cid:7)(cid:10)(cid:3)(cid:12)(cid:8) (cid:12)(cid:8)(cid:25)(cid:3)(cid:7)(cid:12)(cid:3)(cid:8)(cid:10)(cid:13) (cid:3)(cid:18)(cid:6)#(cid:10) (cid:24)(cid:4)(cid:3)(cid:10) (cid:25)(cid:3)(cid:11)#(cid:5) (cid:3) (cid:11)(cid:6)(cid:3)(cid:16) (cid:15)(cid:7)(cid:6)(cid:14)
`memory can return. For example, to satisfy SC, the loads
`(cid:14)(cid:5)(cid:14)(cid:6)(cid:7)(cid:20) (cid:2)(cid:3)(cid:8) (cid:7)(cid:5)(cid:10)#(cid:7)(cid:8)(cid:21) -(cid:6)(cid:7) (cid:5)(cid:23)(cid:3)(cid:14)(cid:9)(cid:11)(cid:5)(cid:28) (cid:10)(cid:6) (cid:13)(cid:3)(cid:10)(cid:12)(cid:13)(cid:15)(cid:20) ,(cid:28) (cid:10)(cid:4)(cid:5) (cid:11)(cid:6)(cid:3)(cid:16)(cid:13)
`and stores from the different processors must appear to the
`(cid:3)(cid:8)(cid:16) (cid:13)(cid:10)(cid:6)(cid:7)(cid:5)(cid:13) (cid:15)(cid:7)(cid:6)(cid:14) (cid:10)(cid:4)(cid:5) (cid:16)(cid:12)(cid:15)(cid:15)(cid:5)(cid:7)(cid:5)(cid:8)(cid:10) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13) (cid:14)#(cid:13)(cid:10) (cid:3)(cid:9)(cid:9)(cid:5)(cid:3)(cid:7) (cid:10)(cid:6) (cid:10)(cid:4)(cid:5)
`programmer to be in some total order where 1) the value of
`(cid:9)(cid:7)(cid:6)(cid:17)(cid:7)(cid:3)(cid:14)(cid:14)(cid:5)(cid:7) (cid:10)(cid:6) (cid:18)(cid:5) (cid:12)(cid:8) (cid:13)(cid:6)(cid:14)(cid:5) (cid:10)(cid:6)(cid:10)(cid:3)(cid:11) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7) (cid:24)(cid:4)(cid:5)(cid:7)(cid:5) /$ (cid:10)(cid:4)(cid:5) (cid:25)(cid:3)(cid:11)#(cid:5) (cid:6)(cid:15)
`a load equals the value of the most recent store to the same
`(cid:3) (cid:11)(cid:6)(cid:3)(cid:16) (cid:5))#(cid:3)(cid:11)(cid:13) (cid:10)(cid:4)(cid:5) (cid:25)(cid:3)(cid:11)#(cid:5) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5) (cid:14)(cid:6)(cid:13)(cid:10) (cid:7)(cid:5)(cid:2)(cid:5)(cid:8)(cid:10) (cid:13)(cid:10)(cid:6)(cid:7)(cid:5) (cid:10)(cid:6) (cid:10)(cid:4)(cid:5) (cid:13)(cid:3)(cid:14)(cid:5)
`address in the total order, and 2) the total order respects the
`(cid:3)(cid:16)(cid:16)(cid:7)(cid:5)(cid:13)(cid:13) (cid:12)(cid:8) (cid:10)(cid:4)(cid:5) (cid:10)(cid:6)(cid:10)(cid:3)(cid:11) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7)(cid:28) (cid:3)(cid:8)(cid:16) ’$ (cid:10)(cid:4)(cid:5) (cid:10)(cid:6)(cid:10)(cid:3)(cid:11) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7) (cid:7)(cid:5)(cid:13)(cid:9)(cid:5)(cid:2)(cid:10)(cid:13) (cid:10)(cid:4)(cid:5)
`program order at each of the processors.
`(cid:9)(cid:7)(cid:6)(cid:17)(cid:7)(cid:3)(cid:14) (cid:6)(cid:7)(cid:16)(cid:5)(cid:7) (cid:3)(cid:10) (cid:5)(cid:3)(cid:2)(cid:4) (cid:6)(cid:15) (cid:10)(cid:4)(cid:5) (cid:9)(cid:7)(cid:6)(cid:2)(cid:5)(cid:13)(cid:13)(cid:6)(cid:7)(cid:13)(cid:21)
`Why is verification difficult? At a high level, protocols
`(cid:1)(cid:2)(cid:17) (cid:5)(cid:6) (cid:16)(cid:12)(cid:8)(cid:5)(cid:13)(cid:5)(cid:10)(cid:3)(cid:4)(cid:5)(cid:9)(cid:14) (cid:18)(cid:5)(cid:13)(cid:13)(cid:5)(cid:10)(cid:19)(cid:11)(cid:4)(cid:15) (cid:1)(cid:10) (cid:3) (cid:4)(cid:12)(cid:17)(cid:4) (cid:11)(cid:5)(cid:25)(cid:5)(cid:11)(cid:28) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13)
`can be represented as in Fig. 1, which illustrates the
`(cid:2)(cid:3)(cid:8) (cid:18)(cid:5) (cid:7)(cid:5)(cid:9)(cid:7)(cid:5)(cid:13)(cid:5)(cid:8)(cid:10)(cid:5)(cid:16) (cid:3)(cid:13) (cid:12)(cid:8) -(cid:12)(cid:17)(cid:21) /(cid:28) (cid:24)(cid:4)(cid:12)(cid:2)(cid:4) (cid:12)(cid:11)(cid:11)#(cid:13)(cid:10)(cid:7)(cid:3)(cid:10)(cid:5)(cid:13) (cid:10)(cid:4)(cid:5)
`specification of a cache controller for a three state (Mod-
`(cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:6)(cid:15) (cid:3) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:8)(cid:10)(cid:7)(cid:6)(cid:11)(cid:11)(cid:5)(cid:7) (cid:15)(cid:6)(cid:7) (cid:3) (cid:10)(cid:4)(cid:7)(cid:5)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) "(cid:29)(cid:6)(cid:16)(cid:26)
`ified, Shared, Invalid) protocol. There are a handful of
`(cid:12)(cid:15)(cid:12)(cid:5)(cid:16)(cid:28) (cid:4)(cid:3)(cid:7)(cid:5)(cid:16)(cid:28) !(cid:8)(cid:25)(cid:3)(cid:11)(cid:12)(cid:16)$ (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:21) +(cid:4)(cid:5)(cid:7)(cid:5) (cid:3)(cid:7)(cid:5) (cid:3) (cid:4)(cid:3)(cid:8)(cid:16)(cid:15)#(cid:11) (cid:6)(cid:15)
`states, with atomic transitions between them.
`(cid:13)(cid:10)(cid:3)(cid:10)(cid:5)(cid:13)(cid:28) (cid:24)(cid:12)(cid:10)(cid:4) (cid:3)(cid:10)(cid:6)(cid:14)(cid:12)(cid:2) (cid:10)(cid:7)(cid:3)(cid:8)(cid:13)(cid:12)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:18)(cid:5)(cid:10)(cid:24)(cid:5)(cid:5)(cid:8) (cid:10)(cid:4)(cid:5)(cid:14)(cid:21)
`Since cache coherence protocols are simply finite state
` (cid:12)(cid:8)(cid:2)(cid:5) (cid:2)(cid:3)(cid:2)(cid:4)(cid:5) (cid:2)(cid:6)(cid:4)(cid:5)(cid:7)(cid:5)(cid:8)(cid:2)(cid:5) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:3)(cid:7)(cid:5) (cid:13)(cid:12)(cid:14)(cid:9)(cid:11)(cid:20) (cid:15)(cid:12)(cid:8)(cid:12)(cid:10)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5)
`machines, it would appear at first glance that it would be
`(cid:14)(cid:3)(cid:2)(cid:4)(cid:12)(cid:8)(cid:5)(cid:13)(cid:28) (cid:12)(cid:10) (cid:24)(cid:6)#(cid:11)(cid:16) (cid:3)(cid:9)(cid:9)(cid:5)(cid:3)(cid:7) (cid:3)(cid:10) (cid:15)(cid:12)(cid:7)(cid:13)(cid:10) (cid:17)(cid:11)(cid:3)(cid:8)(cid:2)(cid:5) (cid:10)(cid:4)(cid:3)(cid:10) (cid:12)(cid:10) (cid:24)(cid:6)#(cid:11)(cid:16) (cid:18)(cid:5)
`easy to specify and verify a common three state (MSI)
`(cid:5)(cid:3)(cid:13)(cid:20) (cid:10)(cid:6) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:20) (cid:3)(cid:8)(cid:16) (cid:25)(cid:5)(cid:7)(cid:12)(cid:15)(cid:20) (cid:3) (cid:2)(cid:6)(cid:14)(cid:14)(cid:6)(cid:8) (cid:10)(cid:4)(cid:7)(cid:5)(cid:5) (cid:13)(cid:10)(cid:3)(cid:10)(cid:5) "(cid:29) !$
`broadcast snooping protocol. Unfortunately, at the level of
`(cid:18)(cid:7)(cid:6)(cid:3)(cid:16)(cid:2)(cid:3)(cid:13)(cid:10) (cid:13)(cid:8)(cid:6)(cid:6)(cid:9)(cid:12)(cid:8)(cid:17) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:21) 0(cid:8)(cid:15)(cid:6)(cid:7)(cid:10)#(cid:8)(cid:3)(cid:10)(cid:5)(cid:11)(cid:20)(cid:28) (cid:3)(cid:10) (cid:10)(cid:4)(cid:5) (cid:11)(cid:5)(cid:25)(cid:5)(cid:11) (cid:6)(cid:15)
`detail required for an actual implementation, even see-
`(cid:16)(cid:5)(cid:10)(cid:3)(cid:12)(cid:11) (cid:7)(cid:5))#(cid:12)(cid:7)(cid:5)(cid:16) (cid:15)(cid:6)(cid:7) (cid:3)(cid:8) (cid:3)(cid:2)(cid:10)#(cid:3)(cid:11) (cid:12)(cid:14)(cid:9)(cid:11)(cid:5)(cid:14)(cid:5)(cid:8)(cid:10)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8)(cid:28) (cid:5)(cid:25)(cid:5)(cid:8) (cid:13)(cid:5)(cid:5)(cid:26)
`mingly straightforward protocols have numerous transient
`(cid:14)(cid:12)(cid:8)(cid:17)(cid:11)(cid:20) (cid:13)(cid:10)(cid:7)(cid:3)(cid:12)(cid:17)(cid:4)(cid:10)(cid:15)(cid:6)(cid:7)(cid:24)(cid:3)(cid:7)(cid:16) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:4)(cid:3)(cid:25)(cid:5) (cid:8)#(cid:14)(cid:5)(cid:7)(cid:6)#(cid:13) (cid:10)(cid:7)(cid:3)(cid:8)(cid:13)(cid:12)(cid:5)(cid:8)(cid:10)
`states and possible race conditions that complicate the tasks
`(cid:13)(cid:10)(cid:3)(cid:10)(cid:5)(cid:13) (cid:3)(cid:8)(cid:16) (cid:9)(cid:6)(cid:13)(cid:13)(cid:12)(cid:18)(cid:11)(cid:5) (cid:7)(cid:3)(cid:2)(cid:5) (cid:2)(cid:6)(cid:8)(cid:16)(cid:12)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:10)(cid:4)(cid:3)(cid:10) (cid:2)(cid:6)(cid:14)(cid:9)(cid:11)(cid:12)(cid:2)(cid:3)(cid:10)(cid:5) (cid:10)(cid:4)(cid:5) (cid:10)(cid:3)(cid:13)(cid:19)(cid:13)
`of specification and verification. While older protocols only
`(cid:6)(cid:15) (cid:13)(cid:9)(cid:5)(cid:2)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8) (cid:3)(cid:8)(cid:16) (cid:25)(cid:5)(cid:7)(cid:12)(cid:15)(cid:12)(cid:2)(cid:3)(cid:10)(cid:12)(cid:6)(cid:8)(cid:21) 1(cid:4)(cid:12)(cid:11)(cid:5) (cid:6)(cid:11)(cid:16)(cid:5)(cid:7) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:6)(cid:8)(cid:11)(cid:20)
`permitted one outstanding miss and required that a request
`(cid:9)(cid:5)(cid:7)(cid:14)(cid:12)(cid:10)(cid:10)(cid:5)(cid:16) (cid:6)(cid:8)(cid:5) (cid:6)#(cid:10)(cid:13)(cid:10)(cid:3)(cid:8)(cid:16)(cid:12)(cid:8)(cid:17) (cid:14)(cid:12)(cid:13)(cid:13) (cid:3)(cid:8)(cid:16) (cid:7)(cid:5))#(cid:12)(cid:7)(cid:5)(cid:16) (cid:10)(cid:4)(cid:3)(cid:10) (cid:3) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)
`and its responses were atomic, current protocols allow
`(cid:3)(cid:8)(cid:16) (cid:12)(cid:10)(cid:13) (cid:7)(cid:5)(cid:13)(cid:9)(cid:6)(cid:8)(cid:13)(cid:5)(cid:13) (cid:24)(cid:5)(cid:7)(cid:5) (cid:3)(cid:10)(cid:6)(cid:14)(cid:12)(cid:2)(cid:28) (cid:2)#(cid:7)(cid:7)(cid:5)(cid:8)(cid:10) (cid:9)(cid:7)(cid:6)(cid:10)(cid:6)(cid:2)(cid:6)(cid:11)(cid:13) (cid:3)(cid:11)(cid:11)(cid:6)(cid:24)
`transactions to be split and allow multiple outstanding
`(cid:10)(cid:7)(cid:3)(cid:8)(cid:13)(cid:3)(cid:2)(cid:10)(cid:12)(cid:6)(cid:8)(cid:13) (cid:10)(cid:6) (cid:18)(cid:5) (cid:13)(cid:9)(cid:11)(cid:12)(cid:10) (cid:3)(cid:8)(cid:16) (cid:3)(cid:11)(cid:11)(cid:6)(cid:24) (cid:14)#(cid:11)(cid:10)(cid:12)(cid:9)(cid:11)(cid:5) (cid:6)#(cid:10)(cid:13)(cid:10)(cid:3)(cid:8)(cid:16)(cid:12)(cid:8)(cid:17)
`requests. Thus, other requests and responses can be
`(cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)(cid:13)(cid:21) +(cid:4)#(cid:13)(cid:28) (cid:6)(cid:10)(cid:4)(cid:5)(cid:7) (cid:7)(cid:5))#(cid:5)(cid:13)(cid:10)(cid:13) (cid:3)(cid:8)(cid:16) (cid:7)(cid:5)(cid:13)(cid:9)(cid:6)(cid:8)(cid:13)(cid:5)(cid:13) (cid:2)(cid:3)(cid:8) (cid:18)(cid:5)
`o The authors are with the Computer Sciences Department, University of
`(cid:1) (cid:1)(cid:2)(cid:3) (cid:4)(cid:5)(cid:6)(cid:2)(cid:7)(cid:8)(cid:9) (cid:4)(cid:8)(cid:3) (cid:10)(cid:11)(cid:6)(cid:2) (cid:6)(cid:2)(cid:3) (cid:12)(cid:7)(cid:13)(cid:14)(cid:5)(cid:6)(cid:3)(cid:8) (cid:15)(cid:16)(cid:11)(cid:3)(cid:17)(cid:16)(cid:3)(cid:9) (cid:18)(cid:3)(cid:14)(cid:4)(cid:8)(cid:6)(cid:13)(cid:3)(cid:17)(cid:6)(cid:19) (cid:20)(cid:17)(cid:11)(cid:21)(cid:3)(cid:8)(cid:9)(cid:11)(cid:6)(cid:22) (cid:7)(cid:23)
`interleaved between a request and its response. This
`(cid:12)(cid:8)(cid:10)(cid:5)(cid:7)(ci
Accessing this document will incur an additional charge of $.
After purchase, you can access this document again without charge.
Accept $ Charge
Still Working On It
This document is taking longer than usual to download. This can happen if we need to contact the court directly to obtain the document and their servers are running slowly.
Give it another minute or two to complete, and then try the refresh button.
A few More Minutes ... Still Working
It can take up to 5 minutes for us to download a document if the court servers are running slowly.
Thank you for your continued patience.
This document could not be displayed.
We could not find this document within its docket. Please go back to the docket page and check the link. If that does not work, go back to the docket and refresh it to pull the newest information.
Your account does not support viewing this document.
You need a Paid Account to view this document. Click here to change your account type.
Your account does not support viewing this document.
Set your membership
status to view this document.
With a Docket Alarm membership, you'll
get a whole lot more, including:
- Up-to-date information for this case.
- Email alerts whenever there is an update.
- Full text search for other cases.
- Get email alerts whenever a new case matches your search.
One Moment Please
The filing “” is large (MB) and is being downloaded.
Please refresh this page in a few minutes to see if the filing has been downloaded. The filing will also be emailed to you when the download completes.
Your document is on its way!
If you do not receive the document in five minutes, contact support at support@docketalarm.com.
Sealed Document
We are unable to display this document, it may be under a court ordered seal.
If you have proper credentials to access the file, you may proceed directly to the court's system using your government issued username and password.
Access Government Site
