Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol.
In this paper, we develop a specification methodology that documents and specifies a cache coherence protocol in eight tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows arbitrary skew. We also present a detailed specification of a new protocol called Multicast Snooping and, in doing so, we better illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the Multicast Snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model.

1. High-level specification for cache controller
Since, at a high level, cache coherence protocols are simply finite state machines, it would appear at first
glance that it would be easy to specify and verify a common three state (MSI) broadcast snooping protocol.
Unfortunately, at the level of detail required for an actual implementation, even seemingly straightforward
protocols have numerous transient states and possible race conditions that complicate the tasks of specifica-
tion and verification. For example, a single cache controller in a simple MSI protocol that we will specify
in Section 2.1 has 11 states (8 of which are transient), 13 possible events, and 21 actions that it may perform.
The other system components are similarly complicated, and the interactions of all of these components are
difficult to specify and verify.
Why is verification important? Rigorous verification is important, since the complexity of a low-level,
implementable protocol makes it difficult to design without any errors. Many protocol errors can be uncovered
by simulation. Simulation with random testing has been shown to be effective at finding certain classes
of bugs, such as lost protocol messages and some deadlock conditions [27]. However, simulation tends not
to be effective at uncovering subtle bugs, especially those related to the consistency model. Subtle consistency
bugs often occur only under unusual combinations of circumstances, and it is unlikely that un-directed
(or random) simulation will drive the protocol to these situations. Thus, systematic and perhaps more formal
verification techniques are needed to expose these subtle bugs.
Verification requires a detailed, low-level specification. Systematic verification of an implementable
cache coherence protocol requires a low-level, detailed specification of the entire protocol. While there exist
numerous verification techniques, all of these techniques seek to show that an implementable specification
meets certain invariants. Verifying an abstract specification only shows that the abstract protocol is correct.
For example, the verification of a high-level specification which omits transient states may show that invariants
hold for this abstraction of the protocol, but it will not show that an implementable version of this protocol
obeys these invariants.
Current specifications are not sufficient. Specifications that have been published in the literature have not
been sufficiently detailed for implementation purposes, and they are thus not suitable for verification pur-
poses. In academia, protocol specifications tend to be high-level, because a complete low-level specification
may not be necessary for the goal of publishing research [4,7,13]. Moreover, a complete low-level specifica-
tion without a concise format does not lend itself to publication in academia. In industry, low-level, detailed
specifications are necessary and exist, but, to the best of our knowledge, none have been published in the lit-
erature. These specifications often match the hardware too closely, which complicates verification and limits
alternative implementations but eliminates the problem of verifying that the implementation satisfies the
specification.
A new table-based specification technique that is sufficient for verification. To address the need for concise
low-level specifications, we have developed a table-based specification methodology. For each system
component that participates in the coherence protocol, there is a table that specifies the component's behavior
with respect to a given cache block. As an illustrative example, Table 1 shows a specification for a sim-
plified atomic cache controller.
The rows of the table correspond to the states that the component can enter, the columns correspond to the
events that can occur, and the entries themselves are the actions taken and resulting state that occur for that
combination of state and event. The actions are coded with letters which are defined below the table. For
example, the entry a/S denotes that a Load event at the cache controller for a block in state I causes the cache
controller to perform a Get Shared and enter state S.
This simple example, however, does not show the power of our specification methodology, because it does
not include the many transient states possessed by realistic coherence protocols. For simple atomic proto-
cols, the traditional specification approach of drawing up state transition diagrams is tractable. However,
non-atomic transactions cause an explosion in the state space, since events can occur between when a


1. Simplified Atomic Cache Controller Transitions
Event
State
Load Store Other GETS Other GETX
I
a/S c/M
I
d/I
a: perform Get-Shared d: send data to requestor
c: perform Get-Exclusive m: send data to memory
request is issued and when it completes, and numerous transient states are used to capture this behavior.
Section 2 illustrates the methodology with a more realistic broadcast snooping protocol and a multicast
snooping protocol [5].
A methodology for proving that table-based specifications are correct. Using our table-based specifica-
tion methodology, we present a methodology for proving that a specification is sequentially consistent, and
we show how this methodology can be used to prove that our multicast protocol satisfies SC. Our method
uses an extension of Lamport's logical clocks [16] to timestamp the load and store operations performed by
the protocol. Timestamps determine how operations should be reordered to witness SC, as intended by the
designer of the protocol. Thus, associated with any execution of the augmented protocol is a sequence of
timestamped operations that witnesses sequential consistency of that execution. Logical clocks and the associated
timestamping actions are, in effect, a conceptual augmentation of the protocol and are specified using
the same table-based transition tables as the protocol itself. We note that the set of all possible operation
traces of the protocol equals that of the augmented protocol, and that the logical clocks are purely conceptual
devices introduced for verification purposes and are never implemented in hardware. We consider the process
of specifying logical clocks and their actions to be intuitive for the designer of the protocol, and indeed
the process is a valuable debugging tool in its own right.
A straightforward invariant of the augmented protocol guarantees that the protocol is sequentially consistent.
Namely, for all executions of the augmented protocol, the associated timestamped sequence of LDs and STs
is consistent with the program order of operations at all processors and the value of each LD equals that of
the most recent ST. To prove this invariant, numerous other support invariants are added as needed. It can
be shown that all executions of the protocol satisfy all invariants by induction on the length of the execution.
This involves a tedious case-by-case analysis of each possible transition of the protocol and each invariant.
To summarize, the strengths of our methodology are that the process of augmenting the protocol with timestamping
is useful in designing correct protocols, and an easily-stated invariant of the augmented protocol
guarantees sequential consistency. However, our methodology also involves tedious case-by-case proofs that
transitions respect invariants. To our knowledge, no automated approach is known that avoids this type of
case analysis. Because the problem of verifying SC is undecidable, automated approaches have been proved
to work only for a limited class of protocols (such as those in which a finite state observer can reorder operations
in order to find a witness to sequential consistency [14]) that does not include the protocols of this
paper. We will discuss other verifications techniques and compare them to ours in Section 4.
What have we contributed? This paper makes four contributions. First, we develop a new table-based
specification methodology that allows us to concisely describe protocols. Second, we provide a detailed,
low-level specification of a three-state broadcast snooping protocol with an unordered data network and an
address network which allows arbitrary skew. Third, we present a detailed, low-level specification of multi-cast
snooping [5], and, in doing so, we better illustrate the utility of the table-based specification methodol-
ogy. The specification of this more complicated protocol is thorough enough to warrant verification. Fourth,
we demonstrate a technique for verification of the Multicast Snooping protocol, through the sketch of a manual
proof that the specification satisfies a sequentially consistent memory model.
Specifying Broadcast and Multicast Snooping Protocols
In this section, we demonstrate our protocol specification methodology by developing two protocols: a
broadcast snooping protocol and a multicast snooping protocol. Both protocols are MSI (Modified, Shared,
Invalid) and use eight tables to document and specify:
the states, events, actions, and transitions of the cache controller
the states, events, actions, and transitions of the memory controller
The controllers are state machines that communicate via queues, and events correspond to messages being
processed from incoming queues. The actions taken when a controller services an incoming queue, including
enqueuing messages on outgoing queues, are considered atomic.
2.1 Specifying a Broadcast Snooping Protocol
In this section, we shall specify the behavior of an MSI broadcast snooping protocol.
2.1.1 System Model and Assumptions
The broadcast snooping system is a collection of processor nodes and memory nodes (possibly collocated)
connected by two logical networks (possibly sharing the same physical network), as shown in Figure 2.
A processor node contains a CPU, cache, and a cache controller which includes logic for implementing the
coherence protocol. It also contains queues between the CPU and the cache controller. The Mandatory queue
contains Loads (LDs) and Stores (STs) requested by the CPU, and they are ordered by program order. LD
and ST entries have addresses, and STs have data. The Optional queue contains Read-Only and Read-Write
Prefetches requested by the CPU, and these entries have addresses. The Load/Store Data queue contains the
LD/ST from the Mandatory queue and its associated data (in the case of a LD). A diagram of a processor
node is also shown in Figure 2.
Processor Node
Address network
FIFO
Mandatory Queue
FIFO
Cache and Controller
Optional Queue
FIFO
TBEs
Load/Store-Data
CPU
Data network
Broadcast
Address Network
Point to Point Data Network


