Rubyphi: Automated model checking for Cache coherence protocols in gem5.
Saved in:
| Title: | Rubyphi: Automated model checking for Cache coherence protocols in gem5. |
|---|---|
| Authors: | XU, Xuezheng1, FANG, Jian1, LIANG, Shaojie1, WANG, Lu1, HUANG, Anwen1, SUI, Jinggao1 suijinggao@163.com, LI, Qiong1 |
| Source: | Computer Engineering & Science / Jisuanji Gongcheng yu Kexue. Jul2025, Vol. 47 Issue 7, p1141-1151. 11p. |
| Subjects: | Multicore processors, Programming languages, Checks, Designers, Memory, Microprocessors |
| 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 protocols 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 verification. Experimental results demonstrate that Rubyphi effectively accomplishes the modeling and verification 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. [ABSTRACT FROM AUTHOR] |
| Copyright of Computer Engineering & Science / Jisuanji Gongcheng yu Kexue is the property of Computer Engineering & Science and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
Be the first to leave a comment!
