Three things beyond a working protocol. A checker strong enough to fail: values judged after every event, not states at the end. Switches that plant each defect as a single changed condition, so the same code is the correct design when they are off. And a way to replay a chosen interleaving, so that a failure found by a random seed can be reduced to a trace a reviewer can read.
Your task | Detail |
|---|---|
Build | A MESI directory model of one line X on three cores, with H's input buffer, a golden checker and three defect switches (all off) |
Interface | run(seed, defects=(), steps=4000, n=3, hq_size=2, resp_size=None, script=None, drain=False, seen=None, log=None, authority=True) returns (first failure or None, a Counter of messages and memory writes) |
Done when | 20 seeds of 4,000 events and one run of 100,000 events pass, the race counters you need later are all non-zero, no request slots make the progress check fire, and each defect switch fails seeds 0 to 4 |
Write your own version from the rules below before you read the solution: the rules are the specification, the code is one implementation of it.
The model extends the one in A Reference Model in Python. Read that lesson for the event loop and the checker idea; this one lists only what changes and the full rules you need to write it.
What changes from the Part 11 model | Why |
|---|---|
MESI: GetS at U grants E, E to M is silent, PutE and EI^A | The capstone protocol; E holders answer forwards like M holders |
H's input is modelled: a link, a buffer with hq_size request slots, separate response slots | Defect (c) is a buffer-sharing bug; it cannot exist in a model with an unbounded network |
A progress check after every step | Deadlock is a failure the value checker cannot see |
Directory exactness at the end of a run | With notified evictions, a quiescent H must record exactly the caches that hold X |
H records the new holder or sharer when the grant is delivered, not when it is sent | Matches the Part 4 tables |
Authority half of the checker (H's record and memory against the holders) | Catches defect b at the bad step |
defects switches, script replay, drain (traffic) mode | Steps 2 and 3 use the same code |
Message at H | Directory | H does |
|---|---|---|
GetS | U | Grants E with Data from memory; exclusive(requester) is recorded at delivery |
GetS | S{...} | Grants S with Data from memory; the requester is added at delivery |
GetS | exclusive(Cn) | Sends Fwd-GetS to Cn; when Cn's Data arrives, writes memory and only then records S{Cn} (S claims memory is current; no sharer if Cn answered from its WB entry), and grants S; the requester is added at delivery |
GetM | U or S{...} | Sends Inv to every recorded sharer except the requester and counts them; each Inv-Ack removes its sender from the sharers; grants M with Data only when every Inv-Ack is in |
GetM | exclusive(Cn) | Sends Fwd-GetM to Cn; when its Data arrives, grants M; exclusive(requester) is recorded at delivery |
PutS, PutE, PutM | Sender is the recorded exclusive holder | PutM: writes memory. Records U, sends Put-Ack |
PutS, PutE, PutM | Sender is a sharer, or not a recorded holder (late Put) | Removes it from the sharers if present, sends Put-Ack, no memory change |
Message at a cache | Legal states, new state |
|---|---|
Data | IS^D to E or S (as granted, the load completes), IM^D or SM^D to M (the store completes) |
Inv | S to I, SM^D to IM^D (keeps the store intent), SI^A to II^A; sends Inv-Ack |
Fwd-GetS | E or M to S, EI^A or MI^A to SI^A; sends Data to H, marked 'from the WB entry' when in EI^A or MI^A |
Fwd-GetM | E or M to I, EI^A or MI^A to II^A; sends Data to H, marked the same way |
Put-Ack | MI^A, EI^A, SI^A or II^A to I: the WB entry is freed now, not earlier |
In SM^D a load hits on the S copy; a store or eviction waits until the M grant arrives. The model carries memory's value in every M grant, including the permission-only grant of an upgrade (it equals the requester's S copy, so no message is added). H changes its entry for a grant when the grant is delivered, so while Data is in flight the entry shows the old record with the pending request, as in Part 4.
Any other pair is a protocol error and fails the run. H serializes X with one pending entry: while it is busy, new requests, Puts included, stay in the buffer, but responses are always handled. The pending entry clears when its Data grant is delivered (the course-model grant-delivery assumption). A cache that receives its grant performs the stalled access before it handles anything else for X, which is the store-before-Fwd policy of Simultaneous Upgrades.
Check | When | Catches |
|---|---|---|
Every usable copy (S, SM^D, E, M) equals the golden value | After every event | Stale copies, even if no load reads them |
The authority half: H's entry is exclusive(Ci) for every Ci in E or M, and memory equals golden whenever H records U or S | After every event | A directory or memory that has lost track of the newest value, before any load reads it |
SWMR: at most one E or M, and never beside an S or SM^D | After every event | Two writers, or a writer beside a reader |
Every load returns the golden value; stores write unique values | At each load | What software would see |
Message legal in the receiver's state; responses H expects | At each delivery | Protocol errors |
Responses in H's buffer never exceed resp_size (n - 1 by default) | After every event | A sizing assumption of the fix for (c) |
Progress: work pending and no enabled move is a deadlock | Every step | Resource cycles |
Quiescent end, exact directory, newest value in memory or the M copy | After draining | Lost writebacks, stuck transients, directory drift |
In the code, the transient states drop their superscripts: IS, IM and SM are IS^D, IM^D and SM^D; SI, EI, MI and II are SI^A, EI^A, MI^A and II^A. The directory value X means exclusive(own). The three defect switches are off by default; the next lesson explains each. The checker collects every failed check of one event, so a message such as 'value: C1 holds 0, golden 1; SWMR: writers [0], readers [1]' shows that both fired at once.
A script is a list of tuples run in order. (i, "load"), (i, "store") or (i, "evict") makes core Ci perform that access; it is ignored while Ci has a request outstanding, except that a load hits in SM^D. (kind, src, dst), for example ("GetM", 1, "H"), delivers the one enabled message that matches: to a cache, into H's buffer, or, if it is already in the buffer, to H's handler. A message that enters H's buffer is handled at once if H can, unless the tuple ends with "wait", as in ("GetM", 1, "H", "wait"), which leaves it queued. After the script the model drains in seeded random order. Passing log=[] records any run in the same format, every operation as (i, what) and every delivery as (kind, src, dst), with "wait" on each entry into H's buffer, so the log of a failing random seed replays as a script.
import random
from collections import Counter
REQ = ("GetS", "GetM", "PutS", "PutE", "PutM") # request class, everything else sent to H is a response
STABLE = ("I", "S", "E", "M")
def run(seed, defects=(), steps=4000, n=3, hq_size=2, resp_size=None, script=None, drain=False,
seen=None, log=None, authority=True):
"""Three-core MESI directory model of one line X. Returns (first failure or None, traffic counts)."""
rng, seen = random.Random(seed), Counter() if seen is None else seen
resp_size, log = n - 1 if resp_size is None else resp_size, [] if log is None else log
c = [{"st": "I", "v": None} for _ in range(n)] # I S E M, IS IM SM (the ^D states), SI EI MI II (^A)
H = {"dir": "U", "sh": set(), "own": None, "mem": 0, "busy": None, "tid": 0} # dir U, S or X(own)
to_c, link, hq = [], [], [] # to caches (always sink), waiting to enter H, H's input buffer
gold, nxt, cnt, bad = [0], [0], Counter(), []
def send(kind, src, dst, **kw):
cnt["msgs"] += 1
(link if dst == "H" else to_c).append(dict(kind=kind, src=src, dst=dst, **kw))
def room(m): # may m enter H's input buffer now?
if "shared-queue" in defects: return len(hq) < hq_size # defect c: one shared buffer
if m["kind"] in REQ: return sum(x["kind"] in REQ for x in hq) < hq_size
return sum(x["kind"] not in REQ for x in hq) < resp_size # reserved response slots
def enter(m):
link.remove(m); hq.append(m)
if m["kind"] == "GetM" and H["busy"]: seen["GetM queued behind busy"] += 1
if "lost-inv" in defects and m["kind"] == "GetM": H["sh"].discard(m["src"]) # defect a
def store(i): nxt[0] += 1; c[i]["v"] = gold[0] = nxt[0] # unique values: a stale read is visible
def load(i):
if c[i]["v"] != gold[0]: bad.append(f"value: load at C{i} got {c[i]['v']}, golden {gold[0]}")
def check(): # the golden checker, after EVERY event
w = [i for i in range(n) if c[i]["st"] in ("E", "M")]
r = [i for i in range(n) if c[i]["st"] in ("S", "SM")]
err = bad + [f"value: C{i} holds {c[i]['v']}, golden {gold[0]}" for i in w + r if c[i]["v"] != gold[0]]
if authority: # the authority half: H's record and memory
rec = f"exclusive(C{H['own']})" if H["dir"] == "X" else H["dir"]
err += [f"value: dir {rec} with C{i} in {c[i]['st']}" for i in w if rec != f"exclusive(C{i})"]
if H["dir"] in ("U", "S") and H["mem"] != gold[0]:
err.append(f"value: dir {rec}, memory {H['mem']}, golden {gold[0]}")
if len(w) > 1 or (w and r): err.append(f"SWMR: writers {w}, readers {r}")
if sum(x["kind"] not in REQ for x in hq) > resp_size: err.append("response slots exceeded")
assert not err, "; ".join(err)
def grant(dst, perm, v): send("Data", "H", dst, v=v, perm=perm) # recorded when delivered
def done(t):
if not t.get("sent") and t["acks"] == 0: t["sent"] = True; grant(t["req"], "M", H["mem"])
def home(m): # H handles one message from its input buffer
hq.remove(m); k, s, b = m["kind"], m["src"], H["busy"]
if k == "GetS":
H["busy"] = {"req": s, "op": k}
if H["dir"] == "X": send("Fwd-GetS", "H", H["own"])
else: grant(s, "E" if H["dir"] == "U" else "S", H["mem"])
elif k == "GetM":
assert not (H["dir"] == "X" and H["own"] == s), f"protocol: GetM from holder C{s}"
H["tid"] += 1; t = H["busy"] = {"req": s, "op": k, "id": H["tid"], "acks": 0}
if H["dir"] == "X": send("Fwd-GetM", "H", H["own"])
else:
for o in sorted(H["sh"] - {s}): t["acks"] += 1; send("Inv", "H", o, id=t["id"])
done(t) # grants only when every Inv-Ack is in
elif k == "Inv-Ack":
assert b and b.get("id") == m["id"], f"protocol: unexpected Inv-Ack from C{s}"
H["sh"].discard(s); b["acks"] -= 1; done(b)
elif k == "Data": # newest data from the exclusive holder, after a Fwd
assert b and b.get("op") in ("GetS", "GetM"), f"protocol: unexpected Data from C{s}"
if b["op"] == "GetS": # MESI: a forwarded read also writes memory
H["mem"] = m["v"]; cnt["memwr"] += 1
H.update(dir="S", sh=set() if m["wb"] else {H["own"]}, own=None)
grant(b["req"], "S" if b["op"] == "GetS" else "M", m["v"])
else: # PutS, PutE, PutM
holder = H["dir"] == "X" and H["own"] == s
if holder or ("late-put" in defects and k == "PutM" and H["dir"] == "X"): # defect b
if k == "PutM": H["mem"] = m["v"]; cnt["memwr"] += 1
H.update(dir="U", own=None)
else: # a sharer, or a late Put from a non-holder
if k != "PutS": seen["late " + k] += 1
H["sh"].discard(s)
if H["dir"] == "S" and not H["sh"]: H["dir"] = "U"
send("Put-Ack", "H", s)
def move(i, k, table): # protocol checker: is k 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(m):
to_c.remove(m); i, k, x = m["dst"], m["kind"], c[m["dst"]]
if k == "Data": # course-model assumption: H sees grant delivery,
H["busy"] = None # and records the new holder or sharer then
if m["perm"] == "S": H["dir"] = "S"; H["sh"].add(i)
else: H.update(dir="X", own=i, sh=set())
x["v"] = m["v"]; move(i, k, {"IS": m["perm"], "IM": "M", "SM": "M"})
store(i) if x["st"] == "M" else load(i) # the stalled access completes first
elif k == "Inv":
send("Inv-Ack", i, "H", id=m["id"]); move(i, k, {"S": "I", "SM": "IM", "SI": "II"})
elif k in ("Fwd-GetS", "Fwd-GetM"): # answered from the array or from the WB entry
send("Data", i, "H", v=x["v"], wb=x["st"] in ("MI", "EI"))
move(i, k, {"E": "S", "M": "S", "EI": "SI", "MI": "SI"} if k == "Fwd-GetS"
else {"E": "I", "M": "I", "EI": "II", "MI": "II"})
else: move(i, k, {"MI": "I", "EI": "I", "SI": "I", "II": "I"}) # Put-Ack frees the WB entry
if x["st"] in ("I", "IM", "II"): x["v"] = None
def op(i, what=None):
x = c[i]
if x["st"] not in STABLE + ("SM",): return # one outstanding request per cache
if what is None:
r = rng.random(); what = "load" if r < 0.45 else "store" if r < 0.8 else "evict"
log.append((i, what))
if x["st"] == "SM": # SM^D: loads hit, stores and evictions wait
if what == "load": load(i); seen["load hit in SM^D"] += 1
elif what == "load":
if x["st"] == "I": x["st"] = "IS"; send("GetS", i, "H")
else: load(i)
elif what == "store":
if x["st"] in ("E", "M"): x["st"] = "M"; store(i) # E to M is silent
else: x["st"] = "SM" if x["st"] == "S" else "IM"; send("GetM", i, "H")
elif x["st"] != "I": # notified eviction: the WB entry keeps the value
send({"S": "PutS", "E": "PutE", "M": "PutM"}[x["st"]], i, "H", v=x["v"]); x["st"] += "I"
def moves():
return ([("c", m) for m in to_c] + [("in", m) for m in link if room(m)]
+ [("h", m) for m in hq if m["kind"] not in REQ or not H["busy"]])
def do(mv): # one delivery, logged in script form
m = mv[1]; log.append((m["kind"], m["src"], m["dst"]) + (("wait",) if mv[0] == "in" else ()))
{"c": cache, "in": enter, "h": home}[mv[0]](m)
step = None
try:
for e in script or (): # directed run: core ops and chosen deliveries
if isinstance(e[0], int): op(*e)
else: # (kind, src, dst[, "wait"]): deliver that message
mv = [x for x in moves() if (x[1]["kind"], x[1]["src"], x[1]["dst"]) == e[:3]]
assert mv, f"script: {e} not enabled"
do(mv[0]); check()
if mv[0][0] == "in" and e[3:] != ("wait",): # and let H handle it, if it can
mv = [x for x in moves() if x[0] == "h" and x[1] is mv[0][1]]
if mv: do(mv[0])
while drain and moves(): do(moves()[0]); check() # traffic mode: nothing overlaps
check()
if script is not None: steps = 0 # after a script: just drain, in seeded order
for step in range(10 ** 6):
mv, pending = moves(), to_c or link or hq
if pending and not mv: # the progress check
raise AssertionError(f"deadlock: no enabled move, H busy {bool(H['busy'])}, "
f"buffer {[x['kind'] for x in hq]}, waiting {[x['kind'] for x in link]}")
for w in {"request" if m["kind"] in REQ else "response" for m in link if not room(m)}:
seen[w + " waits for buffer space"] += 1
if step >= steps and not pending: break
if mv and (step >= steps or rng.random() < 0.6): do(mv[rng.randrange(len(mv))])
elif step < steps: op(rng.randrange(n))
check()
assert H["busy"] is None and all(x["st"] in STABLE for x in c), "end: not quiescent"
holders = {i for i in range(n) if c[i]["st"] != "I"}
recorded = H["sh"] if H["dir"] == "S" else {H["own"]} if H["dir"] == "X" else set()
assert holders == recorded, f"end: directory records {recorded}, caches hold {holders}"
dirty = [x["v"] for x in c if x["st"] == "M"]
assert (dirty[0] if dirty else H["mem"]) == gold[0], "end: newest value lost"
except AssertionError as e:
return (str(e) if step is None else f"step {step}: {e}"), cnt
return None, cnt
seen = Counter()
for seed in range(20): # twenty seeded runs of 4,000 events
fail, _ = run(seed, seen=seen)
assert fail is None, (seed, fail)
fail, long_run = run(2026, steps=100_000) # one long run
assert fail is None and long_run["msgs"] > 30_000, (fail, long_run)
races = [("Inv", "SM"), ("Inv", "SI"), ("Fwd-GetS", "MI"), ("Fwd-GetM", "MI"), ("Fwd-GetS", "EI"),
("Fwd-GetS", "E"), "late PutM", "late PutE", "GetM queued behind busy",
"request waits for buffer space", "load hit in SM^D"]
assert all(seen[r] > 0 for r in races), [r for r in races if not seen[r]]
assert run(0, hq_size=0)[0].startswith("step 1: deadlock") # failing case: the progress check fires
for d in ("lost-inv", "late-put", "shared-queue"): # each defect switch makes runs fail
assert all(run(s, defects=(d,))[0] for s in range(5)), d
print(f"PASS: 20 seeds x 4000 events and one 100000-event run ({long_run['msgs']} messages) keep every check, the races occur, every switch fails")The block asserts three things. The correct model passes twenty seeds of 4,000 events and one run of 100,000 events (38,554 messages). The passing runs contain the races the defects will need: an Inv reaching SM^D and SI^A, forwards reaching MI^A, EI^A and E, late PutM and PutE from non-holders, a GetM waiting behind a busy line, a request waiting for buffer space, and loads hitting in SM^D. And the checks can fail: with no request slots the progress check fires at once, and each defect switch fails seeds 0 to 4. A pass is only evidence for the traffic it generated, which is why the race counts are asserted rather than assumed.
One line, one outstanding request per cache, caches that always accept H's messages (a real cache must reserve space for forwarded requests too), the grant-delivery assumption instead of a completion message, and no timing. Each is a stated simplification of the course model; the memo in step 4 lists them as risks.
With notified evictions every cache that drops X sends a Put and H removes it, so at quiescence H's record equals reality. With silent eviction of S or E, H may still list a cache that has dropped the line; the record is then a superset, and the check would have to allow extra sharers.
A cache in IS^D cannot tell whether other caches hold X; only H knows whether the directory was U (grant E) or S (grant S). If the cache guessed E, it could later write silently beside other readers, an SWMR violation.