Formalising CXL cache coherence
File(s)
Published version
OA Location
Author(s)
Tan, Chengsong
Donaldson, Alastair
Wickerson, John
Type
Conference Paper
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 English prose specification. This led to us identifying and proposing fixes to several parts of the specification that were unclear, ambiguous or inaccurate. 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 used the Isabelle proof assistant to produce 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.
Date Issued
2025-03-30
Date Acceptance
2025-01-28
Citation
ASPLOS '25: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2025, 2, pp.437-450
ISBN
9798400710797
Publisher
ACM
Start Page
437
End Page
450
Journal / Book Title
ASPLOS '25: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
Volume
2
Copyright Statement
© 2025 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution International 4.0 License (https://creativecommons.org/licenses/by/4.0/)
Identifier
10.1145/3676641.3715999
Source
30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
Subjects
CCS Concepts: • Computer systems organization → Architectures
Architectures
• Theory of computation → Logic and verification
Logic and verification
CXL, Cache Coherence, Proof Assistant, Heterogeneous Computing, Formal Proof ASPLOS '25, Rotterdam, Netherlands
Publication Status
Published
Start Date
2025-03-30
Finish Date
2025-04-03
Coverage Spatial
Rotterdam Netherlands