// vim: set sw=3 :

mtype {
   I, M,
   ItoM, MtoI, // from upstream
   SnoopItoM, // from downstream
   Fetch, Store,
   Busy, Done, Fail
}

m_type cachestate; // I, M, Busy
m_type evilstate; // I, Free, ItoM, MtoI
int evilsource; // which upstream is the evilstate "on behalf of"; -1 is downstream
int evilnotsent; // bitmask of upstreams we have not yet sent snoops to
int evilnotreplied; // bitmask of upstreams that have not yet replied to snoops
int evilnewstate; // new M/E/S/I state

evil buffer:
   state
   bitmask of upstreams we have not yet snooped
   bitmask of upstreams that have not yet replied
   source of this buffer's transaction

proctype cache()
{
   do
   :: i = (i + 1) % N
   :: assert(cachestate == I || cachestate == M || cachestate == Busy)
   :: assert(evilstate == I || evilstate == ItoM || evilstate == MtoI || evilstate == SnoopItoM || evilstate == Busy)
   :: atomic { cachestate == I -> cachestate = Busy }
   :: atomic { cachestate == Busy -> cachestate = I }
   :: atomic { evilstate == I -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = Busy }
   :: atomic { evilstate == Busy -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = I }

   :: downrecvq?SnoopItoM -> if
      :: cachestate == M -> cachestate = I -> downsendq!M
      :: else -> if
         :: evilstate == I -> evilstate = SnoopItoM -> evilnotsent = (1 << N) - 1
         :: else -> assert(evilstate != SnoopItoM) -> downsendq!Fail
         fi
      fi
   :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent & (1 << i) && can send to upstream i -> evilnotsent &= ~(1 << i) -> evilnotreplied |= 1 << i -> upsendq[i]!SnoopItoM }
   :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent == 0 && evilnotreplied == 0 -> if :: evilnewstate == I -> if :: evilstate == ItoM -> upsendq[evilsource]!I :: else -> downsendq!I fi :: else -> evilnewstate = I fi -> evilstate = I -> evilsource = -1 }
   :: atomic { uprecvq[i]?I -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) }
   :: atomic { uprecvq[i]?M -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) -> evilnewstate = M -> if :: evilstate == ItoM -> upsendq[evilsource]!M :: else -> downsendq!M fi }








   :: atomic { downrep[i] is empty -> if
      :: upreq[i]?Fetch -> if
         :: atomic { cachestate == Busy -> uprep[i]!Fail }
         :: atomic { cachestate == M -> uprep[i]!Done }
         :: cachestate == I -> do
            :: uprep[i]!Fail
            :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy }
            od
         fi
      :: upreq[i]?Store -> if
         :: atomic { cachestate == Busy -> uprep[i]!Fail }
         :: atomic { cachestate == M -> uprep[i]!Done }
         :: cachestate == I -> do
            :: uprep[i]!Fail
            :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy }
            od
         fi
      :: upreq[i]?ItoM -> if
         :: atomic { cachestate == M -> cachestate = I -> uprep[i]!ItoM }
         :: atomic { cachestate == I && evilstate == I -> if
            :: can send downstream -> evilstate = SnoopItoM -> evilsource = i -> assert(evilwaiting == 0) ->
               j = 0 -> do :: j < N -> if :: i != j -> upsnoop[j]!SnoopItoM -> evilwaiting |= 1 << j :: else fi -> j = j + 1 :: else -> break fi od ->
               uprep[i]!Busy
            :: !can send downstream -> uprep[i]!Fail
            fi }
         fi