Formalising CXL Cache Coherence

Chengsong Tan, Alastair F. Donaldson, John Wickerson

We report our experience formally modelling and verifying CXL.cache, the inter-device cache coherence protocol of the Compute Express Link standard. We have used the Isabelle proof…