2. Broadcast Snooping System
The memory space is partitioned among one or more memory nodes. It is responsible for responding to
coherence requests with data if it is the current owner (i.e., no processor node has the block Modified). It
also receives writebacks from processors and stores this data to memory.
The two logical networks are a totally ordered broadcast network for address messages and an unordered
unicast network for data messages. The address network supports three types of coherence requests: GETS
(Get-Shared), GETX (Get-Exclusive) and PUTX (Dirty-Writeback). Protocol transactions are address messages
that contain a data block address, coherence request type (GETX, GETS, PUTX), and the ID of the
requesting processor. Data messages contain the data and the data block address.
All of the components in the system make transitions based on their current state and current event (e.g., an
incoming request), and we will specify the states, events, and transitions for each component in the rest of
this section. There are many components that make transitions on many blocks of memory, and these transitions
can happen concurrently. We assume, however, that the system appears to behave as if all transitions
occur atomically.
2.1.2 Network Specification
The network consists of two logical networks. The address network is a totally ordered broadcast network.
Total ordering does not, however, imply that all messages are delivered at the same time. For example, in an
asynchronous implementation, the path to one node may take longer than the path to another node. The
address network carries coherence requests. A transition of the address network is modeled as atomically
transferring an address message from the output queue of a node to the input queues of all of the nodes, thus
inserting the message into the total order of address messages.
The data network is an unordered point-to-point network for delivering responses to coherence requests. A
transition of the data network is modeled as atomically transferring a data message from the output queue of
a node to the input queue of the destination node.
All nodes are connected to the networks via queues, and all we assume about these queues is that address
queues from the network to the nodes are served in FIFO order. Data queues and address queues from the
nodes to the network can be served without this restriction. For example, this allows a processor node's
GETX to pass its PUTX for the victim block.
2.1.3 CPU Specification
A transition of the CPU occurs when it places a LD or ST in the Mandatory queue, places a Prefetch in the
Optional queue, or removes data from the LD/ST data queue. It can perform these transitions at any time.
2.1.4 Cache Controller Specification
In each transition, a cache controller may inspect the heads of its incoming queues, inject new messages into
its queues, and make appropriate state changes. All we assume about serving incoming queues is that no
queue is starved and that the Address, Mandatory, and Optional queues are served in strict FIFO order. The
actions taken when a queue is served are considered atomic in that they are all done before another queue
(including the same queue) is served. Before any of the actions are taken, however, the cache controller
checks to ensure that resources, such as space in an outgoing queue or an allocated TBE, are available for all
of the actions. If the sum of the resources required for all of the actions is not available, then the cache controller
aborts the transition, performs none of the actions, and waits for resources to become available (where
we define a cache block to be available for a LD/ST if either the referenced block already exists in the cache
or there exists an empty slot which can accommodate the referenced block when it is received from external
sources). The exception to this rule is having an available block in the cache, and this situation is handled by
treating a LD, ST, or Prefetch for which no cache block is available as a Replacement event for the victim
block.
If the request at the head of the Mandatory or Optional queue cannot be serviced (because the block is not
present with the correct permissions or a transaction for the block is outstanding), then no further requests
from that queue can be serviced. Optional requests can be discarded without affecting correctness.
The cache controller keeps a count of all outstanding coherence transactions issued by that node and, for
each such transaction, one Transaction Buffer Entry (TBE) is reserved. No transactions can be issued if there
is no space in the outgoing address queue or if there is already an outstanding transaction for that block. A
TBE contains the address of the block requested, the current state of the transaction, and any data received.1
1. The data field in the TBE may not be required. An implementation may be able to use the cache's data array to buffer
the data for the block. This modification reduces the size of a TBE and avoids specific actions for transferring data from
the TBE to the cache data array.


