From 4420244e9c0fdef41baf811c283d9f843265d254 Mon Sep 17 00:00:00 2001 From: Julian Blake Kongslie Date: Sat, 8 Apr 2023 13:28:28 -0700 Subject: Add spontaneous evictions. --- spin/Makefile | 2 +- spin/snoopy.pml | 55 +++++++++++++++++++++++++++++++++++++++---------------- 2 files changed, 40 insertions(+), 17 deletions(-) (limited to 'spin') diff --git a/spin/Makefile b/spin/Makefile index 73669f9..65bf08e 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 -run -bfs -bitstate $< #| egrep '^(pan|spin):' [ ! -e $@ ] || spin -c -g -l -p -replay $< .SECONDARY: diff --git a/spin/snoopy.pml b/spin/snoopy.pml index 1aff5af..3d22d21 100644 --- a/spin/snoopy.pml +++ b/spin/snoopy.pml @@ -1,6 +1,6 @@ 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) + 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 } @@ -23,7 +23,7 @@ proctype cache(int recvqbase; int sendqbase; int npeers) #define SQ(i) qs[sendqbase+i] mtype cstate = I; // I, M, or Busy - mtype ebcmd = I; // I, ItoM, 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 @@ -36,26 +36,48 @@ proctype cache(int recvqbase; int sendqbase; int npeers) :: 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(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 + :: 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 && (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 - :: atomic { ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET() } - :: atomic { ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET() } - :: else + :: 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 @@ -70,20 +92,21 @@ proctype cache(int recvqbase; int sendqbase; int npeers) :: else -> assert(false) fi -> ERESET() } -#if 0 // Simulate local cache being occupied by other address - :: atomic { if :: cstate == I -> cstate = Busy :: cstate == Busy -> cstate = I :: else fi } + :: atomic { cstate == I -> cstate = Busy } + :: atomic { cstate == Busy -> cstate = I } // Simulate evilbuffers conducting transaction for other address - :: atomic { if :: ebcmd == I -> ebcmd = Busy :: ebcmd == Busy -> ebcmd = I :: else fi } -#endif + :: 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 0 // 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 } -- cgit v1.2.3