Most whiteboard mistakes are bookkeeping, not protocol: a message drawn before the one it depends on, a state changed at H when no message reached H, a value that vanishes while it is in flight. The fix is a fixed routine that produces the same picture as the course traces, in the same order, every time.
Step | Rule | Why |
|---|---|---|
1. Lanes | Always C0, C1, H, memory, left to right. Add C2 only if the question needs a third cache, and say so. | Same layout as every course trace, so you never mirror a message by accident. |
2. Snapshot | Write the protocol, ack collection, ordering assumption and the starting row: each cache state / value, H's entry, memory, newest data. | Every later row is a change from this one. A trace without a start cannot be checked. |
3. Number | Number each message at delivery. A core's own load or store is L, not a number. H reading or writing memory is a note at H, never an arrow to memory. | Course convention for diagrams; numbering at delivery is what makes no-FIFO races drawable. |
4. Table | After each delivery, one row: only the receiver's state changes, and H's entry changes only when a message reached H. | Stops the commonest error: updating H as if it saw a message it has not received. |
5. Serialization | Circle the step where H accepts the request (directory) or the request wins the bus (snooping). | Every race explanation starts from this point. |
6. End check | At most one writable cache (E or M), and none beside a readable copy; in MOESI also at most one M or O. Every readable copy and, if no dirty-responsible holder exists, memory equal the last write. | The two invariants are the definition of correct; see SWMR Precisely and The Data-Value Invariant. |
The full trace and table are in MSI Protocol, section "A remote read ends the write epoch". Do not memorise it: reproduce it with the routine. Start from that lesson's checkpoint: C0 M / 1, C1 I / -, H exclusive(C0), memory = 0, newest data C0: 1. C1 loads X. The skeleton below is what should be on the board when you finish; the step rows are filled from your own drawing, and you compare them with the lesson afterwards.
# not-run: illustrative whiteboard skeleton (fill the empty rows yourself)
MSI, directory at H, acks at H, no FIFO, reliable. C1 loads X.
C0 C1 H memory
| |--- 1 ---->| (SP: H accepts) |
|<------ 2 -------------| |
|------- 3 ------------>| |
| | [H writes memory] |
| |<--- 4 ----| |
step | C0 | C1 | H | memory | newest
start | M / 1 | I / - | exclusive(C0) | 0 | C0: 1
1 | | | | |
2 | | | | |
3 | | | | |
H note | | | | |
4 | | | | |
(assumed) grant delivered
| | | | |
end | S / 1 | S / 1 | S{C0,C1} | 1 | C0, C1, memory: 1Time (illustrative budget) | On the board | Self-check before moving on |
|---|---|---|
0:00 to 0:15 | Four lanes, protocol and assumptions line | Participant order C0, C1, H, memory |
0:15 to 0:30 | Start row of the table | Memory = 0 while C0 holds M / 1: legal, C0 is dirty-responsible |
0:30 to 1:20 | Messages 1 to 4 and the memory note, each followed by its row | Message 2 goes to C0 because H's entry names it; message 3 carries 1; the newest-data cell names Data(1) in flight |
1:20 to 1:35 | Circle step 1 as the serialization point | Any request arriving later for X waits behind this one |
1:35 to 2:00 | End row and the two invariant checks | One reader epoch, no writer; memory = 1 because MSI has no dirty sharer |
The routine is the same for any transaction. For a cold write use Write Miss and Ownership, for an upgrade Upgrade from Shared, for a dirty read with three hops Three-Hop Versus Four-Hop. Only the messages change; the lanes, the table, the serialization mark and the end check do not.
A board can pass SWMR and still be wrong. The commonest broken ending of the dirty read is S / 1, S / 1 with memory = 0: no writer, so SWMR holds, but no cache is dirty-responsible either, so the next reader served from memory gets 0. The check below applies both invariants to stable rows and shows that the permission check alone misses this ending.
def swmr_ok(row):
states = [row["C0"][0], row["C1"][0]]
writers = states.count("M")
readers = states.count("S")
return writers <= 1 and not (writers and readers)
def data_value_ok(row, last_write):
readable = [row[c][1] for c in ("C0", "C1") if row[c][0] in ("S", "M")]
dirty_holder = any(row[c][0] == "M" for c in ("C0", "C1")) # MSI: only M is dirty-responsible
copies_ok = all(v == last_write for v in readable)
memory_ok = dirty_holder or row["memory"] == last_write
return copies_ok and memory_ok
def end_check(row, last_write):
return swmr_ok(row) and data_value_ok(row, last_write)
# Stable rows of the MSI dirty read (from the MSI Protocol lesson)
checkpoint = {"C0": ("M", 1), "C1": ("I", None), "memory": 0}
end = {"C0": ("S", 1), "C1": ("S", 1), "memory": 1}
assert end_check(checkpoint, 1) # memory stale but C0 is dirty-responsible
assert end_check(end, 1) # one read epoch, memory current
# Broken endings a candidate might draw
stale_memory = {"C0": ("S", 1), "C1": ("S", 1), "memory": 0}
two_epochs = {"C0": ("M", 1), "C1": ("S", 0), "memory": 0}
lost_value = {"C0": ("I", None), "C1": ("S", 0), "memory": 0}
assert swmr_ok(stale_memory) and not data_value_ok(stale_memory, 1) # permissions fine, value lost
assert not swmr_ok(two_epochs) # writer beside a reader
assert swmr_ok(lost_value) and not data_value_ok(lost_value, 1) # C1 read the old value
# General claim: over every MSI state pair with values in {0, 1} and memory in {0, 1},
# neither check alone is sufficient: each accepts endings the other rejects.
import itertools
states = [("I", None), ("S", 0), ("S", 1), ("M", 0), ("M", 1)]
only_swmr = only_value = 0
for a, b, mem in itertools.product(states, states, (0, 1)):
row = {"C0": a, "C1": b, "memory": mem}
only_swmr += swmr_ok(row) and not data_value_ok(row, 1)
only_value += data_value_ok(row, 1) and not swmr_ok(row)
assert only_swmr > 0 and only_value > 0
assert data_value_ok({"C0": ("M", 1), "C1": ("S", 1), "memory": 0}, 1) # values agree, two epochs
print("PASS: end check needs SWMR and the data-value invariant, each alone accepts a wrong ending")The enumeration makes the general point: SWMR alone accepts endings with a lost value, and the value check alone accepts M / 1 beside S / 1, where the values agree but a writer coexists with a reader. On the board, say both checks out loud.
Number at delivery, in the order deliveries happen, and only after the message that causes it. C0 cannot send Data before it has received Fwd-GetS, so the forward is 2 and the Data is 3. Numbering at delivery is also what lets you draw no-FIFO races later, where two messages from the same sender arrive in the opposite order.
SWMR passes, the data-value invariant fails: in MSI no cache is dirty-responsible in S, so memory must hold 1. You left out the note "H writes memory, X = 1" between C0's Data reaching H and H's Data to C1.