paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Formalising CXL Cache Coherence

形式化 CXL 缓存一致性
ASPLOS Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22025匹配度 2/10 · 论文是 CXL 缓存一致性协议的形式化建模与 Isabelle 证明，属于传统形式化验证与证明工程；虽与形式化验证方向沾边，但未结合 LLM/Agent，也不涉及静态分析、浮点程序分析或贝叶斯程序分析，与用户核心交叉方向距离较远。引用 14 inbox
Chengsong Tan, Alastair F. Donaldson, John Wickerson
定理证明与证明工程并发、并行与内存模型
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：在 Isabelle 中形式化并验证 CXL.cache 缓存一致性协议，发现规范问题并开发证明自动化工具。

本文对 Compute Express Link 的跨设备缓存一致性协议 CXL.cache 进行形式化建模与验证。作者依据英文规范在 Isabelle 证明助手中建立形式模型，过程中发现规范中若干不清晰、歧义或不准确之处并提出修复；几乎所有问题与修复均已被 CXL 联盟确认并暂定采纳，仅一项仍在讨论。为验证模型忠实性，作者对 Snoop-pushes-GO 等关键限制进行场景验证，并机械化证明模型的一致性性质。该证明规模庞大，包含数万条引理，促使作者开发新的证明自动化工具，并开放给其他 Isabelle 用户使用。

问题
如何基于自然语言规范严格形式化 CXL.cache 跨设备缓存一致性协议，并验证其关键性质、检查规范本身的准确性？
方法
在 Isabelle 中建立 CXL.cache 形式模型，进行 Snoop-pushes-GO 等场景验证，机械化证明一致性性质，并开发证明自动化工具应对大规模证明。
评估
以场景验证与全机械化一致性证明评估模型忠实性；建模还发现规范中不清晰、歧义或不准确之处，多数修复获 CXL 联盟确认并暂定采纳。
原文摘要（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.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{abs-2410-15908,
  title = {Formalising CXL Cache Coherence},
  author = {Chengsong Tan and Alastair F. Donaldson and John Wickerson},
  booktitle = {ASPLOS},
  year = {2025},
  doi = {10.1145/3676641.3715999}
}