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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 187879538 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Rubyphi: Automated model checking for Cache coherence protocols in gem5. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22XU%2C+Xuezheng%22">XU, Xuezheng</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22FANG%2C+Jian%22">FANG, Jian</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22LIANG%2C+Shaojie%22">LIANG, Shaojie</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22WANG%2C+Lu%22">WANG, Lu</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22HUANG%2C+Anwen%22">HUANG, Anwen</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22SUI%2C+Jinggao%22">SUI, Jinggao</searchLink><relatesTo>1</relatesTo><i> suijinggao@163.com</i><br /><searchLink fieldCode="AR" term="%22LI%2C+Qiong%22">LI, Qiong</searchLink><relatesTo>1</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Computer+Engineering+%26+Science+%2F+Jisuanji+Gongcheng+yu+Kexue%22">Computer Engineering & Science / Jisuanji Gongcheng yu Kexue</searchLink>. Jul2025, Vol. 47 Issue 7, p1141-1151. 11p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Multicore+processors%22">Multicore processors</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Checks%22">Checks</searchLink><br /><searchLink fieldCode="DE" term="%22Designers%22">Designers</searchLink><br /><searchLink fieldCode="DE" term="%22Memory%22">Memory</searchLink><br /><searchLink fieldCode="DE" term="%22Microprocessors%22">Microprocessors</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=187879538 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.3969/j.issn.1007-130X.2025.07.001 Languages: – Code: chi Text: Chinese PhysicalDescription: Pagination: PageCount: 11 StartPage: 1141 Subjects: – SubjectFull: Multicore processors Type: general – SubjectFull: Programming languages Type: general – SubjectFull: Checks Type: general – SubjectFull: Designers Type: general – SubjectFull: Memory Type: general – SubjectFull: Microprocessors Type: general Titles: – TitleFull: Rubyphi: Automated model checking for Cache coherence protocols in gem5. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: XU, Xuezheng – PersonEntity: Name: NameFull: FANG, Jian – PersonEntity: Name: NameFull: LIANG, Shaojie – PersonEntity: Name: NameFull: WANG, Lu – PersonEntity: Name: NameFull: HUANG, Anwen – PersonEntity: Name: NameFull: SUI, Jinggao – PersonEntity: Name: NameFull: LI, Qiong IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 07 Text: Jul2025 Type: published Y: 2025 Identifiers: – Type: issn-print Value: 1007130X Numbering: – Type: volume Value: 47 – Type: issue Value: 7 Titles: – TitleFull: Computer Engineering & Science / Jisuanji Gongcheng yu Kexue Type: main |
| ResultId | 1 |
