Rule: whenever H chooses which caches to send Inv or Fwd to for X, every cache that may hold X must be among them. That includes a cache whose fill H has admitted but not yet delivered, and the cache holding the dirty copy. A change of representation (pointers to overflow, pointers to group bits, entry eviction) must keep this true at every step of the change, not only before and after it.
This is the inclusive-filter invariant of Snoop Filter Correctness, applied here to pointer overflow and its two classic bugs.
The program models one K-pointer Dir_i B entry, as in Limited Pointers and Coarse Vectors, over random GetS, Put and GetM events with a fixed seed. After every event it asserts that the caches really holding X are a subset of the candidates the entry implies: the pointers, or all caches when overflow is set. Two injected bugs must each break that: truncating to K ids without setting overflow, and clearing overflow on a PutS. It also replays the four-core case and checks that C3's GetM invalidates C0, C1 and C2, with C2's ack the wasted one.
# Simplified: one entry, each event completes atomically (no transients or
# in-flight fills), H updates the entry at once, Inv-Acks are not modelled.
import random
def candidates(e, n):
if e["state"] == "U":
return set()
if e["state"] == "S" and e["ovf"]:
return set(range(n)) # Dir_i B: overflow means every cache may hold X
return set(e["ptr"])
def add_sharer(e, c, k, bug):
if c in e["ptr"] or e["ovf"]:
return
if len(e["ptr"]) < k:
e["ptr"].add(c)
elif bug != "truncate":
e["ovf"] = True # keep the K pointers, mark the set incomplete
def step(e, holders, op, c, n, k, bug):
if op == "GetS" and c not in holders:
if e["state"] == "U":
e.update(state="exclusive", ptr={c}, ovf=False) # MESI: sole reader gets E
else:
e["state"] = "S" # a previous exclusive holder is downgraded to S
add_sharer(e, c, k, bug)
holders.add(c)
elif op == "GetM":
inv = candidates(e, n) - {c}
wasted = inv - holders # Inv-Acks sent from I
holders -= inv
holders.add(c)
e.update(state="exclusive", ptr={c}, ovf=False) # cleared only here
return inv, wasted
elif op == "Put" and c in holders: # PutS, or PutE/PutM from the exclusive holder
holders.discard(c)
if e["state"] == "exclusive":
e.update(state="U", ptr=set(), ovf=False)
elif e["ovf"] and bug == "clear_on_puts":
e["ovf"] = False
e["ptr"].discard(c)
elif not e["ovf"]:
e["ptr"].discard(c)
if not e["ptr"]:
e.update(state="U")
return None
def run(n, k, bug=None, seed=7, steps=3000):
rng = random.Random(seed)
e, holders = {"state": "U", "ptr": set(), "ovf": False}, set()
for _ in range(steps):
step(e, holders, rng.choice(["GetS", "GetS", "Put", "GetM"]), rng.randrange(n), n, k, bug)
if not holders <= candidates(e, n):
return False
return True
for n in (4, 8):
for k in (1, 2):
assert run(n, k)
assert not run(n, k, bug="truncate")
assert not run(n, k, bug="clear_on_puts")
# The lesson's 4-core, K = 1 case: C0 and C1 read, then C3 writes.
e, holders = {"state": "U", "ptr": set(), "ovf": False}, set()
for op, c in (("GetS", 0), ("GetS", 1)):
step(e, holders, op, c, 4, 1, None)
assert e["ptr"] == {0} and e["ovf"]
inv, wasted = step(e, holders, "GetM", 3, 4, 1, None)
assert inv == {0, 1, 2} and wasted == {2} and holders == {3}
print("PASS: Dir_i B covers every holder, truncation and PutS clearing both fail")Transition under review | Required evidence |
|---|---|
Grant a new fill | The reader is in H's entry (pointer, overflow or group bit) before Data leaves H. |
Enter pointer overflow | The overflow bit is set before the read that did not fit is granted. |
Clear overflow | Only after a GetM's Inv to every other cache has collected every Inv-Ack. |
Clear a group bit | No cache in that group may still hold X or have an admitted fill. |
Reuse an evicted entry | Every listed sharer has acked its Inv, or the exclusive holder's Data has reached memory. |
Accept the dirty copy | The Data reaches memory or the new holder before H's entry for the old holder is dropped. |
The program checks only candidate coverage. It does not check response matching, data movement or eventual service; those remain with ack and data tracking and the controller resources. A pointer format with good storage arithmetic can still have a broken transition.
No. It proves every cache that may hold X is reached. The Data must still come from the cache holding the dirty copy, or from memory when it is current, and must match the request it answers.