mtype {
    I, M,               // valid cache line states: invalid, modified
    U, X,               // evict/fill/snoop responses that are not valid cache line states: unknown (from DRAM only), fail (you have to try again)
    ItoM, MtoI,         // commands from peers
    Busy,               // used as both cache line state and evil buffer command to denote activity on behalf of other addresses
}

proctype dram(chan recvq; chan sendq)
{
    do
    :: atomic { recvq?ItoM -> sendq!U }
    :: atomic { recvq?MtoI -> sendq!I }
    od
}

chan qs[6] = [1] of { mtype };

proctype cache(int recvqbase; int sendqbase; int npeers)
{
#define ALLPEERS ((1 << npeers) - 1)
#define ERESET() atomic { ebcmd = I; ebstate = I; enotsent = 0; enotrcvd = 0; ereverse = 0; esource = -1; }
#define RQ(i) qs[recvqbase+i]
#define SQ(i) qs[sendqbase+i]

    mtype cstate = I;       // I, M, or Busy
    mtype ebcmd = I;        // I, ItoM, MtoI, or Busy
    int ebstate = I;        // I, M, or U
    int enotsent = 0;       // bitmask of snoops remaining to send
    int enotrcvd = 0;       // bitmask of replies remaining to receive
    int ereverse = 0;       // count of reverse progress
    int esource = -1;       // source of command (-1 is originated locally)
    int i = 0;              // current peer

    do
    // Receive fill request from peer
    :: atomic { RQ(i)?ItoM -> if
        :: cstate == M -> cstate = I -> SQ(i)!M
        :: cstate == I && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS & ~(1 << i) -> esource = i
        :: cstate == I && ebcmd == MtoI && enotsent != 0 -> ERESET() -> SQ(i)!M
        :: else -> SQ(i)!X
        fi }

    // Receive eviction request from peer
    :: atomic { RQ(i)?MtoI -> if
        :: cstate == M || ebcmd == MtoI -> assert(false)
        :: cstate == I && ebcmd == I -> cstate = M -> SQ(i)!I
//        :: cstate == I && ebcmd == ItoM -> ebstate = M -> enotsent = 0 -> SQ(i)!I // Missing logic: cut-through send to esource, clear out eb when enotrcvd is already 0
        :: cstate == I && ebcmd == ItoM -> SQ(i)!X
        :: cstate == I && ebcmd == Busy -> cstate = M -> SQ(i)!I
        :: cstate == Busy && ebcmd == I -> assert(i != npeers-1) -> ebcmd = MtoI -> enotsent = 1 << (npeers-1) -> SQ(i)!I
        :: cstate == Busy && ebcmd != I -> SQ(i)!X
        fi }

    // Receive fill responses from peers
    :: atomic { RQ(i)?I -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> if
        :: ebcmd == ItoM -> enotrcvd = enotrcvd & ~(1 << i)
        :: ebcmd == MtoI -> ERESET()
        :: else -> assert(false)
        fi }
    :: atomic { RQ(i)?M -> assert(ebcmd == ItoM) -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> ebstate = M -> if
        :: esource != -1 -> SQ(esource)!M
        :: else /* ideally put it into the cache right away */
        fi }
    :: atomic { RQ(i)?U -> assert(ebcmd == ItoM) -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> if :: ebstate == I -> ebstate = U :: else fi }
    :: atomic { RQ(i)?X -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> enotsent = enotsent | (1 << i) -> if
        :: ebcmd == ItoM -> ereverse = ereverse + 1 -> if
            :: atomic { ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET() }
            :: atomic { ereverse > npeers - 1 && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET() }
            :: else
            fi
        :: ebcmd == MtoI
        :: else -> assert(false)
        fi }

    // Send not-yet-sent snoops
    :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM }

    // Send not-yet-sent evictions
    :: atomic { ebcmd == MtoI && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!MtoI }

    // Complete requests from peers (sending response if not sent earlier)
    :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource != -1 -> if
        :: ebstate == I -> SQ(esource)!I
        :: ebstate == M
        :: ebstate == U -> SQ(esource)!U
        :: else -> assert(false)
        fi -> ERESET() }

    // Complete locally-originated request when cache space is available to hold the data
    :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource == -1 && cstate == I -> if
        :: (ebstate == M | ebstate == U) -> cstate = M
        :: else -> assert(false)
        fi -> ERESET() }

    // Simulate local cache being occupied by other address
    :: atomic { cstate == I -> cstate = Busy }
    :: atomic { cstate == Busy -> cstate = I }

    // Simulate evilbuffers conducting transaction for other address
    :: atomic { ebcmd == I -> ebcmd = Busy }
    :: atomic { ebcmd == Busy -> ebcmd = I }

    // Simulate local cache spontaneously evicting
    :: atomic { cstate == M && ebcmd == I -> cstate = I -> ebcmd = MtoI -> enotsent = 1 << (npeers-1) }

    // If we're not in a transaction assert that the evil buffer is fully reset (just to make sure we've limited reachable states)
    :: atomic { ebcmd == Busy || ebcmd == I -> assert(ebstate == I && enotsent == 0 && enotrcvd == 0 && ereverse == 0 && esource == -1) }
    // If we're in ItoM transaction assert that it's not in the cache
    :: atomic { ebcmd == ItoM -> assert(cstate == I || cstate == Busy) }

    // Launch locally-requested fills; rely on deadlock avoidance above to protect from multiple peers simultaneously deciding to do this
    :: atomic { cstate != M && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS -> esource = -1 }

    // Cycle through connections to all peers to ensure fairness
    :: atomic { i = (i + 1) % npeers }
    od

#undef ALLPEERS
#undef RQ
#undef SQ
}

//  C1   C2
//    \  /
//     C3
//     |
//    DRAM
//
// [0] is c1-to-c3
// [1] is c2-to-c3
// [2] is dram-to-c3
// [3] is c3-to-c1
// [4] is c3-to-c2
// [5] is c3-to-dram

init
{
    atomic {
        run cache(3, 0, 1);     // C1   (will be proc 1)
        run cache(4, 1, 1);     // C2   (will be proc 2)
        run cache(0, 3, 3);     // C3   (will be proc 3)
        run dram(qs[5], qs[2]); // dram (will be proc 4)
    }
}