436 lines
15 KiB
Text
436 lines
15 KiB
Text
|
|
||
|
/*
|
||
|
* Copyright (c) 1999-2005 Mark D. Hill and David A. Wood
|
||
|
* All rights reserved.
|
||
|
*
|
||
|
* Redistribution and use in source and binary forms, with or without
|
||
|
* modification, are permitted provided that the following conditions are
|
||
|
* met: redistributions of source code must retain the above copyright
|
||
|
* notice, this list of conditions and the following disclaimer;
|
||
|
* redistributions in binary form must reproduce the above copyright
|
||
|
* notice, this list of conditions and the following disclaimer in the
|
||
|
* documentation and/or other materials provided with the distribution;
|
||
|
* neither the name of the copyright holders nor the names of its
|
||
|
* contributors may be used to endorse or promote products derived from
|
||
|
* this software without specific prior written permission.
|
||
|
*
|
||
|
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||
|
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||
|
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||
|
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||
|
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||
|
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||
|
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||
|
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||
|
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||
|
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||
|
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||
|
*/
|
||
|
|
||
|
/*
|
||
|
* $Id$
|
||
|
*/
|
||
|
|
||
|
|
||
|
machine(Directory, "Token protocol") {
|
||
|
|
||
|
MessageBuffer requestFromDir, network="To", virtual_network="1", ordered="false";
|
||
|
MessageBuffer responseFromDir, network="To", virtual_network="2", ordered="false";
|
||
|
|
||
|
MessageBuffer persistentToDir, network="From", virtual_network="3", ordered="true";
|
||
|
MessageBuffer requestToDir, network="From", virtual_network="1", ordered="false";
|
||
|
MessageBuffer responseToDir, network="From", virtual_network="2", ordered="false";
|
||
|
|
||
|
// STATES
|
||
|
enumeration(State, desc="Directory states", default="Directory_State_O") {
|
||
|
// Base states
|
||
|
O, desc="Owner";
|
||
|
NO, desc="Not Owner";
|
||
|
L, desc="Locked";
|
||
|
}
|
||
|
|
||
|
// Events
|
||
|
enumeration(Event, desc="Directory events") {
|
||
|
GETX, desc="A GETX arrives";
|
||
|
GETS, desc="A GETS arrives";
|
||
|
Lockdown, desc="A lockdown request arrives";
|
||
|
Unlockdown, desc="An un-lockdown request arrives";
|
||
|
Data_Owner, desc="Data arrive";
|
||
|
Ack_Owner, desc="Owner token arrived without data because it was clean";
|
||
|
Tokens, desc="Tokens arrive";
|
||
|
}
|
||
|
|
||
|
// TYPES
|
||
|
|
||
|
// DirectoryEntry
|
||
|
structure(Entry, desc="...") {
|
||
|
State DirectoryState, desc="Directory state";
|
||
|
DataBlock DataBlk, desc="data for the block";
|
||
|
int Tokens, default="max_tokens()", desc="Number of tokens for the line we're holding";
|
||
|
|
||
|
// The following state is provided to allow for bandwidth
|
||
|
// efficient directory-like operation. However all of this state
|
||
|
// is 'soft state' that does not need to be correct (as long as
|
||
|
// you're eventually willing to resort to broadcast.)
|
||
|
|
||
|
Set Owner, desc="Probable Owner of the line. More accurately, the set of processors who need to see a GetS or GetO. We use a Set for convenience, but only one bit is set at a time.";
|
||
|
Set Sharers, desc="Probable sharers of the line. More accurately, the set of processors who need to see a GetX";
|
||
|
}
|
||
|
|
||
|
external_type(DirectoryMemory) {
|
||
|
Entry lookup(Address);
|
||
|
bool isPresent(Address);
|
||
|
}
|
||
|
|
||
|
|
||
|
// ** OBJECTS **
|
||
|
|
||
|
DirectoryMemory directory, constructor_hack="i";
|
||
|
|
||
|
PersistentTable persistentTable, constructor_hack="i";
|
||
|
|
||
|
State getState(Address addr) {
|
||
|
return directory[addr].DirectoryState;
|
||
|
}
|
||
|
|
||
|
void setState(Address addr, State state) {
|
||
|
directory[addr].DirectoryState := state;
|
||
|
|
||
|
if (state == State:L) {
|
||
|
assert(directory[addr].Tokens == 0);
|
||
|
}
|
||
|
|
||
|
// We have one or zero owners
|
||
|
assert((directory[addr].Owner.count() == 0) || (directory[addr].Owner.count() == 1));
|
||
|
|
||
|
// Make sure the token count is in range
|
||
|
assert(directory[addr].Tokens >= 0);
|
||
|
assert(directory[addr].Tokens <= max_tokens());
|
||
|
|
||
|
if (state == State:O) {
|
||
|
assert(directory[addr].Tokens >= 1); // Must have at least one token
|
||
|
// assert(directory[addr].Tokens >= (max_tokens() / 2)); // Only mostly true; this might not always hold
|
||
|
}
|
||
|
}
|
||
|
|
||
|
// ** OUT_PORTS **
|
||
|
out_port(responseNetwork_out, ResponseMsg, responseFromDir);
|
||
|
out_port(requestNetwork_out, RequestMsg, requestFromDir);
|
||
|
|
||
|
// ** IN_PORTS **
|
||
|
|
||
|
in_port(persistentNetwork_in, PersistentMsg, persistentToDir) {
|
||
|
if (persistentNetwork_in.isReady()) {
|
||
|
peek(persistentNetwork_in, PersistentMsg) {
|
||
|
assert(in_msg.Destination.isElement(machineID));
|
||
|
|
||
|
if (distributedPersistentEnabled()) {
|
||
|
// Apply the lockdown or unlockdown message to the table
|
||
|
if (in_msg.Type == PersistentRequestType:GETX_PERSISTENT) {
|
||
|
persistentTable.persistentRequestLock(in_msg.Address, in_msg.Requestor, AccessType:Write);
|
||
|
} else if (in_msg.Type == PersistentRequestType:GETS_PERSISTENT) {
|
||
|
persistentTable.persistentRequestLock(in_msg.Address, in_msg.Requestor, AccessType:Read);
|
||
|
} else if (in_msg.Type == PersistentRequestType:DEACTIVATE_PERSISTENT) {
|
||
|
persistentTable.persistentRequestUnlock(in_msg.Address, in_msg.Requestor);
|
||
|
} else {
|
||
|
error("Invalid message");
|
||
|
}
|
||
|
|
||
|
// React to the message based on the current state of the table
|
||
|
if (persistentTable.isLocked(in_msg.Address)) {
|
||
|
trigger(Event:Lockdown, in_msg.Address); // locked
|
||
|
} else {
|
||
|
trigger(Event:Unlockdown, in_msg.Address); // unlocked
|
||
|
}
|
||
|
}
|
||
|
else {
|
||
|
if (in_msg.Type == PersistentRequestType:GETX_PERSISTENT) {
|
||
|
trigger(Event:Lockdown, in_msg.Address); // locked
|
||
|
} else if (in_msg.Type == PersistentRequestType:GETS_PERSISTENT) {
|
||
|
trigger(Event:Lockdown, in_msg.Address); // locked
|
||
|
} else if (in_msg.Type == PersistentRequestType:DEACTIVATE_PERSISTENT) {
|
||
|
trigger(Event:Unlockdown, in_msg.Address); // unlocked
|
||
|
} else {
|
||
|
error("Invalid message");
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
|
||
|
in_port(requestNetwork_in, RequestMsg, requestToDir) {
|
||
|
if (requestNetwork_in.isReady()) {
|
||
|
peek(requestNetwork_in, RequestMsg) {
|
||
|
assert(in_msg.Destination.isElement(machineID));
|
||
|
if (in_msg.Type == CoherenceRequestType:GETS) {
|
||
|
trigger(Event:GETS, in_msg.Address);
|
||
|
} else if (in_msg.Type == CoherenceRequestType:GETX) {
|
||
|
trigger(Event:GETX, in_msg.Address);
|
||
|
} else {
|
||
|
error("Invalid message");
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
|
||
|
in_port(responseNetwork_in, ResponseMsg, responseToDir) {
|
||
|
if (responseNetwork_in.isReady()) {
|
||
|
peek(responseNetwork_in, ResponseMsg) {
|
||
|
assert(in_msg.Destination.isElement(machineID));
|
||
|
if (in_msg.Type == CoherenceResponseType:DATA_OWNER) {
|
||
|
trigger(Event:Data_Owner, in_msg.Address);
|
||
|
} else if ((in_msg.Type == CoherenceResponseType:ACK) ||
|
||
|
(in_msg.Type == CoherenceResponseType:DATA_SHARED)) {
|
||
|
trigger(Event:Tokens, in_msg.Address);
|
||
|
} else if (in_msg.Type == CoherenceResponseType:ACK_OWNER) {
|
||
|
trigger(Event:Ack_Owner, in_msg.Address);
|
||
|
} else {
|
||
|
DEBUG_EXPR(in_msg.Type);
|
||
|
error("Invalid message");
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
|
||
|
// Actions
|
||
|
|
||
|
action(a_sendTokens, "a", desc="Send tokens to requestor") {
|
||
|
// Only send a message if we have tokens to send
|
||
|
if (directory[address].Tokens > 0) {
|
||
|
peek(requestNetwork_in, RequestMsg) {
|
||
|
// enqueue(responseNetwork_out, ResponseMsg, latency="DIRECTORY_CACHE_LATENCY") {// FIXME?
|
||
|
enqueue(responseNetwork_out, ResponseMsg, latency="DIRECTORY_LATENCY") {// FIXME?
|
||
|
out_msg.Address := address;
|
||
|
out_msg.Type := CoherenceResponseType:ACK;
|
||
|
out_msg.Sender := machineID;
|
||
|
out_msg.SenderMachine := MachineType:Directory;
|
||
|
out_msg.Destination.add(in_msg.Requestor);
|
||
|
out_msg.Tokens := directory[in_msg.Address].Tokens;
|
||
|
out_msg.MessageSize := MessageSizeType:Response_Control;
|
||
|
}
|
||
|
}
|
||
|
directory[address].Tokens := 0;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
action(aa_sendTokensToStarver, "\a", desc="Send tokens to starver") {
|
||
|
// Only send a message if we have tokens to send
|
||
|
if (directory[address].Tokens > 0) {
|
||
|
// enqueue(responseNetwork_out, ResponseMsg, latency="DIRECTORY_CACHE_LATENCY") {// FIXME?
|
||
|
enqueue(responseNetwork_out, ResponseMsg, latency="DIRECTORY_LATENCY") {// FIXME?
|
||
|
out_msg.Address := address;
|
||
|
out_msg.Type := CoherenceResponseType:ACK;
|
||
|
out_msg.Sender := machineID;
|
||
|
out_msg.SenderMachine := MachineType:Directory;
|
||
|
out_msg.Destination.add(persistentTable.findSmallest(address));
|
||
|
out_msg.Tokens := directory[address].Tokens;
|
||
|
out_msg.MessageSize := MessageSizeType:Response_Control;
|
||
|
}
|
||
|
directory[address].Tokens := 0;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
action(d_sendDataWithAllTokens, "d", desc="Send data and tokens to requestor") {
|
||
|
peek(requestNetwork_in, RequestMsg) {
|
||
|
enqueue(responseNetwork_out, ResponseMsg, latency="MEMORY_LATENCY") {
|
||
|
out_msg.Address := address;
|
||
|
out_msg.Type := CoherenceResponseType:DATA_OWNER;
|
||
|
out_msg.Sender := machineID;
|
||
|
out_msg.SenderMachine := MachineType:Directory;
|
||
|
out_msg.Destination.add(in_msg.Requestor);
|
||
|
assert(directory[address].Tokens > 0);
|
||
|
out_msg.Tokens := directory[in_msg.Address].Tokens;
|
||
|
out_msg.DataBlk := directory[in_msg.Address].DataBlk;
|
||
|
out_msg.Dirty := false;
|
||
|
out_msg.MessageSize := MessageSizeType:Response_Data;
|
||
|
}
|
||
|
}
|
||
|
directory[address].Tokens := 0;
|
||
|
}
|
||
|
|
||
|
action(dd_sendDataWithAllTokensToStarver, "\d", desc="Send data and tokens to starver") {
|
||
|
enqueue(responseNetwork_out, ResponseMsg, latency="MEMORY_LATENCY") {
|
||
|
out_msg.Address := address;
|
||
|
out_msg.Type := CoherenceResponseType:DATA_OWNER;
|
||
|
out_msg.Sender := machineID;
|
||
|
out_msg.SenderMachine := MachineType:Directory;
|
||
|
out_msg.Destination.add(persistentTable.findSmallest(address));
|
||
|
assert(directory[address].Tokens > 0);
|
||
|
out_msg.Tokens := directory[address].Tokens;
|
||
|
out_msg.DataBlk := directory[address].DataBlk;
|
||
|
out_msg.Dirty := false;
|
||
|
out_msg.MessageSize := MessageSizeType:Response_Data;
|
||
|
}
|
||
|
directory[address].Tokens := 0;
|
||
|
}
|
||
|
|
||
|
action(f_incrementTokens, "f", desc="Increment the number of tokens we're tracking") {
|
||
|
peek(responseNetwork_in, ResponseMsg) {
|
||
|
assert(in_msg.Tokens >= 1);
|
||
|
directory[address].Tokens := directory[address].Tokens + in_msg.Tokens;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
action(j_popIncomingRequestQueue, "j", desc="Pop incoming request queue") {
|
||
|
requestNetwork_in.dequeue();
|
||
|
}
|
||
|
|
||
|
action(k_popIncomingResponseQueue, "k", desc="Pop incoming response queue") {
|
||
|
responseNetwork_in.dequeue();
|
||
|
}
|
||
|
|
||
|
action(l_popIncomingPersistentQueue, "l", desc="Pop incoming persistent queue") {
|
||
|
persistentNetwork_in.dequeue();
|
||
|
}
|
||
|
|
||
|
action(m_writeDataToMemory, "m", desc="Write dirty writeback to memory") {
|
||
|
peek(responseNetwork_in, ResponseMsg) {
|
||
|
directory[in_msg.Address].DataBlk := in_msg.DataBlk;
|
||
|
DEBUG_EXPR(in_msg.Address);
|
||
|
DEBUG_EXPR(in_msg.DataBlk);
|
||
|
}
|
||
|
}
|
||
|
|
||
|
action(n_checkIncomingMsg, "n", desc="Check incoming token message") {
|
||
|
peek(responseNetwork_in, ResponseMsg) {
|
||
|
assert(in_msg.Type == CoherenceResponseType:ACK_OWNER);
|
||
|
assert(in_msg.Dirty == false);
|
||
|
assert(in_msg.MessageSize == MessageSizeType:Writeback_Control);
|
||
|
assert(directory[in_msg.Address].DataBlk == in_msg.DataBlk);
|
||
|
}
|
||
|
}
|
||
|
|
||
|
action(r_bounceResponse, "r", desc="Bounce response to starving processor") {
|
||
|
peek(responseNetwork_in, ResponseMsg) {
|
||
|
enqueue(responseNetwork_out, ResponseMsg, latency="NULL_LATENCY") {
|
||
|
out_msg.Address := address;
|
||
|
out_msg.Type := in_msg.Type;
|
||
|
out_msg.Sender := machineID;
|
||
|
out_msg.SenderMachine := MachineType:Directory;
|
||
|
out_msg.Destination.add(persistentTable.findSmallest(address));
|
||
|
out_msg.Tokens := in_msg.Tokens;
|
||
|
out_msg.MessageSize := in_msg.MessageSize;
|
||
|
out_msg.DataBlk := in_msg.DataBlk;
|
||
|
out_msg.Dirty := in_msg.Dirty;
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
|
||
|
action(s_bounceDatalessOwnerToken, "s", desc="Bounce clean owner token to starving processor") {
|
||
|
peek(responseNetwork_in, ResponseMsg) {
|
||
|
assert(in_msg.Type == CoherenceResponseType:ACK_OWNER);
|
||
|
assert(in_msg.Dirty == false);
|
||
|
assert(in_msg.MessageSize == MessageSizeType:Writeback_Control);
|
||
|
|
||
|
// NOTE: The following check would not be valid in a real
|
||
|
// implementation. We include the data in the "dataless"
|
||
|
// message so we can assert the clean data matches the datablock
|
||
|
// in memory
|
||
|
assert(directory[in_msg.Address].DataBlk == in_msg.DataBlk);
|
||
|
|
||
|
// Bounce the message, but "re-associate" the data and the owner
|
||
|
// token. In essence we're converting an ACK_OWNER message to a
|
||
|
// DATA_OWNER message, keeping the number of tokens the same.
|
||
|
enqueue(responseNetwork_out, ResponseMsg, latency="NULL_LATENCY") {
|
||
|
out_msg.Address := address;
|
||
|
out_msg.Type := CoherenceResponseType:DATA_OWNER;
|
||
|
out_msg.Sender := machineID;
|
||
|
out_msg.SenderMachine := MachineType:Directory;
|
||
|
out_msg.DestMachine := MachineType:L1Cache;
|
||
|
out_msg.Destination.add(persistentTable.findSmallest(address));
|
||
|
out_msg.Tokens := in_msg.Tokens;
|
||
|
out_msg.DataBlk := directory[in_msg.Address].DataBlk;
|
||
|
out_msg.Dirty := in_msg.Dirty;
|
||
|
out_msg.MessageSize := MessageSizeType:Response_Data;
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
|
||
|
|
||
|
// TRANSITIONS
|
||
|
|
||
|
// Trans. from O
|
||
|
transition(O, GETX, NO) {
|
||
|
d_sendDataWithAllTokens;
|
||
|
j_popIncomingRequestQueue;
|
||
|
}
|
||
|
|
||
|
transition(O, GETS, NO) {
|
||
|
d_sendDataWithAllTokens;
|
||
|
j_popIncomingRequestQueue;
|
||
|
}
|
||
|
|
||
|
transition(O, Lockdown, L) {
|
||
|
dd_sendDataWithAllTokensToStarver;
|
||
|
l_popIncomingPersistentQueue;
|
||
|
}
|
||
|
|
||
|
transition(O, Tokens) {
|
||
|
f_incrementTokens;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
// Trans. from NO
|
||
|
transition(NO, GETX) {
|
||
|
a_sendTokens;
|
||
|
j_popIncomingRequestQueue;
|
||
|
}
|
||
|
|
||
|
transition(NO, GETS) {
|
||
|
j_popIncomingRequestQueue;
|
||
|
}
|
||
|
|
||
|
transition(NO, Lockdown, L) {
|
||
|
aa_sendTokensToStarver;
|
||
|
l_popIncomingPersistentQueue;
|
||
|
}
|
||
|
|
||
|
transition(NO, Data_Owner, O) {
|
||
|
m_writeDataToMemory;
|
||
|
f_incrementTokens;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
transition(NO, Ack_Owner, O) {
|
||
|
n_checkIncomingMsg;
|
||
|
f_incrementTokens;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
transition(NO, Tokens) {
|
||
|
f_incrementTokens;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
// Trans. from L
|
||
|
transition(L, {GETX, GETS}) {
|
||
|
j_popIncomingRequestQueue;
|
||
|
}
|
||
|
|
||
|
transition(L, Lockdown) {
|
||
|
l_popIncomingPersistentQueue;
|
||
|
}
|
||
|
|
||
|
// we could change this to write the data to memory and send it cleanly
|
||
|
transition(L, Data_Owner) {
|
||
|
r_bounceResponse;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
transition(L, Tokens) {
|
||
|
r_bounceResponse;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
transition(L, Ack_Owner) {
|
||
|
s_bounceDatalessOwnerToken;
|
||
|
k_popIncomingResponseQueue;
|
||
|
}
|
||
|
|
||
|
|
||
|
transition(L, Unlockdown, NO) {
|
||
|
l_popIncomingPersistentQueue;
|
||
|
}
|
||
|
|
||
|
}
|