By giving it one. A checker that has never failed proves little: it may be checking nothing. Injecting known bugs into the model (or, later, into the design) and confirming that each one fails is how a team measures its testbench. Each bug below is a single changed condition, the kind of mistake that survives code review.
Bug | The change | What goes wrong | What the run must contain to expose it |
|---|---|---|---|
a. Early grant | H sends Data with M when one Inv-Ack is still outstanding | The requester can write while a sharer still reads its S copy | A GetM with at least one other sharer, and Data reaching the requester before the last Inv reaches its sharer |
b. No downgrade | A cache in M answers Fwd-GetS with Data but stays M | Two readable copies, one of them writable | A GetS while another cache holds M |
c. Stale memory read | H answers a GetS from memory although a cache holds M | The reader gets an old value while the holder keeps M | A GetS while another cache holds M and has stored since memory was last written |
This is the broken grant of What a Violation Looks Like, with the Inv still in flight. Same roles and start (C0 S / 0 upgrades, C1 S / 0 is the sharer, H S{C0,C1}, memory = 0), but the buggy H does send Inv to C1: it sends it together with the M grant to C0, with acks 0/1 still outstanding. With no FIFO order, either can arrive first. If the grant wins, steps 1 and 2 and the two local accesses are exactly the linked trace: C0 reaches M / 1 while C1 is still S / 0 and its load returns 0. What is new is the end, when the late Inv arrives:
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
3. Inv at C1 | M / 1 | I / - | S{C0,C1}, pend GetM C0, acks 0/1 (BUG: granted early) | 0 | C0: 1 |
4. Inv-Ack at H | M / 1 | I / - | exclusive(C0) | 0 | C0: 1 |
After step 4 every label is legal again, and the directory has no trace of the window in which two caches held usable copies with one of them writable. A state checker that samples only when nothing is pending passes this run; only a per-event SWMR check, or a value check on C1's load, catches it.
If the Inv had arrived first, C1 would be I before C0 became M and nothing observable would go wrong: the same bug, a different interleaving, a clean run. And even in the bad order, the value check fires only if C1 happens to load inside the window between steps 2 and 3. The SWMR check fires at step 2 regardless. Bugs b and c are less picky: they need a common traffic pattern (a read of a line another cache holds in M), and they fail at the next Data delivery.
The block below is a compact, self-contained version of the previous lesson's model (evictions and H's check for unmatched responses removed to keep it short, so that bug a is reported by the check this lesson is about; the rest is the same protocol and checker) with a switch for each bug, a delay knob that holds back chosen message kinds, and a switch that turns the SWMR check off.
import random
def run(seed, bug=None, steps=3000, n=3, slow=(), swmr_check=True):
"""Compact MSI model (no evictions). Returns None if every check passed, else the first failure."""
rng = random.Random(seed)
c = [{"st": "I", "v": None} for _ in range(n)] # I S M IS IM SM
H = {"dir": "U", "sh": set(), "own": None, "mem": 0, "busy": None, "tid": 0}
net, gold, nxt = [], [0], [0]
def send(kind, dst, **kw): net.append(dict(kind=kind, dst=dst, **kw))
def store(i): nxt[0] += 1; c[i]["v"] = gold[0] = nxt[0]
def load(i): assert c[i]["v"] == gold[0], f"value: load at C{i} got {c[i]['v']}, golden {gold[0]}"
def check():
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}"
def grant(t):
if not t.get("sent") and t["acks"] <= (1 if bug == "a" else 0): # bug a: one ack early
H.update(dir="M", own=t["req"], sh=set()); t["sent"] = True
send("Data", t["req"], v=H["mem"])
def home(m):
k, s, b = m["kind"], m.get("src"), H["busy"]
if k == "GetS" and H["dir"] == "M" and bug != "c": # bug c: skips this branch
H["busy"] = {"req": s, "op": "GetS"}; send("Fwd-GetS", H["own"])
elif k == "GetS":
H.update(dir="S", busy={"req": s}); H["sh"].add(s); send("Data", s, v=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["own"])
else:
for o in H["sh"] - {s}: t["acks"] += 1; send("Inv", 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":
if b["op"] == "GetS": H.update(mem=m["v"], dir="S", sh={H["own"], b["req"]}, own=None)
else: H["own"] = b["req"]
send("Data", b["req"], v=m["v"])
def to(i, k, table):
assert c[i]["st"] in table, f"protocol: {k} at C{i} in {c[i]['st']}"
c[i]["st"] = table[c[i]["st"]]
def cache(i, m):
x, k = c[i], m["kind"]
if k == "Data":
H["busy"] = None; x["v"] = m["v"]; to(i, k, {"IS": "S", "IM": "M", "SM": "M"})
load(i) if x["st"] == "S" else store(i)
elif k == "Inv":
send("Inv-Ack", "H", src=i, id=m["id"]); to(i, k, {"S": "I", "SM": "IM"})
else: # Fwd-GetS or Fwd-GetM
send("Data", "H", src=i, v=x["v"])
if not (bug == "b" and k == "Fwd-GetS"): # bug b: stays M
to(i, k, {"M": "S"} if k == "Fwd-GetS" else {"M": "I"})
def op(i):
x, r = c[i], rng.random()
if x["st"] not in ("I", "S", "M"): return
if r < 0.55 and x["st"] != "I": load(i)
elif r < 0.55: x["st"] = "IS"; send("GetS", "H", src=i)
elif x["st"] == "M": store(i)
else: x["st"] = "SM" if x["st"] == "S" else "IM"; send("GetM", "H", src=i)
try:
for step in range(10 ** 6):
live = [m for m in net if not (m["kind"].startswith("Get") and H["busy"])]
live = [m for m in live if m["kind"] not in slow] or live # delay knob
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)
home(m) if m["dst"] == "H" else cache(m["dst"], m)
elif step < steps: op(rng.randrange(n))
if swmr_check: check()
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 str(e)
SEEDS = range(10)
for seed in SEEDS:
assert run(seed) is None and run(seed, slow={"Inv"}) is None
first = {bug: run(seed, bug=bug) for bug in "abc"} # every bug, every seed
assert all(first.values()), (seed, first)
assert first["a"].startswith("SWMR") and first["c"].startswith("value"), (seed, first)
def hits(bug, **kw): return sum(run(s, bug=bug, steps=30, **kw) is not None for s in range(100))
rand_a, slow_a, values_only_a = hits("a"), hits("a", slow={"Inv"}), hits("a", swmr_check=False)
assert rand_a < 60 and slow_a >= 90 and values_only_a < 20, (rand_a, slow_a, values_only_a)
print(f"PASS: correct model passes, bugs a b c all caught, short runs catch a {rand_a}/100 random, {slow_a}/100 with Inv delayed, {values_only_a}/100 with values only")What the measured numbers say (30-event runs, seeds 0 to 99, printed by the block): with random delivery, bug a is caught in 52 runs; with the Inv delay knob, in 99; with only the value and protocol checks, in 9. In full 3,000-event runs every bug is caught on every one of seeds 0 to 9. In those runs, measured and asserted by the block, bug a was always first reported by the SWMR check and bug c by the load-value check; bug b by either, depending on whether the holder stored before the reader's Data arrived.
Technique | What it gives | What it misses |
|---|---|---|
Many random seeds | Combinations nobody thought of; every failure reproduces exactly from its seed | Narrow windows are hit rarely, and coverage of a window is never guaranteed |
Directed races and delay knobs | Forces a known window, such as Data before Inv, in every run | Only the windows someone predicted |
Checks after every event | Catches a violation when it happens, even if no load observes it | Needs white-box state, or a shadow model of it |
Value checks on loads | Black-box: judges what software would see | Only fires if a load lands in the bad window |
Use both kinds of stimulus. Random seeds find the unexpected combinations; directed races and knobs (delay one virtual channel, starve one port, hold one response) push each known window open. Keep every failing seed as a regression test, as Seeds and Regressions describes. Directed race stress is developed further in Directed Race Stress.
H's stale memory read would return 0, which equals the golden value, so no value check fires. The SWMR check still catches the M holder beside the new S copy, but a black-box value checker would miss the bug entirely. Unique store values make a stale read visible.
Three things must line up: a GetM with another sharer, the grant arriving before that sharer's Inv, and a load by the sharer between the two. Without the per-event SWMR check, the bug is visible only when all three happen in the 30 events.