The coherence domain is the set of caches H may send Inv or Fwd to and must wait for. A cache leaves it with five steps, always in this order: stop new requests, drain the MSHRs, flush, leave (H confirms it will send nothing more), power off. It rejoins in reverse: power on with every line I, enable the snoop port, join, and only then accept core requests.
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. H keeps a domain list next to the directory; a broadcast, a coarse vector or a stale sharer bit can only target members of that list.
Leave from C0 asks H to remove C0 from the domain. H first clears every entry that names C0 only as a clean sharer: a stale bit, an imprecise filter record (compare Filter Eviction and Back-Invalidation), or an S line C0 dropped locally because a bulk Leave follows. An entry that still names C0 as exclusive holder cannot owe data: C0 sends Leave only after every PutM has its Put-Ack, so the line was clean (a silently dropped E line) and memory is current. H clears it. A design that forbids silent E eviction treats such an entry as a protocol error and asserts. For a bulk Leave, H walks its directory, or the sets C0 could map to, clearing C0's bits; that walk is the cost a bulk Leave trades for per-line PutS. H sends Leave-Ack only when no entry names C0 and no Inv or Fwd it sent to C0 is still unanswered. Until Leave-Ack arrives, C0 keeps answering. Leave cannot carry dirty data, so dirty lines must already be written back with PutM.
A real interface does the same job: AMBA CHI (Arm IHI 0050 Issue E.a, Chapter 15 'System Coherency Interface', section 15.2 'Handshake' and Table 15-1) connects an RN-F to the coherence domain with a four-phase SYSCOREQ/SYSCOACK handshake. The node raises SYSCOREQ (Join) and must already be able to service snoops, and it may not issue any transaction that lets it cache a coherent location until the interconnect raises SYSCOACK (Join-Ack). To leave, its caches must hold no coherent data and every such transaction must be complete before it lowers SYSCOREQ (Leave). It keeps servicing snoops until SYSCOACK goes LOW (Leave-Ack), and the interconnect completes all outstanding snoops to the interface and generates no new ones before lowering SYSCOACK.
Step | If done too early | Failure |
|---|---|---|
Gate the core first | Flush runs while the core still misses | New refills arrive behind the flush engine; it never finishes, or finishes with a valid line. |
Drain before flushing | Flush declared done with a GetS outstanding | Data arrives after the flush; H records C0 as a sharer of a line nobody will release. |
Flush before Leave | Leave sent with a dirty line still in M | H stops sending to C0, so a reader gets memory's stale value: a safety failure, not just a hang. |
Leave-Ack before power-off | Power removed when Leave is sent | An Inv or Fwd that H sent before it processed Leave reaches nothing; its requester hangs. |
Snoop port on until Leave-Ack | Snoop logic gated with the core | Same hang as above, even though the supply is still on. |
MSI, X = 0 in memory, no cached copies. C0's load misses and it sends GetS. Before Data returns, the power controller asks C0 to power down. C1 is idle throughout.
Step | C0 state / value | C1 state / value | H directory | Memory | Newest data | H domain list |
|---|---|---|---|---|---|---|
L. Load misses, then power-down request | IS^D / - | I / - | U | 0 | memory: 0 | {C0,C1} |
1. GetS at H | IS^D / - | I / - | U, pend GetS C0 | 0 | memory: 0 | {C0,C1} |
H reads memory | IS^D / - | I / - | U, pend GetS C0 | 0 | memory: 0, Data(0) in flight to C0 | {C0,C1} |
2. Data at C0 | S / 0 | I / - | U, pend GetS C0 | 0 | C0 and memory: 0 | {C0,C1} |
(assumed) grant delivered | S / 0 | I / - | S{C0} | 0 | C0 and memory: 0 | {C0,C1} |
Flush engine sends PutS | SI^A / - | I / - | S{C0} | 0 | memory: 0 | {C0,C1} |
3. PutS at H | SI^A / - | I / - | U | 0 | memory: 0 | {C0,C1} |
4. Put-Ack at C0 | I / - | I / - | U | 0 | memory: 0 | {C0,C1} |
5. Leave at H | I / - | I / - | U | 0 | memory: 0 | {C1} |
6. Leave-Ack at C0 | I / - | I / - | U | 0 | memory: 0 | {C1} |
C0 powers off | off | I / - | U | 0 | memory: 0 | {C1} |
Power on, snoop port enabled | I / - | I / - | U | 0 | memory: 0 | {C1} |
7. Join at H | I / - | I / - | U | 0 | memory: 0 | {C0,C1} |
8. Join-Ack at C0 | I / - | I / - | U | 0 | memory: 0 | {C0,C1} |
The GetS cannot be cancelled once sent: H has accepted it and will deliver Data. Draining means letting it complete, then releasing what it brought. At row 5, H can send Leave-Ack at once because no entry names C0 and nothing it sent to C0 is unanswered.
Power-up leaves the array with retained or random bits, so the valid bits are reset before anything reads them; I means no usable copy whatever the bits say. The snoop port is enabled before Join because the moment H adds C0 to the list, a broadcast or multicast may target it. Core requests wait for Join-Ack because H must accept C0 as a member before it can record C0 as a holder; in a snooping system, C0 must also be observing the bus before its own first request is ordered.
// snippet
// Power-off is legal only after drain, flush and Leave-Ack.
property p_power_off_safe;
@(posedge clk) disable iff (!rst_n)
pwr_off_req |-> (core_gated && mshr_busy == '0 && wb_busy == '0
&& valid_lines == 0 && leave_acked);
endproperty
a_power_off_safe: assert property (p_power_off_safe);
// No core request may leave the cache before the rejoin handshake completes.
a_no_req_before_join: assert property (@(posedge clk) disable iff (!rst_n)
req_valid |-> join_acked);After Leave-Ack, H no longer sends Inv or Fwd to C0. If C0 still held X in M / 1, a GetS from C1 would be served from memory = 0: C1 reads a stale value with no error and no hang. Order matters because Leave changes what H believes.