Scope: the MP example from the previous lesson, MSI on the course model, with C0 as the reader and C1 as the writer.
Warm-up: both caches read X earlier and hold S / 0, H has S{C0,C1}, memory = 0. C0's older R Y has missed and waits for its own GetS(Y); the transactions for Y are not traced. C0's younger R X hits and performs with 0, and its load-queue entry records X's line.
C1's store to X is an upgrade from S, the same four legs as the upgrade trace (roles reversed from that lesson: C1 upgrades, C0 is the sharer). The only new part is at C0: the Inv matches the load queue, C0 marks R X for replay and sends Inv-Ack straight away. It never delays the Inv-Ack until the replay, because C1's write must complete before C0's R Y can see Y = 1. After R Y performs, the replayed R X misses and becomes the MSI dirty read from the MSI lesson, which is not redrawn here.
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
Warm-up | S / 0 | S / 0 | S{C0,C1} | 0 | C0, C1 and memory: 0 |
L0 R X performs early (load queue: X's line) | S / 0 | S / 0 | S{C0,C1} | 0 | C0, C1 and memory: 0 |
1 GetM(X) at H | S / 0 | SM^D / 0 | S{C0,C1}, pend GetM C1, acks 0/1 | 0 | C0, C1 and memory: 0 |
2 Inv(X) at C0, replay marked | I / - | SM^D / 0 | S{C0,C1}, pend GetM C1, acks 0/1 | 0 | C1 and memory: 0 |
3 Inv-Ack at H | I / - | SM^D / 0 | S{C1}, pend GetM C1, acks 1/1 | 0 | C1 and memory: 0 |
4 Data(M permission, no refill) at C1 | I / - | M / 0 | S{C1}, pend GetM C1, acks 1/1 | 0 | C1 and memory: 0 |
(assumed) H learns C1 delivery | I / - | M / 0 | exclusive(C1) | 0 | C1 and memory: 0 |
L1 C1 stores X=1 | I / - | M / 1 | exclusive(C1) | 0 | C1: 1 |
L2 C0's R Y returns 1 | I / - | M / 1 | exclusive(C1) | 0 | C1: 1 |
5-6 replay GetS(X): MSI dirty read as in the MSI lesson with roles reversed | S / 1 | S / 1 | S{C0,C1} | 1 | C0, C1 and memory: 1 |
L3 replayed R X commits 1 | S / 1 | S / 1 | S{C0,C1} | 1 | C0, C1 and memory: 1 |
The committed pair is (1, 1). Had R Y returned 0 instead, the replay would still have been taken (the decision is made when the Inv arrives) and the result would be (0, 0) or (0, 1), both allowed. The load-queue entry and the cache state are separate records: the line went to I at step 2 whatever the replay decision.
Event | Compared against | Replay? |
|---|---|---|
Inv or Fwd-GetM for a line | Line address of every performed, uncommitted load | Yes, if an older load is still unperformed |
C0's own eviction of a line | Line address | Yes, if an older load is still unperformed: C0 is no longer a sharer and will see no later Inv for it |
Fwd-GetS | Nothing | No: no read permission is removed, so no other core can write yet |
Write to another word in the same line | Line address (the Inv covers the whole line) | Yes, a false replay: correct but wasted work |
The load at the head of the reorder buffer has no older unperformed load, so an invalidation never squashes it. It always commits, and replays cannot livelock that core.
The model below enumerates every interleaving of C1's two stores with C0's flag load, its payload load (early or in order) and at most one eviction of X. It compares the committed outcomes with SC's, with and without the load-queue check.
# MP, roles as in this lesson: C1 writes X=1 then Y=1, C0 reads flag Y then payload X.
# Outcomes are (flag, payload) = (r1, r2). C0 starts with X's line in S / 0.
def sc_outcomes():
found = set()
def walk(w, r, mem, regs):
if w == 2 and r == 2:
found.add(regs)
return
if w < 2:
walk(w + 1, r, mem[:w] + (1,) + mem[w + 1:], regs)
if r < 2:
loc = 1 - r # first Y (index 1), then X (index 0)
walk(w, r + 1, mem, regs[:r] + (mem[loc],) + regs[r + 1:])
walk(0, 0, (0, 0), (0, 0))
return found
def ooo_outcomes(snoop_inv, snoop_evict):
found, seen = set(), set()
todo = [(0, 0, 0, True, None, None, False)] # wpc, X, Y, C0 holds X, flag, payload, evicted
while todo:
s = todo.pop()
if s in seen:
continue
seen.add(s)
wpc, x, y, held, flag, pay, ev = s
def squash(p): # replay rule: older flag load still unperformed
return None if (p is not None and flag is None) else p
if wpc == 2 and flag is not None and pay is not None:
found.add((flag, pay))
continue
if wpc == 0: # C1's GetM(X): Inv reaches C0 only if C0 holds X
todo.append((1, 1, y, False, flag, squash(pay) if (held and snoop_inv) else pay, ev))
if wpc == 1:
todo.append((2, x, 1, held, flag, pay, ev))
if flag is None:
todo.append((wpc, x, y, held, y, pay, ev))
if pay is None: # early (before flag) or in-order payload load
todo.append((wpc, x, y, True, flag, x, ev))
if held and not ev: # C0 evicts X once (PutS, so H drops C0)
todo.append((wpc, x, y, False, flag, squash(pay) if snoop_evict else pay, True))
return found
SC = sc_outcomes()
assert SC == {(0, 0), (0, 1), (1, 1)}
assert ooo_outcomes(snoop_inv=True, snoop_evict=True) == SC
assert (1, 0) in ooo_outcomes(snoop_inv=False, snoop_evict=False)
assert (1, 0) in ooo_outcomes(snoop_inv=True, snoop_evict=False)
print("PASS: snooping Inv and own evictions keeps MP at SC's outcomes, missing either allows (1, 0)")The third assertion is the missing check. The fourth is the eviction hole: C0 performs R X early, evicts X, C1's GetM sends it no Inv, and (1, 0) commits.
No. The check is conservative: it squashes because an older load was still unperformed, not because 0 was proven wrong. If R Y had returned 0, keeping 0 would have been legal, but the replay is still correct.