3 * Copyright (c) 1999-2005 Mark D. Hill and David A. Wood
6 * Redistribution and use in source and binary forms, with or without
7 * modification, are permitted provided that the following conditions are
8 * met: redistributions of source code must retain the above copyright
9 * notice, this list of conditions and the following disclaimer;
10 * redistributions in binary form must reproduce the above copyright
11 * notice, this list of conditions and the following disclaimer in the
12 * documentation and/or other materials provided with the distribution;
13 * neither the name of the copyright holders nor the names of its
14 * contributors may be used to endorse or promote products derived from
15 * this software without specific prior written permission.
17 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
18 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
19 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
20 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
21 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
22 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
23 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
24 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
25 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
26 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
27 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
31 * $Id: MOESI_token-dir.sm 1.5 04/11/17 14:07:50-06:00 mikem@emperor15.cs.wisc.edu $
34 machine(Directory, "Token protocol") {
36 MessageBuffer responseFromDir, network="To", virtual_network="0", ordered="false";
38 MessageBuffer responseToDir, network="From", virtual_network="0", ordered="false";
39 MessageBuffer requestToDir, network="From", virtual_network="1", ordered="false";
40 MessageBuffer persistentToDir, network="From", virtual_network="2", ordered="true";
44 enumeration(State, desc="Directory states", default="Directory_State_O") {
52 enumeration(Event, desc="Directory events") {
53 GETX, desc="A GETX arrives";
54 GETS, desc="A GETS arrives";
55 Lockdown, desc="A lockdown request arrives";
56 Unlockdown, desc="An un-lockdown request arrives";
57 Data_Owner, desc="Data arrive, includes the owner token";
58 Data_Shared, desc="Data arrive, does not include the owner token";
59 Ack, desc="Tokens arrive";
60 Ack_Owner, desc="Tokens arrive, including the owner token";
66 structure(Entry, desc="...") {
67 State DirectoryState, desc="Directory state";
68 DataBlock DataBlk, desc="data for the block";
69 int Tokens, default="max_tokens()", desc="Number of tokens for the line we're holding";
72 external_type(DirectoryMemory) {
73 Entry lookup(Address);
74 bool isPresent(Address);
79 DirectoryMemory directory, constructor_hack="i";
81 PersistentTable persistentTable, constructor_hack="i";
83 State getState(Address addr) {
84 return directory[addr].DirectoryState;
87 void setState(Address addr, State state) {
88 directory[addr].DirectoryState := state;
90 if (state == State:L) {
91 assert(directory[addr].Tokens == 0);
94 // Make sure the token count is in range
95 assert(directory[addr].Tokens >= 0);
96 assert(directory[addr].Tokens <= max_tokens());
98 if (state == State:O) {
99 assert(directory[addr].Tokens >= 1); // Must have at least one token
100 assert(directory[addr].Tokens >= (max_tokens() / 2)); // Only mostly true; this might not always hold
105 out_port(responseNetwork_out, ResponseMsg, responseFromDir);
109 in_port(persistentNetwork_in, PersistentMsg, persistentToDir) {
110 if (persistentNetwork_in.isReady()) {
111 peek(persistentNetwork_in, PersistentMsg) {
113 // Apply the lockdown or unlockdown message to the table
114 if (in_msg.Type == PersistentRequestType:GETX_PERSISTENT) {
115 persistentTable.persistentRequestLock(in_msg.Address, in_msg.Requestor, AccessType:Write);
116 } else if (in_msg.Type == PersistentRequestType:GETS_PERSISTENT) {
117 persistentTable.persistentRequestLock(in_msg.Address, in_msg.Requestor, AccessType:Read);
118 } else if (in_msg.Type == PersistentRequestType:DEACTIVATE_PERSISTENT) {
119 persistentTable.persistentRequestUnlock(in_msg.Address, in_msg.Requestor);
121 error("Invalid message");
124 // React to the message based on the current state of the table
125 if (persistentTable.isLocked(in_msg.Address)) {
126 trigger(Event:Lockdown, in_msg.Address); // locked
128 trigger(Event:Unlockdown, in_msg.Address); // unlocked
134 in_port(requestNetwork_in, RequestMsg, requestToDir) {
135 if (requestNetwork_in.isReady()) {
136 peek(requestNetwork_in, RequestMsg) {
137 if (in_msg.Type == CoherenceRequestType:GETS) {
138 trigger(Event:GETS, in_msg.Address);
139 } else if (in_msg.Type == CoherenceRequestType:GETX) {
140 trigger(Event:GETX, in_msg.Address);
142 error("Invalid message");
148 in_port(responseNetwork_in, ResponseMsg, responseToDir) {
149 if (responseNetwork_in.isReady()) {
150 peek(responseNetwork_in, ResponseMsg) {
151 if (in_msg.Type == CoherenceResponseType:DATA_OWNER) {
152 trigger(Event:Data_Owner, in_msg.Address);
153 } else if (in_msg.Type == CoherenceResponseType:ACK) {
154 trigger(Event:Ack, in_msg.Address);
155 } else if (in_msg.Type == CoherenceResponseType:DATA_SHARED) {
156 trigger(Event:Data_Shared, in_msg.Address);
157 } else if (in_msg.Type == CoherenceResponseType:ACK_OWNER) {
158 trigger(Event:Ack_Owner, in_msg.Address);
160 error("Invalid message");
169 action(a_sendTokens, "a", desc="Send tokens to requestor") {
170 // Only send a message if we have tokens to send
171 if (directory[address].Tokens > 0) {
172 peek(requestNetwork_in, RequestMsg) {
173 enqueue(responseNetwork_out, ResponseMsg, latency="DIRECTORY_LATENCY") {
174 out_msg.Address := address;
175 out_msg.Type := CoherenceResponseType:ACK;
176 out_msg.Sender := machineID;
177 out_msg.SenderMachine := MachineType:Directory;
178 out_msg.Destination.add(in_msg.Requestor);
179 out_msg.DestMachine := MachineType:L1Cache;
180 out_msg.Tokens := directory[in_msg.Address].Tokens;
181 out_msg.MessageSize := MessageSizeType:Response_Control;
184 directory[address].Tokens := 0;
188 action(aa_sendTokensToStarver, "\a", desc="Send tokens to starver") {
189 // Only send a message if we have tokens to send
190 if (directory[address].Tokens > 0) {
191 enqueue(responseNetwork_out, ResponseMsg, latency="DIRECTORY_LATENCY") {
192 out_msg.Address := address;
193 out_msg.Type := CoherenceResponseType:ACK;
194 out_msg.Sender := machineID;
195 out_msg.SenderMachine := MachineType:Directory;
196 out_msg.Destination.add(persistentTable.findSmallest(address));
197 out_msg.DestMachine := MachineType:L1Cache;
198 out_msg.Tokens := directory[address].Tokens;
199 out_msg.MessageSize := MessageSizeType:Response_Control;
201 directory[address].Tokens := 0;
206 action(d_sendDataWithAllTokens, "d", desc="Send data and tokens to requestor") {
207 peek(requestNetwork_in, RequestMsg) {
208 enqueue(responseNetwork_out, ResponseMsg, latency="MEMORY_LATENCY") {
209 out_msg.Address := address;
210 out_msg.Type := CoherenceResponseType:DATA_OWNER;
211 out_msg.Sender := machineID;
212 out_msg.SenderMachine := MachineType:Directory;
213 out_msg.Destination.add(in_msg.Requestor);
214 out_msg.DestMachine := MachineType:L1Cache;
215 assert(directory[address].Tokens > 0);
216 out_msg.Tokens := directory[in_msg.Address].Tokens;
217 out_msg.DataBlk := directory[in_msg.Address].DataBlk;
218 out_msg.Dirty := false;
219 out_msg.MessageSize := MessageSizeType:Response_Data;
222 directory[address].Tokens := 0;
225 action(dd_sendDataWithAllTokensToStarver, "\d", desc="Send data and tokens to starver") {
226 enqueue(responseNetwork_out, ResponseMsg, latency="MEMORY_LATENCY") {
227 out_msg.Address := address;
228 out_msg.Type := CoherenceResponseType:DATA_OWNER;
229 out_msg.Sender := machineID;
230 out_msg.SenderMachine := MachineType:Directory;
231 out_msg.Destination.add(persistentTable.findSmallest(address));
232 out_msg.DestMachine := MachineType:L1Cache;
233 assert(directory[address].Tokens > 0);
234 out_msg.Tokens := directory[address].Tokens;
235 out_msg.DataBlk := directory[address].DataBlk;
236 out_msg.Dirty := false;
237 out_msg.MessageSize := MessageSizeType:Response_Data;
239 directory[address].Tokens := 0;
242 action(f_incrementTokens, "f", desc="Increment the number of tokens we're tracking") {
243 peek(responseNetwork_in, ResponseMsg) {
244 assert(in_msg.Tokens >= 1);
245 directory[address].Tokens := directory[address].Tokens + in_msg.Tokens;
250 action(j_popIncomingRequestQueue, "j", desc="Pop incoming request queue") {
251 requestNetwork_in.dequeue();
254 action(k_popIncomingResponseQueue, "k", desc="Pop incoming response queue") {
255 responseNetwork_in.dequeue();
258 action(l_popIncomingPersistentQueue, "l", desc="Pop incoming persistent queue") {
259 persistentNetwork_in.dequeue();
262 action(m_writeDataToMemory, "m", desc="Write dirty writeback to memory") {
263 peek(responseNetwork_in, ResponseMsg) {
264 directory[in_msg.Address].DataBlk := in_msg.DataBlk;
265 DEBUG_EXPR(in_msg.Address);
266 DEBUG_EXPR(in_msg.DataBlk);
270 action(n_checkIncomingMsg, "n", desc="Check incoming token message") {
271 peek(responseNetwork_in, ResponseMsg) {
272 assert(in_msg.Type == CoherenceResponseType:ACK_OWNER);
273 assert(in_msg.Dirty == false);
274 assert(in_msg.MessageSize == MessageSizeType:Writeback_Control);
275 assert(directory[in_msg.Address].DataBlk == in_msg.DataBlk);
279 action(r_bounceResponse, "r", desc="Bounce response to starving processor") {
280 peek(responseNetwork_in, ResponseMsg) {
281 enqueue(responseNetwork_out, ResponseMsg, latency="NULL_LATENCY") {
282 out_msg.Address := address;
283 out_msg.Type := in_msg.Type;
284 out_msg.Sender := machineID;
285 out_msg.SenderMachine := MachineType:Directory;
286 out_msg.Destination.add(persistentTable.findSmallest(address));
287 out_msg.DestMachine := MachineType:L1Cache;
288 out_msg.Tokens := in_msg.Tokens;
289 out_msg.DataBlk := in_msg.DataBlk;
290 out_msg.Dirty := in_msg.Dirty;
291 out_msg.MessageSize := in_msg.MessageSize;
296 action(s_bounceDatalessOwnerToken, "s", desc="Bounce clean owner token to starving processor") {
297 peek(responseNetwork_in, ResponseMsg) {
298 assert(in_msg.Type == CoherenceResponseType:ACK_OWNER);
299 assert(in_msg.Dirty == false);
300 assert(in_msg.MessageSize == MessageSizeType:Writeback_Control);
302 // NOTE: The following check would not be valid in a real
303 // implementation. We include the data in the "dataless"
304 // message so we can assert the clean data matches the datablock
306 assert(directory[in_msg.Address].DataBlk == in_msg.DataBlk);
308 // Bounce the message, but "re-associate" the data and the owner
309 // token. In essence we're converting an ACK_OWNER message to a
310 // DATA_OWNER message, keeping the number of tokens the same.
311 enqueue(responseNetwork_out, ResponseMsg, latency="NULL_LATENCY") {
312 out_msg.Address := address;
313 out_msg.Type := CoherenceResponseType:DATA_OWNER;
314 out_msg.Sender := machineID;
315 out_msg.SenderMachine := MachineType:Directory;
316 out_msg.Destination.add(persistentTable.findSmallest(address));
317 out_msg.DestMachine := MachineType:L1Cache;
318 out_msg.Tokens := in_msg.Tokens;
319 out_msg.DataBlk := directory[in_msg.Address].DataBlk;
320 out_msg.Dirty := in_msg.Dirty;
321 out_msg.MessageSize := MessageSizeType:Response_Data;
329 transition(O, GETX, NO) {
330 d_sendDataWithAllTokens;
331 j_popIncomingRequestQueue;
334 transition(O, GETS, NO) {
335 d_sendDataWithAllTokens;
336 // Since we found the owner, no need to forward
337 j_popIncomingRequestQueue;
340 transition(O, Lockdown, L) {
341 dd_sendDataWithAllTokensToStarver;
342 l_popIncomingPersistentQueue;
345 transition(O, {Data_Shared, Ack}) {
347 k_popIncomingResponseQueue;
351 transition(NO, GETX) {
353 j_popIncomingRequestQueue;
356 transition(NO, GETS) {
357 j_popIncomingRequestQueue;
360 transition(NO, Lockdown, L) {
361 aa_sendTokensToStarver;
362 l_popIncomingPersistentQueue;
365 transition(NO, Data_Owner, O) {
368 k_popIncomingResponseQueue;
371 transition(NO, Ack_Owner, O) {
374 k_popIncomingResponseQueue;
377 transition(NO, {Data_Shared, Ack}) {
379 k_popIncomingResponseQueue;
383 transition(L, {GETX, GETS}) {
384 j_popIncomingRequestQueue;
387 transition(L, Lockdown) {
388 l_popIncomingPersistentQueue;
391 transition(L, {Data_Owner, Data_Shared, Ack}) {
393 k_popIncomingResponseQueue;
396 transition(L, Ack_Owner) {
397 s_bounceDatalessOwnerToken;
398 k_popIncomingResponseQueue;
401 transition(L, Unlockdown, NO) {
402 l_popIncomingPersistentQueue;