计算机工程与科学2025，Vol.47Issue(7)：1141-1151,11.DOI:10.3969/j.issn.1007-130X.2025.07.001
Rubyphi:面向gem5的Cache一致性协议自动化模型检验
Rubyphi:Automated model checking for Cache coherence protocols in gem5
摘要
Abstract
Cache coherence protocols serve as the cornerstone for ensuring data consistency in multi-core systems and directly impact the performance of the memory subsystem,making it a longstanding focal point in microprocessor design and verification.The design and optimization of coherence protocols typically rely on software simulators like gem5 for rapid implementation.Additionally,errors in proto-cols are difficult to trigger,locate,and repair during simulation,necessitating the use of model checking tools such as Murphi for formal verification.However,there is a significant difference in programming languages and levels of abstraction between simulator-based protocol design and optimization and model-checking-based protocol verification.Designers are required to separately implement simulator code and construct model-checking frameworks,which not only increases time cost but also introduces potential discrepancies in equivalence between the two approaches.To address this challenge,this paper designs and implements Rubyphi,an automated model checking method for Cache coherence protocols targeting the gem5 simulator.By extracting and translating the protocol descriptions and implementations from gem5,Rubyphi automatically generates Murphi-based model checking framework to conduct formal veri-fication.Experimental results demonstrate that Rubyphi effectively accomplishes the modeling and veri-fication of coherence protocols in gem5,successfully uncovering two existing bugs in gem5's protocols.The related issues and patches have been confirmed by the community.关键词
Cache一致性协议/多核处理器/模型检验/形式化验证Key words
Cache coherence protocol/multi-core processor/model checking/formal verification分类
信息技术与安全科学引用本文复制引用
徐学政,方健,梁少杰,王璐,黄安文,隋京高,李琼..Rubyphi:面向gem5的Cache一致性协议自动化模型检验[J].计算机工程与科学,2025,47(7):1141-1151,11.基金项目
国家自然科学基金(62102439) （62102439）
