Formalising CXL Cache Coherence

A new industry standard lets a CPU, a GPU and a network card from three different vendors share memory as if they were cores in one machine, which only works if all three implement the same rules — and the rules are written in English, where a sentence containing the word "per" twice turns out to have two readings and neither is correct; this work (Imperial College) rewrote the protocol as mathematics, found five defects the consortium has mostly agreed to fix, and proved one coherence property in a 211,000-line proof.

Why this problem is worth solving

The guarantee being specified is one that every multiprocessor already depends on.

Proving that it holds runs immediately into a technical obstacle.

What people did before, and where it broke

• Write the protocol in prose and let vendors implement it. How essentially every hardware standard works, this one included. Where it broke. Prose admits readings its authors never intended, and nobody notices until two implementations disagree in silicon. The authors found one rule with two plausible readings, neither of which was correct.
• Review the document carefully. The standard has been through consortium review by the engineers who wrote it. Where it broke. Reading does not surface these problems, because a human reader fills gaps unconsciously. Writing a transition rule does surface them, because you cannot write one without deciding exactly when it fires.
• Rely on the specification’s message-sequence diagrams. The standard illustrates its protocol with worked examples showing legal exchanges. Where it broke. Examples show what is allowed and say nothing about what is forbidden, so they cannot establish that a restriction is necessary — or that one is redundant, which the authors also found.
• Verify a specific implementation instead of the standard. The usual target for hardware verification. Where it broke. It tells you whether one vendor’s chip matches their reading of the document. Compatibility across vendors depends on the document being unambiguous, which is a different question.
• Model the interconnect abstractly. Earlier formal work on heterogeneous memory ordering treats the interconnect as a black box. Where it broke. The ambiguities here live precisely in the interconnect’s message ordering rules, so abstracting it away removes the thing worth examining.
• The gap. A standard this widely backed will be implemented many times over by parties who cannot compare notes, and the only artefact they share is a document nobody had attempted to write down precisely — which is exactly the exercise that finds the places where it does not say what it means.

How the standard gets formalised

The idea

You cannot find these defects by reading; you find them by being forced to decide. The example the paper leads with is small enough to hold in your head and completely convincing. The standard says the host may have one snoop pending at a time per cacheline address per device. Read it quickly and it seems clear. Read it as a specification and the word “per” appears twice, so two pending snoops must differ in address and device, or in address or device — and the paper reports that neither is right, because the rule fails to mention that several pending snoops on one cacheline are legal provided they belong to the same transaction. A human reader glides over this, filling the gap with whichever reading seems natural; someone writing a transition rule cannot, because the rule needs a guard and the guard needs a decision. That mechanism produced five findings in total — one outright inconsistency, one redundant rule that repeats an earlier one, one missed efficiency, and two places needing clarification — of which four have been confirmed for the next version of the standard with the fifth still under discussion. Rewriting an informal design as something a machine can check, and treating the discrepancies that surface as the point, is the same exercise as the distributed system model compilation work covered elsewhere on this site.

Verification is used in both directions, which is the unusual part. The obvious use of a formal model is to confirm the protocol does what it promises, and the paper does that — replaying message sequences drawn from the specification’s own diagrams to check the model permits legal exchanges and forbids illegal ones. The less obvious use is checking that the standard is not too strong. Every restriction the document imposes constrains every implementation forever, so a restriction that is not actually needed is a permanent tax on performance across the entire industry. The authors therefore take each constraint in turn, relax it in the model, and confirm that a coherence violation then becomes reachable — establishing that the restriction earns its place. This is where the redundant rule turned up, and it is also the spirit of the one finding still unresolved: a proposed optimisation letting the host tell a device not to bother sending data it already knows is stale, which the consortium is evaluating for backward compatibility and whether the performance gain is real. Writing down precisely what a system is permitted to do and then testing whether the artefact matches is the same discipline as the speculation contract work covered elsewhere on this site.

The proof’s size is not an incidental detail — it is one of the results. The coherence property being proved says that if one device has write access to a location, no other device has read or write access to it. That is not self-sustaining under induction, so it has to be reinforced, and reinforcing it required 796 separate clauses. With 68 transition rules, showing that every rule preserves every clause means 53,332 obligations. The final artefact is 73 files totalling around 211,000 lines, most of it consumed by 68 enormous per-rule lemmas of roughly 2,500 lines each, built over twelve person-months, taking three to five hours to check. And the process was iterative in the worst way: the invariant needed about a dozen revisions, because adding a clause to make one obligation go through required proving that clause preserved by all the rules, which routinely demanded further clauses. That loop is what motivated the third contribution, a tool that runs Isabelle’s automated prover unsupervised across a whole file and writes discovered proofs back in — needed because manual intervention would otherwise be required tens of thousands of times. Confronting how much machinery a genuine hardware correctness proof actually demands is the same reckoning as the register-transfer verification work covered elsewhere on this site.

Finding an ambiguity

