Because the base protocol's safety and deadlock freedom were argued, and often model-checked, for exactly its states and messages. A new message adds interleavings nobody checked and must fit into a message class without creating a cycle. The examples below are illustrative and generic; they do not describe any product.
Extension (illustrative) | What it does | New risk |
|---|---|---|
Prefetch hint | Ask H to fetch X into an outer cache or memory buffer, no permission granted | Low if it creates no cached copy. Must never be treated as a grant. |
Prefetch-to-shared | A GetS issued early by hardware | Low: reuses GetS and IS^D. Costs bandwidth and sharer-list space. |
Stash or inject | H, or a device through H, pushes data into a cache that did not ask | New unsolicited message, a new receiver state and a race with that cache's own requests and evictions. |
Non-temporal full-line write | Write X to memory without allocating in the writer's cache | H must invalidate every copy and drain any dirty holder before memory is written. A new race with readers. |
Ownership hint (read for ownership) | A load that expects a store asks for exclusive permission | Low if mapped onto GetM. High if a new state means exclusive but not yet usable. |
New stable state (for example a forwarding clean sharer) | Changes who supplies data | Every row of the state table changes. The sourcing rules must be argued again. |
Step | Question | Evidence |
|---|---|---|
1. State table diff | Which (state, event) cells are new or changed, at caches and at H? | The base table with every changed cell marked, including 'cannot occur' cells that now can |
2. Message class placement | Is each new message a request, forward or response? What may its consumer wait on? | The request < forward < response rule: consuming it may wait only on later classes |
3. New transient states | Which waits did the extension add, and what does each do with Inv, Fwd and Data? | A completed table like the one in Part 4 |
4. Value and permission invariants | Can SWMR or the data-value invariant fail in any interleaving? | A model check, not a few directed tests |
5. Progress | Can the new message be refused? What happens then? | A stated fallback with no new cycle |
Step 2 is where many extensions fail. Take an unsolicited stash. The receiver may need a free way, which means evicting a victim, which means sending a PutM (a request) and waiting for Put-Ack. If the stash is a forward that must be accepted, consuming a forward now waits on a request: the class order is broken and the deadlock-freedom argument no longer holds. The usual repair is to make the stash refusable: the receiver may decline it, and H then writes the data to memory.
Course model, MSI, reset state: C0 I / -, C1 I / -, H U, memory = 0. The extension: H may push Stash(X=0, S) to C1, and C1 replies StashAck. In the first design H records C1 as a sharer only when StashAck arrives, and does not mark X busy while the Stash is in flight. C0 has a GetM outstanding.
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
Initial | IM^D / - | I / - | U | 0 | memory: 0 |
H sends Stash | IM^D / - | I / - | U | 0 | memory: 0, Stash(0) in flight to C1 |
1. GetM at H | IM^D / - | I / - | U, pend GetM C0 | 0 | memory: 0, Stash(0) in flight to C1 |
H reads memory | IM^D / - | I / - | U, pend GetM C0 | 0 | memory: 0, Data(0) in flight to C0 |
2. Data at C0 | M / 0 | I / - | U, pend GetM C0 | 0 | C0 and memory: 0 |
(assumed) grant delivered | M / 0 | I / - | exclusive(C0) | 0 | C0 and memory: 0 |
L. Local store | M / 1 | I / - | exclusive(C0) | 0 | C0: 1 |
3. Stash at C1 | M / 1 | S / 0 | exclusive(C0) | 0 | C0: 1. Violation: C1 S / 0 alongside M |
4. StashAck at H | M / 1 | S / 0 | exclusive(C0) | 0 | C0: 1. C1 holds a stale S / 0 that H does not record |
SWMR fails at step 3 and C1 can now read the stale 0. Two fixes keep the extension: treat the stash as a transaction (H marks X pending until StashAck, so the GetM waits), or record C1 when the Stash is sent and give C1 a rule for an Inv that arrives before its Stash, as IS^D_I did for early Inv. The model check below finds the bad interleaving in the first design and proves the busy fix in this small model.
def moves(s, fixed):
c0, c1, busy, d, net, sent = s
out = []
if not sent and not busy and d != "X0": # H decides to stash
out.append((c0, c1, fixed, d, net | {"Stash"}, True))
for m in net:
n = net - {m}
if m == "GetM" and not busy:
if d == "S1":
out.append((c0, c1, True, d, n | {"Inv"}, sent))
else:
out.append((c0, c1, busy, "X0", n | {"DataM"}, sent))
elif m == "Inv":
out.append((c0, "I", busy, d, n | {"InvAck"}, sent))
elif m == "InvAck":
out.append((c0, c1, False, "X0", n | {"DataM"}, sent))
elif m == "DataM":
out.append(("M1", c1, busy, d, n, sent)) # grant, then store 1
elif m == "Stash":
out.append((c0, "S0" if c1 == "I" else c1, busy, d, n | {"StashAck"}, sent))
elif m == "StashAck":
out.append((c0, c1, False, "S1" if d == "U" else d, n, sent))
return out
def explore(fixed):
start = ("IM", "I", False, "U", frozenset({"GetM"}), False)
seen, todo, bad, ends = {start}, [start], 0, []
while todo:
s = todo.pop()
if s[0] == "M1" and s[1] == "S0":
bad += 1
nxt = moves(s, fixed)
if not nxt:
ends.append(s)
for t in nxt:
if t not in seen:
seen.add(t)
todo.append(t)
return bad, ends
bad, _ = explore(fixed=False)
assert bad > 0 # the unrecorded stash is caught
bad, ends = explore(fixed=True)
assert bad == 0 # busy-until-StashAck is safe here
assert ends and all(e[0] == "M1" and e[1] == "I" and not e[4] for e in ends)
print("PASS: unrecorded stash breaks SWMR, busy-until-StashAck fix is safe and completes")The checker explores every delivery order of this two-cache, one-line model and checks the SWMR condition in every reachable state, and completion in every final state. It proves nothing about three caches, two lines or finite buffers. Part 11 (Verification) covers how to grow such a model and keep it honest; the point here is that an extension is not reviewed until a check like this has run on it.
Accepting it may require evicting a victim, which sends a PutM request and waits for Put-Ack. Consuming a forward would then wait on a request-class resource, which breaks request < forward < response. With finite buffers a cycle can form. Making the stash refusable, with H writing memory instead, removes that wait.