mtype {
    I, M,               // valid cache line states: invalid, modified
    U, X,               // 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 RQ(i) qs[recvqbase+i]
#define SQ(i) qs[sendqbase+i]

    mtype cstate = I;       // I, M, or Busy
    mtype ebcmd = I;        // I, ItoM, 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
        :: else -> SQ(i)!X
        fi }

    // Receive fill responses from peers
    :: atomic { RQ(i)?I -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) }
    :: atomic { RQ(i)?M -> assert(ebcmd == ItoM && (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 && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> if :: ebstate == I -> ebstate = U :: else fi }
    :: atomic { RQ(i)?X -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> enotsent = enotsent | (1 << i) -> ereverse = ereverse + 1 -> if
        // To prevent deadlock, if we get X'd too many times abandon the transaction and send X to its source
        :: ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ebcmd = I -> ebstate = I -> enotsent = 0 -> ereverse = 0 -> esource = -1
        :: ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ebcmd = I -> ebstate = I -> enotsent = 0 -> ereverse = 0 -> esource = -1
        :: else
        fi }

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

    // 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 -> ebcmd = I -> ebstate = I -> ereverse = 0 -> esource = -1 }

    // 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 -> ebcmd = I -> ebstate = I }

        :: else -> atomic { if
            // 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 }

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

            // Cycle through connections to all peers to ensure fairness
            :: atomic { i = (i + 1) % npeers }
            fi }
    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)
    }
}