src/mem/protocol/MOESI_SMP_directory-dir.sm

   1
   2 /*
   3  * Copyright (c) 1999-2005 Mark D. Hill and David A. Wood
   4  * All rights reserved.
   5  *
   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.
  16  *
  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.
  28  */
  29
  30 /*
  31  * $Id$
  32  */
  33
  34 machine(Directory, "Directory protocol") {
  35
  36   MessageBuffer forwardFromDir, network="To", virtual_network="1", ordered="false";
  37   MessageBuffer responseFromDir, network="To", virtual_network="2", ordered="false";
  38
  39   MessageBuffer requestToDir, network="From", virtual_network="0", ordered="false";
  40   MessageBuffer unblockToDir, network="From", virtual_network="3", ordered="false";
  41
  42   // STATES
  43   enumeration(State, desc="Directory states", default="Directory_State_I") {
  44     // Base states
  45     I, desc="Invalid";
  46     S, desc="Shared";
  47     O, desc="Owner";
  48     M, desc="Modified";
  49
  50     IS, desc="Blocked, was in idle";
  51     SS, desc="Blocked, was in shared";
  52     OO, desc="Blocked, was in owned";
  53     MO, desc="Blocked, going to owner or maybe modified";
  54     MM, desc="Blocked, going to modified";
  55
  56     MI, desc="Blocked on a writeback";
  57     OS, desc="Blocked on a writeback";
  58   }
  59
  60   // Events
  61   enumeration(Event, desc="Directory events") {
  62     GETX, desc="A GETX arrives";
  63     GETS, desc="A GETS arrives";
  64     PUTX, desc="A PUTX arrives";
  65     PUTO, desc="A PUTO arrives";
  66     Unblock, desc="An unblock message arrives";
  67     Last_Unblock, desc="An unblock message arrives, we're not waiting for any additional unblocks";
  68     Exclusive_Unblock, desc="The processor become the exclusive owner (E or M) of the line";
  69     Clean_Writeback, desc="The final message as part of a PutX/PutS, no data";
  70     Dirty_Writeback, desc="The final message as part of a PutX/PutS, contains data";
  71   }
  72
  73   // TYPES
  74
  75   // DirectoryEntry
  76   structure(Entry, desc="...") {
  77     State DirectoryState,          desc="Directory state";
  78     DataBlock DataBlk,             desc="data for the block";
  79     NetDest Sharers,                   desc="Sharers for this block";
  80     NetDest Owner,                     desc="Owner of this block";
  81     int WaitingUnblocks,           desc="Number of acks we're waiting for";
  82   }
  83
  84   external_type(DirectoryMemory) {
  85     Entry lookup(Address);
  86     bool isPresent(Address);
  87   }
  88
  89   // External function
  90   void profile_sharing(Address addr, AccessType type, NodeID requestor, Set sharers, Set owner);
  91
  92   // ** OBJECTS **
  93
  94   DirectoryMemory directory, constructor_hack="i";
  95
  96   State getState(Address addr) {
  97     return directory[addr].DirectoryState;
  98   }
  99
 100   void setState(Address addr, State state) {
 101     if (directory.isPresent(addr)) {
 102
 103       if ((state == State:I) || (state == State:IS)) {
 104         assert(directory[addr].Owner.count() == 0);
 105         assert(directory[addr].Sharers.count() == 0);
 106       }
 107
 108       if ((state == State:S) || (state == State:SS)) {
 109         assert(directory[addr].Owner.count() == 0);
 110         assert(directory[addr].Sharers.count() != 0);
 111       }
 112
 113       if ((state == State:O) || (state == State:OO)) {
 114         assert(directory[addr].Owner.count() == 1);
 115         assert(directory[addr].Sharers.isSuperset(directory[addr].Owner) == false);
 116       }
 117
 118       if (state == State:M) {
 119         assert(directory[addr].Owner.count() == 1);
 120         assert(directory[addr].Sharers.count() == 0);
 121       }
 122
 123       if ((state != State:SS) && (state != State:OO)) {
 124         assert(directory[addr].WaitingUnblocks == 0);
 125       }
 126
 127       directory[addr].DirectoryState := state;
 128     }
 129   }
 130
 131   // ** OUT_PORTS **
 132   out_port(forwardNetwork_out, RequestMsg, forwardFromDir);
 133   out_port(responseNetwork_out, ResponseMsg, responseFromDir);
 134   out_port(requestQueue_out, ResponseMsg, requestToDir); // For recycling requests
 135
 136   // ** IN_PORTS **
 137
 138   in_port(unblockNetwork_in, ResponseMsg, unblockToDir) {
 139     if (unblockNetwork_in.isReady()) {
 140       peek(unblockNetwork_in, ResponseMsg) {
 141         if (in_msg.Type == CoherenceResponseType:UNBLOCK) {
 142           if (directory[in_msg.Address].WaitingUnblocks == 1) {
 143             trigger(Event:Last_Unblock, in_msg.Address);
 144           } else {
 145             trigger(Event:Unblock, in_msg.Address);
 146           }
 147         } else if (in_msg.Type == CoherenceResponseType:UNBLOCK_EXCLUSIVE) {
 148           trigger(Event:Exclusive_Unblock, in_msg.Address);
 149         } else if (in_msg.Type == CoherenceResponseType:WRITEBACK_DIRTY) {
 150           trigger(Event:Dirty_Writeback, in_msg.Address);
 151         } else if (in_msg.Type == CoherenceResponseType:WRITEBACK_CLEAN) {
 152           trigger(Event:Clean_Writeback, in_msg.Address);
 153         } else {
 154           error("Invalid message");
 155         }
 156       }
 157     }
 158   }
 159
 160   in_port(requestQueue_in, RequestMsg, requestToDir) {
 161     if (requestQueue_in.isReady()) {
 162       peek(requestQueue_in, RequestMsg) {
 163         if (in_msg.Type == CoherenceRequestType:GETS) {
 164           trigger(Event:GETS, in_msg.Address);
 165         } else if (in_msg.Type == CoherenceRequestType:GETX) {
 166           trigger(Event:GETX, in_msg.Address);
 167         } else if (in_msg.Type == CoherenceRequestType:PUTX) {
 168           trigger(Event:PUTX, in_msg.Address);
 169         } else if (in_msg.Type == CoherenceRequestType:PUTO) {
 170           trigger(Event:PUTO, in_msg.Address);
 171         } else {
 172           error("Invalid message");
 173         }
 174       }
 175     }
 176   }
 177
 178   // Actions
 179
 180   action(a_sendWriteBackAck, "a", desc="Send writeback ack to requestor") {
 181     peek(requestQueue_in, RequestMsg) {
 182       enqueue(forwardNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
 183         out_msg.Address := address;
 184         out_msg.Type := CoherenceRequestType:WB_ACK;
 185         out_msg.Requestor := in_msg.Requestor;
 186         out_msg.Destination.add(in_msg.Requestor);
 187         out_msg.MessageSize := MessageSizeType:Writeback_Control;
 188       }
 189     }
 190   }
 191
 192   action(b_sendWriteBackNack, "b", desc="Send writeback nack to requestor") {
 193     peek(requestQueue_in, RequestMsg) {
 194       enqueue(forwardNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
 195         out_msg.Address := address;
 196         out_msg.Type := CoherenceRequestType:WB_NACK;
 197         out_msg.Requestor := in_msg.Requestor;
 198         out_msg.Destination.add(in_msg.Requestor);
 199         out_msg.MessageSize := MessageSizeType:Writeback_Control;
 200       }
 201     }
 202   }
 203
 204   action(c_clearOwner, "c", desc="Clear the owner field") {
 205     directory[address].Owner.clear();
 206   }
 207
 208   action(cc_clearSharers, "\c", desc="Clear the sharers field") {
 209     directory[address].Sharers.clear();
 210   }
 211
 212   action(d_sendData, "d", desc="Send data to requestor") {
 213     peek(requestQueue_in, RequestMsg) {
 214       enqueue(responseNetwork_out, ResponseMsg, latency="MEMORY_LATENCY") {
 215         out_msg.Address := address;
 216
 217         if (in_msg.Type == CoherenceRequestType:GETS && directory[address].Sharers.count() == 0) {
 218           out_msg.Type := CoherenceResponseType:DATA_EXCLUSIVE_CLEAN;
 219         } else {
 220           out_msg.Type := CoherenceResponseType:DATA;
 221         }
 222
 223         out_msg.Sender := machineID;
 224         out_msg.Destination.add(in_msg.Requestor);
 225         out_msg.DataBlk := directory[in_msg.Address].DataBlk;
 226         out_msg.Dirty := false; // By definition, the block is now clean
 227         out_msg.Acks := directory[address].Sharers.count();
 228         if (directory[address].Sharers.isElement(in_msg.Requestor)) {
 229           out_msg.Acks := out_msg.Acks - 1;
 230         }
 231         out_msg.MessageSize := MessageSizeType:Response_Data;
 232       }
 233     }
 234   }
 235
 236   action(e_ownerIsUnblocker, "e", desc="The owner is now the unblocker") {
 237     peek(unblockNetwork_in, ResponseMsg) {
 238       directory[address].Owner.clear();
 239       directory[address].Owner.add(in_msg.Sender);
 240     }
 241   }
 242
 243   action(f_forwardRequest, "f", desc="Forward request to owner") {
 244     peek(requestQueue_in, RequestMsg) {
 245       enqueue(forwardNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
 246         out_msg.Address := address;
 247         out_msg.Type := in_msg.Type;
 248         out_msg.Requestor := in_msg.Requestor;
 249         out_msg.Destination := directory[in_msg.Address].Owner;
 250         out_msg.Acks := directory[address].Sharers.count();
 251         if (directory[address].Sharers.isElement(in_msg.Requestor)) {
 252           out_msg.Acks := out_msg.Acks - 1;
 253         }
 254         out_msg.MessageSize := MessageSizeType:Forwarded_Control;
 255       }
 256     }
 257   }
 258
 259   action(g_sendInvalidations, "g", desc="Send invalidations to sharers, not including the requester") {
 260     peek(requestQueue_in, RequestMsg) {
 261       if ((directory[in_msg.Address].Sharers.count() > 1) ||
 262           ((directory[in_msg.Address].Sharers.count() > 0) && (directory[in_msg.Address].Sharers.isElement(in_msg.Requestor) == false))) {
 263         enqueue(forwardNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
 264           out_msg.Address := address;
 265           out_msg.Type := CoherenceRequestType:INV;
 266           out_msg.Requestor := in_msg.Requestor;
 267           out_msg.Destination := directory[in_msg.Address].Sharers;
 268           out_msg.Destination.remove(in_msg.Requestor);
 269           out_msg.MessageSize := MessageSizeType:Forwarded_Control;
 270         }
 271       }
 272     }
 273   }
 274
 275   action(i_popIncomingRequestQueue, "i", desc="Pop incoming request queue") {
 276     // Profile the request
 277     peek(requestQueue_in, RequestMsg) {
 278       if (in_msg.Type == CoherenceRequestType:GETX) {
 279         // profile_sharing(address, AccessType:Write, machineIDToNodeID(in_msg.Requestor), directory[address].Sharers, directory[address].Owner);
 280       } else if (in_msg.Type == CoherenceRequestType:GETS) {
 281         // profile_sharing(address, AccessType:Read, machineIDToNodeID(in_msg.Requestor), directory[address].Sharers, directory[address].Owner);
 282       }
 283     }
 284
 285     requestQueue_in.dequeue();
 286   }
 287
 288   action(j_popIncomingUnblockQueue, "j", desc="Pop incoming unblock queue") {
 289     unblockNetwork_in.dequeue();
 290   }
 291
 292   action(l_writeDataToMemory, "l", desc="Write PUTX/PUTO data to memory") {
 293     peek(unblockNetwork_in, ResponseMsg) {
 294       assert(in_msg.Dirty);
 295       assert(in_msg.MessageSize == MessageSizeType:Writeback_Data);
 296       directory[in_msg.Address].DataBlk := in_msg.DataBlk;
 297       DEBUG_EXPR(in_msg.Address);
 298       DEBUG_EXPR(in_msg.DataBlk);
 299     }
 300   }
 301
 302   action(ll_checkDataInMemory, "\l", desc="Check PUTX/PUTO data is same as in the memory") {
 303     peek(unblockNetwork_in, ResponseMsg) {
 304       assert(in_msg.Dirty == false);
 305       assert(in_msg.MessageSize == MessageSizeType:Writeback_Control);
 306
 307       // NOTE: The following check would not be valid in a real
 308       // implementation.  We include the data in the "dataless"
 309       // message so we can assert the clean data matches the datablock
 310       // in memory
 311       assert(directory[in_msg.Address].DataBlk == in_msg.DataBlk);
 312     }
 313   }
 314
 315   action(m_addUnlockerToSharers, "m", desc="Add the unlocker to the sharer list") {
 316     peek(unblockNetwork_in, ResponseMsg) {
 317       directory[address].Sharers.add(in_msg.Sender);
 318     }
 319   }
 320
 321   action(n_incrementOutstanding, "n", desc="Increment outstanding requests") {
 322     directory[address].WaitingUnblocks := directory[address].WaitingUnblocks + 1;
 323   }
 324
 325   action(o_decrementOutstanding, "o", desc="Decrement outstanding requests") {
 326     directory[address].WaitingUnblocks := directory[address].WaitingUnblocks - 1;
 327     assert(directory[address].WaitingUnblocks >= 0);
 328   }
 329
 330   //  action(z_stall, "z", desc="Cannot be handled right now.") {
 331     // Special name recognized as do nothing case
 332   //  }
 333
 334   action(zz_recycleRequest, "\z", desc="Recycle the request queue") {
 335     requestQueue_in.recycle();
 336   }
 337
 338   // TRANSITIONS
 339
 340   transition(I, GETX, MM) {
 341     d_sendData;
 342     i_popIncomingRequestQueue;
 343   }
 344
 345   transition(S, GETX, MM) {
 346     d_sendData;
 347     g_sendInvalidations;
 348     i_popIncomingRequestQueue;
 349   }
 350
 351   transition(I, GETS, IS) {
 352     d_sendData;
 353     i_popIncomingRequestQueue;
 354   }
 355
 356   transition({S, SS}, GETS, SS) {
 357     d_sendData;
 358     n_incrementOutstanding;
 359     i_popIncomingRequestQueue;
 360   }
 361
 362   transition({I, S, M}, PUTO) {
 363     b_sendWriteBackNack;
 364     i_popIncomingRequestQueue;
 365   }
 366
 367   transition({I, S, O}, PUTX) {
 368     b_sendWriteBackNack;
 369     i_popIncomingRequestQueue;
 370   }
 371
 372   transition(O, GETX, MM) {
 373     f_forwardRequest;
 374     g_sendInvalidations;
 375     i_popIncomingRequestQueue;
 376   }
 377
 378   transition({O, OO}, GETS, OO) {
 379     f_forwardRequest;
 380     n_incrementOutstanding;
 381     i_popIncomingRequestQueue;
 382   }
 383
 384   transition(M, GETX, MM) {
 385     f_forwardRequest;
 386     i_popIncomingRequestQueue;
 387   }
 388
 389   transition(M, GETS, MO) {
 390     f_forwardRequest;
 391     i_popIncomingRequestQueue;
 392   }
 393
 394   transition(M, PUTX, MI) {
 395     a_sendWriteBackAck;
 396     i_popIncomingRequestQueue;
 397   }
 398
 399   transition(O, PUTO, OS) {
 400     a_sendWriteBackAck;
 401     i_popIncomingRequestQueue;
 402   }
 403
 404   transition({MM, MO, MI, OS}, {GETS, GETX, PUTO, PUTX}) {
 405     zz_recycleRequest;
 406   }
 407
 408   transition({MM, MO}, Exclusive_Unblock, M) {
 409     cc_clearSharers;
 410     e_ownerIsUnblocker;
 411     j_popIncomingUnblockQueue;
 412   }
 413
 414   transition(MO, Unblock, O) {
 415     m_addUnlockerToSharers;
 416     j_popIncomingUnblockQueue;
 417   }
 418
 419   transition({IS, SS, OO}, {GETX, PUTO, PUTX}) {
 420     zz_recycleRequest;
 421   }
 422
 423   transition(IS, GETS) {
 424     zz_recycleRequest;
 425   }
 426
 427   transition(IS, Unblock, S) {
 428     m_addUnlockerToSharers;
 429     j_popIncomingUnblockQueue;
 430   }
 431
 432   transition(IS, Exclusive_Unblock, M) {
 433     cc_clearSharers;
 434     e_ownerIsUnblocker;
 435     j_popIncomingUnblockQueue;
 436   }
 437
 438   transition(SS, Unblock) {
 439     m_addUnlockerToSharers;
 440     o_decrementOutstanding;
 441     j_popIncomingUnblockQueue;
 442   }
 443
 444   transition(SS, Last_Unblock, S) {
 445     m_addUnlockerToSharers;
 446     o_decrementOutstanding;
 447     j_popIncomingUnblockQueue;
 448   }
 449
 450   transition(OO, Unblock) {
 451     m_addUnlockerToSharers;
 452     o_decrementOutstanding;
 453     j_popIncomingUnblockQueue;
 454   }
 455
 456   transition(OO, Last_Unblock, O) {
 457     m_addUnlockerToSharers;
 458     o_decrementOutstanding;
 459     j_popIncomingUnblockQueue;
 460   }
 461
 462   transition(MI, Dirty_Writeback, I) {
 463     c_clearOwner;
 464     cc_clearSharers;
 465     l_writeDataToMemory;
 466     j_popIncomingUnblockQueue;
 467   }
 468
 469   transition(OS, Dirty_Writeback, S) {
 470     c_clearOwner;
 471     l_writeDataToMemory;
 472     j_popIncomingUnblockQueue;
 473   }
 474
 475   transition(MI, Clean_Writeback, I) {
 476     c_clearOwner;
 477     cc_clearSharers;
 478     ll_checkDataInMemory;
 479     j_popIncomingUnblockQueue;
 480   }
 481
 482   transition(OS, Clean_Writeback, S) {
 483     c_clearOwner;
 484     ll_checkDataInMemory;
 485     j_popIncomingUnblockQueue;
 486   }
 487
 488   transition(MI, Unblock, M) {
 489     j_popIncomingUnblockQueue;
 490   }
 491
 492   transition(OS, Unblock, O) {
 493     j_popIncomingUnblockQueue;
 494   }
 495 }