-- 3-hop, nack-free, invalidation protocol with local node optimizations
-- Murphi code, Brian Gold, 2004


----------------------------------------------------------------------
-- Constants
----------------------------------------------------------------------
Const   
  RemoteCount: 4;
  HomeCount: 1;
  NodeCount: RemoteCount + HomeCount;
  AddrCount: 1;
  AddrPerProc: AddrCount/HomeCount;

  VC0: 0;                -- low priority
  VC1: 1;
  VC2: 2;                -- high priority
  NumVCs: VC2 - VC0 + 1;

  TSRFMax: 2;

  NetMax: 2*RemoteCount*AddrCount;
  MailboxSize: 1;


----------------------------------------------------------------------
-- Types
----------------------------------------------------------------------
Type
  RemoteRange: scalarset(RemoteCount);
  HomeRange: scalarset(HomeCount);
  NodeRange: union { RemoteRange, HomeRange };
  NodeIdxType: 0..NodeCount-1;
  AddrType: 0..AddrCount-1;
  MailboxRange: scalarset(MailboxSize);

  VCType: VC0..VC2;

  MessageType: enum {
    ReadReq,                 -- VC0
    WriteReq,                -- VC0
    UpgradeReq,              -- VC0
    FlushReq,                -- VC1
    WritebackReq,            -- VC1

    -- Requests From Directory to Cache
    LocalInvalidationReq,    -- VC1  
    RemoteInvalidationReq,   -- VC1  
    ForwardedReadReq,        -- VC1   
    ForwardedWriteReq,       -- VC1    
    RecallReadReq,           -- VC1     
    RecallWriteReq,          -- VC1    

    -- Replies From Cache to Directory
    ForwardedWriteAck,       -- VC2
    ForwardedReadAck,        -- VC2
    RecallReadAck,           -- VC2
    RecallWriteAck,          -- VC2
    LocalInvalidationAck,    -- VC2

    -- Replies From Directory to Cache
    ReadAck,                 -- VC2
    WriteAck,                -- VC2
    UpgradeAck,              -- VC2
    WritebackAck,            -- VC2
    WritebackStaleRdAck,     -- VC2
    WritebackStaleWrAck,     -- VC2
    FlushAck,              

    -- Replies From Cache to Cache
    RemoteInvalidationAck,   -- VC2
    ReadFwd,                 -- VC2
    WriteFwd,                -- VC2

    -- Requests from Local caches to Directory (HE)
    -- LocalRead,            -- not modeled
    -- LocalWriteAccess,     -- not modeled
    LocalUpgradeAccess       -- VC0
    -- LocalFlush,           -- not modeled
    -- LocalDropHint,        -- not modeled
    -- LocalEvict,           -- not modeled
    -- LocalPrefetchRead     -- not modeled
  };  -- end MessageType

  Message:
    Record
      mtype: MessageType;
      address: AddrType;
      src: NodeRange;
      -- don't need a destination for verification
      vc: VCType;
      aux: NodeRange;  -- participating node (used when forwarding msgs)
      cnt: NodeIdxType;
  End;

  CacheEntry: 
    Record
      clean: Boolean;
      state: enum {I, S, M,
		   dirTIS, dirTMS, dirTML, dirTMI, dirTMM,
		   remTIS,  remTIL,  remTWIF, remTWIS, remTMI, 
		   remTRIF, remTRIS, remIM,   remIIM,  remTSM, 
		   remTAM,  remTISM, remTIAM, remTRIM, remTLIM, remTII};
  End;

  TSRFState: enum {Runnable, Waiting, Blocked, Completed};

  TSRFEntry:
    Record
      state: TSRFState;
      acnt: NodeIdxType;
      msg: Message;
  End;
      
  NodeType:
    Record
      -- local cache/directory
      cache: array [AddrType] of CacheEntry;

      -- tsrfs
      tsrfs: multiset [TSRFMax] of TSRFEntry;

      -- receive ports
      ports: array [VCType] of Message;
    End;

  AddressMapType:
    Record
      home: NodeRange;
      sharers: array [NodeRange] of Boolean;  -- also keeps owner
    End;


----------------------------------------------------------------------
-- Variables
----------------------------------------------------------------------
Var
  Nodes: array [NodeRange] of NodeType;
  Net:   array [NodeRange] of multiset [NetMax] of Message;
  AddrMap: array [AddrType] of AddressMapType;
  uniqueAddressCounter: AddrType;
  
----------------------------------------------------------------------
-- Functions
----------------------------------------------------------------------
Function IsLocal(addr:AddrType; n:NodeRange) : Boolean;
Begin

  if AddrMap[addr].home = n
  then
    return true;
  else
    return false;
  endif;

End;  -- Function IsLocal

Function HomeFromAddress(addr:AddrType) : NodeRange;
Begin
  return AddrMap[addr].home;
End;  -- Function HomeFromAddress

Function OwnerFromAddress(addr:AddrType) : NodeRange;
Begin
  for n:NodeRange do
    if AddrMap[addr].sharers[n]
    then
      return n;
    endif;
  endfor;

  error "Couldn't find owner";
