A reference model is an executable specification: given the same stimulus, it says what the design may do. For coherence it has two halves. The protocol half is a simple, obviously correct version of the course protocol. The checker half holds the golden memory and asserts the invariants after every event, not only at the end. The model below is about a hundred lines, runs thousands of events in a fraction of a second, and is reused, with bugs injected, in the next lesson.
It follows the course model with one extension, stated here: three caches C0, C1 and C2, because ack counting and a grant that waits for the last of several Inv-Acks need at least two sharers besides the requester. Protocol MSI, one line X, X = 0 in memory and in no cache at the start.
Piece | In the code | Course rule it follows |
|---|---|---|
Caches | State I, S, M or a transient (IS, IM, SM for IS^D, IM^D, SM^D; MI, SI, II for MI^A, SI^A, II^A) and a value | One outstanding request per cache, stalled access completes first when the grant arrives |
Home H | Directory U, S with a sharer set, or exclusive(holder) (dir 'M' in the code); memory; one busy entry for X | H serializes requests for X: while busy, new GetS, GetM, PutS and PutM wait in the network |
Messages | GetS, GetM, PutS, PutM, Fwd-GetS, Fwd-GetM, Inv, Inv-Ack, Data, Put-Ack | Inv-Acks are collected at H, data from a holder travels through H |
Network | An unordered list; each step delivers any ready message chosen by the seeded generator | No FIFO order between any two nodes or message classes |
Grant delivery | H's busy entry clears when its Data reaches the requester | The course-model assumption that H can tell its grant was delivered |
Checker | Golden value, SWMR, every usable copy equals golden, every load equals golden, message legal in the receiver's state, end-of-run drain check | SWMR and the data-value invariant, checked after every event |
Message at H | Directory | H does |
|---|---|---|
GetS | U or S | Adds the requester to the sharers, sends Data from memory |
GetS | exclusive(holder) (dir 'M' in the code) | Sends Fwd-GetS to the holder; when its Data arrives, writes memory, records S{holder, requester}, or S{requester} if the holder answered from its WB entry (Data says PutM outstanding), and sends Data |
GetM | U or S | Sends Inv to every other sharer and counts them; when the count reaches zero, records exclusive(requester) and sends Data |
GetM | exclusive(holder) | Sends Fwd-GetM to the holder; when its Data arrives, records exclusive(requester) and sends Data |
PutM | exclusive(sender) | Writes memory, records U, sends Put-Ack |
PutS or PutM | Sender is a sharer or no longer a holder | Removes it from the sharers if present, sends Put-Ack, memory unchanged (late Put) |
Two simplifications of the course protocol, stated as the course requires. Deviation, as in Small Models and Parameters: the M grant always carries memory's value, including the permission-only grant of an upgrade (memory is current while the line has sharers in MSI). And H records the new holder or sharer when it sends the grant, while its busy entry stays set until the Data is delivered; the capstone model records it at delivery, as the Part 4 tables do. Neither changes what a correct run does, because no other request for X is served while the entry is busy.
Message at a cache | Legal states and new state |
|---|---|
Data | IS to S (the load completes), IM or SM to M (the store completes) |
Inv | S to I, SM to IM (keeps the store intent), SI to II; sends Inv-Ack |
Fwd-GetS | M to S, MI to SI; sends Data to H, from MI marked PutM outstanding |
Fwd-GetM | M to I, MI to II; sends Data to H, from MI marked PutM outstanding |
Put-Ack | MI, SI or II to I |
Any other message-state pair is a protocol error and fails the run, at a cache or at H (an Inv-Ack or Data that no pending entry at H is waiting for): that is the model's protocol checker. The eviction rows are order B of Eviction Versus Intervention: a cache in MI^A still answers a forward from its writeback buffer, its Data says PutM outstanding so H does not record it as a sharer, and its late PutM, now from a non-holder, gets Put-Ack without touching the directory or memory.
import random
from collections import Counter
REQ = {"GetS", "GetM", "PutS", "PutM"} # requests H may stall while the line is busy
def run(seed, bug=None, steps=3000, n=3, early_clear=False, seen=None):
rng, seen = random.Random(seed), Counter() if seen is None else seen
c = [{"st": "I", "v": None} for _ in range(n)] # states I S M IS IM SM MI SI II (^D, ^A dropped)
H = {"dir": "U", "sh": set(), "own": None, "mem": 0, "busy": None, "tid": 0}
net, gold, nxt = [], [0], [0] # unordered in-flight set, golden X, next store value
def send(kind, src, dst, **kw): net.append(dict(kind=kind, src=src, dst=dst, **kw))
def give(dst, v): # the grant: Data from H to the requester
send("Data", "H", dst, v=v)
if early_clear: H["busy"] = None # variant: H forgets the grant once it is sent
def store(i): nxt[0] += 1; c[i]["v"] = gold[0] = nxt[0] # unique values: stale is detectable
def load(i): assert c[i]["v"] == gold[0], f"load C{i} got {c[i]['v']}, golden {gold[0]}"
def check(): # after EVERY event
w = [i for i in range(n) if c[i]["st"] == "M"]
r = [i for i in range(n) if c[i]["st"] in ("S", "SM")]
assert len(w) <= 1 and not (w and r), f"SWMR: writers {w}, readers {r}"
for i in w + r: assert c[i]["v"] == gold[0], f"value: C{i} holds {c[i]['v']}, golden {gold[0]}"
def grant(t):
if not t.get("sent") and t["acks"] == 0:
H.update(dir="M", own=t["req"], sh=set()); t["sent"] = True; give(t["req"], H["mem"])
def home(m):
k, s, b = m["kind"], m["src"], H["busy"]
if k == "GetS" and H["dir"] == "M":
H["busy"] = {"req": s, "op": "GetS"}; send("Fwd-GetS", "H", H["own"])
elif k == "GetS":
H.update(dir="S", busy={"req": s}); H["sh"].add(s); give(s, H["mem"])
elif k == "GetM":
H["tid"] += 1; t = H["busy"] = {"req": s, "op": "GetM", "id": H["tid"], "acks": 0}
if H["dir"] == "M": send("Fwd-GetM", "H", H["own"])
else:
for o in H["sh"] - {s}: t["acks"] += 1; send("Inv", "H", o, id=t["id"])
grant(t)
elif k == "Inv-Ack" and b and b.get("id") == m["id"]:
b["acks"] -= 1; grant(b)
elif k == "Data": # newest data from the exclusive holder
assert b and b.get("op"), f"protocol: Data at H, busy {b}"
if b["op"] == "GetS": # a holder answering from its WB entry is no sharer
sh = {b["req"]} | (set() if m["wb"] else {H["own"]})
H.update(mem=m["v"], dir="S", sh=sh, own=None)
else: H["own"] = b["req"]
give(b["req"], m["v"])
elif k in ("PutS", "PutM"):
if H["dir"] == "M" and H["own"] == s:
if bug != "lost-writeback": H["mem"] = m["v"]
H.update(dir="U", own=None)
else: # sharer, or late Put from a non-holder
if k == "PutM": seen["late PutM"] += 1
H["sh"].discard(s)
if H["dir"] == "S" and not H["sh"]: H["dir"] = "U"
send("Put-Ack", "H", s)
else: assert False, f"protocol: {k} at H, busy {b}" # e.g. an Inv-Ack nobody waits for
def to(i, k, table): # protocol checker: message legal in this state?
assert c[i]["st"] in table, f"protocol: {k} at C{i} in {c[i]['st']}"
seen[(k, c[i]["st"])] += 1; c[i]["st"] = table[c[i]["st"]]
def cache(i, m):
x, k = c[i], m["kind"]
if k == "Data":
if not early_clear: H["busy"] = None # course-model assumption: H sees grant delivery
x["v"] = m["v"]; to(i, k, {"IS": "S", "IM": "M", "SM": "M"})
load(i) if x["st"] == "S" else store(i) # the stalled access completes first
elif k == "Inv":
send("Inv-Ack", i, "H", id=m["id"]); to(i, k, {"S": "I", "SM": "IM", "SI": "II"})
elif k in ("Fwd-GetS", "Fwd-GetM"):
send("Data", i, "H", v=x["v"], wb=x["st"] == "MI") # wb: PutM outstanding
to(i, k, {"M": "S", "MI": "SI"} if k == "Fwd-GetS" else {"M": "I", "MI": "II"})
elif k == "Put-Ack": to(i, k, {"MI": "I", "SI": "I", "II": "I"})
def op(i):
x, r = c[i], rng.random()
if x["st"] not in ("I", "S", "M"): return # one outstanding request per cache
if r < 0.5:
if x["st"] == "I": x["st"] = "IS"; send("GetS", i, "H")
else: load(i)
elif r < 0.85:
if x["st"] == "M": store(i)
else: x["st"] = "SM" if x["st"] == "S" else "IM"; send("GetM", i, "H")
elif x["st"] != "I":
send("PutM" if x["st"] == "M" else "PutS", i, "H", v=x["v"]); x["st"] += "I"
try:
for step in range(10 ** 6):
live = [m for m in net if not (m["dst"] == "H" and m["kind"] in REQ and H["busy"])]
if step >= steps and not live: break
if live and (step >= steps or rng.random() < 0.6):
m = live[rng.randrange(len(live))]; net.remove(m) # any ready message: no FIFO
home(m) if m["dst"] == "H" else cache(m["dst"], m)
elif step < steps: op(rng.randrange(n))
check()
assert not net and H["busy"] is None and all(x["st"] in ("I", "S", "M") for x in c), "not quiescent"
holder = [x["v"] for x in c if x["st"] == "M"]
assert (holder[0] if holder else H["mem"]) == gold[0], "end: newest value lost"
except AssertionError as e:
return f"step {step}: {e}"
return None
seen = Counter()
for seed in range(20): assert run(seed, seen=seen if seed < 3 else None) is None, (seed, run(seed))
races = [("Fwd-GetS", "MI"), ("Fwd-GetM", "MI"), ("Inv", "SI"), ("Inv", "SM"), "late PutM"]
assert all(seen[r] > 0 for r in races), seen # seeds 0 to 2 contain every eviction race
caught = run(1, bug="lost-writeback")
assert caught and "golden" in caught, caught
for s in range(5): # variant: busy cleared when H sends the grant
e = run(s, early_clear=True); assert e and "protocol" in e and int(e.split()[1][:-1]) < 150, e
print("PASS: 20 seeded runs of 3000 events keep SWMR and every value, the eviction races occur, a lost writeback is caught")The final assertions test both directions. Twenty seeds of 3,000 events each pass every check: each run delivers on the order of a thousand messages, and the block asserts that seeds 0 to 2 contain every eviction race above: MI^A receiving both forwards, SI^A (after a PutS) and SM^D receiving Inv, and the late PutM from a non-holder that follows each forward to MI^A. The failing case, a home that acknowledges PutM without writing memory, is caught by the value check the next time a reader is served from memory.
A pass means: for these seeds, this protocol kept SWMR and the data-value invariant at every event. It says nothing about traffic the generator never produced. The model also simplifies: one line, one request per cache, no E or O states, data always through H, requests waiting in the network rather than in a modelled queue, and the grant-delivery oracle. A real design without that oracle must handle an Inv or Fwd that overtakes its Data, as Racing Requests at the Home shows; a model of such a design needs those transient states too. How far to go is a judgement about reference model depth.
With repeated values, a load that read an old write can return the same number as the newest write and pass. Unique values make every returned value name exactly one write, so any stale read is detected. Random small values would hide some of the bugs in the next lesson.
H could then start the next transaction for X and send an Inv or Fwd to the requester while its Data is still in flight. With no FIFO order the Inv or Fwd can arrive first, at a cache still waiting in IS^D, IM^D or SM^D, which this model treats as illegal. The block's early_clear variant does exactly this: on seeds 0 to 4 every run fails with such a protocol error within about a hundred events (measured: between 5 and 102), and the block asserts it: the race that Part 4 resolves with a completion message or extra transient states.