2. Broadcast Snooping Cache Controller States
Stable
states
Transient
states
State
Cache
State Description
I invalid
shared
modified
ISAD busy invalid, issued GETS, have not seen GETS or data yet
ISA busy invalid, issued GETS, have not seen GETS, have seen data
ISD busy invalid, issued GETS, have seen GETS, have not seen data yet
IMAD busy invalid, issued GETX, have not seen GETX or data yet
IMA busy invalid, issued GETX, have not seen GETX, have seen data
IMD busy invalid, issued GETX, have seen GETX, have not seen data yet
MIA I modified, issued PUTX, have not seen PUTX yet
IIA I
modified, issued PUTX, have not seen PUTX, then saw other
GETS or GETX (reachable from MIA)
The possible block states and descriptions of these states are listed in Table 2. Note that there are two types
of states for a cache block: the stable state and the transient state. The stable state is one of M (Modi-
fied), S (Shared), or I (Invalid), it is recorded in the cache, and it indicates the state of the block before the
latest outstanding transaction for that block (if any) started. The transient state, as shown in Table 2, is
recorded in a TBE, and it indicates the current state of an outstanding transaction for that block (if any).
When future tables refer to the state of a block, it is understood that this state is obtained by returning the
transient state from a TBE (if there is an outstanding transaction for this block), or else (if there is no outstanding
by accessing the cache to obtain the stable state. Blocks not present in the cache are
assumed to have the stable state of I. Each transient state has an associated cache state, as shown in Table 2,
assuming that the tag matches in the cache. A cache state of busy implies that there is a TBE entry for this
block, and its state is a transient state other than MIA or IIA.
To represent the transient states symbolically, we have developed an encoding of these transient states which
consists of a sequence of two or more stable states (initial, intended, and zero or more pending states), where
the second state has a superscript which denotes which part(s) of the transaction - address (A) and/or data
(D) - are still outstanding. For example, a processor which has block B in state I, sends a GETS into the
Address-Out queue, and sees the data response but has not yet seen the GETS, would have B in state ISA.
When the GETS arrives, the state becomes S.
Events at the cache controller depend on incoming messages. The events are listed and described in Table 3.
Note that, in the case of Replacements, block B refers to the address of the victim block. The allowed cache
controller actions are listed in Table 4. Cache controller behavior is detailed in Table 5, where each entry
contains a list of <actions / next state> tuples. When the current state of a block corresponds to the row of


3. Broadcast Snooping Cache Controller Events
Event Description Block B
Load
Read-Only
Prefetch
Store
Read-Write
Prefetch
Mandatory
Replacement
Optional
Replacement
Own GETS
Own GETX
Own PUTX
Other GETS
Other GETX
Other PUTX
Data
LD at head of Mandatory queue
Read-Only Prefetch at head of Optional
queue
ST at head of Mandatory queue
Read-Write Prefetch at head of Optional
queue
LD/ST at head of Mandatory queue for
which no cache block is available
Read-Write Prefetch at head of Optional
queue for which no cache block is available
Occurs when we observe our own GETS
request in the global order
Occurs when we observe our own GETX
request in the global order
Occurs when we observe our own PUTX
request in the global order
Occurs when we observe a GETS request
from another processor
Occurs when we observe a GETX request
from another processor
Occurs when we observe a PUTX request
from another processor
Data for this block from the data network
address of LD at head of Mandatory
Queue
address of Read-Only Prefetch at
head of Optional Queue
address of ST at head of Mandatory
Queue
address of Read-Write Prefetch at
head of Optional Queue
address of victim block for LD/ST
at head of Mandatory queue
address of victim block for
Prefetch at head of Optional queue
address of transaction at head of
incoming address queue
same as above
same as above
same as above
same as above
same as above
address of data message at head of
incoming data queue
the entry and the next event corresponds to the column of the entry, then the specified actions are performed
and the state of the block is changed to the specified new state. If only a next state is listed, then no action is
required. All shaded cases are impossible.
Memory Node Specification
One of the advantages of broadcast snooping protocols is that the memory nodes can be quite simple. The
memory nodes in this system, like those in the Synapse [9], maintain some state about each block for which
this memory node is the home, in order to make decisions about when to send data to requestors. This state
includes the state of the block and the current owner of the block. Memory states are listed in Table 6, events
are in

Table

7, actions are in Table 8, and transitions are in Table 9.
2.2 Specifying a Multicast Snooping Protocol
In this section, we will specify an MSI multicast snooping protocol with the same methodology used to
describe the broadcast snooping protocol. Multicast snooping requires less snoop bandwidth and provides


4. Broadcast Snooping Cache Controller Actions
Action Description
a Allocate TBE with Address=B
c Set cache tag equal to tag of block B.
d Deallocate TBE.
f Issue GETS: insert message in outgoing Address queue with Type=GETS, Address=B, Sender=N.
Issue GETX:insert message in outgoing Address queue with Type=GETX, Address=B, Sender=N
h Service LD/ST (a cache hit) from the cache and (if a LD) enqueue the data on the LD/ST data queue.
incoming address queue.
incoming data queue.
l Pop optional queue.
Send data from TBE to memory.
Send data from cache to memory.
Issue PUTX: insert message in outgoing Address queue with Type=PUTX, Address=B, Sender=N
q Copy data from cache to TBE.
r Send data from the cache to the requestor
s Save data in data field of TBE.
Service LD from TBE, pop mandatory queue, and enqueue the data on the LD/ST data queue if the
LD at the head of the Mandatory queue is for this block.
Service LD/ST from TBE, pop mandatory queue, and (if a LD) enqueue the data on the LD/ST data
queue if the LD/ST at the head of the Mandatory queue is for this block.
w Write data from data field of TBE into cache
y Send data from the TBE to the requestor.
z Cannot be handled right now.
higher throughput of address transactions, thus enabling larger systems than are possible with broadcast
snooping.
2.2.1 System Model and Assumptions
Multicast snooping, as described by Bilir et al. [5], incorporates features of both broadcast snooping and
directory protocols. It differs from broadcast snooping in that coherence requests use a totally ordered multi-cast
address network instead of a broadcast network. Multicast masks are predicted by processors, and they
must always include the processor itself and the directory for this block (but not any other directories), yet


5. Broadcast Snooping Cache Controller Transitions
I
caf/I caf/IS cag/I cag/I
SAD AD MAD MAD
hk l ag/IM ag/IM I I
AD AD
hk l hk l aqp/M aqp/M
IA IA
ISAD
IMAD
z z z z z z
z z z z z z
i/ISD
sj/ISA
sj/IMA
i/IMD
ISA
IMA
z z z z z z
z z z z z z
uwdi/S
vwdi/
MIA
IIA
z z z z z z
z z z z z z
ISD
IMD
z z z z z z
z z z z z z
suwdj/
svwdj/
State
Load
RPeraedf-eOtcnhly
Store
RMeOePparplndaetdf-cieWoaetnmtcoraheirltnyet
Own GPGUETXS
Other PGUETXS
Other GETX
Data
z z i
. Only change the cache state to I if the tag matches.
they are allowed to be incorrect. A GETS mask is incorrect if it omits the current owner, and a GETX mask
is incorrect if it omits the current owner or any of the current sharers. This scenario is resolved by a simple
directory which can detect mask mispredictions and retry these requests (with an improved mask) on behalf
of the requestors.
The multicast snooping protocol described here differs from that specified in Bilir et al. in a couple of significant
ways. First, we specify an MSI protocol here instead of an MOSI protocol. Second, we specify the protocol
here at a lower, more detailed level. Third, the directory in this protocol can retry requests with
incorrect masks on behalf of the original requester.
A multicast system is shown in Figure 3. The processor nodes are structured like those in the broadcast
snooping protocol. Instead of memory nodes, though, the multicast snooping protocol has directory nodes,
which are memory nodes with extra protocol logic for handling retries, and they are also shown in Figure 3.
In the next two subsections, we will specify the behaviors of processor and directory components in an MSI
multicast snooping protocol.


6. Broadcast Snooping Memory Controller States
State Description
MSA
MSD
Shared or Invalid
Modified
Modified, have not seen GETS/PUTX, have seen data
Modified, have seen GETS or PUTX, have not seen data


7. Broadcast Snooping Memory Controller Events
Event Description Block B
Other Home
GETS
PUTX (requestor is
PUTX (requestor is
not owner)
Data
A request arrives for a block whose
home is not at this memory
A GETS at head of incoming
address queue
A GETX at head of incoming
address queue
A PUTX from owner at head of
incoming address queue
A PUTX from non-owner at head
of incoming address queue
Data at head of incoming data
queue
address of transaction at head of
incoming address queue
same as above
same as above
same as above
same as above
address of message at head of
incoming data queue


8. Broadcast Snooping Memory Controller Actions
Action Description
c
d
z
owner equal to directory.
Send data message to requestor.
address queue.
data queue.
owner equal to requestor.
Write data to memory.
Delay transactions to this block.


9. Broadcast Snooping Memory Controller Transitions
State
wk/MSA
Other Home
GETS
PiP(srUeoqTwuXneesrto)r
(requestor
not owner)
Data
Directory Node
Multicast
Address Network
Point to Point Data Network
Address network
FIFO
Directory
Block
state
Memory
Data network


3. Multicast Snooping System
2.2.2 Network Specification
The data network behaves identically to that of the broadcast snooping protocol, but the address network
behaves slightly differently. As the name implies, the address network uses multicasting instead of broadcasting
and, thus, a transition of the address network consists of taking a message from the outgoing address
queue of a node and placing it in the incoming address queues of the nodes specified in the multicast mask,
as well as the requesting node and the memory node that is the home of the block being requested (if these
nodes are not already part of the mask).
Address messages contain the coherence request type (GETS, GETX, or PUTX), requesting node ID, multi-cast
mask, block address, and a retry count. Data messages contain the block address, sending node ID, destination
node ID, data message type (DATA or NACK), data block, and the retry count of the request that
triggered this data message.
2.2.3 CPU Specification
The CPU behaves identically to the CPU in the broadcast snooping protocol.
2.2.4 Cache Controller Specification
Cache controllers behave much like they did in the broadcast snooping protocol, except that they must deal
with retried and nacked requests and they are more aggressive in processing incoming requests. This added
complexity leads to additional states, TBE fields, protocol actions, and protocol transitions.
There are additional states in the multicast protocol specified here due to the more aggressive processing of
incoming requests. Instead of buffering incoming requests (with the 'z' action) while in transient states, a
cache controller in this protocol ingests some of these requests, thereby moving into new transient states. An
example is the state IMDI, which occurs when a processor in state IMD ingests an incoming GETX request
from another processor instead of buffering it. The notation signifies that a processor started in I, is waiting
for data to go to M, and will then go to I immediately (except for in cases in which forward progress issues
require the processor to perform a LD or ST before relinquishing the data, as will be discussed below). There
are also three additional states that are necessary to describe situations where a processor sees a nack to a
request that it has seen yet.
There are four additional fields in the TBE: ForwardProgress, ForwardID, RetryCount, and ForwardIDRe-
tryCount. The ForwardProgress bit is set when a processor sees its own request that satisfies the head of the
Mandatory queue. This flag is used to determine when a processor must perform a single load or store on the
cache line before relinquishing the block.2 For example, when data arrives in state IMDI, a processor can service
a LD or ST to this block before forwarding the block if and only if ForwardProgress is set. The Forwar-
dID field records the node to which a processor must send the block in cases such as this. In this example,
ForwardID equals the ID of the node whose GETX caused the processor to go from IMD to IMDI. Retry-
Count records the retry number of the most recent message, and ForwardIDRetryCount records the retry
count associated with the block that will be forwarded to the node specified by ForwardID.
We use the same table-driven methodology as was used to describe the broadcast snooping protocol. Tables
10, 11, 12, and 13 specify the states, events, actions, and transitions, respectively, for processor nodes.
2.2.5 Directory Node Specification
Unlike broadcast snooping, the multicast snooping protocol requires a simplified directory to handle incorrect
masks. A directory node, in addition to its incoming and outgoing queues, maintains state information
for each block of memory that it controls. The state information includes the block state, the ID of the current
owner (if the state is M), and a bit vector that encodes a superset of the sharers (if the state is S). The
possible block states for a directory are listed in Table 14. As before, we refer to M, S and I as stable states
and others as transient states. Initially, for all blocks, the state is set to I, the owner is set to memory and the
bit-vector is set to encode an empty set of sharers. The state notation is the same as for processor nodes,
although the state MXA refers to the situation in which a directory is in M and receives data, but has not seen
the corresponding coherence request yet and therefore does not know (or care) whether it is PUTX data or
data from a processor that is downgrading from M to S in response to another processor's GETS.
A directory node inspects its incoming queues for the address and data networks and removes the message at
the head of a queue (if any). Depending on the incoming message and the current block state, a directory
may inject a new message into an outgoing queue and may change the state of the block. For simplicity, a
directory currently delays all requests for a block for which a PUTX or downgrade is outstanding.3
2. Another viable scheme would be to set this bit when a processor observes its own address request and this request
corresponds to the address of the head of the Mandatory queue. It is also legal to set ForwardProgress when a LD/ST
gets to the head of the Mandatory queue while there is an outstanding transaction for which we have not yet seen the
address request. However, sequential consistency is not preserved by a scheme where ForwardProgress is set when data
returns for a request and the address of the request matches the address at the head of the Mandatory queue.


10. Multicast Snooping Cache Controller States
State
Cache
State Description
I Invalid
Shared
Modified
ISAD busy invalid, issued GETS, have not seen GETS or data yet
IMAD busy invalid, issued GETX, have not seen GETX or data yet
SMAD busy shared, issued GETX, have not seen GETX or data yet
ISA busy invalid, issued GETS, have not seen GETS, have seen data
IMA busy invalid, issued GETX, have not seen GETX, have seen data
SMA busy shared, issued GETX, have not seen GETX, have seen data
ISA* busy invalid, issued GETS, have not seen GETS, have seen nack
IMA* busy invalid, issued GETX, have not seen GETX, have seen nack
SMA* busy shared, issued GETX, have not seen GETX, have seen nack
MIA I modified, issued PUTX, have not seen PUTX yet
IIA I modified, issued PUTX, have not seen PUTX, then saw other GETS or GETX
ISD busy invalid, issued GETS, have seen GETS, have not seen data yet
ISDI busy invalid, issued GETS, have seen GETS, have not seen data, then saw other GETX
IMD busy invalid, issued GETX, have seen GETX, have not seen data yet
IMDS busy invalid, issued GETX, have seen GETX, have not seen data yet, then saw other GETS
IMDI busy invalid, issued GETX, have seen GETX, have not seen data yet, then saw other GETX
IMDSI busy
invalid, issued GETX, have seen GETX, have not seen data yet, then saw other GETS,
then saw other GETX
SMD busy shared, issued GETX, have seen GETX, have not seen data yet
SMDS busy shared, issued GETX, have seen GETX, have not seen data yet, then saw other GETS
The directory events, actions and transitions are listed in Tables 15, 16, and Table 17, respectively. The
action 'z' (delay transactions to this block) relies on the fact that a directory can delay address messages
for a given block arbitrarily while waiting for a data message. Conceptually, we have one directory per
block. Since there is more than one block per directory, an implementation would have to be able to delay
only those transactions which are for the specific block. Note that consecutive GETS transactions for the
same block could be coalesced.
3. This restriction maintains the invariant that there is at most one data message per block that the directory can receive,
thus eliminating the need for buffers and preserving the sanity of the protocol developers.


11. Multicast Snooping Cache Controller Events
Event Description Block B
Load
Read-Only
Prefetch
Store
Read-Write
Prefetch
Mandatory
Replacement
Optional
Replacement
Own GETS
Own GETX
Own GETS
Own GETX
Own PUTX
Other GETS
Other GETX
Other PUTX
Data
Data
LD at head of Mandatory queue
Read-Only Prefetch at head of Optional
queue
ST at head of Mandatory queue
Read-Write Prefetch at head of Optional
queue
LD/ST at head of Mandatory queue for
which no cache block is available
Read-Write Prefetch at head of Optional
queue for which no cache block is available
Occurs when we observe our own GETS
request in the global order
Occurs when we observe our own GETX
request in the global order
Occurs when we observe our own GETS
request in the global order, but the Retry-
Count of the GETS does not match Retry-
Count of the TBE
Occurs when we observe our own GETX
request in the global order, but the Retry-
Count of the GETS does not match Retry-
Count of the TBE
Occurs when we observe our own PUTX
request in the global order
Occurs when we observe a GETS request
from another processor
Occurs when we observe a GETX request
from another processor
Occurs when we observe a PUTX request
from another processor
Data for this block arrives
Data for this block arrives, but the Retry-
Count of the data message does not match
RetryCount of the TBE
address of LD at head of Mandatory Queue
address of Read-Only Prefetch at head of
Optional Queue
address of ST at head of Mandatory Queue
address of Read-Write Prefetch at head of
Optional Queue
address of victim block for LD/ST at head of
Mandatory queue
address of victim block for Prefetch at head
of Optional queue
address of transaction at head of incoming
address queue
same as above
same as above
same as above
same as above
same as above
same as above
same as above
address of message at head of incoming data
queue
address of message at head of incoming data
queue
3 Verification of Snooping Protocols
In this section, we present a methodology for proving that a specification is sequentially consistent, and we
show how this methodology can be used to prove that our multicast protocol satisfies SC. Our method uses
an extension of Lamport's logical clocks [16] to timestamp the load and store operations performed by the
protocol. Timestamps determine how operations should be reordered to witness SC, as intended by the


12. Multicast Snooping Cache Controller Actions
Action Description
a
Allocate TBE with Address=B, ForwardID=null, RetryCount=zero, ForwardIDRetryCount=zero, For-
wardProgress bit=unset.
b Set ForwardProgress bit if request at head of address queue satisfies request at head of Mandatory queue.
c Set cache tag equal to tag of block B.
d Deallocate TBE.
e Record ID of requestor in ForwardID and record retry number of transaction in ForwardIDRetryCount.
f
Issue GETS: insert message in outgoing Address queue with Type=GETS, Address=B, Sender=N, Retry-
Count=zero.
Issue GETX: insert message in outgoing Address queue with Type=GETX, Address=B, Sender=N,
RetryCount=zero.
h Service load/store (a cache hit) from the cache and (if a LD) enqueue the data on the LD/ST data queue.
incoming address queue.
incoming data queue.
l Pop optional queue.
Send data from TBE to memory.
Send data from cache to memory.
data and ForwardIDRetryCount from the TBE to the processor indicated by ForwardID.
Issue PUTX: insert message in outgoing Address queue with Type=PUTX, Address=B, Sender=N.
q Copy data from cache to TBE.
r Send data from the cache to the requestor
s Save data in data field of TBE.
Copy retry field from message at head of incoming Data queue to Retry field in TBE, set
null, and set ForwardIDRetryCount=zero.
Service LD from TBE, pop mandatory queue, and enqueue the data on the LD/ST data queue if the LD at
the head of the mandatory queue is for this block.
v Treat as either h or z (optional cache hit). If it is a cache hit, then pop the mandatory queue.
w Write data from the TBE into the cache.
x
If (and only if) ForwardProgress bit is set, service LD from TBE, pop mandatory queue,and enqueue the
data on the LD/ST data queue.
y Send data from the TBE to the requestor.
z
Cannot be handled right now. Either wait or discard request (can discard if this request is in the Optional
queue).
a
Copy retry field from message at head of incoming address queue to Retry field in TBE, set
null, and set ForwardIDRetryCount=zero.
Service LD/ST from TBE, pop mandatory queue, and (if a LD) enqueue the data on the LD/ST data
queue if the LD/ST at the head of the mandatory queue is for this block. (If ST, store data to TBE).
l Optionally service LD/ST from TBE.
d
If (and only if) ForwardProgress bit is set, service LD/ST from TBE, pop mandatory queue,and (if a LD)
enqueue the data on the LD/ST data queue.


13. Multicast Snooping Cache Controller Transitions
I
caf/ caf/ cag/ cag/
ISAD ISAD IMAD IMAD
hk l ag/ ag/ I I
hk l hk l aqp/ aqp/
MIA MIA
ISAD
IMAD
z l z z z z
z l z l z z
l z l z z
bi/
ISD
IMAD
sj/ stj/ tj/ tj/
ISA ISA ISA* ISA*
sj/ stj/ tj/ tj/
IMA IMA IMA* IMA*
sj/ stj/ tj/ tj/
SMA SMA SMA* SMA*
ISA*
IMA*
z l z z z z
z l z l z z
l z l z z
ISA
IMA
z l z z z z
z l z l z z
l z l z z
uwdi/
MIA
IIA
l z l z z z
z z z z z z
A
ISD
ISDI
IMD
IMDS
IMDI
IMDSI
z l z z z z
z z z z z z
z l z l z z
z l z z z z
z z z z z z
z z z z z z
z l z l z z
z l z z z z
IMDS IMDI
SI
SMDS IMDI
IMDSI
suwdj/ stj/ISA dj/I tj
sxdj/I stj/ISA dj/I tj
sgwdj/ stj/ dj/I tj
sdom- stj/ dj/I tj
wdj/S IMA
sdodj/ stj/ dj/I tj
I IMA
sdomd stj/ dj/I tj
j/I IMA
sgwdj/ stj/ dj/S tj
sgom- stj/ dj/S tj
wdj/S SMA
State
Load
read-wonrliyteprreefefetctch
Store
Mandatory Replacement
Optional Replacement
Own GETS
Own GETX
Own GETS (mismatch)
Own GETX (mismatch)
Own PUTX
Other GPUETXS
Other GETX
Data
nack
bi/
IMD
bi/
di/I
di/S
gwdi/
gwdi/
mdi/I
di/I
ai/ISD
ai/IMD
ai/IMD
ai/IMD
ai/SMD
Only change the state to I if the tag matches.


14. Multicast Snooping Memory Controller States
State Description
I Invalid - all processors are Invalid
Shared - at least one processor is Shared
Modified - one processor is Modified and the rest are Invalid
MXA Modified, have not seen GETS/PUTX, have seen data
MSD Modified, have seen GETS, have not seen data
MID Modified, have seen PUTX, have not seen data


15. Multicast Snooping Memory Controller Events
Event Description Block B
GETS
GETS-RETRY
GETS-NACK
GETX-RETRY
GETX-NACK
PUTX (requestor is
(requestor is not
Data
GETS with successful mask at head of
incoming address queue
GETX with successful mask at head of
incoming address queue
GETS with unsuccessful mask at head of
incoming queue. Room in outgoing
address queue for a retry.
GETS with unsuccessful mask at head of
incoming queue. No room in outgoing
address queue for a retry.
GETX with unsuccessful mask at head of
incoming queue. Room in outgoing
address queue for a retry.
GETX with unsuccessful mask at head of
incoming queue. No room in outgoing
address queue for a retry.
PUTX from owner at head of incoming
address queue.
PUTX from non-owner at head of incoming
address queue.
Data message at head of incoming data
queue
address of transaction at head
of incoming address queue
same as above
same as above
same as above
same as above
same as above
same as above
same as above
address of message at head of
incoming data queue
designer of the protocol. Logical clocks and the associated timestamping actions are a conceptual augmentation
of the protocol and are specified using the same table-based transition tables as the protocol itself. We
note that the set of all possible operation traces of the protocol equals that of the augmented protocol.
The process of developing a timestamping scheme is a valuable debugging tool in its own right. For exam-
ple, an early implementation of the multicast protocol did not include a ForwardProgress bit in the TBE,
and, upon receiving the data for a GETX request when in state IMDI, always satisfied an OP at the head of
the mandatory queue before forwarding the data. Attempts to timestamp OP reveal the need for a forward


16. Multicast Snooping Memory Controller Actions
Action Description
c Clear set of sharers.
d Send data message to requestor with RetryCount equal to RetryCount of request.
address queue.
data queue.
owner equal to requestor.
Send nack to requestor with RetryCount equal to RetryCount of request.
q Add owner to set of sharers.
r
Retry by re-issuing the request. Before re-issuing, the directory improves the multicast
mask and increments the retry field. If the transaction has reached the maximum number of
retries, the multicast mask is set to the broadcast mask.
s Add requestor to set of sharers.
w Write data to memory.
x Set owner equal to directory.
z Delay transactions to this block.


17. Multicast Snooping Memory Controller Transitions
I
dsj/S dmj/M
dsj cdmj/M
qsxj/MSD mj
wk/MXA
MXA qsxj/S mj rj nj rj nj xj/I j
MSD
MID
z z
z z
wk/S
wk/I
State
GETS
(Unsuccessful mask)
(unsuccessful mask)
(requestor is owner)
(requestor not owner)
Data
progress bit, roughly to ensure that OP can indeed be timestamped so that it appears to occur just after the
time of the GETX, and that this OP's logical timestamp also respects program order.
In brief, our methodology for proving sequential consistency consists of the following steps.
Augment the system with logical clocks and with associated actions that assign timestamps to LD and
ST operations. The logical clocks are purely conceptual devices introduced for verification purposes
and are never implemented in hardware
Associate a global history with any execution of the augmented protocol. Roughly, the history includes
the configuration at each node of the system (states, TBEs, cache contents, logical clocks, and queues),
the totally ordered sequence of transactions delivered by the network, and the memory operations serviced
so far, in program order, along with their logical timestamps.
Using invariants, define the notion of a legal global history. The invariants are quite intuitive when
expressed using logical timestamps. It follows immediately from the definition of a legal global history
that the corresponding execution is sequentially consistent.
Finally, prove that the initial history of the system is legal, that each transition of the protocol maps legal
global histories to legal global histories, and that the entries labelled impossible in the protocol speci-
fication tables are indeed impossible. It then follows by induction that the protocol is sequentially consistent

The first step above, that of augmenting the system with logical clocks, can be done hand in hand with development
of the protocol. Thus, it is, on its own, a valuable debugging tool. The second step is straightforward.
It is also straightforward to select a core set of invariants in the third step that are strong enough to guarantee
that the execution corresponding to any legal global history is sequentially consistent. The final step of the
proof methodology above requires a proof for every transition of the protocol and every invariant, and may
necessitate the addition of further invariants to the definition of legal. This step of the proof, while not diffi-
cult, is certainly tedious.
In the rest of this section, we describe the first three steps of this process in more detail, namely how the multicast
protocol is augmented with logical clocks, and what is a global history and a legal global history. We
include examples of the cases covered in the final proof step in Appendix A.
3.1 Augmenting the System with Logical Clocks
In this section, we shall describe how we augment the system specified earlier with logical clocks and with
actions that increment clocks and timestamp operations and data. These timestamps will make future defini-
tions (of global states and legal global states) simpler and more intuitive. These augmentations do not
change the behavior of the system as originally specified.
3.1.1 The Augmented System
The system is augmented with the following counters, all of which are initialized to zero:
One counter (global pulse number) associated with the multicast address network.
Two counters (global and local clocks) associated with each processor node of the system.
One counter (pulse number) added to each data field and to each ForwardID field of each TBE.
One counter (pulse number) field added to each data message.
One counter (global clock) associated with each directory node of the system.


18. Processor clock actions
Action Description
Set global clock equal to pulse of transaction being handled, and set local clock to zero
Increment local clock. The timestamp of the LD/ST is set equal to the associated global
and local clock values.
pulse equal to transaction pulse.
Optionally treat as h.
data message pulse equal to TBE ForwardID pulse.
data pulse equal to pulse of incoming data message.
If first Op in Mandatory queue is a LD for this block, then increment local clock. The
timestamp of the LD/ST is set equal to the associated global and local clock values.
If first Op in Mandatory queue is a LD/ST for this block, then increment local clock. The
timestamp of the LD/ST is set equal to the associated global and local clock values.
x
If ForwardProgress bit is set (i.e., head of Mandatory Queue is a LD or this block), then
no clock update, set global timestamp of LD equal to pulse of incoming data message,
and set local clock value equal to 1.
y Set data message pulse equal to transaction pulse.
z Same as x, but allow a LD or ST for this block.
3.1.2 Behavior of the Augmented System
In the augmented system, the clocks get updated and timestamps (or pulses) are assigned to operations and
data upon transitions of the protocol according to the following rules.
Network: Each new address transaction that is appended to the total order of address transactions by the net-work
causes the global pulse number to increment by 1. The new value of the pulse number is associated
with the new transaction.
Processor: Tables describe how the global and local clocks are updated. The TBE counter is used
to record the timestamp of a request that cannot be satisfied until the data arrives. When the data arrives, the
owner sends the data with the timestamp that was saved in the TBE.
Directory: Briefly, upon handling any transaction, the directory updates its clock to equal the global pulse of
that transaction. The pulse attached to any data message is set to be the value of the directory's clock.
3.2 Global Histories
The global history associated with an execution of the protocol is a 3-tuple <TransSeq,Config,Ops>. Trans-
records information on the sequence of transactions requested to date: the type of transaction, requester,
address, mask, retry-number, pulse (possibly undefined), and status (successful, unsuccessful, nack, or unde-
termined). Config records the configuration of the nodes: state per block, cache contents, queue contents,
TBEs, and logical clock values. Ops records properties of all operations generated by the CPUs to date:
operations along with address, timestamp (possibly undefined), value, and rank in program order.


19. Processor clock updates
Processor/Cache Request See Own See Other See Own
Retry
Match
Retry
Mismatch
I
gy gy
ISAD
IMAD
ISA*
IMA*
ISA
IMA
MIA
IIA
gy
gy
gy gy
ISD
ISDI
IMD
IMDS
IMDI
IMDSI
zot t
zot t
zot t
zot t
Current
State
LD
Mreadn-dowanrtloiytreyprRreefefpetlctachchement
Optional Replacement
GETSX
GETSX
GETSX
RMReattrcyh
Mismatch
RMReattrcyh
Mismatch
The global history is defined inductively on the sequence of transitions in the execution. In the initial global
history, Trans-Seq and Ops are empty. In Config, all processors are in state I for all blocks, have empty
queues, no TBEs and clocks initialized to zero. For all blocks, the directory is in state I, the owner s is set to
the directory, and the list of sharers is empty. All incoming queues are empty. Upon each transition, Trans-
Seq, Ops, and Config are updated in a manner consistent with according to the actions of that transition.
3.3 Legal Global Configurations and Legal Global Histories
There are several requirements for a global history <TransSeq,Config,Ops> to be legal. Briefly, these are as
follows. The first requirement is sufficient to imply sequential consistency. The remaining four requirements
supply additional invariants that are useful in building up to the proof that the first requirement holds.
Ops is legal with respect to program order. That is, the following should hold:
3.3.1 Ops respects program order. That is, for any two operations O1 and O2, if O1 has a smaller
timestamp than O2 in Ops, then O1 must also appear before O2 in program order.
3.3.2 Every LD returns the value of the most recent ST to the same address in timestamp order.
TransSeq is legal. To describe the type of constraints that TransSeq must satisfy, we introduce the notion
of A-state vectors. The A-state vector corresponding to TransSeq for a given block B records, for each
processor N, whether TransSeq confers Shared (S), Modified (M), or no (I) access to block B to processor
N. For example, in a system with three processors, if TransSeq consists of a successful GETS to
block B by processor 1, followed by an unsuccessful GETX to block B by processor 2, followed by a
successful GETS to block B by processor 3, then the corresponding A-state for block B is (S,I,S). The
constraints on TransSeq require, for example, that a GETX on block B should not be successful if its
mask does not include all processors that, upon completion of the transaction just prior to the GETX,
may have Shared or Modified access to B. That is, if TransSeq consist of TransSeq' followed by GETX
on block B and A is the A-state for block B corresponding to TransSeq', then the mask of the GETX
should contain all processors whose entries in A are not equal to I. The precise definition of a legal
transaction sequence is included in Appendix A.
Ops is legal with respect to Trans-Seq. Intuitively, for all operations op in Ops, if op is performed by
processor N at global timestamp t, then the A-state for processor N at logical time t should be either S or
M and should be M if op is a ST.
Config is legal with respect to TransSeq. This involves several constraints, since there are many components
to Config. For example, if processor N is in state ISAD for block B, then a GETS for block B,
requested by N, with timestamp greater than that of N (or undefined) should be in TransSeq.
Config is legal with respect to Ops. That is, for all blocks B and nodes N, the following should hold:
3.3.3 If N is a processor and its state for block B is one of S, M, MIA, SMAD, or SMA, then the
value of block B in N's cache equals that of the most recent ST in Ops, relative to N's clock. By
most recent ST relative to N's clock we mean a ST whose timestamp is less then or equal to
N's clock.
3.3.4 If N is a processor and block B is in one of N's TBEs, then its value equals that of the most
recent ST in Ops, relative to p.0.0, where p is the pulse in the data field of the TBE.
3.3.5 If data for block B is in N's incoming data queue, its value equals the most recent ST in Ops
(relative to the data's timestamp, not N's current time).
3.3.6 If N is the directory of block B, then for each block B for which N is the owner, its value
equals that of the most recent ST in Ops (relative to N's clock).
3.4 Properties of Legal Global Histories
It is not hard to show that the global history of the system is initially legal. The main task of the proof is to
show the following:
Theorem 1: Each protocol transition takes the system from a legal global history to a legal global history.
To illustrate how Theorem 1 is proved, we include in Appendix A the proof of why the transition at each
entry of Table 13 (cache controller transitions) maps a legal global history, <TransSeq,Ops,Config>, to a
new global history, <TransSeq',Ops',Config'> in which TransSeq' is legal.


20. Classification of Related Work
Manual Semi-automated Automated
Complete
method
lazy caching[2]
DASH memory model [12]
Lamport Clocks [25, 21, 6, 15],
Lamport Clocks (this paper),
term rewriting [24]
Incomplete
method
RMO testing[19],
Origin2000 coherence[8],
FLASH coherence [20],
Alpha 21264/21364 [3],
HP Runway testing[11, 18]
4 Related Work
We focus on papers that specify and prove a complete protocol correct, rather than on efforts that focus on
describing many alternative protocols and consistency models, such as [1, 10]. There is a large body of literature
on the subject of formal protocol verification4 which we have classified into a taxonomy along two
independent axes: automation and completeness [23]. We distinguish verification methods based on the level
of automation they support: manual, semi-automated or automated. Manual methods involve humans who
read the specification and construct the proofs. Semi-automated methods involve some computer programs
(a model checker or theorem prover) which are guided by humans who understand the specification and provide
the programs with the invariants or lemmas to prove. Automated methods take the human out of the
loop and involve a computer program that reads a specification and produces a correctness proof completely
automatically. We also distinguish techniques that are complete (proof that a system implements a particular
consistency model) from those that are incomplete (proof of coherence or selected invariants). Table 20 provides
a summary of our taxonomy. We discuss each column of the table separately below.
4. Formal methods involve construction of rigorous mathematical proofs of correctness while informal methods include
such techniques as simulation and random testing which do not guarantee correctness. We only consider formal methods
in this review.
Manual techniques: Lazy caching [2] was one of the earliest examples of a formal specification and verifica-
tion of a protocol (lazy caching) that implemented sequential consistency. The authors use I/O automata as
their formal system models and provide a manual proof that a lazy caching system implements SC. Their use
of history variables in the proof is similar to the manner in which we use Lamport Clock timestamps in our
proofs. Gibbons et al. [12] provide a framework for verifying that shared memory systems implement
relaxed memory models. The method involves specifying both the system to be verified as well as an operational
definition of a memory model as I/O automata and then proving that the system automaton implements
the model automaton. As an example, they provide a specification of the Stanford DASH memory
system and manually prove that it implements the Release Consistency memory model. Our table-based
specification methodology is complementary in that it could also be used to describe I/O automata.
Our previous papers [25, 21, 6, 15] specified various shared memory systems (directory and bus protocols)
at a high level, and employed manual proofs using our Lamport Clocks technique to show that these systems
implemented various memory models (SC, TSO, Alpha). This paper is our latest effort which demonstrates
our technique applied to more detailed table-based specifications of snooping protocols. Shen and Arvind
[24] propose using term rewriting systems (TRSs) to both specify and verify memory system protocols.
Their verification technique involves showing that the system under consideration and the operational definition
of a memory model, when expressed as TRSs, can simulate each other. This proof technique is similar
to the I/O automata approach used by Gibbons et al. [12]. Both TRSs and our table-based specification
method can be used in a modular and flexible fashion. A drawback of TRSs is that they lack the visual clarity
of our table-based specification. Although their current proofs are manual, they mention the possibility of
using a model checker to automate tedious parts of the proof.
Semi-automated techniques: Park and Dill [19] provide an executable specification of the Sun RMO memory
model written in the language of the Murj model checker. This language, which is similar to a typical
imperative programming language, is unambiguous but not necessarily compact. They use this specification
to check the correctness of small synchronization routines. Eiriksson and McMillan [8] describe a methodology
which integrates design and verification where common state machine tables drive a model checker and
generators of simulators and documentation. The protocol specification tables they describe were designed
to be consumed by automated generators rather than by humans, and they do not describe the format of the
text specifications generated from these tables. They use the SMV model checker (which accepts specifica-
tions in temporal logic) to prove the coherence of the protocol used in the SGI Origin 2000. However, the
system verified had only one cache block (which is sufficient to prove coherence, but not consistency). Pong
et al. [22] verify the memory system of the Sun S3.mp multiprocessor using the Murj and SSM (Symbolic
State Model) model checkers, but again the verified system had only one cache block and thus cannot verify
whether the system satisfies a memory model. Park and Dill [20] express both the definition of the memory
model and the system being verified in the same specification language and then use aggregation to map
the system specification to the model specification (similar to the use of TRSs by Shen and Arvind[24] and
I/O automata by Gibbons et al. [12]). As an example, they specify the Stanford FLASH protocol in the language
of the PVS theorem prover (the language is a typed high-order logic) and use this aggregation technique
to prove that the Delayed mode of the FLASH memory system is sequentially consistent. Akhiani et
al. [3] summarize their experience with using TLA+ (a form of temporal logic) and a combination of manual
proofs and a TLA+ model checker (TLC) to specify and verify the Compaq Alpha 21264 and 21364 memory
system protocols. Although they did find a bug that would not have been caught by simulation or model
checking, their manual proofs were quite large and only a small portion could be finished even with 4 people
and 7 person-months of effort. The TLA+ specifications are complete and formal, but they are both nearly
two thousand lines long. Nalumasu et al. [11, 18] propose an extension of Collier's ArchTest suite which
provides a collection of programs that test certain properties of a memory model. Their extension creates the
effect of having infinitely long test programs (and thus checking all possible interleavings of test programs)
by abstracting the test programs into non-deterministic finite automata which drive formal specifications of
the system being verified. Both the automata and the implementations were specified in Verilog and the VIS
symbolic model checker was used to verify that various invariants are satisfied by the system when driven by
these automata. The technique is useful in practice and has been applied to commercial systems such as the
HP PA-8000 Runway bus protocol. However, it is incomplete in that the invariants being tested do not imply
SC (they are necessary, but not sufficient).
Automated techniques: Henzinger et al. [14] provide completely automated proofs of lazy and a certain
snoopy cache coherence protocol using the MOCHA model checker. Their protocol specifications (with the
system being expressed in a language similar to a typical imperative programming language and the proof
requirements expressed in temporal logic) are augmented with a specification of a finite observer which
can reorder protocol transactions in order to produce a witness ordering which satisfies the definition of a
memory model. They provide such observers for the two protocols they specify in the paper. However, the
general problem of verifying sequential consistency is undecidable and such finite observers do not exist for
the protocols we specify in this paper or in the protocols used in modern high-performance shared-memory
multiprocessors.
To the best of our knowledge, there are no published examples of a completely automated proof of correctness
of a system specified at a low level of abstraction.
Conclusions
In this paper, we have developed a specification methodology that documents and specifies a cache coherence
protocol in eight tables: the states, events, actions, and transitions of the cache and memory controllers.
We have used this methodology to specify a detailed, low-level three-state broadcast snooping protocol with
an unordered data network and an ordered address network which allows arbitrary skew. We have also presented
a detailed, low-level specification of the Multicast Snooping protocol [5], and, in doing so, we have
shown the utility of the table-based specification methodology. Lastly, we have demonstrated a technique for
verification of the Multicast Snooping protocol, through the sketch of a manual proof that the specification
satisfies a sequentially consistent memory model.

Acknowledgments

This work is supported in part by the National Science Foundation with grants EIA-9971256, MIPS-
9625558, MIP-9225097, CCR 9257241, and CDA-9623632, a Wisconsin Romnes Fellowship, and donations
from Sun Microsystems and Intel Corporation. Members of the Wisconsin Multifacet Project contributed
significantly to improving the protocols and protocol specification model presented in this paper,
especially Anastassia Ailamaki, Ross Dickson, Charles Fischer, and Carl Mauer.


--R

Designing Memory Consistency Models for Shared-Memory Multiprocessors





Parallel Computer Architecture: A Hardware/Software Approach.


Memory Consistency Models for Shared-Memory Multiprocessors


Computer Architecture: A Quantitative Approach.














--TR
Cache coherence protocols: evaluation using a multiprocessor simulation model
A class of compatible cache consistency protocols and their support by the IEEE futurebus
Proving sequential consistency of high-performance shared memories (extended abstract)
Lazy caching
Designing memory consistency models for shared-memory multiprocessors
An executable specification, analyzer and verifier for RMO (relaxed memory order)
Verification of FLASH cache coherence protocol by aggregation of distributed transactions
Memory consistency models for shared-memory multiprocessors
Verification techniques for cache coherence protocols
Lamport clocks
Using MYAMPERSANDldquo;test model-checkingMYAMPERSANDrdquo; to verify the Runway-PA8000 memory model
Design Verification of the S3.mp Cache-Coherent Shared-Memory System
Computer architecture (2nd ed.)
Multicast snooping
A system-level specification framework for I/O architectures
Formal Automatic Verification of Cache Coherence in Multiprocessors with Relaxed Memory Models
Time, clocks, and the ordering of events in a distributed system
Introduction To Automata Theory, Languages, And Computation
Verifying a Multiprocessor Cache Controller Using Random Test Generation
Cache Coherence Verification with TLA+
The ''Test Model-Checking'' Approach to the Verification of Formal Memory Models of Multiprocessors
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems
Using Formal Verification/Analysis Methods on the Critical Path in System Design
Origin System Design Methodology and Experience
Using Lamport Clocks to Reason About Relaxed Memory Models

--CTR
Collin McCurdy , Charles Fischer, Using Pin as a memory reference generator for multiprocessor simulation, ACM SIGARCH Computer Architecture News, v.33 n.5, December 2005
Collin McCurdy , Charles Fischer, A localizing directory coherence protocol, Proceedings of the 3rd workshop on Memory performance issues: in conjunction with the 31st international symposium on computer architecture, p.23-29, June 20-20, 2004, Munich, Germany
Ahmed Louri , Avinash Karanth Kodi, An Optical Interconnection Network and a Modified Snooping Protocol for the Design of Large-Scale Symmetric Multiprocessors (SMPs), IEEE Transactions on Parallel and Distributed Systems, v.15 n.12, p.1093-1104, December 2004
Milo M. K. Martin , Daniel J. Sorin , Bradford M. Beckmann , Michael R. Marty , Min Xu , Alaa R. Alameldeen , Kevin E. Moore , Mark D. Hill , David A. Wood, Multifacet's general execution-driven multiprocessor simulator (GEMS) toolset, ACM SIGARCH Computer Architecture News, v.33 n.4, November 2005
Felix Garcia-Carballeira , Jesus Carretero , Alejandro Calderon , Jose M. Perez , Jose D. Garcia, An Adaptive Cache Coherence Protocol Specification for Parallel Input/Output Systems, IEEE Transactions on Parallel and Distributed Systems, v.15 n.6, p.533-545, June 2004
Milo M. K. Martin , Pacia J. Harper , Daniel J. Sorin , Mark D. Hill , David A. Wood, Using destination-set prediction to improve the latency/bandwidth tradeoff in shared-memory multiprocessors, ACM SIGARCH Computer Architecture News, v.31 n.2, May
Michael R. Marty , Mark D. Hill, Coherence Ordering for Ring-based Chip Multiprocessors, Proceedings of the 39th Annual IEEE/ACM International Symposium on Microarchitecture, p.309-320, December 09-13, 2006
memory consistency;protocol specification;cache coherence;protocol verification;multicast snooping