A checklist is useful only if each item names the evidence that closes it. 'Deadlock: considered' closes nothing; 'progress: class graph acyclic under assumptions A1 to A6, model check of the request queue with depth 1' does. Use the table below for any coherence block review: a new protocol, a change, or a controller handed over to a new team. The right-hand column says where this course teaches the item.
Area | Question to ask | Evidence that answers it | Taught in |
|---|---|---|---|
Invariants | Which safety properties hold at every moment, stated per line? | SWMR and the data-value invariant written down, and checked by an assertion or a reference model | |
Serialization point | Where are conflicting requests for one line ordered, and what does a completion mean? | The ordering point named for every path, including DMA and evictions | |
Data sourcing | In every directory state, who supplies Data, and when may memory answer? | A table of state to source, with the stale-memory states marked | |
Evictions and late writebacks | What happens when a Put races a Fwd or Inv, or reaches H from a cache it no longer records? | Handling for MI^A, EI^A, SI^A and II^A, and the late-writeback rule | |
Transient states | For every transient state, what happens to every incoming message? | A complete (state, event) table with no blank cells | |
Progress assumptions | Which fairness, delivery and buffering assumptions does the deadlock-freedom argument use? | A numbered assumption list and the class order each message obeys | |
Resources and credits | What does each request reserve before it is accepted, and what happens when none is free? | Sizing per resource, and backpressure, queue or NACK rules with a fairness argument | |
Power and reset | How does a cache leave and rejoin the coherence domain, and what is the directory at reset? | Flush-then-leave sequence, the directory state that records the departure, and reset values that agree | |
RAS | What happens on an ECC error in a tag, data or directory entry? | Detection per structure, poison rules, and the recovery limit for lost directory state | |
Verification evidence | Which checks would catch a stale value, and what coverage proves the races were hit? | Value checking, assertions, race coverage and a closure report | |
Observability | If this hangs in silicon, what can be read out? | Pending-entry dump, trace points and counters listed per controller |
Apply the list to the protocol this course has used since Part 2: MSI on two cores (MESI where E is the subject), H with a full directory, data through H, Inv-Acks collected at H, notified evictions. The point is to see what 'evidence' looks like for each line, not to re-teach it.
Area | The baseline's answer | Evidence in the course |
|---|---|---|
Invariants | SWMR, data-value invariant | Reference model and its injected bugs, SWMR assertion |
Serialization point | H, per line; a transaction ends when its grant is delivered | Course-model grant-delivery rule; completion messages in Part 4 |
Data sourcing | Memory if U or S; the exclusive holder by forward otherwise | Who May Supply Data; When Memory Is Stale |
Evictions | PutS, PutE, PutM each wait for Put-Ack; a Put from a non-holder gets Put-Ack with no change | Eviction Versus Intervention |
Transient states | IS^D, IM^D, SM^D, MI^A, EI^A, SI^A, II^A, each with a defined reaction | Part 4 race tables |
Progress | Responses always sink; request < forward < response | Part 5 class lessons with their assumption list |
Resources | Pending entry reserved before acceptance, a queue per line at H | MSHRs and Pending Entries |
Power, RAS, observability | Taught as extensions, not part of the minimal model | Parts 10 and 12 |
Verification | Value checks, not state checks | Check Values, Not States |
One row covers three areas 'taught as extensions'. In a real review that is an open item, not a pass: a reviewer records it as a finding with an owner, exactly as a missing (state, event) cell would be. A change such as the silent E eviction of the previous lesson reopens four rows at once (data sourcing, evictions, transient states, verification), which is a quick way to judge how big a change really is.
Send the checklist with the proposal, and ask the author to fill the evidence column before the meeting. Gaps then show up as blank cells, not as a debate.
Grade each row: evidence exists and was reviewed, evidence exists but was not reviewed, or no evidence. Only the first closes a row.
Record each open row as a finding with an owner and the evidence that will close it, as in the findings table of the previous lesson.
Re-run the list on every change to a closed design: a change is reviewed against the rows it touches, and the rest stay closed only if the change cannot reach them.
ECC detects and corrects some errors; the row also asks what happens on an uncorrectable directory error. If the entry is lost, H no longer knows who may hold dirty data, so the design needs a defined response (poison, a recovery broadcast, or a declared machine-check limit) and evidence that it was tested. Detection alone does not close the row.