Department of Computer Science
CPSC 513: Simple (Buggy) MSI Cache Coherence Protocol

Overview

This is a directory-based cache coherence protocol, as we discussed in class. The system consists of a bunch of processor/cache nodes hooked up via an interconnection network to a single memory/directory. The processor/caches (henceforth referred to as processors) generate requests for exclusive (modifiable) and shared (read-only) copies of memory addresses for their caches. At most one exclusive copy is allowed at any time, but there can be many shared copies as long as no processor has an exclusive copy. The memory/directory (henceforth referred to as the memory) keeps track of who has each address cached.

So, for example, if processors P1 and P2 have shared copies of address A1 cached, and processor P3 wants an exclusive copy, P3 sends a request for an exclusive copy to the memory, the memory sends invalidate messages to P1 and P2, P1 and P2 discard their copies of A1 and send invalidate acknowledgments back to the memory, and when the memory receives all the acknowledgments, it sends an exclusive copy to P3.

Processor/Cache Model

In order to avoid trying to model a processor running programs, we allow the processors to request shared or exclusive copies of any address non-deterministically. This generates a stream of memory references just as running programs would.

In order to avoid trying to model a real cache (with tag bits and replacement policies, etc.), we give each processor a cache big enough to hold all of memory.

For each address in the cache, the cache line can be in one of five states: Exclusive, Shared, Invalid, WaitExclusive, and WaitShared. The Exclusive, Shared, and Invalid states have the obvious meanings. The Wait states indicate the processor has sent a request for a shared or exclusive copy of this line, but hasn't received the reply from the memory yet. In addition, each cache line has a value field that indicates the current value cached for that address.

Memory/Directory Model

The memory obviously has a value for each possible address. In addition, each address also has a directory, which indicates the state of this line (Uncached, CachedShared, CachedExclusive, WaitingWriteBack, WaitingInvalidate), which processors have this line cached, and some temporary fields needed to keep track of requests waiting for writebacks or invalidation acknowledgments.

The WaitingWriteBack and WaitingInvalidate states indicate that this address is waiting to receive a writeback or invalidate before a pending request (some processor has requested shared or exclusive) can be served. When the writeback or last invalidate acknowledgment has arrived, the memory completes the transcation by sending the data reply to the processor indicated by the replyto field and setting its state to the value indicated by the replytype field.

If a request arrives for an address for which there is already a pending request, the memory sends a Retry message back to the requestor.

Network Model

Typically, often high-performance networks do not preserve message order, because different messages might end up taking different routes to get from the same source to the same destination. This cache coherence protocol assumes that the network does not preserve message order. However, the protocol does assume that the network does not lose messages.

Processors can send messages to memory. There are four possible message types a processor can send: ReqShared, ReqExclusive, InvAck and WriteBack. ReqShared and ReqExclusive request a shared or exclusive copy of an address from memory. InvAck is an invalidate acknowledgment, and WriteBack writes back data that had been cached exclusive.

There are four possible message types that memory can send to a processor: Data, Invalidate, ForcedWriteBack, and Retry. A Data message delivers data to the processor that requested it. Invalidate asks a processor to invalidate it's shared copy of an address. ForcedWriteBack asks a processor to write back its exclusively cached copy of an address. Retry tells a processor that the memory can't handle it's most recent request.

We will model the network as two multisets of messages. The multiset datatype is a Murphi data structure that gives an unordered collection of objects (in this case, messages). Murphi automatically provides symmetry reductions for multisets.

Transition Tables

Here are the details of the protocol. The columns before the vertical bar indicate preconditions necessary for that row of the table to apply. The column after the bar indicate what actions result if we take this transition. Blanks indicate a don't-care on preconditions or no-change on actions. Conditions that are not covered in the table should never occur. These tables are the definitive specification of the protocol.

Processor/Cache Initiated Transitions

The processors can decide to initiate activity for any address.

Present State: | New State: Send Message: Update Cached Value: Comments:
Invalid | WaitShared ReqShared Wants shared copy.
Invalid | WaitExclusive ReqExclusive Wants exclusive copy.
Exclusive | Invalid WriteBack Undefined Spontaneous write back.
Shared | Invalid Undefined Eviction of shared.
Exclusive | Exclusive Non-deterministic Can write arbitrary value.
``Undefined'' means that we use the Murphi Undefine statement to erase the value. ``Non-deterministic'' means we use a Ruleset to allow any value to be stored.

