1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
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
|
