C0 has started its flush and sent PutM for X. Before the PutM reaches H, C1's GetM does, and H, still recording exclusive(C0), sends Fwd-GetM to C0. The two messages cross. This is the forward-first order of Eviction Versus Intervention, with the same roles (C0 evicts, C1 requests), but with Fwd-GetM instead of Fwd-GetS and with the PutM reaching H before C0's Data, a sub-order Part 4 does not draw. The power-down adds one temptation: to treat 'PutM sent' as 'flush done' and remove power.
Course-model extension for this topic: C0's cache can be powered down. A powered-off or retained controller answers nothing, not even 'I do not have it'. The topic adds four course-defined messages, Leave, Leave-Ack, Join and Join-Ack, for leaving and rejoining the coherence domain; they are not messages of any named protocol. Everything else follows the course model.
Rule 1, at C0: a line in MI^A answers Inv and Fwd from its WB entry, and the cache keeps its controller powered until every Put-Ack has arrived. Rule 2, at H: H acknowledges a Put from C0 only when no Inv or Fwd it sent to C0 for that line is unanswered. Without FIFO order a Put-Ack sent early could overtake the Fwd-GetM; rule 2 makes Put-Ack mean 'nothing more is coming for this line'. Rule 2 is not specific to power-down: it is now also course convention 29, and Part 4's Eviction Versus Intervention mentions this order in words. It is what makes the late-writeback rule safe without FIFO order. The held PutM waits in X's pending entry ('queued PutM C0'), not at the head of the request ingress, so other lines are not blocked. The alternative fix on the home side, never forwarding to a cache that has announced its departure, still needs rule 1 for messages sent before the announcement arrived.
H processes first | What happens | Race? |
|---|---|---|
C0's PutM | H writes memory, records U, sends Put-Ack. C1's GetM is served from memory = 1. No forward to C0. | No: the order of Eviction Versus Intervention, writeback first |
C1's GetM | H sends Fwd-GetM to C0 while PutM is in flight. Traced below. | Yes: the messages cross |
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data |
|---|---|---|---|---|---|
0. Warm-up | M / 1 | I / - | exclusive(C0) | 0 | C0: 1 |
Flush evicts X | MI^A / 1 (in WB) | I / - | exclusive(C0) | 0 | C0 WB: 1, PutM(1) in flight to H |
1. GetM at H | MI^A / 1 (in WB) | IM^D / - | exclusive(C0), pend GetM C1 | 0 | C0 WB: 1, PutM(1) in flight to H |
2. Fwd-GetM at C0 | II^A / - (WB entry held) | IM^D / - | exclusive(C0), pend GetM C1 | 0 | Data(1) and PutM(1) in flight to H |
3. PutM at H, held | II^A / - (WB entry held) | IM^D / - | exclusive(C0), pend GetM C1, queued PutM C0 | 0 | H buffer: 1, Data(1) in flight to H |
4. Data at H | II^A / - (WB entry held) | IM^D / - | exclusive(C0), pend GetM C1, queued PutM C0 | 0 | H buffer: 1, Data(1) in flight to C1 |
5. Data at C1 | II^A / - (WB entry held) | M / 1 | exclusive(C0), pend GetM C1, queued PutM C0 | 0 | C1: 1 |
(assumed) grant delivered | II^A / - (WB entry held) | M / 1 | exclusive(C1), queued PutM C0 | 0 | C1: 1 |
H processes the queued PutM: non-holder, no change | II^A / - (WB entry held) | M / 1 | exclusive(C1) | 0 | C1: 1 |
6. Put-Ack at C0 | I / - | M / 1 | exclusive(C1) | 0 | C1: 1 |
Memory stays 0, which is legal: C1 is now the dirty holder, as in Three-Hop Versus Four-Hop. The late PutM must not be written to memory or change the entry: by the course's late-writeback rule, a Put from a cache H no longer records as a holder gets Put-Ack only. H may send the Put-Ack as soon as C0's Data reaches it (row 4), as the model below does; Rule 2 needs only the forward answered. After row 6, C0 continues its power-down: Leave, Leave-Ack, power off.
Broken step | At row 2 | End state |
|---|---|---|
C0 powers off when PutM is sent | Fwd-GetM reaches a powered-off cache and is dropped | H holds PutM waiting for the Fwd answer, C1 waits in IM^D: hang. The 1 survives only in H's held PutM buffer. |
H acks the PutM at once (breaks rule 2) | Put-Ack can overtake the Fwd-GetM, C0 frees its WB entry and powers off | The Fwd-GetM is never answered: hang, even though memory may hold 1. |
C0 powers off before flushing | Not reached | The only 1 is lost with the array: lost data, and the next forward hangs. |
The model below explores every delivery order of C0's power-down against C1's GetM, with no FIFO order. The correct sequence must never lose the value 1 and must always end with C1 holding 1 and C0 off. Each broken sequence must fail in at least one order.
# C0 holds X in M / 1 and powers down while C1 may send GetM(X) at any time.
# Every interleaving is explored, with no FIFO order between any messages.
# c1 is None (idle), "IM^D", or the value it received.
def explore(variant):
def step(s, m): # deliver message m, or None if nobody answers
c0, wb, on, c1, holder, fwd_out, held, mem, msgs = s
msgs = list(msgs); msgs.remove(m); dst, kind, d = m
if dst == "C0":
if kind == "Put-Ack" and not on:
return (c0, wb, on, c1, holder, fwd_out, held, mem, tuple(sorted(msgs, key=str)))
if not on or c0 == "I":
return None # powered off, or a Fwd for a line already gone
if kind == "Fwd-GetM": # answer from the array or the WB entry
msgs.append(("H", "Data", 1 if c0 == "M" else wb))
c0 = "I" if c0 == "M" else "II^A"
else: # Put-Ack frees the WB entry
c0, wb = "I", None
elif dst == "C1":
c1 = d
elif kind == "GetM":
if holder == "C0":
msgs.append(("C0", "Fwd-GetM", None)); fwd_out = True
else:
msgs.append(("C1", "Data", mem)); holder = "C1"
elif kind == "Data": # Fwd answered: grant C1, then release a held Put
msgs.append(("C1", "Data", d)); holder, fwd_out = "C1", False
if held is not None: # C0 is no longer a holder: ack, no change
msgs.append(("C0", "Put-Ack", None)); held = None
elif fwd_out and variant != "ack_while_fwd_unanswered":
held = d # rule 2: PutM and its data wait for the Fwd answer
else:
if holder == "C0":
mem = d
holder = holder if fwd_out else None
msgs.append(("C0", "Put-Ack", None))
return (c0, wb, on, c1, holder, fwd_out, held, mem, tuple(sorted(msgs, key=str)))
def may_power_off(c0, wb):
if variant == "off_before_flush": return True
if variant == "off_after_putm": return c0 != "M"
return c0 == "I" and wb is None # rule 1: flushed and every Put-Ack received
start = ("M", None, True, None, "C0", False, None, 0, ())
seen, todo, errors = set(), [start], set()
while todo:
s = todo.pop()
if s in seen: continue
seen.add(s)
c0, wb, on, c1, holder, fwd_out, held, mem, msgs = s
live = [1 if c0 == "M" and on else None, wb if on else None, c1, mem, held] + [d for *_, d in msgs]
if 1 not in live:
errors.add("lost data"); continue
nxt = []
for m in msgs:
r = step(s, m)
if r is None: errors.add("hang: %s unanswered" % m[1])
else: nxt.append(r)
if on and c0 == "M" and variant != "off_before_flush":
nxt.append(("MI^A", 1, on, c1, holder, fwd_out, held, mem, tuple(sorted(msgs + (("H", "PutM", 1),), key=str))))
if on and may_power_off(c0, wb):
nxt.append(("off", None, False, c1, holder, fwd_out, held, mem, msgs))
if c1 is None:
nxt.append((c0, wb, on, "IM^D", holder, fwd_out, held, mem, tuple(sorted(msgs + (("H", "GetM", None),), key=str))))
if not nxt and not (c1 == 1 and not on):
errors.add("hang: C1 is %s" % c1)
todo.extend(nxt)
return errors, seen
errors, seen = explore("correct")
assert errors == set(), errors
assert any(s[0] == "II^A" for s in seen) # the crossing Fwd-GetM case was explored
assert explore("off_before_flush")[0] == {"lost data"}
for broken in ["off_after_putm", "ack_while_fwd_unanswered"]:
assert "hang: Fwd-GetM unanswered" in explore(broken)[0], broken
print("PASS: the correct sequence never loses 1 or hangs, each broken one fails")The model is one line, one requester and one eviction, with reliable delivery and unbounded buffers. It confirms that the crossing case (C0 in II^A) is reachable and safe under rules 1 and 2, that powering off before the flush loses data, and that powering off on PutM sent, or acknowledging the PutM while the forward is unanswered, leaves a Fwd-GetM that nobody answers.
No. Its data is safe at that point, but the PutM is still outstanding: H will send a Put-Ack to C0, and under rule 2 that acknowledgement is how C0 learns nothing more is coming for X. Powering off at row 2 relies on H never sending C0 another message for X, which C0 cannot know until Put-Ack. Under a Leave-based design the same holds for Leave-Ack.