End;  -- Function HomeFromAddress

Function SharersListSize(addr:AddrType) : NodeIdxType;
  var cnt:NodeIdxType;
Begin
  cnt := 0;
  for n:NodeRange do
    if AddrMap[addr].sharers[n]
    then
      cnt := cnt + 1;
    endif;
  endfor;

  return cnt;
End;

Function CountTSRFs(n:NodeRange; addr:AddrType; state:TSRFState): 0..TSRFMax-1;
Begin
  return MultiSetCount(t:Nodes[n].tsrfs, 
	               Nodes[n].tsrfs[t].state       = state &
		       Nodes[n].tsrfs[t].msg.address = addr);
End;
		       

Function SpaceForTSRF(mtype:MessageType; n:NodeRange) : Boolean;
Begin
  if (MultiSetCount(t:Nodes[n].tsrfs, true) < TSRFMax)
  then
    -- FIXME: base decision on message type and need to reserve extra tsrfs
    return true;
  endif;

  return false;
End;

Function CreateTSRF(state: TSRFState; msg: Message) : TSRFEntry;
  var tsrf:TSRFEntry;
Begin
  tsrf.state  := state;  
  tsrf.msg    := msg;

  if IsUndefined(msg.cnt)
  then
    undefine tsrf.acnt;
  else
    tsrf.acnt := msg.cnt;
  endif;  

  return tsrf;
End;


----------------------------------------------------------------------
-- Procedures
----------------------------------------------------------------------
Procedure InitializeNode(n:NodeRange);
Begin

  for a:AddrType do
    Nodes[n].cache[a].clean := true;
    Nodes[n].cache[a].state := I;   
    AddrMap[a].sharers[n] := false; 
  endfor;

  if IsMember(n, HomeRange)
  then
    for a:0..AddrPerProc-1 do
      AddrMap[uniqueAddressCounter].home := n;

      -- only increment counter when it's not at limit
      if (uniqueAddressCounter < AddrCount-1)
      then
        uniqueAddressCounter := uniqueAddressCounter + 1;
      endif;
    endfor;
  endif;

End;

Procedure Send(dst:NodeRange; msg:Message);
Begin
  Assert (MultiSetCount(i:Net[dst], true) < NetMax) "Too many messages";  
  MultiSetAdd(msg, Net[dst]);
End;

Function CreateMsg(mtype:MessageType; 
 	           address:AddrType; 
		   src:NodeRange;
		   vc:VCType;
		   aux:NodeRange;
                   cnt:0..NodeCount-1) : Message;
  var msg:Message;
Begin
  msg.mtype   := mtype;
  msg.address := address;
  msg.src     := src;
  msg.vc      := vc;
  msg.aux     := aux;
  msg.cnt     := cnt;
  return msg;
End;

Procedure InvalidateAndClearSharers(addr:AddrType; 
		                    src:NodeRange; 
				    aux:NodeRange;
				    except:NodeRange);
  var msg:Message;
Begin
  for i:NodeRange do
    if AddrMap[addr].sharers[i] & i != except
    then
      msg := CreateMsg(IsMember(aux, RemoteRange) ? 
                         RemoteInvalidationReq : LocalInvalidationReq, 
		       addr, src, VC1, aux, UNDEFINED);
      Send(i,msg);
      AddrMap[addr].sharers[i] := false;
    endif;
  endfor;
End;

Procedure InitiateXact(mtype:MessageType; 
	               addr:AddrType;  
	               src:NodeRange; 
		       dest:NodeRange; 
		       vc:VCType);
  var tsrf:TSRFEntry;
Begin
  Assert(SpaceForTSRF(mtype, src)) "Not enough space for TSRF";

  -- create new TSRF for this xaction
  tsrf.state := Waiting;
  tsrf.acnt  := 0;
  tsrf.msg   := CreateMsg(mtype, addr, src, vc, UNDEFINED, UNDEFINED);
  MultiSetAdd(tsrf, Nodes[src].tsrfs);

  -- send message 
  Send(dest, tsrf.msg);
End;


----------------------------------------------------------------------
-- ProcessLocal
----------------------------------------------------------------------
Function ProcessLocal(n:NodeRange; var tsrf: TSRFEntry) : Boolean;
  var processed:Boolean;
  var newmsg:Message;
Begin

Alias 
  node:Nodes[n];
  msg:tsrf.msg;
  address:msg.address;
  cache:node.cache[address];
  state:cache.state;
