| %& latex |
| \documentclass[11pt]{article} |
| \usepackage{graphics} |
| \usepackage{color} |
| |
| \textheight 9.0 in |
| \topmargin -0.5 in |
| \textwidth 6.5 in |
| \oddsidemargin -0.0 in |
| \evensidemargin -0.0 in |
| |
| \begin{document} |
| |
| \definecolor{dark}{gray}{0.5} |
| |
| \newcommand{\syntax}[1]{% |
| \begin{center} |
| \fbox{\tt \small |
| \begin{tabular}{l} |
| #1\end{tabular}}\end{center}} |
| |
| \begin{center} |
| {\LARGE Tutorial for SLICC v0.2} \\ |
| \vspace{.25in} |
| {\large Milo Martin} \\ |
| {\large 8/25/1999} |
| \end{center} |
| |
| \section*{Overview} |
| |
| This document attempts to illustrate the syntax and expressiveness of |
| the cache coherence protocol specification language through a small |
| example. A ``stupido'' cache coherence protocol is described in prose |
| and then expressed in the language. |
| |
| The protocol used as the running example is described. Then each of |
| the elements of the protocol is discussed and expressed in the |
| language: states, events, transitions, and actions. |
| |
| \section*{Protocol Description} |
| |
| In order to make this example a simple as possible, the protocol |
| described is a simple as possible and makes many simplifying |
| assumptions. These simplifications were made only to clarify the |
| exposition and are not indications of limitations of the |
| expressiveness of the description language. We have already specified |
| a more complicated MSI broadcast snooping protocol, a multicast |
| snooping protocol, and a directory protocol. The simplifying |
| assumptions are listed below. The remaining details of the protocol |
| are described in the sections where we give the syntax of the |
| language. |
| |
| \begin{itemize} |
| |
| \item |
| The protocol uses broadcast snooping that assumes that a broadcast can |
| only occur if all processors have processed all of their incoming |
| address transactions. In essence, when a processor issue an address |
| request, that request will be next in the global order. This allows |
| us to avoid needed to handle the cases before we have observed our |
| request in the global order. |
| |
| \item |
| The protocol has only Modified and Idle stable states. (Note: Even |
| the Shared state is omitted.) |
| |
| \item |
| To avoid describing replacement (PutX's) and writebacks, the caches |
| are in treated as infinite in size. |
| |
| \item |
| No forward progress bit is used, so the protocol as specified does not |
| guarantee forward progress. |
| |
| \item |
| Only the mandatory request queue is used. No optional or prefetch |
| queue is described. |
| |
| \item |
| The above simplifications reduce the need for TBEs (Translation Buffer |
| Entries) and thus the idea of a TBE is not include. |
| |
| \item |
| Each memory module is assumed to have some state associated with each |
| cache block in the memory. This requires a simple directory/memory |
| state machine to work as a compliment to the processor state machine. |
| Traditional broadcast snooping protocols often have no ``directory'' |
| state in the memory. |
| |
| \end{itemize} |
| |
| \section*{Protocol Messages} |
| |
| Cache coherence protocols communicate by sending well defined |
| messages. To fully specify a cache coherence protocol we need to be |
| able to specify the message types and fields. For this protocol we |
| have address messages ({\tt AddressMsg}) which are broadcast, and data |
| messages ({\tt DataMsg}) which are point-to-point. Address messages |
| have an address field ({\tt Address}), a request type ({\tt Type}), |
| and which processor made the request ({\tt Requestor}). Data message |
| have an address field ({\tt Address}), a destination ({\tt |
| Destination}), and the actual cache block being transfered ({\tt |
| DataBlk}). The names in parenthesis are important because those are |
| the names which code later in the specification will reference various |
| message types and fields in the messages. |
| |
| Messages are declared by creating types with {\tt new\_type()} and |
| adding fields with {\tt type\_field()}. The exact syntax for |
| declaring types and message is a bit ugly right now and is going to be |
| changed in the near future. If you wish, please see the appendix for |
| an example of the current syntax. |
| |
| |
| |
| \section*{Cache States} |
| |
| Idle and Modified are the two stable states in our protocol. In |
| addition the we have a single transient processor state. This state |
| is used after a processor has issued a request and is waiting for the |
| data response to arrive. |
| |
| Declaring states in the language is the first of a number of |
| declarations we will be using. All of these declarations have a |
| similar format. Below is the format for a state declaration. |
| |
| \syntax{ |
| {\tt state({\em identifier}, {\em shorthand}, {\em pair1}, {\em pair2}, ...);} |
| } |
| |
| {\em identifier} is a name that is used later to |
| refer to this state later in the description. It must start with a |
| letter and after than can have any combination of letters, numbers, |
| and the underscore character. {\em shorthand} is a quoted string |
| which contains the shorthand that should be used for the state when |
| generating tables and such. |
| |
| The {\em pair}'s are used to associate arbitrary information with each |
| state. Zero or more pairs can be included in each declaration. For |
| example we want to have a more verbose description of each state when |
| we generate the table which contains the states and descriptions. |
| This information is encoded in the language by adding a {\tt desc} |
| parameter to a declaration. The name of the parameter is followed by |
| an equal sign and a string with the description. The {\tt desc} pair |
| technically optional, however the table generation tool will complain |
| about a missing description if it is not present. |
| |
| The three states for our protocol are expressed as follows: |
| |
| \begin{verbatim} |
| state(I, "I", desc="Idle"); |
| state(M, "M", desc="Modified"); |
| state(IM, "IM", desc="Idle, issued request but have not seen data yet"); |
| \end{verbatim} |
| |
| \section*{Cache Events} |
| |
| Events are external stimulus that cause the state machine to take |
| action. This is most often a message in one of the queues from the |
| network or processor. Events form the columns of the protocol table. |
| Our simple protocol has one event per incoming queue. When a message |
| is waiting in one of these queues and event can occur. We can see a |
| request from the processor in the mandatory queue, another processor's |
| request, or a data response. |
| |
| Events are declared in the language similarly to states. The {\em |
| identifier}, {\em shorthand}, and {\em pair}'s have the same purpose |
| as in a state declaration. |
| |
| \syntax{ |
| event({\em identifier}, {\em shorthand}, {\em pair1}, {\em pair2}, ...) \{ \\ |
| \hspace{.1in} {\em statement\_list} \\ |
| \} \\ |
| } |
| |
| Events are different in that they have a list of statements which |
| allows exact specification of when the event should ``trigger'' a |
| transition. These statements are mini-programming language with |
| syntax similar to that of C. For example the {\tt peek} construct in |
| this context checks to see if there is a message at the head of the |
| specified queue, and if so, conceptually copies the message to a |
| temporary variable accessed as {\tt in\_msg}. The language also |
| supports various procedure calls, functions, conditional statements, |
| assignment, and queue operations such as peek, enqueue and dequeue. |
| The {\tt trigger()} construct takes an address as the only parameter. |
| This is the address that should be triggered for the event. To give |
| you a feel for what this code looks like, the three events for our |
| simple protocol are below. |
| |
| \begin{verbatim} |
| event(LoadStore, "LoadStore", desc="Load or Store request from local processor") { |
| peek(mandatoryQueue_ptr, CacheMsg) { |
| trigger(in_msg.Address); |
| } |
| } |
| |
| event(Other_GETX, "Other GETX", desc="Observed a GETX request from another processor") { |
| peek(addressNetwork_ptr, AddressMsg) { |
| if (in_msg.Requestor != id) { |
| trigger(in_msg.Address); |
| } |
| } |
| } |
| |
| event(Data, "Data", desc="Data for this block from the data network") { |
| peek(dataNetwork_ptr, DataMsg) { |
| trigger(in_msg.Address); |
| } |
| } |
| \end{verbatim} |
| |
| \section*{Cache Actions} |
| |
| Actions are the privative operations that are performed by various |
| state transitions. These correspond (by convention) to the lower case |
| letters in the tables. We need several actions in our protocol |
| including issuing a GetX request, servicing a cache hit, send data |
| from the cache to the requestor, writing data into the cache, and |
| popping the various queues. |
| |
| The syntax of an action declaration is similar to an event |
| declaration. The difference is that statements in the statement list |
| are used to implement the desired action, and not triggering an event. |
| |
| \syntax{action({\em identifier}, {\em shorthand}, {\em pair1}, {\em pair2}, ...) \{ \\ |
| \hspace{.1in} {\em statement\_list} \\ |
| \} |
| } |
| |
| The actions for this protocol use more of the features of the |
| language. Some of the interesting case are discussed below. |
| |
| \begin{itemize} |
| |
| \item |
| To manipulate values we need assignment statements (notice the use of |
| {\verb+:=+} as the assignment operator). The action to write data |
| into the cache looks at the incoming data message and puts the data in |
| the cache. Notice the use of square brackets to lookup the block in |
| the cache based on the address of the block. |
| |
| \begin{verbatim} |
| action(w_writeDataToCache, "w", desc="Write data from data message into cache") { |
| peek(dataNetwork_ptr, DataMsg) { |
| cacheMemory_ptr[address].DataBlk := in_msg.DataBlk; |
| } |
| } |
| \end{verbatim} |
| |
| \item |
| In addition to peeking at queues, we also enqueue messages. The {\tt |
| enqueue} construct works similarly to the {\tt peek} construct. {\tt |
| enqueue} creates a temporary called {\tt out\_msg}. You can assign |
| the fields of this message. At the end of the {\tt enqueue} construct |
| the message is implicitly inserted in the outgoing queue of the |
| specified network. Notice also how the type of the message is |
| specified and how the assignment statements use the names of the |
| fields of the messages. {\tt address} is the address for which the |
| event was {\tt trigger}ed. |
| |
| \begin{verbatim} |
| action(g_issueGETX, "g", desc="Issue GETX.") { |
| enqueue(addressNetwork_ptr, AddressMsg) { |
| out_msg.Address := address; |
| out_msg.Type := "GETX"; |
| out_msg.Requestor := id; |
| } |
| } |
| \end{verbatim} |
| |
| \item |
| Some times we need to use both {\tt peek} and {\tt enqueue} together. |
| In this example we look at an incoming address request to figure out |
| who to whom to forward the data value. |
| |
| \begin{verbatim} |
| action(r_cacheToRequestor, "r", desc="Send data from the cache to the requestor") { |
| peek(addressNetwork_ptr, AddressMsg) { |
| enqueue(dataNetwork_ptr, DataMsg) { |
| out_msg.Address := address; |
| out_msg.Destination := in_msg.Requestor; |
| out_msg.DataBlk := cacheMemory_ptr[address].DataBlk; |
| } |
| } |
| } |
| \end{verbatim} |
| |
| \item |
| We also need to pop the various queues. |
| \begin{verbatim} |
| action(k_popMandatoryQueue, "k", desc="Pop mandatory queue.") { |
| dequeue(mandatoryQueue_ptr); |
| } |
| \end{verbatim} |
| |
| \item |
| Finally we have the ability to call procedures and functions. The |
| following is an example of a procedure call. Currently all of the |
| procedures and functions are used to handle all of the more specific |
| operations. These are currently hard coded into the generator. |
| |
| \begin{verbatim} |
| action(h_hit, "h", desc="Service load/store from the cache.") { |
| serviceLdSt(address, cacheMemory_ptr[address].DataBlk); |
| } |
| \end{verbatim} |
| |
| \end{itemize} |
| |
| \section*{Cache Transitions} |
| |
| The cross product of states and events gives us the set of possible |
| transitions. For example, for our example protocol the empty would |
| be: |
| |
| \begin{center} |
| \begin{tabular}{|l||l|l|l|} \hline |
| & LoadStore & Other GETX & Data \\ \hline \hline |
| I & & & \\ \hline |
| M & & & \\ \hline |
| IM & & & \\ \hline |
| \end{tabular} |
| \end{center} |
| |
| |
| Transitions are atomic and are the heart of the protocol |
| specification. The transition specifies both what the next state, and |
| also what actions are performed for each unique state/event pair. The |
| transition declaration looks different from the other declarations: |
| |
| \syntax{ |
| transition({\em state}, {\em event}, {\em new\_state}, {\em pair1}, {\em pair2}, ...) \{ \\ |
| \hspace{.1in} {\em action\_identifier\_list}\\ |
| \} |
| } |
| |
| {\em state} and {\em event} are the pair which uniquely identifies the |
| transition. {\em state} correspond to the row where {\em event} |
| selects the column. {\em new\_state} is an optional parameter. If |
| {\em new\_state} is specified, that is the state when the atomic |
| transition is completed. If the parameter is omitted there is assumed |
| to be no state change. An impossible transition is specified by |
| simply not declaring an event for that state/event pair. |
| |
| We also place list of actions in the curly braces. The {\em |
| action\_identifier}'s correspond to the identifier specified as the |
| first parameter of an action declaration. The action list is a list |
| of operations to be performed when this transition occurs. The |
| actions also knows what preconditions are necessary are required for |
| the action to be performed. For example a necessary precondition for |
| an action which sends a message is that there is a space available in |
| the outgoing queue. Each transition is considered atomic, and thus |
| the generated code ensures that all of the actions can be completed |
| before performing and of the actions. |
| |
| In our running example protocol it is only possible to receive data in |
| the {\em IM} state. The other seven cases can occur and are declared |
| as follows. Below are a couple of examples. See the appendix for a |
| complete list. |
| |
| \newpage |
| \begin{verbatim} |
| transition(I, LoadStore, IM) { |
| g_issueGETX; |
| } |
| |
| transition(M, LoadStore) { |
| h_hit; |
| k_popMandatoryQueue; |
| } |
| |
| transition(M, Other_GETX, I) { |
| r_cacheToRequestor; |
| i_popAddressQueue; |
| } |
| \end{verbatim} |
| |
| From the above declarations we can generate a table. Each box can |
| have lower case letters which corresponds to the list of actions |
| possibly followed by a slash and a state (in uppercase letters). If |
| there is no slash and state, the transition does not change the state. |
| |
| \begin{center} |
| \begin{tabular}{|l||l|l|l|} \hline |
| & LoadStore & Other GETX & Data \\ \hline \hline |
| I & g/IM & i & (impossible)\\ \hline |
| M & hk & ri/I & (impossible)\\ \hline |
| IM & z & z & wj/M \\ \hline |
| \end{tabular} |
| \end{center} |
| |
| There is a useful shorthand for specifying many transitions with the |
| same action. One or both of {\em event} and {\em state} can be a list |
| in curly braces. This defines the cross product of the sets in one |
| declaration. If no {\em new\_state} is specified none of the |
| transitions cause a state change. If {\em new\_state} is specified, |
| all of the transitions in the cross product of the sets has the same |
| next state. For example, in the below transitions both IM/LoadStore |
| and IM/Other\_GETX have the action {\tt z\_delayTrans}. |
| \begin{verbatim} |
| transition(IM, LoadStore) { |
| z_delayTrans; |
| } |
| |
| transition(IM, Other_GETX) { |
| z_delayTrans; |
| } |
| \end{verbatim} |
| These can be specified in a single declaration: |
| \begin{verbatim} |
| transition(IM, {LoadStore, Other_GETX}) { |
| z_delayTrans; |
| } |
| \end{verbatim} |
| |
| |
| \newpage |
| \section*{Appendix - Sample Cache Controller Specification} |
| |
| {\small |
| \begin{verbatim} |
| machine(processor, "Simple MI Processor") { |
| |
| // AddressMsg |
| new_type(AddressMsg, "AddressMsg", message="yes", desc=""); |
| type_field(AddressMsg, Address, "address", |
| desc="Physical address for this request", |
| c_type=PhysAddress, c_include="Address.hh", murphi_type=""); |
| type_field(AddressMsg, Type, "type", |
| desc="Type of request (GetS, GetX, PutX, etc)", |
| c_type=CoherenceRequestType, c_include="CoherenceRequestType.hh", murphi_type=""); |
| type_field(AddressMsg, Requestor, "requestor", |
| desc="Node who initiated the request", |
| c_type=ComponentID, c_include="ComponentID.hh", murphi_type=""); |
| |
| // DataMsg |
| new_type(DataMsg, "DataMsg", message="yes", desc=""); |
| type_field(DataMsg, Address, "address", |
| desc="Physical address for this request", |
| c_type=PhysAddress, c_include="Address.hh", murphi_type=""); |
| type_field(DataMsg, Destination, "destination", |
| desc="Node to whom the data is sent", |
| c_type=Set, c_include="Set.hh", murphi_type=""); |
| type_field(DataMsg, DataBlk, "data", |
| desc="Node to whom the data is sent", |
| c_type=DataBlock, c_include="DataBlock.hh", murphi_type=""); |
| |
| // CacheEntry |
| new_type(CacheEntry, "CacheEntry"); |
| type_field(CacheEntry, CacheState, "Cache state", desc="cache state", |
| c_type=CacheState, c_include="CacheState.hh", murphi_type=""); |
| type_field(CacheEntry, DataBlk, "data", desc="data for the block", |
| c_type=DataBlock, c_include="DataBlock.hh", murphi_type=""); |
| |
| // DirectoryEntry |
| new_type(DirectoryEntry, "DirectoryEntry"); |
| type_field(DirectoryEntry, DirectoryState, "Directory state", desc="Directory state", |
| c_type=DirectoryState, c_include="DirectoryState.hh", murphi_type=""); |
| type_field(DirectoryEntry, DataBlk, "data", desc="data for the block", |
| c_type=DataBlock, c_include="DataBlock.hh", murphi_type=""); |
| |
| \end{verbatim} |
| \newpage |
| \begin{verbatim} |
| // STATES |
| state(I, "I", desc="Idle"); |
| state(M, "M", desc="Modified"); |
| state(IM, "IM", desc="Idle, issued request but have not seen data yet"); |
| |
| // EVENTS |
| |
| // From processor |
| event(LoadStore, "LoadStore", desc="Load or Store request from local processor") { |
| peek(mandatoryQueue_ptr, CacheMsg) { |
| trigger(in_msg.Address); |
| } |
| } |
| |
| // From Address network |
| event(Other_GETX, "Other GETX", desc="Observed a GETX request from another processor") { |
| peek(addressNetwork_ptr, AddressMsg) { |
| if (in_msg.Requestor != id) { |
| trigger(in_msg.Address); |
| } |
| } |
| } |
| |
| // From Data network |
| event(Data, "Data", desc="Data for this block from the data network") { |
| peek(dataNetwork_ptr, DataMsg) { |
| trigger(in_msg.Address); |
| } |
| } |
| |
| // ACTIONS |
| action(g_issueGETX, "g", desc="Issue GETX.") { |
| enqueue(addressNetwork_ptr, AddressMsg) { |
| out_msg.Address := address; |
| out_msg.Type := "GETX"; |
| out_msg.Requestor := id; |
| } |
| } |
| |
| action(h_hit, "h", desc="Service load/store from the cache.") { |
| serviceLdSt(address, cacheMemory_ptr[address].DataBlk); |
| } |
| |
| action(i_popAddressQueue, "i", desc="Pop incoming address queue.") { |
| dequeue(addressNetwork_ptr); |
| } |
| |
| action(j_popDataQueue, "j", desc="Pop incoming data queue.") { |
| dequeue(dataNetwork_ptr); |
| } |
| |
| action(k_popMandatoryQueue, "k", desc="Pop mandatory queue.") { |
| dequeue(mandatoryQueue_ptr); |
| } |
| |
| action(r_cacheToRequestor, "r", desc="Send data from the cache to the requestor") { |
| peek(addressNetwork_ptr, AddressMsg) { |
| enqueue(dataNetwork_ptr, DataMsg) { |
| out_msg.Address := address; |
| out_msg.Destination := in_msg.Requestor; |
| out_msg.DataBlk := cacheMemory_ptr[address].DataBlk; |
| } |
| } |
| } |
| |
| action(w_writeDataToCache, "w", desc="Write data from data message into cache") { |
| peek(dataNetwork_ptr, DataMsg) { |
| cacheMemory_ptr[address].DataBlk := in_msg.DataBlk; |
| } |
| } |
| |
| action(z_delayTrans, "z", desc="Cannot be handled right now.") { |
| stall(); |
| } |
| |
| // TRANSITIONS |
| |
| // Transitions from Idle |
| transition(I, LoadStore, IM) { |
| g_issueGETX; |
| } |
| |
| transition(I, Other_GETX) { |
| i_popAddressQueue; |
| } |
| |
| // Transitions from Modified |
| transition(M, LoadStore) { |
| h_hit; |
| k_popMandatoryQueue; |
| } |
| |
| transition(M, Other_GETX, I) { |
| r_cacheToRequestor; |
| i_popAddressQueue; |
| } |
| |
| // Transitions from IM |
| transition(IM, {LoadStore, Other_GETX}) { |
| z_delayTrans; |
| } |
| |
| transition(IM, Data, M) { |
| w_writeDataToCache; |
| j_popDataQueue; |
| } |
| } |
| \end{verbatim} |
| } |
| \end{document} |
| |