// vim: set sw=3 :

mtype { FETCH, FETCHDONE, STORE, STOREDONE, FILLREQ, FILLRESP, EVICT, SNOOP, SNOOPRESP, NACK, M, E, S, I }
#define CACHE00 0
#define CACHE01 1
#define CACHE10 2
#define NUM_CACHES 3

// System diagram
//
// CPU0    CPU1
// |       |
// CACHE00  CACHE01
// |       |
// CACHE10-+
// |
// DRAM
//
// c2m queues are named c2m_<receiving process>, e.g. c2m_cache10
//
// m2c queues are stored in the global m2c_info array so that they can be found as needed for snoops

typedef m2c_info_t {
   chan m2c;
   int snoops_from;
}

m2c_info_t m2c_info[2];

#define C2M_T [0] of {mtype /* message type */, chan /* response channel */, mtype /* have */, mtype /* want */}
#define M2C_T [0] of {mtype /* message type */, mtype /* result */}

proctype dram(chan c2m)
{
   chan r;
   mtype want;
   do
   :: c2m?FETCH,r,_,_ -> r!FETCHDONE,S
   :: c2m?STORE,r,_,_ -> r!STOREDONE,M
   :: c2m?FILLREQ,r,_,want -> r!FILLRESP,want
   :: c2m?EVICT,r,_,want
   od
}

proctype cache(chan up; chan down; chan m2c; int whoami)
{
   chan r;
   mtype cachestate = I; // this should be part of a global array so we can assert that at most one cache has M or E state
   do
   :: up?FETCH,r,_,_ -> if
      :: /* no buffer available */ r!NACK,I
      :: cachestate != I -> r!FETCHDONE,S
      :: cachestate == I -> down!FILLREQ,m2c,cachestate,S ->
         do
         :: if
            :: atomic { m2c?FILLRESP,cachestate -> r!FETCHDONE,S -> break }
            :: atomic { m2c?NACK,_ -> down!FILLREQ,m2c,cachestate,S }
            :: atomic { m2c?SNOOP,_ -> down!SNOOPRESP,m2c,cachestate,I }
            fi
         od
      fi
   :: up?STORE,r,_,_
   :: up?FILLREQ,r,_,S
   :: up?FILLREQ,r,_,E
   :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> cachestate = M }
   :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> down!EVICT,m2c,M,I }
   :: m2c?SNOOP,E -> atomic { down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
   :: m2c?SNOOP,E -> if
      :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
      :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
      :: atomic { cachestate == S -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
      :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
      fi
   :: m2c?SNOOP,S -> if
      :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
      :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,S -> cachestate = S }
      :: atomic { cachestate == S -> down!SNOOPRESP,m2c,cachestate,cachestate }
      :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,downgraded_cachestate -> cachestate = downgraded_cachestate }
      fi
   :: atomic { cachestate == M -> down!EVICT,m2c,cachestate,I -> cachestate = I }
   od
}

proctype cpu(chan c2m; chan m2c)
{
progress:
   do
   :: do
      :: c2m!FETCH,m2c,I,S -> if
         :: m2c?FETCHDONE,_ -> break
         :: m2c?NACK,_
         fi
      od
   :: do
      :: c2m!STORE,m2c,I,M -> if
         :: m2c?STOREDONE,_ -> break
         :: m2c?NACK,_
         fi
      od
   od
}

init
{
   // downstream channels
   chan c2m_cache00 = C2M_T;
   chan c2m_cache01 = C2M_T;
   chan c2m_cache10 = C2M_T;
   chan c2m_dram = C2M_T;

   // upstream channels
   chan m2c_cpu0 = M2C_T;
   chan m2c_cpu1 = M2C_T;
   chan m2c_cache00 = M2C_T;
   chan m2c_cache01 = M2C_T;
   chan m2c_cache10 = M2C_T;

   atomic
   {
      // construct snoop table
      m2c_info[0].m2c = m2c_cache00; m2c_info[0].snoops_from = CACHE10;
      m2c_info[1].m2c = m2c_cache01; m2c_info[1].snoops_from = CACHE10;

      // construct processes
      run cpu(c2m_cache00, m2c_cpu0);
      run cpu(c2m_cache01, m2c_cpu1);
      run cache(c2m_cache00, c2m_cache10, m2c_cache00, CACHE00);
      run cache(c2m_cache01, c2m_cache10, m2c_cache01, CACHE01);
      run cache(c2m_cache10, c2m_dram, m2c_cache10, CACHE10);
      run dram(c2m_dram);
   }
}