A protocol model checker explores every reachable state of an abstract protocol: every order of core events, every order of message delivery. The cost is the number of states, which grows quickly with each cache, address, data value and buffer slot. The practical answer is to check a small configuration exhaustively rather than a large one partially.
Coherence bugs are races between a few agents on one line: a GetM meeting a sharer, an Inv crossing a PutS, a Fwd-GetM arriving at a cache in IM^D. Two or three caches, one or two addresses and two data values can already build those interleavings. This is the small-scope hypothesis, a general guideline rather than a theorem: most bugs have a small counterexample. It justifies choosing parameters, not skipping larger checks; some bugs need more agents (a third sharer to exercise an ack counter above 1), two addresses (replacement, or a resource shared between lines) or a deeper buffer.
Parameter | Smallest useful value | What a larger value adds |
|---|---|---|
Caches | 2 (a reader and a writer) | 3: ack counts above 1, a third request queued during a race |
Addresses | 1 | 2: eviction and replacement, shared buffers, cross-line resource cycles |
Data values | 2 (enough to tell a lost write from a kept one) | More values rarely add behaviour if the protocol never inspects data |
Outstanding per cache | 1 | Several MSHRs: request merging, cross-line deadlock |
The program models MSI on the course model with a deliberately smaller scope, stated here: one address X, data domain {0, 1}, no evictions (so no PutS, PutM or Put-Ack), and caches C0, C1 (and C2 for the three-cache count). Delivery is unordered: the network is a multiset and any message in it may be delivered next. H serializes X: it accepts a new request only when idle, collects Inv-Acks itself (the course convention), forwards to an exclusive holder with Fwd-GetS or Fwd-GetM and relays that holder's Data. As in Parts 1 to 3, H learns when its grant has been delivered (assumed), so in the model H becomes idle when Data reaches the requester. H records the new holder or sharers when it sends the grant, not at delivery as the Part 4 tables do; no other request for X is served in between, so this changes no reachable behaviour. An Inv-Ack with no pending entry is dropped (reachable only with the early-grant bug). The program's directory has no separate U: an empty sharer set stands for U. One deviation is deliberate: Data on an upgrade carries memory's copy, unlike the course's permission-only Data, so a cache in SM^D installs the value H sends. In a correct protocol memory is current whenever the line has sharers, so this changes nothing; with a lost writeback it is the path by which the stale value reaches a cache.
A state is the tuple (cache states and values, directory, memory, H's pending entry, messages in flight, ghost). Breadth-first search starts at reset (both I, memory = 0), applies every enabled event, and checks SWMR and the data-value invariant on each new state. Because the search is breadth first, the first violation found has a shortest trace, which the parent links reconstruct.
from collections import deque
DOM = (0, 1) # small data domain
READABLE = {"S", "SM^D", "M"} # states in which a load hits
def successors(s, bug):
caches, dirx, mem, pend, net, ghost = s
def mk(i=None, st=None, d=dirx, m=mem, p=pend, add=(), drop=None, g=ghost):
c, n = list(caches), list(net)
if i is not None:
c[i] = st
n.remove(drop) if drop else None
return (tuple(c), d, m, p, tuple(sorted(n + list(add))), g)
for i, (st, v) in enumerate(caches): # core events
if st == "I":
yield f"C{i} load", mk(i, ("IS^D", None), add=[("GetS", i)])
yield f"C{i} store", mk(i, ("IM^D", None), add=[("GetM", i)])
if st == "S":
yield f"C{i} store", mk(i, ("SM^D", v), add=[("GetM", i)])
if st == "M":
for w in DOM:
yield f"C{i} store {w}", mk(i, ("M", w), g=w)
for msg in set(net): # unordered: any message may go next
kind, who = msg[0], msg[1]
st, v = caches[who]
if kind in ("GetS", "GetM") and pend is None: # H serializes X
if dirx[0] == "X": # forward to the exclusive holder
yield f"H {kind}", mk(p=(kind, who), add=[("Fwd" + kind[3], dirx[1])], drop=msg)
elif kind == "GetS":
yield "H GetS", mk(d=("S", dirx[1] | {who}), p=("grant",),
add=[("Data", who, mem, "S")], drop=msg)
else:
invs = [("Inv", j) for j in sorted(dirx[1] - {who})]
if not invs or bug == "early-grant": # BUG: M before Inv-Acks
yield "H GetM", mk(d=("X", who), p=("grant",),
add=invs + [("Data", who, mem, "M")], drop=msg)
else:
yield "H GetM", mk(p=("acks", who, len(invs)), add=invs, drop=msg)
elif kind == "Inv":
new = {"S": ("I", None), "SM^D": ("IM^D", None)}.get(st, (st, v))
yield f"C{who} Inv", mk(who, new, add=[("InvAck", who)], drop=msg)
elif kind == "InvAck":
if pend and pend[0] == "acks" and pend[2] > 1:
yield "H InvAck", mk(p=("acks", pend[1], pend[2] - 1), drop=msg)
elif pend and pend[0] == "acks":
yield "H InvAck", mk(d=("X", pend[1]), p=("grant",),
add=[("Data", pend[1], mem, "M")], drop=msg)
else:
yield "H late InvAck", mk(drop=msg)
elif kind in ("FwdS", "FwdM"):
new = ("S", v) if kind == "FwdS" else ("I", None)
yield f"C{who} {kind}", mk(who, new, add=[("DataH", who, v)], drop=msg)
elif kind == "DataH" and pend[0] == "GetS": # H writes memory, both S
m = mem if bug == "no-writeback" else msg[2]
yield "H DataH", mk(m=m, d=("S", frozenset({who, pend[1]})), p=("grant",),
add=[("Data", pend[1], msg[2], "S")], drop=msg)
elif kind == "DataH":
yield "H DataH", mk(d=("X", pend[1]), p=("grant",),
add=[("Data", pend[1], msg[2], "M")], drop=msg)
elif kind == "Data": # (assumed) H learns the grant arrived
yield f"C{who} Data", mk(who, (msg[3], msg[2]), p=None, drop=msg)
def violation(s, full):
caches, ghost = s[0], s[5]
writers = [i for i, (st, _) in enumerate(caches) if st == "M"]
readers = [i for i, (st, _) in enumerate(caches) if st in READABLE]
if writers and readers != writers:
return "SWMR"
if full and any(v != ghost for st, v in caches if st in READABLE):
return "data-value"
def check(n, bug=None, full=True):
init = (tuple([("I", None)] * n), ("S", frozenset()), 0, None, (), 0)
parent, frontier = {init: None}, deque([init])
while frontier: # breadth first: shortest trace
s = frontier.popleft()
if violation(s, full):
kind, trace = violation(s, full), []
while parent[s]:
s, label = parent[s]
trace.append(label)
return kind, trace[::-1]
for label, t in successors(s, bug):
if t not in parent:
parent[t] = (s, label)
frontier.append(t)
return len(parent), None
(n2, ok2), (n3, ok3) = check(2), check(3)
assert ok2 is None and ok3 is None and (n2, n3) == (189, 1996)
assert check(2, "early-grant") == ("SWMR", ["C0 load", "C1 store", "H GetS", "C0 Data", "H GetM", "C1 Data"])
kind, trace = check(2, "no-writeback")
assert kind == "data-value" and len(trace) == 14
assert check(2, "no-writeback", full=False) == (187, None) # SWMR alone misses it
print(f"PASS: {n2} states (2 caches), {n3} (3 caches) safe, early grant fails SWMR in 6 steps, lost writeback fails data-value")Configuration of this model | Reachable states | Time on a laptop |
|---|---|---|
2 caches, data {0, 1} | 189 | well under 0.1 s |
2 caches, data {0, 1, 2} | 343 (measured) | well under 0.1 s |
3 caches, data {0, 1} | 1,996 | well under 0.1 s |
3 caches, data {0, 1, 2} | 3,435 (measured) | well under 0.1 s |
4 caches, data {0, 1} | 23,249 (measured) | about 0.1 s |
These counts come from the program above: the first and third are asserted, and the others, marked measured, were produced by changing DOM and n. Each extra cache multiplies the count by roughly ten here, because it adds its own states, its own messages in flight and their orderings. Adding addresses, buffer slots or evictions compounds that growth, which is why real protocol models keep the scope small and use symmetry between caches and other reductions.
With the seeded bug, H grants M at the same time as it sends the Inv instead of after the Inv-Ack. The search returns a six-event trace (MSI, from reset) that is the trace of Racing Requests at the Home with H sending the step 6 grant together with the step 4 Inv: C0's GetS (1) and C1's GetM (2) are both sent, H serves the GetS and C0 receives Data (3), with the GetM waiting meanwhile (the model keeps it in the network until H is idle, which is equivalent to H's queue). The search found this race without anyone having to think of it. Only steps 4 and 6 differ; step 5 (the Inv-Ack) has not happened when the grant is sent, so only steps 4 and 6 are drawn.
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
After step 3, as in Racing Requests | S / 0 | IM^D / - | S{C0}, queued GetM C1 | 0 | C0 and memory: 0 |
H starts B (BUG): 4. Inv and 6. Data sent together | S / 0 | IM^D / - | S{C0}, pend GetM C1, acks 0/1 (BUG: granted early) | 0 | C0 and memory: 0, Data(0) in flight to C1 |
6. Data at C1 | S / 0 | M / 0 | S{C0}, pend GetM C1, acks 0/1 (BUG: granted early) | 0 | C0, C1 and memory: 0, SWMR fails |
As in What a Violation Looks Like, the failure appears while every copy still holds 0; a value-only check would wait for C1's store. The fix is the acknowledgement boundary: H keeps the GetM pending with acks 0/1 until C0's Inv-Ack, and only then sends Data with M permission (the correct model in the program). The second seeded bug, H forgetting to write memory when it relays the dirty Data for a Fwd-GetS, keeps every permission legal: a check with SWMR only explores all 187 states and passes (asserted), while the data-value invariant finds a 14-event trace: C1 writes 1, C0's GetS leaves both in S with memory still 0, and C1's upgrade Data, which carries memory's copy (the scope deviation above), gives C1 M with the stale 0 after the last store wrote 1.
An ack-counting bug that only appears with more than one sharer, such as granting after the first Inv-Ack instead of the last. With 2 caches a GetM can have at most one other sharer, so the counter never goes above 1. Three caches let two sharers be invalidated by one GetM.