A proposal usually arrives as one sentence and a performance argument: 'let the dirty holder send Data straight to the requester', or 'drop clean E lines without a PutE'. Your job is not to agree or disagree but to find what the sentence leaves out. Custom Extensions and Their Risks gave a five-step evaluation for a new message. A senior review adds two things that decide most real arguments: how the change will be verified, and whether the performance claim has evidence.
Review step | The question | What a complete answer contains |
|---|---|---|
1. State-table diff | Which (state, event) cells change at each cache and at H? | The base table with changed cells marked, including cells that used to read 'cannot occur' |
2. New transient states | Which new waits exist, and what does each do with Inv, Fwd and Data? | A row per new wait, with every incoming event handled |
3. New races | Which existing message can now arrive in which new state? | A table of (message, state) pairs, each with its handling and the failure without it |
4. Message classes and deadlock | Which class does each new message use, and what may its consumer wait on? | Placement under request < forward < response and the argument that no new cycle exists |
5. Verification impact | Which coverage cells are new, and has a model check been run? | The new cells named, and a small-model check of safety and completion |
6. Performance claim | What is saved, what is added, and how often each happens? | A break-even formula and the measured or modelled rates that go into it |
Step 3 is where reviews find bugs. The method is mechanical: for every state the change creates or makes reachable, list every message of the protocol and ask whether it can arrive there now. A removed message is reviewed the same way, because the cells it used to rule out become reachable.
The proposal (illustrative): in MESI on the course model, a cache evicting a clean E line drops it without sending PutE. The claim: one PutE and one Put-Ack saved per clean exclusive eviction. Clean Eviction: Silent or Notified already showed silent S eviction and noted that E is harder; this review shows why. Start from the checkpoint of a cold read in MESI and the Exclusive State: C0 E / 0, C1 I / -, H exclusive(C0), memory = 0. C0 drops X, then C1 reads.
The course has no message for 'I hold no copy', so the change needs one. This review calls it NoData: a proposed response from a forwarded cache, not one of the course's messages.
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
Checkpoint (assumed) | E / 0 | I / - | exclusive(C0) | 0 | C0 and memory: 0 |
C0 drops X silently | I / - | I / - | exclusive(C0) | 0 | memory: 0 |
1. GetS at H | I / - | IS^D / - | exclusive(C0), pend GetS C1 | 0 | memory: 0 |
2. Fwd-GetS at C0 | I / - | IS^D / - | exclusive(C0), pend GetS C1 | 0 | memory: 0 |
3. NoData at H | I / - | IS^D / - | U, pend GetS C1 | 0 | memory: 0 |
H reads memory | I / - | IS^D / - | U, pend GetS C1 | 0 | memory: 0, Data(0) in flight to C1 |
4. Data at C1 | I / - | E / 0 | U, pend GetS C1 | 0 | C1 and memory: 0 |
(assumed) grant delivered | I / - | E / 0 | exclusive(C1) | 0 | C1 and memory: 0 |
H's entry is unchanged by the drop, because no message reached H. H may answer from memory at step 3 only because the line was E: a dirty line never leaves silently, it always sends PutM. C1 gets E because C0 has confirmed it holds no copy.
Existing message | Can now arrive at | Before the change | Required handling | Without it |
|---|---|---|---|---|
Fwd-GetS, Fwd-GetM | C0 in I | Cannot occur: H recorded C0 only while C0 was E, M, EI^A or MI^A | Reply NoData at once | H waits for ever: a hang |
Fwd-GetS, Fwd-GetM | C0 in IS^D or IM^D (dropped, then asked again; its request is queued at H behind C1's) | Only as an early forward for C0's own pending grant (Racing Requests at the Home: in IM^D, stall until Data) | Reply NoData at once, stay in IS^D or IM^D | Deadlock if C0 stalls it (below) |
GetS or GetM from C0 | H in exclusive(C0) | Cannot occur: C0 hits in E or M, or stalls in EI^A or MI^A until Put-Ack | Treat as 'C0 has no copy', serve from memory | H forwards to the requester itself |
NoData (new) | H with a pending GetS or GetM from another cache | Not in the message set | Read memory, then grant | No defined action |
Inv | C0 in I | Already possible with silent S | Inv-Ack, as Part 3 requires | None new |
The second row is the finding that matters. Part 4 lets a cache in IM^D stall a Fwd-GetM until its own Data arrives, which is safe when the Fwd is for the grant C0 is waiting for. Suppose instead that C0 dropped its E copy, then wanted to store and sent GetM, while C1's GetM reached H first. H still records exclusive(C0), so it sends Fwd-GetM to C0, which is in IM^D. This Fwd is for the copy C0 already dropped, and C0's own GetM is queued at H behind C1's. Stalling it closes a cycle:
C0 cannot tell the two cases apart from the message alone. The change is therefore safe only together with one of: the grant-delivery rule or completion messages (then H never sends an early Fwd, so a Fwd in IS^D or IM^D is always for an old copy and is answered at once), or a grant identity in each Fwd, so the cache can see which copy it refers to.
# | Finding | Severity | Required before approval |
|---|---|---|---|
F1 | A Fwd can reach a cache in I, and the message set has no reply | Blocking | Add NoData as a response, or reject the change |
F2 | A Fwd for a dropped copy can reach IS^D or IM^D and deadlocks under the stall rule | Blocking | Completion messages or grant identities in Fwd, and a rule to answer old-copy forwards at once |
F3 | H's (exclusive(C0), request from C0) cell is undefined | Must fix | Serve from memory, argued from 'dirty data never leaves silently, MI^A stalls new requests' |
F4 | NoData lets H trust memory | Must fix | An assertion that a NoData sender holds no dirty data for X, and no silent M or O eviction anywhere |
F5 | NoData's class | Note | Response class: it sinks into the existing pending entry, and the memory read it triggers is part of that entry. No new cycle once F2 is fixed |
F6 | Verification | Must fix | Ten new coverage cells (six cache cells for the two forwards in I, IS^D and IM^D, two H cells for a request from the recorded holder, two for NoData with GetS or GetM pending), eleven with a sparse directory (NoData answering H's own recall), and a model check |
F7 | Performance claim has no rates | Must fix | Measure the clean E eviction rate and the fraction q of dropped lines requested by another cache before H's record changes, and the fraction r recalled by H first |
F8 | Stale exclusive entries stay in a sparse directory | Note | Count the extra directory evictions they cause |
The model check for F6 needs C0, C1, H and one line, an unordered network, re-requests after a drop, and both forward types. It checks SWMR and the data-value invariant in every reachable state, and that every final state has an empty network and no pending entry. Small Models and Parameters says how far such a model can be trusted, and Race and Cross Coverage how to turn the new cells into coverage.
For F7, per clean E eviction the change saves 2 messages (PutE, Put-Ack). With probability q the line is next requested by another cache while H still names C0, and that request pays 2 extra messages (Fwd, NoData) and 2 extra serial legs before memory is read. Net message saving is 2(1 - q - r) per eviction, where r is the fraction of dropped lines whose stale entry is recalled before any request (the recall pays Fwd and NoData too), and the latency cost lands on a fraction q of those misses. With an illustrative q = 0.3 and r = 0.1 the change saves 1.2 messages per eviction and adds two legs to 30% of the following misses: whether that is a win depends on which resource limits the design, and the proposal must say.
With completion messages H never forwards to a cache before its grant has been delivered, so a Fwd that finds C0 in IS^D must refer to the copy C0 dropped, and NoData is the truth. With early forwards, the same Fwd could be for the grant C0 is about to receive: answering NoData would make H grant C1 from memory while C0's own exclusive grant is still arriving: two exclusive holders, an SWMR violation. C0 needs a grant identity in the Fwd to tell the cases apart.