/*
 * 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: MOSI_directory-dir.sm 1.14 04/09/07 13:52:52-05:00 mikem@maya.cs.wisc.edu $
 */

machine(Directory, "MOSI Directory Optimized") {


  MessageBuffer forwardedRequestFromDir, network="To", virtual_network="1", ordered="true";
  MessageBuffer responseFromDir, network="To", virtual_network="2", ordered="false";
  MessageBuffer requestToDir, network="From", virtual_network="0", ordered="false";

  // STATES
  enumeration(State, desc="Directory states", default="Directory_State_I") {
    // Base states
    I, desc="Idle";
    S, desc="Shared";
    O, desc="Owned";
    M, desc="Modified", format="!b";
  }

  // Events
  enumeration(Event, desc="Directory events") {
    GETS, desc="A GETS arrives";
    GETX_Owner, desc="A GETX arrives, requestor is owner";
    GETX_NotOwner, desc="A GETX arrives, requestor is not owner";
    PUTX_Owner, "PUTX (requestor is owner)", desc="A PUTX arrives, requestor is owner";
    PUTX_NotOwner, "PUTX (requestor not owner)",desc="A PUTX arrives, requestor is not owner";
  }

  // TYPES

  // DirectoryEntry
  structure(Entry, desc="...") {
    State DirectoryState,          desc="Directory state";
    NetDest Sharers,                   desc="Set of sharers";
    bool DirOwner, default="true", desc="Is dir owner?";
    MachineID ProcOwner,  desc="Processor owner";
    DataBlock DataBlk,             desc="data for the block";
  }

  external_type(DirectoryMemory) {
    Entry lookup(Address);
    bool isPresent(Address);
  }

  // ** OBJECTS **

  DirectoryMemory directory, constructor_hack="i";

  State getState(Address addr) {
    if (directory.isPresent(addr)) {
      return directory[addr].DirectoryState;
    }
    return State:I;
  }

  void setState(Address addr, State state) {
    if (directory.isPresent(addr)) {
      directory[addr].DirectoryState := state;
    }
  }

  // ** OUT_PORTS **
  out_port(forwardedRequestNetwork_out, RequestMsg, forwardedRequestFromDir);
  out_port(responseNetwork_out, ResponseMsg, responseFromDir);

  // ** IN_PORTS **

  in_port(requestNetwork_in, RequestMsg, requestToDir) {
    if (requestNetwork_in.isReady()) {
      peek(requestNetwork_in, RequestMsg) {
        if (in_msg.Type == CoherenceRequestType:GETS) {
          trigger(Event:GETS, in_msg.Address);
        } else if (in_msg.Type == CoherenceRequestType:GETX) {
          if(directory[in_msg.Address].DirOwner == false && in_msg.Requestor == directory[in_msg.Address].ProcOwner) {
            trigger(Event:GETX_Owner, in_msg.Address);
          } else {
            trigger(Event:GETX_NotOwner, in_msg.Address);
          }
        } else if (in_msg.Type == CoherenceRequestType:PUTX) {
          if (directory[in_msg.Address].DirOwner == false && in_msg.Requestor == directory[in_msg.Address].ProcOwner) {
            trigger(Event:PUTX_Owner, in_msg.Address);
          } else {
            trigger(Event:PUTX_NotOwner, in_msg.Address);
          }
        } else {
          error("Invalid message");
        }
      }
    }
  }


  // Actions

  // a_addRequestorToSharers

  action(a_addRequestorToSharers, "a", desc="Add requestor to list of sharers") {
    peek(requestNetwork_in, RequestMsg) {
      directory[address].Sharers.add(in_msg.Requestor);
      DEBUG_EXPR(directory[address].Sharers);
    }
  }

  // b_dataToRequestor

  action(b_dataToRequestor, "b", desc="Send data to requestor") {
    peek(requestNetwork_in, RequestMsg) {
      enqueue(responseNetwork_out, ResponseMsg, latency="MEMORY_LATENCY") {
        out_msg.Address := address;
        out_msg.Type := CoherenceResponseType:DATA;
        out_msg.Sender := machineID;
        out_msg.SenderMachine := MachineType:Directory;
        if(in_msg.Type == CoherenceRequestType:GETX) {
          out_msg.NumPendingAcks := directory[address].Sharers.count();
        } else {
          out_msg.NumPendingAcks := 0; // don't need to send pending ack count to GETS requestor
        }
        out_msg.Destination.add(in_msg.Requestor);
        out_msg.DestMachine := MachineType:L1Cache;
        out_msg.DataBlk := directory[address].DataBlk;
        DEBUG_EXPR(out_msg.NumPendingAcks);
        DEBUG_EXPR(out_msg.Destination);
        out_msg.MessageSize := MessageSizeType:Data;
      }
    }
  }

  // d_forwardRequestToOwner

  action(d_forwardRequestToOwner, "d", desc="Forward request to owner") {
    peek(requestNetwork_in, RequestMsg) {
      enqueue(forwardedRequestNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
        out_msg.Address := address;
        out_msg.Type := in_msg.Type;
        out_msg.Requestor := in_msg.Requestor;
        out_msg.Destination.add(directory[address].ProcOwner);
        DEBUG_EXPR(out_msg.Destination);

        if(in_msg.Type == CoherenceRequestType:GETX) {
          out_msg.NumPendingAcks := directory[address].Sharers.count();
        } else {
          out_msg.NumPendingAcks := 0; // don't need to send pending ack count to GETS requestor
        }
        out_msg.MessageSize := MessageSizeType:Control;
      }
    }
  }

  action(f_setOwnerToRequestor, "f", desc="Set owner equal to requestor") {
    peek(requestNetwork_in, RequestMsg) {
      directory[address].ProcOwner := in_msg.Requestor;
      directory[address].DirOwner := false;
    }
    DEBUG_EXPR(directory[address].ProcOwner);
  }

  action(g_clearSharers, "g", desc="Clear list of sharers") {
    directory[address].Sharers.clear();
  }

  // currently done via multicast message

  action(h_invToSharers, "h", desc="Send INVs to all sharers") {
    peek(requestNetwork_in, RequestMsg) {
      if(directory[address].Sharers.count() != 0){
        enqueue(forwardedRequestNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
          out_msg.Address := address;
          out_msg.Type := CoherenceRequestType:INV;
          out_msg.Requestor := in_msg.Requestor;
          out_msg.Destination := directory[address].Sharers;
          out_msg.MessageSize := MessageSizeType:Control;
        }
      }
    }
    DEBUG_EXPR(directory[address].Sharers);
  }

  action(j_popIncomingRequestQueue, "j", desc="Pop incoming request queue") {
    requestNetwork_in.dequeue();
  }

  action(l_writeRequestDataToMemory, "l", desc="Write PUTX/DWN data to memory") {
    peek(requestNetwork_in, RequestMsg) {
      directory[in_msg.Address].DataBlk := in_msg.DataBlk;
      DEBUG_EXPR(in_msg.Address);
      DEBUG_EXPR(in_msg.DataBlk);
    }
  }

  action(n_writebackAckToRequestor, "n", desc="Send WB_ack to requestor") {
    peek(requestNetwork_in, RequestMsg) {
      // This needs to be DIRECTORY_LATENCY to keep the queue fifo
      enqueue(forwardedRequestNetwork_out, RequestMsg, latency="DIRECTORY_LATENCY") {
        out_msg.Address := address;
        out_msg.Type := CoherenceRequestType:WB_ACK;
        out_msg.Requestor := machineID;
        out_msg.Destination.add(in_msg.Requestor);
        out_msg.MessageSize := MessageSizeType:Control;
      }
    }
  }

  action(p_clearOwner, "p", desc="Clear owner") {
    directory[address].DirOwner := true;  // set owner equal to dir
  }

  action(r_addOwnerToSharers, "r", desc="Add owner to list of sharers") {
    directory[address].Sharers.add(directory[address].ProcOwner);
  }

  action(t_removeOwnerFromSharers, "t", desc="Remove owner from list of sharers") {
    directory[address].Sharers.remove(directory[address].ProcOwner);
  }

  action(u_removeRequestorFromSharers, "u", desc="Remove requestor from list of sharers") {
    peek(requestNetwork_in, RequestMsg) {
      directory[address].Sharers.remove(in_msg.Requestor);
    }
  }

  // TRANSITIONS

  transition({I, S, M, O}, PUTX_NotOwner) {
    n_writebackAckToRequestor;
    j_popIncomingRequestQueue;
  }

  // Transitions from Idle
  transition(I, GETS, S) {
    a_addRequestorToSharers;
    b_dataToRequestor;
    j_popIncomingRequestQueue;
  }

  transition(I, GETX_NotOwner, M) {
    f_setOwnerToRequestor;
    b_dataToRequestor;
    j_popIncomingRequestQueue;
  }

  // Transitions from Shared
  transition(S, GETS) {
    a_addRequestorToSharers;
    b_dataToRequestor;
    j_popIncomingRequestQueue;
  }

  transition(S, GETX_NotOwner, M) {
    u_removeRequestorFromSharers;
    b_dataToRequestor;
    f_setOwnerToRequestor;
    h_invToSharers;
    g_clearSharers;
    j_popIncomingRequestQueue;
  }

  // Transitions from Owned
  transition(O, GETS) {
    a_addRequestorToSharers;
    d_forwardRequestToOwner;
    j_popIncomingRequestQueue;
  }

  transition(O, {GETX_NotOwner, GETX_Owner}, M) {
    u_removeRequestorFromSharers;
    t_removeOwnerFromSharers;
    d_forwardRequestToOwner;
    f_setOwnerToRequestor;
    h_invToSharers;
    g_clearSharers;
    j_popIncomingRequestQueue;
  }

  transition(O, PUTX_Owner, S) {
    u_removeRequestorFromSharers;
    l_writeRequestDataToMemory;
    n_writebackAckToRequestor;
    p_clearOwner;
    j_popIncomingRequestQueue;
  }


  // Transitions from Modified
  transition(M, GETS, O) {
    a_addRequestorToSharers;
    r_addOwnerToSharers;
    d_forwardRequestToOwner;
    j_popIncomingRequestQueue;
  }

  transition(M, GETX_NotOwner) {
    d_forwardRequestToOwner;
    f_setOwnerToRequestor;
    j_popIncomingRequestQueue;
  }

  transition(M, PUTX_Owner, I) {
    l_writeRequestDataToMemory;
    n_writebackAckToRequestor;
    p_clearOwner;
    j_popIncomingRequestQueue;
  }
}