A snoop is the message the host sends to ask a device to give up its copy of a cache line, typically because another device wants write access. Bounding how many can be outstanding matters because the protocol deliberately provides very weak ordering guarantees between channels.

Why it works

• A guard cannot be ambiguous the way a sentence can. Prose leaves quantifiers and scopes unresolved while still reading naturally → but a transition rule must state exactly when it fires → so every place the document is unclear becomes a decision the modeller cannot avoid making and therefore cannot avoid noticing.
• Replaying the document’s own examples tests the model, not the document. The specification illustrates legal exchanges with message sequence diagrams → so running those through the model and checking they are permitted and end in the expected state validates the formalisation → which has to come first, since a proof about an unfaithful model would establish nothing.
• Relaxing a restriction tests whether it deserves to exist. Every constraint in a standard binds every implementation permanently → so removing one and checking that a violation becomes reachable confirms it is load-bearing → and a restriction that survives relaxation is a permanent cost imposed for no reason.
• The property must be strengthened before induction can work. Knowing only that no two devices currently conflict does not determine what the next message can do → so the property has to be reinforced with clauses about transient states and in-flight messages until it sustains itself → which is where 796 clauses and essentially all the effort come from.
• Strengthening compounds, so it needs automation. Each added clause must be shown preserved by every one of 68 rules → and each such proof frequently reveals that yet another clause is required → so the obligations reach tens of thousands and a tool that discharges them unsupervised stops being a convenience.

What it costs (trade-offs and scope)

• Only half of coherence is proved. The property established is that a writer excludes other readers and writers. The companion property, that a read returns the most recently written value, is explicitly left as future work — and both are needed together for coherence.
• The model has exactly two devices. Several rules depend on there being only two, such as granting ownership immediately when the other cache is invalid. Extending is described as straightforward for the model and as requiring suitable abstraction and generalisation for the proof, which is the hard half.
• The model has exactly one memory location. Adequate for the property proved, which concerns a single location, but the authors note other properties and liveness would require more.
• Ten message types are omitted. Each omission is individually justified — some do not change cache state, some duplicate others for the purposes of this property, and several would require modelling more of the memory hierarchy — but the model is a subset of the protocol, not the protocol.
• No liveness properties are addressed. Everything proved is a safety property. Nothing here establishes that a request eventually completes.
• Some implementation mechanisms are abstracted. Real hardware tracks state such as whether a device is the last sharer using bit vectors; the model uses a globally accessible counter for transaction identifiers instead, which the standard does not specify.
• The exercise cost twelve person-months. For one property, on a two-device single-location subset of one part of one standard. That is the honest measure of what mechanised proof at this level currently costs.
• Four of five fixes are agreed, not shipped. The consortium has confirmed four will be incorporated into the next version; the fifth, a proposed optimisation, remains under discussion pending backward-compatibility analysis.
• Faithfulness rests on interpretation and consultation. The model was built from the authors’ reading of the specification and refined through discussion with consortium experts, then validated by replaying the document’s examples. That is about as good as available, and it is not a proof that the model matches the document.

The evaluation

Check yourself

Sources

The paper is “Formalising CXL Cache Coherence” by Chengsong Tan, Alastair F. Donaldson and John Wickerson, with the work done at Imperial College London, published at ASPLOS 2025 Volume 2, pages 437-450, DOI 10.1145/3676641.3715999. It is open access under a Creative Commons Attribution licence, and the Isabelle theory files are public.

This explainer is written from the full text, read from the authors’ copy on arXiv (2410.15908) alongside the published version. Everything above comes from the paper’s own sections 2 through 9: the overview of the coherence protocol as an asymmetric scheme routing all inter-device messages through a central host, with separate request, response and data channels in each direction and deliberately weak ordering guarantees; the section 3 model of system state covering device and host caches, their stable and transient states, and the message channels, together with the transition rules and their guards, including the rules capturing the requirement that a snoop cannot overtake a grant of access and that a grant cannot follow a snoop too closely; the section 4 account of five defects found while modelling — the ambiguous rule about pending snoops with its two incorrect readings and the omitted same-transaction case, the redundant restatement of a snoop rule in a different section, the clarification needed about write-pull responses, the proposed efficiency allowing the host to tell a device to discard stale eviction data, and further minor clarifications — with their proposed wording and current status with the consortium; the section 5 scenario verification covering both replay of specification-derived message sequences and the deliberate relaxation of restrictions to confirm violations become reachable; the section 6 proof of the single-writer-multiple-reader property with its 796-clause invariant, 68 rules, 53,332 obligations, 73 theory files, 211,000 lines, twelve person-months and three-to-five-hour check time; the section 7 description of the automation tool built to discharge those obligations unsupervised; and the section 8 statement of assumptions and limitations covering the unproved companion property, the two-device and single-location restrictions, the omitted message types, the absence of liveness reasoning, and the abstraction of hardware tracking mechanisms.