Do
  
  processed := true;  -- set to false only when CANNOT process msg

  switch state

  case I:
    switch msg.mtype
    case ReadReq:
      -- force downgrade in local hierarchy
      cache.clean := true;
      -- send read ack
      newmsg := CreateMsg(ReadAck, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      -- update sharers' list
      AddrMap[address].sharers[msg.src] := true;      
      -- mark TSRF completed
      tsrf.state := Completed;
      -- change state to S  
      state := S;
    case WriteReq,
         UpgradeReq:
      -- force downgrade in local hierarchy
      cache.clean := true;
      -- send write ack
      newmsg := CreateMsg(WriteAck, address, n, VC2, UNDEFINED, 0);
      Send(msg.src, newmsg);
      -- set new owner
      AddrMap[address].sharers[msg.src] := true;
      -- mark TSRF completed
      tsrf.state := Completed;
      -- change state to M  
      state := M;
    else
      error "Unhandled message type in home engine";
    endswitch;

  case S:
    switch msg.mtype
    case ReadReq:
      -- send read ack
      newmsg := CreateMsg(ReadAck, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      -- update sharer's list
      AddrMap[address].sharers[msg.src] := true;
      -- mark TSRF completed
      tsrf.state := Completed;
    case WriteReq:
      -- force invalidation in local hierarchy
      cache.clean := true;
      -- send WriteAck
      if AddrMap[address].sharers[msg.src]
      then
        newmsg := CreateMsg(WriteAck, address, n, VC2, 
                            UNDEFINED, SharersListSize(address)-1);
      else
        newmsg := CreateMsg(WriteAck, address, n, VC2, 
                            UNDEFINED, SharersListSize(address));
      endif;
      Send(msg.src, newmsg);
      -- invalidate and clear sharers' list
      InvalidateAndClearSharers(address, n, msg.src, msg.src);
      -- change state
      state := M;
      -- new owner
      AddrMap[address].sharers[msg.src] := true;
      -- mark TSRF completed
      tsrf.state := Completed;
    case UpgradeReq:
      -- force invalidation in local hierarchy
      cache.clean := true;
      -- is request from sharer
      if AddrMap[address].sharers[msg.src] 
      then    -- yes
        newmsg := CreateMsg(UpgradeAck, address, n, VC2, UNDEFINED,
			    SharersListSize(address)-1);
      else
        newmsg := CreateMsg(WriteAck, address, n, VC2, UNDEFINED,
			    SharersListSize(address));
      endif;
      Send(msg.src, newmsg);
      -- invalidate and clear sharers' list, but not msg.src
      InvalidateAndClearSharers(address, n, msg.src, msg.src);
      -- ensure msg.src is owner (in case of UpgradeReq not from sharer)
      AddrMap[address].sharers[msg.src] := true;
      -- change state
      state := M;
      tsrf.state := Completed;
    else
      error "Unhandled message type in home engine";
    endswitch;

  case M:
    switch msg.mtype
    case ReadReq:
      -- send forwarded read req
      newmsg := CreateMsg(ForwardedReadReq, address, n, 
                          VC1, msg.src, UNDEFINED);
      Send(OwnerFromAddress(address), newmsg);
      -- add new sharer
      AddrMap[address].sharers[msg.src] := true;
      tsrf.state := Waiting;
      state := dirTMS;
    case WriteReq,
         UpgradeReq:
      -- send forwarded write req
      newmsg := CreateMsg(ForwardedWriteReq, address, n, 
 	                  VC1, msg.src, UNDEFINED);
      Send(OwnerFromAddress(address), newmsg);
      -- new owner
      AddrMap[address].sharers[OwnerFromAddress(address)] := false;
      AddrMap[address].sharers[msg.src] := true; 
      tsrf.state := Waiting;
      state := dirTMM;
    case WritebackReq:      
      newmsg := CreateMsg(WritebackAck, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      -- wo/ SpuriousSharerOpt
      AddrMap[address].sharers[msg.src] := false;
      tsrf.state := Completed;
      state := I;      
    else
      error "Unhandled message type in home engine";
    endswitch;

  case dirTMS:
    switch msg.mtype
    case ForwardedReadAck:
      state := S;
      tsrf.state := Completed;
    case WritebackReq:
      newmsg := CreateMsg(WritebackStaleRdAck, address, n, VC2, 
	                  UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      AddrMap[address].sharers[msg.src] := false;
      tsrf.state := Completed;
      state := S;
    else
      error "Unhandled message type in home engine";
    endswitch;

  case dirTML:
    switch msg.mtype
    case RecallReadAck:
      -- close tsrf
      tsrf.state := Completed;
      -- move to S
      state := S;      
    case WritebackReq:
      -- race of writeback req and our recall read req
      -- don't ack the wb -- the remote engine will have received
      -- the recall req and isn't expecting a wback
      AddrMap[address].sharers[msg.src] := false;
      tsrf.state := Completed;
      state := I;
    else
      error "Unhandled message type in home engine";
    endswitch;

  case dirTMI:
    switch msg.mtype
    case RecallWriteAck,
         WritebackReq,
         FlushReq:
      state := I;
      tsrf.state := Completed;
      -- get rid of old owner
      AddrMap[address].sharers[msg.src] := false;
    else
      error "Unhandled message type in home engine";
    endswitch;

  case dirTMM:
    switch msg.mtype
    case ForwardedWriteAck:
      state := M;
      tsrf.state := Completed;
    case WritebackReq:
      if AddrMap[address].sharers[msg.src]
      then
        -- writeback from new owner
	      processed := false; -- refuse
      else
        -- writeback from old owner
        newmsg := CreateMsg(WritebackStaleWrAck, address, n, VC2, 
	                    UNDEFINED, UNDEFINED);
        Send(msg.src, newmsg);
        AddrMap[address].sharers[msg.src] := false;
	      tsrf.state := Completed;
	      state := M;
      endif;		
    else
      error "Unhandled message type in home engine";
    endswitch;

  case dirTIS:
    switch msg.mtype
    case LocalInvalidationAck:
      assert (tsrf.acnt > 0) "received more inval acks than expected";
      tsrf.acnt := tsrf.acnt - 1;
      
      if tsrf.acnt = 0
      then
        state := I;
	tsrf.state := Completed;
      else
        tsrf.state := Waiting;
      endif;
    else
      error "Unhandled message type in home engine";
    endswitch;

  else 
    error "Unhandled cache state in home engine";

  endswitch;
  

  return processed;
EndAlias;

End; -- function ProcessLocal


----------------------------------------------------------------------
-- ProcessRemote
----------------------------------------------------------------------
Function ProcessRemote(n:NodeRange; var tsrf: TSRFEntry) : Boolean;
  var processed:Boolean;
  var newmsg:Message;
Begin

Alias 
  node:Nodes[n];
  msg:tsrf.msg;
  address:msg.address;
  cache:node.cache[address];
  state:cache.state;
Do
  
  processed := true;  -- set to false only when CANNOT process tsrf

  switch state

  case I:
    switch msg.mtype
    case RemoteInvalidationReq:
      state := I;
      newmsg := CreateMsg(RemoteInvalidationAck, address, n, VC2, 
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      -- mark TSRF complete
      tsrf.state := Completed;
    case LocalInvalidationReq:
      state := I;
      newmsg := CreateMsg(LocalInvalidationAck, address, n, VC2,
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case S:  -- receive invalidate
    switch msg.mtype
    case RemoteInvalidationReq:
      state := I;
      newmsg := CreateMsg(RemoteInvalidationAck, address, n, VC2, 
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      -- mark TSRF complete
      tsrf.state := Completed;
    case LocalInvalidationReq:
      state := I;
      newmsg := CreateMsg(LocalInvalidationAck, address, n, VC2,
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case M:  -- receive recall, invalidate, etc.
    switch msg.mtype
    case ForwardedReadReq:
      -- downgrade local hierarchy
      cache.clean := true;

      newmsg := CreateMsg(ReadFwd, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);

      newmsg := CreateMsg(ForwardedReadAck, address, n, VC2, 
			  UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      -- update state
      state := S;
      -- mark TSRF complete
      tsrf.state := Completed;
    case ForwardedWriteReq:
      -- invalidate local hierarchy
      cache.clean := true;

      newmsg := CreateMsg(WriteFwd, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);

      newmsg := CreateMsg(ForwardedWriteAck, address, n, VC2, 
			  UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      -- update state
      state := I;
      -- mark TSRF complete
      tsrf.state := Completed
    case RecallReadReq:
      -- downgrade local hierarchy
      cache.clean := true;
      newmsg := CreateMsg(RecallReadAck, address, n, VC2, 
		          UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      state := S;
      -- mark TSRF complete
      tsrf.state := Completed;
    case RecallWriteReq:
      -- invalidate local hierarchy
      cache.clean := true;
      newmsg := CreateMsg(RecallWriteAck, address, n, VC2, 
		          UNDEFINED, UNDEFINED);
      Send(msg.src, newmsg);
      state := I;
      -- mark TSRF complete
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTIS:  -- waiting for ReadAck/ReadFwd
    switch msg.mtype
    case ReadAck:
      state := S;
      tsrf.state := Completed;
    case ReadFwd:
      state := S;
      tsrf.state := Completed;
    case RemoteInvalidationReq:
      state := remTIL;
      newmsg := CreateMsg(RemoteInvalidationAck, address, n, VC2, 
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      -- mark TSRF complete
      tsrf.state := Waiting;
    case LocalInvalidationReq:
      state := remTIL;
      newmsg := CreateMsg(LocalInvalidationAck, address, n, VC2,
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      tsrf.state := Waiting;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTIL:
    switch msg.mtype
    case ReadAck,
         ReadFwd:
      state := I;
      tsrf.state := Completed;
    case LocalInvalidationReq,
         RemoteInvalidationReq:
      -- NOT IN NIKOS' diagrams.  
      -- SOLUTION: refuse
      processed := false;
    else
      error "Unhandled message type in remote engine";
    endswitch;  

  case remIM:  -- waiting for WriteAck
    switch msg.mtype
    case RemoteInvalidationAck:
      tsrf.acnt := tsrf.acnt + 1;  -- initially count up
      tsrf.state := Waiting;
    case WriteAck:
      assert (msg.cnt >= tsrf.acnt) "received more inval acks than expected";
      tsrf.acnt := msg.cnt - tsrf.acnt; -- prepare to count down
      
      if tsrf.acnt = 0
      then
	      state := M;
	      tsrf.state := Completed;       
      else
        state := remIIM;
        tsrf.state := Waiting;
      endif;
    case WriteFwd:
      state := M;
      tsrf.state := Completed;
    case RemoteInvalidationReq:
      newmsg := CreateMsg(RemoteInvalidationAck, address, n, VC2, 
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      -- mark TSRF complete
      tsrf.state := Waiting;
    case LocalInvalidationReq:
      newmsg := CreateMsg(LocalInvalidationAck, address, n, VC2,
                          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      tsrf.state := Waiting;
    case ForwardedReadReq,
	       ForwardedWriteReq,
	       RecallReadReq,
         RecallWriteReq:
      processed := false; -- refuse
    else
      error "Unhandled message type in remote engine";
    endswitch;     

  case remIIM:
    switch msg.mtype
    case RemoteInvalidationAck:
      assert (tsrf.acnt > 0) "received more inval acks than expected";
      tsrf.acnt := tsrf.acnt - 1;
      
      if tsrf.acnt = 0
      then
        state := M;
	      tsrf.state := Completed;
      else
        tsrf.state := Waiting;
      endif;
    case ForwardedReadReq,
	       ForwardedWriteReq,
	       RecallReadReq,
         RecallWriteReq:
      processed := false; -- refuse
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTSM: -- waiting for UpgradeAck/(WriteAck)
    switch msg.mtype
    case UpgradeAck:
      -- if invcount is 0, proceed directly to M
      -- otherwise, wait for RemoteInvalAcks
      if msg.cnt = 0
      then
	      state := M;	
	      tsrf.state := Completed;
      else
        tsrf.acnt := msg.cnt;
	      state := remTAM;
	      tsrf.state := Waiting;	
      endif;
    case RemoteInvalidationReq:
      newmsg := CreateMsg(RemoteInvalidationAck, address, n, VC2, 
		          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      state := remTRIM;
      tsrf.state := Waiting;      
    case LocalInvalidationReq:
      newmsg := CreateMsg(LocalInvalidationAck, address, n, VC2, 
		          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      state := remTLIM;
      tsrf.state := Waiting;      
    case RemoteInvalidationAck:
      tsrf.acnt := tsrf.acnt + 1;  -- count up at first
      state := remTISM;
      tsrf.state := Waiting;
    case RecallReadReq,
         RecallWriteReq,
	       ForwardedReadReq,
	       ForwardedWriteReq:
      processed := false;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTISM:
    switch msg.mtype
    case RemoteInvalidationAck:
      tsrf.acnt := tsrf.acnt + 1;
      tsrf.state := Waiting;
    case UpgradeAck,
         WriteAck:
      assert (msg.cnt >= tsrf.acnt) "received more inval acks than expected";
      tsrf.acnt := msg.cnt - tsrf.acnt; -- prepare to count down
      if tsrf.acnt = 0
      then
        state := M;
	      tsrf.state := Completed;
      else
        state := remTIAM;
        tsrf.state := Waiting;
      endif;
    case RecallWriteReq,
         RecallReadReq,
	       ForwardedReadReq,
	       ForwardedWriteReq:
      processed := false;  -- refuse;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTIAM:
    switch msg.mtype
    case RemoteInvalidationAck:
      assert (tsrf.acnt > 0) "received more inval acks than expected";
      tsrf.acnt := tsrf.acnt - 1;
      if tsrf.acnt = 0
      then
        state := M;
	      tsrf.state := Completed;
      else
        tsrf.state := Waiting;
      endif;
    case RecallWriteReq,
         RecallReadReq,
	       ForwardedReadReq,
	       ForwardedWriteReq:
      processed := false; -- true;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTAM:
    switch msg.mtype
    case RemoteInvalidationAck:
      assert (tsrf.acnt > 0) "Received more inval acks than expected";
      tsrf.acnt := tsrf.acnt - 1;
      if tsrf.acnt = 0
      then
        state := M;
	      tsrf.state := Completed;
      else
        tsrf.state := Waiting;
      endif;
    case ForwardedWriteReq,
         ForwardedReadReq,
	       RecallWriteReq,
         RecallReadReq:
      -- NOT ON NIKOS' diagrams, but should be (?)
      processed := false;  -- refuse
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTRIM:
    switch msg.mtype
    case WriteFwd:         
      state := M;
      tsrf.state := Completed;
    case WriteAck:   
      -- NOT IN NIKOS' diagram... P1 has S.  P2 gets M, sending inval to P1.  
      -- P1 sends upgrade before getting inval.  P1 gets inval, goes to 
      -- remTRIM.  Home node still hasn't gotten upgrade and does local 
      -- WRITE (RecallWriteReq), which goes to p2.  Recall completes, so P1 
      -- and H are I.  Upgrade now processed, coming from a non-sharer, so 
      -- response is WriteAck. 
      -- SOLN: go straight to M.
      -- CASE 2: P1 has S, P2 gets M, sending inval to P1.  P1 sends upgrade 
      -- before getting inval.  P1 gets inval, goes to remTRIM.  Home node
      -- still hasn't gotten upgrade and does local READ (RecallReadReq), 
      -- which goes to P2.  Recall completes, so P2 and H are sharers.
      -- Upgrade now processed, coming from a non-sharer, so response is
      -- WriteAck (and P1 gets invalidated).  WriteAck beats InvalAck. 
      -- SOLN: Go to remTAM if inval cnt > 0, M otherwise (just like 
      -- remTSM -> remTAM)
      if msg.cnt = 0
      then
	      state := M;	
	      tsrf.state := Completed;
      else
        tsrf.acnt := msg.cnt;
	      state := remTAM;
	      tsrf.state := Waiting;	
      endif;        
    case RemoteInvalidationAck:
      -- NOT IN NIKOS' diagram... this one is tough.  P1 has S.  P2 gets M, 
      -- sending inval to P1.  P1 sends upgrade before getting inval.  P1
      -- gets inval, goes to remTRIM.  Home node still hasn't gotten upgrade
      -- and does local read (RecallReadReq), which goes to P2.  Recall 
      -- completes, so P2 and H are sharers.  P1's upgrade finally processed,
      -- resulting in invalidation to P2.  P2 responds to P1 w/ inval ack.
      -- SOLN: Go to remTISM, as though we were back in remTSM.  Yay!
      tsrf.acnt := tsrf.acnt + 1;  -- count up at first
      state := remTISM;
      tsrf.state := Waiting;
    case RecallWriteReq,
         RecallReadReq,
	       ForwardedReadReq,
	       ForwardedWriteReq:
      processed := false;  -- refuse      
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTLIM:
    switch msg.mtype
    case WriteAck:
      -- NOT IN NIKOS' diagram, sort of.  We can get msg.cnt > 0!  See remTRIM
      -- for similar sequence of events.
      if msg.cnt = 0
      then
	      state := M;	
	      tsrf.state := Completed;
      else
        tsrf.acnt := msg.cnt;
	      state := remTAM;
	      tsrf.state := Waiting;	
      endif;  
    case WriteFwd:
      -- NOT IN NIKOS' diagram.  P1 has S.  H starts local upgrade, and P1
      -- sends upgrade request.  P1 gets local inval, goes to TLIM.
      -- H goes to I, and gets write request from P2 (P1's upgrade still
      -- in ether).  P2's write request is serviced, and THEN P1's upgrade
      -- is serviced, resulting in ForwardedWriteReq and a WriteFwd from P2.
      state := M;
      tsrf.state := Completed;
    case RemoteInvalidationAck:
      -- NOT IN NIKOS' diagram... similar to RIAck recvd in remTRIM.
      tsrf.acnt := tsrf.acnt + 1;  -- count up at first
      state := remTISM;
      tsrf.state := Waiting;
    case RecallWriteReq,
         RecallReadReq,
	 ForwardedReadReq,
	 ForwardedWriteReq:
      processed := false; -- refuse
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTMI:
    switch msg.mtype
    case WritebackAck:
      state := I;
      tsrf.state := Completed;
    case RecallWriteReq,
         RecallReadReq:
      -- equivalent to writeback ack (for our purposes)
      state := I;
      tsrf.state := Completed;
    case ForwardedWriteReq:
      cache.clean := true;

      newmsg := CreateMsg(WriteFwd, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      
      state := remTWIF;  -- wait for WBStaleWriteAck
      tsrf.state := Waiting;
    case ForwardedReadReq:
      cache.clean := True;

      newmsg := CreateMsg(ReadFwd, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      
      state := remTRIF;  -- wait for WBStaleWriteAck
      tsrf.state := Waiting;      
    case WritebackStaleWrAck:
      state := remTWIS;
      tsrf.state := Waiting;
    case WritebackStaleRdAck:
      state := remTRIS;
      tsrf.state := Waiting;
    case LocalInvalidationReq:
      cache.clean := true;
      newmsg := CreateMsg(LocalInvalidationAck, address, n, VC2, 
		          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      state := remTII;
      tsrf.state := Waiting;
    case RemoteInvalidationReq:
      cache.clean := true;
      newmsg := CreateMsg(RemoteInvalidationAck, address, n, VC2, 
		          UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      state := remTII;
      tsrf.state := Waiting;      
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTWIF:
    switch msg.mtype
    case WritebackStaleWrAck:
      state := I;
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTRIF:
    switch msg.mtype
    case WritebackStaleRdAck:
      state := I;
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTWIS:
    switch msg.mtype
    case ForwardedWriteReq:
      cache.clean := true;

      newmsg := CreateMsg(WriteFwd, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      
      state := I;
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTRIS:
    switch msg.mtype
    case ForwardedReadReq:
      cache.clean := true;

      newmsg := CreateMsg(ReadFwd, address, n, VC2, UNDEFINED, UNDEFINED);
      Send(msg.aux, newmsg);
      
      state := I;
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  case remTII:
    switch msg.mtype
    case WritebackAck:
      state := I;
      tsrf.state := Completed;
    else
      error "Unhandled message type in remote engine";
    endswitch;

  else
    error "Unhandled cache state in remote engine";

  endswitch;
  

  return processed;
EndAlias;

End; -- function ProcessRemote


----------------------------------------------------------------------
-- Rules
----------------------------------------------------------------------
RuleSet n:NodeRange Do
RuleSet a:AddrType Do

Alias 
  cache:Nodes[n].cache[a];
  node:Nodes[n];
Do

  rule "Read Request (remote)"
    !IsLocal(a, n) & cache.state = I & 
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(ReadReq, n)
  ==>
    -- initiate xaction w/ read request
    InitiateXact(ReadReq, a, n, HomeFromAddress(a), VC0); 
    cache.state := remTIS;
  endrule;

  rule "Read Request (local)"
    IsLocal(a, n) & cache.state = M & 
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(RecallReadReq, n)
  ==>
    InitiateXact(RecallReadReq, a, n, OwnerFromAddress(a), VC1);
    cache.state := dirTML;
  endrule;

  rule "Write request (remote)"
    !IsLocal(a, n) & cache.state = I & 
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(WriteReq, n)
  ==>
    InitiateXact(WriteReq, a, n, HomeFromAddress(a), VC0);
    cache.state := remIM;
  endrule;

  rule "Write request (local)"
    IsLocal(a, n) & cache.state = M & 
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(RecallWriteReq, n)
  ==>
    InitiateXact(RecallWriteReq, a, n, OwnerFromAddress(a), VC1);
    cache.state := dirTMI;
  endrule;

  rule "Upgrade request (remote)"
    !IsLocal(a, n) & cache.state = S & 
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(UpgradeReq, n)
  ==>
    InitiateXact(UpgradeReq, a, n, HomeFromAddress(a), VC0);
    cache.state := remTSM;
  endrule;

  rule "Upgrade request (local)"
    IsLocal(a, n) & cache.state = S &
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(LocalUpgradeAccess, n)
  ==>
    var tsrf:TSRFEntry;
  begin
    if SharersListSize(a) = 0
    then
      cache.state := I;
    else
      -- create new TSRF for this xaction
      tsrf.state := Waiting;
      tsrf.acnt  := SharersListSize(a);
      tsrf.msg   := CreateMsg(LocalUpgradeAccess, a, n, VC0, UNDEFINED, UNDEFINED);
      MultiSetAdd(tsrf, Nodes[n].tsrfs);

      -- send invalidation requests
      InvalidateAndClearSharers(a, n, n, UNDEFINED);

      cache.state := dirTIS;
    endif;
  endrule;

  rule "Evict (remote)"
    !IsLocal(a, n) & cache.state = S
  ==>
    cache.state := I;
  endrule;

  rule "Writeback (remote)"
    !IsLocal(a, n) & cache.state = M &  -- FIXME: & cache.clean = false
    MultiSetCount(t:node.tsrfs, node.tsrfs[t].msg.address = a) = 0 &
    SpaceForTSRF(WritebackReq, n)
  ==>
    var tsrf:TSRFEntry;
  begin
    InitiateXact(WritebackReq, a, n, HomeFromAddress(a), VC1);
    cache.state := remTMI;
  endrule

EndAlias;

EndRuleSet;
EndRuleSet;

-- Process messages in mailbox
ruleset n:NodeRange do

ruleset vc:VC0..VC1 do
alias
  node:Nodes[n];
  msg:node.ports[vc];
do
  
  rule "recover lost msg"
    !IsUndefined(msg.address) & 
    MultiSetCount(t:node.tsrfs, 
                  node.tsrfs[t].msg.address = msg.address) = 0 &
    SpaceForTSRF(msg.mtype, n)
  ==>
    var newtsrf:TSRFEntry;
  begin
    -- Cleanup lost messages stuck in a port but neglected due to
    -- race conditions.
    newtsrf := CreateTSRF(Runnable, msg);
    MultiSetAdd(newtsrf, node.tsrfs);
    undefine msg;  -- clear port
  endrule;

endalias;
endruleset;

choose t:Nodes[n].tsrfs do
alias
  node:Nodes[n];
  tsrf:Nodes[n].tsrfs[t];
do

ruleset vc:VC1..VC2 do
alias msg:node.ports[vc] do

  rule "wake waiting tsrf"
    tsrf.state = Waiting & !IsUndefined(msg.vc) & 
    tsrf.msg.address = msg.address
  ==>
    tsrf.state := Runnable;
    tsrf.msg   := msg;
  endrule;

endalias;
endruleset;

  rule "wake blocked tsrf"
    tsrf.state = Blocked &
    MultiSetCount(i:node.tsrfs, 
		  (node.tsrfs[i].state = Waiting |
		   (node.tsrfs[i].state = Runnable & 
		    node.tsrfs[i].msg.vc >= tsrf.msg.vc)) &
                  node.tsrfs[i].msg.address = tsrf.msg.address) = 0
    -- We don't have to consider priority here - the "run tsrf" rule takes
    -- care of that.  Note that "run tsrf" checks for ANY higher priority
    -- tsrf, Runnable or not!
  ==>
    tsrf.state := Runnable;
  endrule;

  rule "run tsrf"
    tsrf.state = Runnable &
    ((tsrf.msg.vc = VC2) |
     (tsrf.msg.vc = VC1 & 
        MultiSetCount(i:node.tsrfs, node.tsrfs[i].msg.vc=VC2) = 0) |
     (tsrf.msg.vc = VC0 & 
        MultiSetCount(i:node.tsrfs, node.tsrfs[i].msg.vc=VC2) = 0 &
        MultiSetCount(i:node.tsrfs, node.tsrfs[i].msg.vc=VC1) = 0 &
        MultiSetCount(i:node.tsrfs, node.tsrfs[i].msg.vc=VC0 &
				    node.tsrfs[i].state = Waiting) = 0))
  ==>
    var newtsrf:TSRFEntry;
  begin

    if (IsLocal(tsrf.msg.address, n) & ProcessLocal(n, tsrf)) | 
       (!IsLocal(tsrf.msg.address, n) & ProcessRemote(n, tsrf))
    then
      -- TSRF successfully processed.  If this was from VC1 it may have
      -- been a message delivered to waiting thread -> remove msg from
      -- the mailbox.  If from VC2 it MUST have a msg in mailbox.
      if (tsrf.msg.vc = VC1 & !IsUndefined(node.ports[tsrf.msg.vc].vc)) |
        tsrf.msg.vc = VC2
      then
	      undefine node.ports[tsrf.msg.vc];
      endif;
    else
      -- tsrf was refused, make sure we still have something sitting in
      -- the proper mailbox
      assert (tsrf.msg.vc != VC0) "TSRF w/ VC0 priority was refused";
      assert (!IsUndefined(node.ports[tsrf.msg.vc].vc)) 
	      "TSRF refused, but no message in mailbox (port)";
      -- set current tsrf back to waiting
      tsrf.state := Waiting;

      -- create new tsrf, if space available
      if SpaceForTSRF(node.ports[tsrf.msg.vc].mtype, n)
      then
        newtsrf := CreateTSRF(Blocked, node.ports[tsrf.msg.vc]);
        MultiSetAdd(newtsrf, node.tsrfs);
	      undefine node.ports[tsrf.msg.vc];
      endif;
    endif;
 
    -- remove TSRF if completed
    if tsrf.state = Completed
    then
      MultiSetRemove(t, node.tsrfs);
    endif;
 
  endrule;


endalias;
endchoose;
endruleset;

ruleset n:NodeRange do
choose midx:Net[n] do
alias chan:Net[n];
      msg:chan[midx];
      node:Nodes[n];
do

  rule "receive"
    IsUndefined(node.ports[msg.vc].mtype) &
    ((msg.vc = VC2) |
     (msg.vc = VC1 & IsUndefined(node.ports[VC2].mtype) 
		   & MultiSetCount(m:chan, chan[m].vc = VC2) = 0) |
     (msg.vc = VC0 & IsUndefined(node.ports[VC2].mtype) 
	           & IsUndefined(node.ports[VC1].mtype)
		   & MultiSetCount(m:chan, chan[m].vc = VC2) = 0
		   & MultiSetCount(m:chan, chan[m].vc = VC1) = 0))
  ==>
    var tsrf:TSRFEntry;
  begin

    -- Insert message into port.  Think mailbox with one letter slot.
    -- We can have only one letter in the slot at a given time.
    node.ports[msg.vc] := msg;

    -- TSRF creation.
    switch msg.vc

    case VC0:
      -- Create new TSRF (space permitting).  Set to runnable if 
      -- no other thread is waiting.  Blocked otherwise.
      if SpaceForTSRF(msg.mtype, n)
      then
        tsrf := CreateTSRF(Blocked, msg);
        tsrf.state := 
	        CountTSRFs(n, msg.address, Waiting) = 0 ? Runnable : Blocked;
	      MultiSetAdd(tsrf, node.tsrfs);
        undefine node.ports[msg.vc];  -- remove from mailbox
      endif;

    case VC1:
      -- If waiting thread, change to runnable.  If no waiting thread, 
      -- create new TSRF (space permitting).  Set to runnable.
      if CountTSRFs(n, msg.address, Waiting) = 0 & SpaceForTSRF(msg.mtype, n)
      then
        tsrf := CreateTSRF(Blocked, msg);	
        tsrf.state := Runnable;
	      MultiSetAdd(tsrf, node.tsrfs);
	      undefine node.ports[msg.vc];
      endif;
      -- If there's a waiting thread, we'll handle it in the thread
      -- scheduler by seeing a message in the port mailbox.  We
      -- don't set it to runnable here b/c there's no "easy" way
      -- to pluck the right TSRF out of the multiset (w/o hacking murphi).

    case VC2:
      -- Change waiting thread to runnable.  Thread can "refuse" 
      -- this new message and start a new (blocked) TSRF.
      --   Do this in the TSRF scheduler, where we've "chosen" the 
      --   waiting thread.
    endswitch;

    -- remove the message from the network
    MultiSetRemove(midx, chan);   

  endrule;

endalias;
endchoose;
endruleset;

----------------------------------------------------------------------
-- Start State
----------------------------------------------------------------------
StartState
  assert (AddrCount % HomeCount = 0) 
    "# home nodes must be multiple of # addresses";

  undefine Nodes;
  undefine AddrMap;
  uniqueAddressCounter := 0;

  for i:NodeRange do
    InitializeNode(i);
  endfor;

  undefine uniqueAddressCounter;

EndStartState;