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/Makefile | 11 +++++ spin/mesi.pml | 132 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ spin/mi.pml | 80 ++++++++++++++++++++++++++++++++++ spin/snoopy.pml | 115 ++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 338 insertions(+) create mode 100644 spin/Makefile create mode 100644 spin/mesi.pml create mode 100644 spin/mi.pml create mode 100644 spin/snoopy.pml (limited to 'spin') diff --git a/spin/Makefile b/spin/Makefile new file mode 100644 index 0000000..73669f9 --- /dev/null +++ b/spin/Makefile @@ -0,0 +1,11 @@ +default: $(addsuffix .trail, $(wildcard *.pml)) + +clean: + rm -f pan* *.pml.* + +%.pml.trail: %.pml + @rm -f $@ + spin -search -bitstate -l $< | egrep '^(pan|spin):' + [ ! -e $@ ] || spin -c -g -l -p -replay $< + +.SECONDARY: diff --git a/spin/mesi.pml b/spin/mesi.pml new file mode 100644 index 0000000..5bb1c69 --- /dev/null +++ b/spin/mesi.pml @@ -0,0 +1,132 @@ +// vim: set sw=3 : + +mtype { FETCH, FETCHDONE, STORE, STOREDONE, FILLREQ, FILLRESP, EVICT, SNOOP, SNOOPRESP, NACK, M, E, S, I } +#define CACHE00 0 +#define CACHE01 1 +#define CACHE10 2 +#define NUM_CACHES 3 + +// System diagram +// +// CPU0 CPU1 +// | | +// CACHE00 CACHE01 +// | | +// CACHE10-+ +// | +// DRAM +// +// c2m queues are named c2m_, e.g. c2m_cache10 +// +// m2c queues are stored in the global m2c_info array so that they can be found as needed for snoops + +typedef m2c_info_t { + chan m2c; + int snoops_from; +} + +m2c_info_t m2c_info[2]; + +#define C2M_T [0] of {mtype /* message type */, chan /* response channel */, mtype /* have */, mtype /* want */} +#define M2C_T [0] of {mtype /* message type */, mtype /* result */} + +proctype dram(chan c2m) +{ + chan r; + mtype want; + do + :: c2m?FETCH,r,_,_ -> r!FETCHDONE,S + :: c2m?STORE,r,_,_ -> r!STOREDONE,M + :: c2m?FILLREQ,r,_,want -> r!FILLRESP,want + :: c2m?EVICT,r,_,want + od +} + +proctype cache(chan up; chan down; chan m2c; int whoami) +{ + chan r; + mtype cachestate = I; // this should be part of a global array so we can assert that at most one cache has M or E state + do + :: up?FETCH,r,_,_ -> if + :: /* no buffer available */ r!NACK,I + :: cachestate != I -> r!FETCHDONE,S + :: cachestate == I -> down!FILLREQ,m2c,cachestate,S -> + do + :: if + :: atomic { m2c?FILLRESP,cachestate -> r!FETCHDONE,S -> break } + :: atomic { m2c?NACK,_ -> down!FILLREQ,m2c,cachestate,S } + :: atomic { m2c?SNOOP,_ -> down!SNOOPRESP,m2c,cachestate,I } + fi + od + fi + :: up?STORE,r,_,_ + :: up?FILLREQ,r,_,S + :: up?FILLREQ,r,_,E + :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> cachestate = M } + :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> down!EVICT,m2c,M,I } + :: m2c?SNOOP,E -> atomic { down!SNOOPRESP,m2c,cachestate,I -> cachestate = I } + :: m2c?SNOOP,E -> if + :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I } + :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I } + :: atomic { cachestate == S -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I } + :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I } + fi + :: m2c?SNOOP,S -> if + :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I } + :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,S -> cachestate = S } + :: atomic { cachestate == S -> down!SNOOPRESP,m2c,cachestate,cachestate } + :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,downgraded_cachestate -> cachestate = downgraded_cachestate } + fi + :: atomic { cachestate == M -> down!EVICT,m2c,cachestate,I -> cachestate = I } + od +} + +proctype cpu(chan c2m; chan m2c) +{ +progress: + do + :: do + :: c2m!FETCH,m2c,I,S -> if + :: m2c?FETCHDONE,_ -> break + :: m2c?NACK,_ + fi + od + :: do + :: c2m!STORE,m2c,I,M -> if + :: m2c?STOREDONE,_ -> break + :: m2c?NACK,_ + fi + od + od +} + +init +{ + // downstream channels + chan c2m_cache00 = C2M_T; + chan c2m_cache01 = C2M_T; + chan c2m_cache10 = C2M_T; + chan c2m_dram = C2M_T; + + // upstream channels + chan m2c_cpu0 = M2C_T; + chan m2c_cpu1 = M2C_T; + chan m2c_cache00 = M2C_T; + chan m2c_cache01 = M2C_T; + chan m2c_cache10 = M2C_T; + + atomic + { + // construct snoop table + m2c_info[0].m2c = m2c_cache00; m2c_info[0].snoops_from = CACHE10; + m2c_info[1].m2c = m2c_cache01; m2c_info[1].snoops_from = CACHE10; + + // construct processes + run cpu(c2m_cache00, m2c_cpu0); + run cpu(c2m_cache01, m2c_cpu1); + run cache(c2m_cache00, c2m_cache10, m2c_cache00, CACHE00); + run cache(c2m_cache01, c2m_cache10, m2c_cache01, CACHE01); + run cache(c2m_cache10, c2m_dram, m2c_cache10, CACHE10); + run dram(c2m_dram); + } +} diff --git a/spin/mi.pml b/spin/mi.pml new file mode 100644 index 0000000..52a384e --- /dev/null +++ b/spin/mi.pml @@ -0,0 +1,80 @@ +// vim: set sw=3 : + +mtype { + I, M, + ItoM, MtoI, // from upstream + SnoopItoM, // from downstream + Fetch, Store, + Busy, Done, Fail +} + +m_type cachestate; // I, M, Busy +m_type evilstate; // I, Free, ItoM, MtoI +int evilsource; // which upstream is the evilstate "on behalf of"; -1 is downstream +int evilnotsent; // bitmask of upstreams we have not yet sent snoops to +int evilnotreplied; // bitmask of upstreams that have not yet replied to snoops +int evilnewstate; // new M/E/S/I state + +evil buffer: + state + bitmask of upstreams we have not yet snooped + bitmask of upstreams that have not yet replied + source of this buffer's transaction + +proctype cache() +{ + do + :: i = (i + 1) % N + :: assert(cachestate == I || cachestate == M || cachestate == Busy) + :: assert(evilstate == I || evilstate == ItoM || evilstate == MtoI || evilstate == SnoopItoM || evilstate == Busy) + :: atomic { cachestate == I -> cachestate = Busy } + :: atomic { cachestate == Busy -> cachestate = I } + :: atomic { evilstate == I -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = Busy } + :: atomic { evilstate == Busy -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = I } + + :: downrecvq?SnoopItoM -> if + :: cachestate == M -> cachestate = I -> downsendq!M + :: else -> if + :: evilstate == I -> evilstate = SnoopItoM -> evilnotsent = (1 << N) - 1 + :: else -> assert(evilstate != SnoopItoM) -> downsendq!Fail + fi + fi + :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent & (1 << i) && can send to upstream i -> evilnotsent &= ~(1 << i) -> evilnotreplied |= 1 << i -> upsendq[i]!SnoopItoM } + :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent == 0 && evilnotreplied == 0 -> if :: evilnewstate == I -> if :: evilstate == ItoM -> upsendq[evilsource]!I :: else -> downsendq!I fi :: else -> evilnewstate = I fi -> evilstate = I -> evilsource = -1 } + :: atomic { uprecvq[i]?I -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) } + :: atomic { uprecvq[i]?M -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) -> evilnewstate = M -> if :: evilstate == ItoM -> upsendq[evilsource]!M :: else -> downsendq!M fi } + + + + + + + + + :: atomic { downrep[i] is empty -> if + :: upreq[i]?Fetch -> if + :: atomic { cachestate == Busy -> uprep[i]!Fail } + :: atomic { cachestate == M -> uprep[i]!Done } + :: cachestate == I -> do + :: uprep[i]!Fail + :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy } + od + fi + :: upreq[i]?Store -> if + :: atomic { cachestate == Busy -> uprep[i]!Fail } + :: atomic { cachestate == M -> uprep[i]!Done } + :: cachestate == I -> do + :: uprep[i]!Fail + :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy } + od + fi + :: upreq[i]?ItoM -> if + :: atomic { cachestate == M -> cachestate = I -> uprep[i]!ItoM } + :: atomic { cachestate == I && evilstate == I -> if + :: can send downstream -> evilstate = SnoopItoM -> evilsource = i -> assert(evilwaiting == 0) -> + j = 0 -> do :: j < N -> if :: i != j -> upsnoop[j]!SnoopItoM -> evilwaiting |= 1 << j :: else fi -> j = j + 1 :: else -> break fi od -> + uprep[i]!Busy + :: !can send downstream -> uprep[i]!Fail + fi } + fi + 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