From fa364103127162af6656950c56be2e8953010d25 Mon Sep 17 00:00:00 2001 From: Mike Haertel Date: Tue, 21 Mar 2023 08:35:13 -0700 Subject: Messy spin snapshot with bug demo --- spin/Makefile | 2 +- spin/snoopy.pml | 74 ++++++++++++++++++++++++++++++++++----------------------- 2 files changed, 45 insertions(+), 31 deletions(-) (limited to 'spin') diff --git a/spin/Makefile b/spin/Makefile index 73669f9..cb862cf 100644 --- a/spin/Makefile +++ b/spin/Makefile @@ -5,7 +5,7 @@ clean: %.pml.trail: %.pml @rm -f $@ - spin -search -bitstate -l $< | egrep '^(pan|spin):' + spin -search -bit $< | egrep '^(pan|spin):' [ ! -e $@ ] || spin -c -g -l -p -replay $< .SECONDARY: diff --git a/spin/snoopy.pml b/spin/snoopy.pml index 4774b1a..0b4de5d 100644 --- a/spin/snoopy.pml +++ b/spin/snoopy.pml @@ -20,70 +20,84 @@ 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] +#define ERESET() atomic { ebcmd = I; ebstate = I; enotsent = 0; enotrcvd = 0; ereverse = 0; esource = -1; } +#define P() noprogress = 0 mtype cstate = I; // I, M, or Busy mtype ebcmd = I; // I, ItoM, or Busy - int ebstate = I; // I, M, or U + mtype 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 + int fairmask = 0; // fairness mask to ensure servicing all peers + int noprogress = 0; // increment loop breaker 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 != M && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS & ~(1 << i) -> esource = i :: else -> SQ(i)!X - fi } + fi -> P() } // 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)?I -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> P() } :: 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 } + fi -> P() } + :: 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 -> P() } :: 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 + :: ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET() + :: ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET() :: else - fi } + fi -> P() } // Send not-yet-sent snoops - :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM } + :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM -> P() } - // Complete requests from peers (sending response if not sent earlier) + // Complete requests from peers (sending response to source if not already sent earlier) :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource != -1 -> if :: ebstate == I -> SQ(esource)!I - :: ebstate == M + :: ebstate == M -> skip :: ebstate == U -> SQ(esource)!U :: else -> assert(false) - fi -> ebcmd = I -> ebstate = I -> ereverse = 0 -> esource = -1 } + fi -> ERESET() -> P() } // 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 } + fi -> ERESET() -> P() } -> skip + +#if 0 + // Simulate local resources in use due to activity at other addresses + :: atomic { if :: cstate == I -> cstate = Busy :: cstate == Busy -> cstate = I fi } + :: atomic { if :: ebcmd == I -> ebcmd = Busy :: ebcmd == Busy -> ebcmd = I } +#endif + +#if 0 // these assertions further explode the states + // 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) } +#endif + + // 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 -> P() } + +#if 1 + // Cycle through connections to all peers to ensure fairness + :: atomic { noprogress < 2 -> i = (i + 1) % npeers -> if :: i == 0 -> noprogress = noprogress + 1 :: else fi } +#else + :: atomic { noprogress < 2 && npeers >= 1 && (fairmask & 1) == 0 -> i = 0 -> fairmask = fairmask | 1 } + :: atomic { noprogress < 2 && npeers >= 2 && (fairmask & 2) == 0 -> i = 1 -> fairmask = fairmask | 2 } + :: atomic { noprogress < 2 && npeers >= 3 && (fairmask & 4) == 0 -> i = 2 -> fairmask = fairmask | 4 } + :: atomic { fairmask == (1 << npeers) - 1 -> fairmask = 0 -> noprogress = noprogress + 1 } +#endif od #undef ALLPEERS -- cgit v1.2.3