Yes. SWMR is a rule about permissions; the data-value invariant is a rule about bytes. A design can move permissions perfectly and still route the wrong data into a grant. A checker that looks only at state labels, directory entries and legal transitions passes that design. The user of the cache sees only values, so the checker must judge values.
Coherence promises, for each location separately, a single order of all writes to it: its write serialization (also called its modification order). The checker's specification follows directly:
Rule | In the course model | What the checker keeps |
|---|---|---|
Every write to X takes one place in X's write order | A store performs when a cache holding M changes the line; only one cache can be in M, so stores are serialized by the permission hand-off | A per-location list of writes, newest last: the golden memory |
A load returns the newest write in X's order that it is serialized after | A load performs when it reads a usable S or M copy, or when the Data for its miss arrives | Compare the returned value with the golden value at that moment |
At the core port, the architectural model decides | Not needed at the coherence interface; it matters at the core, where a store buffer can forward a core's own store early | Per-location coherence, which every mainstream model keeps: never a write older in X's order than one returned by this core's program-order-earlier load or written by its program-order-earlier store (CoRR, CoWR), never this core's program-order-later store or a newer write (CoRW). Store-buffer forwarding of the core's own unperformed store is allowed. |
The third row is why you must say where the checker observes. Below the store buffer, at the cache's coherence interface, the course protocol gives one order per location and the golden value is exact. At the core, the named memory model decides which other values are allowed; the coherence-versus-consistency lesson and SC, TSO and store buffers show which older observations are legal there. A checker placed at the core but using the strict golden rule reports legal store-buffer forwarding as a bug.
Take the MSI dirty read traced in MSI Protocol: C0 holds M / 1, C1 sends GetS, H forwards Fwd-GetS to C0, C0 returns Data(1), H writes memory, then sends Data with S permission to C1. The messages and step numbers are the same as there. Inject one design bug: to save latency, H starts a speculative memory read when the GetS arrives, and its data-select logic sends that speculative buffer, holding 0, instead of the Data(1) that C0 returned. Nothing else changes.
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
Checkpoint | M / 1 | I / - | exclusive(C0) | 0 | C0: 1 |
1. GetS at H, speculative read starts | M / 1 | IS^D / - | exclusive(C0), pend GetS C1 | 0 | C0: 1 (H's speculative buffer holds stale 0) |
2. Fwd-GetS at C0 | S / 1 | IS^D / - | exclusive(C0), pend GetS C1 | 0 | C0: 1, Data(1) in flight to H |
3. Data at H | S / 1 | IS^D / - | exclusive(C0), pend GetS C1 | 0 | C0 and H buffer: 1 |
H writes memory, BUG selects stale buffer | S / 1 | IS^D / - | S{C0}, pend GetS C1 | 1 | C0 and memory: 1, Data(0) in flight to C1 is stale |
4. Data at C1 | S / 1 | S / 0 | S{C0}, pend GetS C1 | 1 | C0 and memory: 1, C1 holds stale 0 |
(assumed) grant delivered | S / 1 | S / 0 | S{C0,C1} | 1 | C0 and memory: 1, C1 holds stale 0 |
L. C1 load returns 0 | S / 1 | S / 0 | S{C0,C1} | 1 | Golden value 1: value failure |
Look only at the labels: no two caches are writable together, the directory S{C0,C1} matches both tags, and every transition is a legal MSI transition. A state checker passes every row. The only evidence of the bug is the 0 in C1's cell and in the value C1's load returns. A value checker fails at the L row; a white-box check that compares every usable copy with the golden value fails earlier, at step 4.
# The MSI dirty read on the course model (C0 holds M, C1 reads X), with a data-select bug flag.
# Every event logs (event, value, states, values, H record, H holders, pending) after it is applied.
def dirty_read(data_select_bug, c0_store=1, downgrade=True):
st, val = {"C0": "M", "C1": "I"}, {"C0": 0, "C1": None}
H = {"rec": "M", "who": {"C0"}, "mem": 0, "pend": False}
log = []
def ev(kind, value=None):
log.append((kind, value, dict(st), dict(val), H["rec"], set(H["who"]), H["pend"]))
val["C0"] = c0_store; ev("store", c0_store) # C0 stores in M
st["C1"] = "IS"; spec = H["mem"]; H["pend"] = True; ev("1. GetS at H") # speculative read starts
if downgrade: st["C0"] = "S"
data = val["C0"]; ev("2. Fwd-GetS at C0") # C0 returns Data(data) to H
ev("3. Data at H") # H still records exclusive(C0)
H.update(mem=data, rec="S", who={"C0"}); ev("H writes memory") # S claims memory is current
payload = spec if data_select_bug else data # the data-select: the bug picks spec
st["C1"], val["C1"] = "S", payload; ev("4. Data at C1")
H["who"].add("C1"); H["pend"] = False; ev("(assumed) grant delivered")
ev("load", val["C1"]) # L. C1 loads X
return log
def state_checker(log): # SWMR, and H's record matches the tags when nothing is pending
for _, _, st, _, rec, who, pend in log:
w = {c for c, s in st.items() if s == "M"}; r = {c for c, s in st.items() if s == "S"}
if len(w) > 1 or (w and r): return False
if not pend and who != (w if rec == "M" else r): return False
return True
def value_checker(log, golden=0): # golden memory: newest write in X's write order
for kind, value, *_ in log:
if kind == "store": golden = value
if kind == "load" and value != golden: return False
return True
def first_bad_copy(log, golden=0): # white-box: every usable copy equals the golden value
for kind, value, st, val, *_ in log:
if kind == "store": golden = value
if any(st[c] in ("S", "M") and val[c] != golden for c in st): return kind
good, bad = dirty_read(False), dirty_read(True)
assert state_checker(good) and value_checker(good) and first_bad_copy(good) is None
assert state_checker(bad) # computed, not assumed: every state and record is legal
assert not value_checker(bad) # the load of 0 after the write of 1 is caught
assert first_bad_copy(bad) == "4. Data at C1" # the white-box check fires before any load
assert not state_checker(dirty_read(False, downgrade=False)) # the state checker can fail
same = dirty_read(True, c0_store=0) # the store wrote the old value again
assert state_checker(same) and value_checker(same) # bug present but invisible: use unique values
print("PASS: states look legal in the buggy run, only the value checks catch the stale 0")The block simulates the transaction and computes every verdict: the state checker (SWMR, and H's record against the tags whenever nothing is pending) passes the buggy run as a result, and the same checker does fail when C0 is not downgraded, so it is not a constant. The last two assertions carry a second lesson. If C0 had stored 0, the value it already held, the stale buffer would return the right number and the bug would be invisible. Testbenches therefore make every store write a value nobody has written before (a counter, or the writer's id and a sequence number), so that every returned value names exactly one write.
Only (3). C0 and C1 are both S, so (1) passes. H's entry is still pending at step 4 and records S{C0,C1}, matching both tags, in the next row, so (2) passes. C1's copy holds 0 while the newest write in X's order is 1, so (3) fails at step 4, before any load runs.