A stale read has two halves: the symptom (a load got an older value) and the cause (an earlier step that left an old copy usable or made memory answer). What a Violation Looks Like showed that the first illegal step comes before the bad load. On silicon you must find that step from a capture.
Step | Question | Evidence |
|---|---|---|
1 | Which line, which word, what value came back and what was expected? | Failure report, core trace or software check |
2 | Is the older value forbidden, or allowed by the memory model? | Litmus shape and model, see Ordering Bugs |
3 | What are the write epochs: who wrote which value, in H's order? | GetM grants and forwarded Data for the line |
4 | Which agent supplied the stale value: the reader's own copy, memory or another cache? | The Data record that installed the reader's copy, or its absence |
5 | Which rule did that agent's supply break? | Map to a bug class below |
Bug class | Signature in a captured log | Rule broken |
|---|---|---|
Missed Inv | GetM from C0 while C1 is a sharer, then Data with M to C0, and no Inv to C1 in the transaction | Every sharer must be revoked before M is granted |
Grant before Inv-Ack | Inv to C1 sent, Data with M to C0 sent, C1's Inv-Ack arrives afterwards | Acks complete before the grant (Ack Counting and Late Data) |
Memory answered while dirty | Directory exclusive(C0), GetS from C1, Data to C1 with no Fwd-GetS and no Data from C0 | A dirty-responsible holder supplies the data |
Lost writeback | PutM from C0, Put-Ack to C0, no memory write in between, then memory serves a reader | PutM, then the memory write, then Put-Ack |
Late PutM accepted | H records exclusive(C1), then a PutM from C0 arrives and H writes memory with it and clears the entry; memory later serves a reader | A Put from a cache H no longer records as a holder gets Put-Ack with no directory or memory change |
Late Data after Inv | Inv reaches a cache in IS^D, which later keeps the Data as S | IS^D_I uses the Data once (Racing Requests at the Home) |
Warm-up: C0 wrote 1 and C1 read it through the MSI dirty read, so C0 S / 1, C1 S / 1, H S{C0,C1}, memory = 1. C0 then upgrades to write 2. The report: C1 later loaded 1. The capture shows H sent the Inv to C1, then sent C0's grant before the Inv-Ack arrived (an injected bug in this illustrative case).
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
Checkpoint | S / 1 | S / 1 | S{C0,C1} | 1 | C0, C1 and memory: 1 |
1. GetM at H | SM^D / 1 | S / 1 | S{C0,C1}, pend GetM C0, acks 0/1 | 1 | C0, C1 and memory: 1 |
H sends Inv, then Data (BUG) | SM^D / 1 | S / 1 | S{C0,C1}, pend GetM C0, acks 0/1 (BUG: granted early) | 1 | C0, C1 and memory: 1 |
2. Data at C0 | M / 1 | S / 1 | S{C0,C1}, pend GetM C0, acks 0/1 (BUG: granted early) | 1 | C0, C1 and memory: 1, SWMR already fails |
L. C0 store | M / 2 | S / 1 | S{C0,C1}, pend GetM C0, acks 0/1 (BUG: granted early) | 1 | C0: 2 |
L. C1 load returns 1 | M / 2 | S / 1 | S{C0,C1}, pend GetM C0, acks 0/1 (BUG: granted early) | 1 | C0: 2, returned 1 is stale |
3. Inv at C1 | M / 2 | I / - | S{C0,C1}, pend GetM C0, acks 0/1 (BUG: granted early) | 1 | C0: 2 |
4. Inv-Ack at H | M / 2 | I / - | exclusive(C0) | 1 | C0: 2 |
Triage: C1 hit its own copy (no Data record installed a new value for C1 after 0x12), so follow the top branch. An Inv was sent, and the grant was sent before its Inv-Ack: grant before Inv-Ack. The first illegal step is H's send of the grant, two records before the symptom.
The analyser below replays a log against the MSI rules of the course model and reports every broken rule, earliest first. Records are taken at H's port (requests and responses when they arrive, H's own messages when sent), plus L records from the core traces on a common time base. It tracks the value each cache holds, dropping it when that cache's Inv-Ack, forwarded Data for a GetM or acknowledged PutM reaches H, and checks that every load returns a value its cache holds and that this value is the newest written. Puts follow the late-writeback rule: a Put waits behind any open GetS or GetM for X (Rule 2 of A Power-Down Race), so it gets no Put-Ack while a Fwd or Inv H sent to its sender is unanswered; a forward answered from a WB entry (Data marked PutM outstanding) adds no sharer; and a Put from a cache H no longer records as a holder must get Put-Ack with no memory write and no directory change. It simplifies the course protocol in one way: H's record changes when H sends the grant, not when the grant is delivered. It is a teaching tool, not a product checker.
def analyse(log, rules=True):
sharers, excl, mem, newest, copy, pend, put, out = set(), None, 0, 0, {}, None, None, []
for i, (kind, src, dst, val) in enumerate(log):
bad = lambda why: out.append((i, why))
if kind in ("GetS", "GetM"):
pend = {"req": src, "kind": kind, "inv": set(), "owed": set(), "buf": None, "wb": False, "holder": excl}
elif kind == "PutM": # waits in X's entry, never overwrites pend
put = {"req": src, "buf": val}
elif kind in ("Inv", "Fwd-GetS", "Fwd-GetM"):
pend["owed"].add(dst) # dst owes H an answer
if kind == "Inv": pend["inv"].add(dst)
elif kind == "Inv-Ack": # src has invalidated its copy
copy.pop(src, None); sharers.discard(src)
if pend: pend["owed"].discard(src)
elif kind == "Data" and dst == "H": # holder answers a Fwd: 1 or (1, "wb")
wb = isinstance(val, tuple)
pend["buf"], pend["wb"] = (val[0] if wb else val), wb
pend["owed"].discard(src)
if pend["kind"] == "GetM" or wb: copy.pop(src, None)
elif kind == "MemWr":
if pend and pend["buf"] is not None: pass # H writes the forwarded Data
elif rules and put and put["req"] != excl:
bad("memory written by a Put from a non-holder")
mem = val
elif kind == "Put-Ack":
if rules and pend and put["req"] in pend["owed"]:
bad("Put-Ack while a Fwd or Inv to the sender is unanswered")
if put["req"] == excl: # a real writeback
if rules and mem != put["buf"]: bad("Put-Ack before memory holds the written-back value")
excl = None
copy.pop(put["req"], None); put = None # late writeback: no change at H
elif kind == "Data": # H grants (value or None, permission)
v, perm, req, holder = val[0], val[1], dst, pend["holder"]
if rules and holder not in (None, req) and pend["buf"] is None:
bad(f"memory answered while {holder} held the line exclusive")
for s in sorted(sharers - {req}) if rules and perm == "M" else []:
bad(f"M granted to {req} with no Inv sent to {s}" if s not in pend["inv"]
else f"M granted to {req} before Inv-Ack from {s}")
if rules and perm == "S" and holder and mem != pend["buf"]:
bad("S granted before memory was written")
if v is not None: copy[req] = v
if perm == "M": excl, sharers = req, set()
else: # a WB-answered holder is not a sharer
keep = {req} if pend["wb"] else {holder, req}
sharers, excl = (keep if holder else sharers | {req}), None
pend = None
elif kind == "Store":
if rules and excl != src: bad(f"{src} stored without M")
copy[src] = newest = val
elif kind == "Load":
if rules and copy.get(src) != val: bad(f"{src} loaded {val}, not from a copy it held")
if val != newest: bad(f"stale load: {src} read {val}, newest is {newest}")
return out
CLEAN = [("GetM", "C0", "H", None), ("Data", "H", "C0", (0, "M")), ("Store", "C0", None, 1),
("GetS", "C1", "H", None), ("Fwd-GetS", "H", "C0", None), ("Data", "C0", "H", 1),
("MemWr", "H", "H", 1), ("Data", "H", "C1", (1, "S")), ("Load", "C1", None, 1),
("GetM", "C0", "H", None), ("Inv", "H", "C1", None), ("Inv-Ack", "C1", "H", None),
("Data", "H", "C0", (None, "M")), ("Store", "C0", None, 2),
("GetS", "C1", "H", None), ("Fwd-GetS", "H", "C0", None), ("Data", "C0", "H", 2),
("MemWr", "H", "H", 2), ("Data", "H", "C1", (2, "S")), ("Load", "C1", None, 2)]
LATE = CLEAN[:3] + [("GetM", "C1", "H", None), ("Fwd-GetM", "H", "C0", None), ("Data", "C0", "H", 1),
("Data", "H", "C1", (1, "M")), ("Store", "C1", None, 2), ("PutM", "C0", "H", 1), # C0 in MI^A
("Put-Ack", "H", "C0", None), ("Load", "C1", None, 2)] # no change at H
ORDER_B = CLEAN[:3] + [("GetS", "C1", "H", None), ("Fwd-GetS", "H", "C0", None), # C0 in MI^A
("PutM", "C0", "H", 1), # waits: the Fwd to C0 is unanswered
("Data", "C0", "H", (1, "wb")), ("MemWr", "H", "H", 1), ("Data", "H", "C1", (1, "S")),
("Put-Ack", "H", "C0", None), ("Load", "C1", None, 1), # C0 no longer recorded: no change
("GetM", "C1", "H", None), ("Data", "H", "C1", (None, "M")), ("Store", "C1", None, 2)]
EARLY_ACK = ORDER_B[:6] + [("Put-Ack", "H", "C0", None)] # C0 frees its WB entry, Fwd unanswered
grant, store2, stale = ("Data", "H", "C0", (None, "M")), ("Store", "C0", None, 2), ("Load", "C1", None, 1)
BUGS = { # name: (log, index of the injected step, words the finding must contain)
"missed Inv": (CLEAN[:10] + [grant, store2, stale], 10, "no Inv sent to C1"),
"grant before Inv-Ack": (CLEAN[:11] + [grant, store2, stale, CLEAN[11]], 11, "before Inv-Ack"),
"memory answered": (CLEAN[:14] + [CLEAN[14], ("Data", "H", "C1", (1, "S")), stale], 15, "memory answered"),
"lost writeback": (CLEAN[:14] + [("PutM", "C0", "H", 2), ("Put-Ack", "H", "C0", None),
CLEAN[14], ("Data", "H", "C1", (1, "S")), stale], 15, "Put-Ack before memory"),
"late PutM accepted": (LATE[:9] + [("MemWr", "H", "H", 1), LATE[9], ("GetS", "C0", "H", None),
("Data", "H", "C0", (1, "S")), ("Load", "C0", None, 1)], 9, "Put from a non-holder"),
}
for clean in (CLEAN, LATE, ORDER_B):
assert analyse(clean) == [] and analyse(clean, rules=False) == []
for name, (log, at, words) in BUGS.items():
found = analyse(log)
assert found[0][0] == at and words in found[0][1], (name, found)
assert found[-1][1].startswith("stale load") and found[-1][0] > at # symptom comes later
value_only = analyse(log, rules=False) # broken variant
assert value_only and value_only[0][0] != at # it misses the cause
assert analyse(CLEAN[:10] + [grant]) and analyse(CLEAN[:10] + [grant], rules=False) == []
assert analyse(CLEAN[:2] + [("Load", "C1", None, 0)]) # load with no copy
found = analyse(EARLY_ACK) # Put-Ack overtakes the Fwd
assert found[0] == (6, "Put-Ack while a Fwd or Inv to the sender is unanswered")
assert analyse(EARLY_ACK, rules=False) == [] # no load: values see nothing
print("PASS: replay finds each injected step before its stale load, clean logs report nothing")The clean log (cold write, dirty read, upgrade to 2, second dirty read) reports nothing. So does a late writeback (C0's PutM(1) arrives after C1 was granted M, and H sends Put-Ack with no change), and so does order B of Eviction Versus Intervention: C0's PutM arrives while the Fwd-GetS to C0 is unanswered and waits, C0 answers from its WB entry, C1 is granted S{C1}, the Put-Ack changes nothing, and C1's later GetM needs no Inv to C0. Sending that Put-Ack before C0's Data arrives is reported as the first illegal step, although no load is wrong yet: C0 would free its WB entry with the Fwd still to answer. For each of the five injected bugs, the first finding is the injected step and the stale load is reported later. The broken variant checks values only: it reports the stale load, never the cause, and when the log ends before any load it reports nothing at all. That is why a replay must check the protocol's rules and not only the values.
The ack-before-grant order is correct, so H is not at fault. C1 acknowledged without making its copy unusable, or a late Data installed a copy after the Inv. Look at C1's controller: its handling of Inv in S and in IS^D (the IS^D_I case).