Formalising CXL Cache Coherence

TL;DR

This paper presents a formal model of the CXL.cache protocol using Isabelle, identifies ambiguities, proposes fixes, and develops new proof automation tools to verify coherence properties, influencing standard adoption.

Contribution

The authors formally model CXL.cache in Isabelle, identify ambiguities, propose fixes, and create proof automation tools, advancing protocol verification methods.

Findings

Identified and fixed ambiguities in CXL.cache specification

Proposed fixes accepted by the CXL consortium

Developed new proof automation tools for large proofs

Abstract

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 assistant to create a formal model for CXL.cache based on the prose English specification. This led to us identifying and proposing fixes to several problems we identified as unclear, ambiguous or inaccurate, some of which could lead to incoherence if left unfixed. Nearly all our issues and proposed fixes have been confirmed and tentatively accepted by the CXL consortium for adoption, save for one which is still under discussion. To validate the faithfulness of our model we performed scenario verification of essential restrictions such as "Snoop-pushes-GO", and produced a fully mechanised proof of a coherence property of the model. The considerable size of this proof, comprising tens of thousands of lemmas, prompted us to develop new proof automation tools, which we have made available for other Isabelle users working with similarly cumbersome proofs.