声明
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。
国内刊号：43-1258/TP
国际刊号：1007-130X
发布日期:
作者：徐学政, 方健, 梁少杰, 王璐, 黄安文, 隋京高, 李琼
单位：（军事科学院国防科技创新研究院，北京 100071）
关键词：Cache一致性协议,多核处理器,模型检验,形式化验证,
基金：国家自然科学基金（62102439）
Cache一致性协议是多核系统数据一致性的保障，也直接影响内存子系统的性能，一直是微处理器设计和验证的重点。Cache一致性协议的设计和优化通常需借助gem5等软件模拟器快速实现。同时，由于协议设计中存在的错误在仿真测试中具有难触发、难定位和难修复的特点，需借助Murphi等模型检验工具进行形式化验证。然而，基于模拟器的协议设计优化和基于模型检验的协议验证在编程语言和抽象层次上存在巨大差异，设计者需要分别进行模拟器实现和模型检验建模，这不仅增加了时间成本，也为二者的等价性带来了隐患。设计并实现了面向gem5模拟器的Cache一致性协议自动化模型检验方法Rubyphi，通过提取gem5中实现的协议，自动完成基于Murphi的模型检验建模，进而对协议进行形式化验证。实验表明，Rubyphi能够有效地完成gem5中一致性协议的建模和验证，并成功发现了2个gem5现有协议中存在的错误，相关问题和解决方案已得到社区确认。
来源：2025年第7期
《计算机工程与科学》期刊编辑部
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。