Processor/Cache Response to Message

This table describes what a processor does when it receives a message from memory. In each case, the action depends on the message received and the processor's current state (for the address specified in the message). In all cases, the incoming message is removed from network (i.e., cannot push messages back into network for later delivery).

Message: Present State: | New State: Send Message: Update Cached Value: Comments:
Data WaitShared | Shared From Message Shared req answered.
Data WaitExclusive | Exclusive From Message Exclusive req answered.
Data Invalid | Invalid Stale data message. Discard.
ForceWriteBack Exclusive | Invalid WriteBack Undefined Normal writeback.
ForceWriteBack WaitExclusive | Invalid InvAck ForcedWriteBack arrived before Data. Send an InvAck to distinguish this case. Will discard stale data when it arrives.
ForceWriteBack anything else | I must have written back already. Ignore.
Invalidate Shared | Invalid InvAck Undefined Normal invalidate.
Invalidate WaitShared | Invalid InvAck Invalidate arrived before Data. Will discard stale data when it arrives.
Invalidate anything else | InvAck I must have evicted already. Acknowledge invalidate.
Retry WaitShared | Invalid Failed request.
Retry WaitExclusive | Invalid Failed request.
``From Message'' indicates that the value contained in the Data message is copied into the cache.

Memory/Directory Response to Messages

This is the most complex table because we must keep track of who has a given address cached. The ``Sender Cached'' column tests whether the sender of this message is currently listed in the directory as having the address cached. The ``Last Sender'' column tests whether the sender of this message (InvAck) is the last one to respond (after which we know all invalidates are complete).

Message Present State Sender Cached Last Sender | New State Send Message Update Memory Value Update Sharing List Set replyto Set replytype Comments
ReqShared Uncached | CachedShared Data Add Sender First sharing request
ReqShared CachedShared | CachedShared Data Add Sender Add'l sharing request
ReqShared CachedExclusive Yes | CachedExclusive Retry Haven't received previous write back yet
ReqShared CachedExclusive No | WaitingWriteBack ForceWriteBack Sender CachedShared Must get write back before responding
ReqShared WaitingWriteBack | WaitingWriteBack Retry Pending transaction
ReqShared WaitingInvalidate | WaitingInvalidate Retry Pending transaction
ReqExclusive Yes | Retry Haven't received write back yet
ReqExclusive Uncached No | CachedExclusive Data Add Sender Normal exclusive req
ReqExclusive CachedShared No | WaitingInvalidate Invalidate All Sender CachedExclusive Must invalidate sharers before responding
ReqExclusive CachedExclusive No | WaitingWriteBack Invalidate All Sender CachedExclusive Must get write back before responding
ReqExclusive WaitingWriteBack No | WaitingWriteBack Retry Pending transaction
ReqExclusive WaitingInvalidate No | WaitingInvalidate Retry Pending transaction
WriteBack CachedExclusive | Uncached From Message Delete Sender Normal write back
WriteBack WaitingWriteBack | From replytype Data to replyto From Message Delete Sender, Add replyto Undefined Undefined Forced write back
InvAck WaitingInvalidate No | WaitingInvalidate Delete Sender Normal invalidate
InvAck WaitingInvalidate Yes | From replytype Data to replyto Delete Sender, Add replyto Undefined Undefined Last invalidate
InvAck WaitingWriteBack | From replytype Data to replyto Delete Sender, Add replyto Undefined Undefined Proc was forced to write back before data message arrived. Can proceed as if write back occurred.
For messages to be sent: ``Invalidate All'' indicates that an Invalidate message must be sent to all processors listed as having the address cached. The ``ForceWriteBack'' message is sent to the processor who has the address cached. ``Data to replyto'' indicates that a data message should be sent to the processor stored in the replyto variable. All other messages are sent to the processor who sent the message being responded to.

For the new state, ``From replytype'' indicates that the new state is copied from the value set in the replytype variable.