From 7e93a297c4ac68a51b5b5847979827a8c5975ceb Mon Sep 17 00:00:00 2001 From: Julian Blake Kongslie Date: Sun, 19 Mar 2023 14:22:39 -0700 Subject: Add various spin models, including one that might actually work. --- spin/snoopy.pml | 115 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 spin/snoopy.pml (limited to 'spin/snoopy.pml') diff --git a/spin/snoopy.pml b/spin/snoopy.pml new file mode 100644 index 0000000..4774b1a --- /dev/null +++ b/spin/snoopy.pml @@ -0,0 +1,115 @@ +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) + } +} -- cgit v1.2.3