Cache一致性协议模型检验的抽象研究

论文摘要

随着高性能计算机性能的不断提升、规模不断增大,Cache一致性协议变得异常复杂,协议的状态数随系统规模成指数级增长,导致状态空间爆炸。为了缓解状态空间爆炸问题对Cache一致性协议模型检验的影响,迫切需要研究模型检验优化技术。本文深入剖析了模型检验工具Murphi,介绍了Murphi的语法、模型检验的流程、执行模式和采用的优化技术。通过对简单协议进行验证,分析并总结出模型检验中状态数目与状态分量的值域之间的关系,并归纳出Murphi中状态空间分配规律,找出状态空间爆炸现象出现的原因。抽象是缓解状态空间爆炸问题的重要技术之一,它借助等价关系将原始模型映射到一个简化的抽象模型。抽象模型相对于原始模型大大化简,从而减少了模型检验时需要遍历的状态数目。本文提出了一种基于SMT求解器的谓词抽象技术。首先对高级描述语言Murphi进行BDD建模,将Murphi描述转换成相应的BDD公式；然后结合给定的谓词,将抽象问题转换成可满足性模型理论问题,并利用最新的SMT求解器进行求解；最后利用模型检验工具对抽象模型进行验证。实验表明,基于SMT求解器的谓词抽象能够在保证验证结果正确的同时显著减少对状态空间的需求。文章对谓词抽象的关键算法进行了分析,采用非递归方式实现下一抽象状态的计算,提高了谓词抽象的效率。详细分析了经典的Cache一致性协议,给出了共享读、独占写和数据写回三种处理流程的消息传递规则。对谓词抽象前后的Cache协议进行模型检验,比较了两种方法在验证时间和空间上的差别。实验结果表明基于谓词抽象的模型检验能够减少验证所需的状态空间,满足更大规模系统的验证需求。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景
• 1.1.1 Cache一致性协议是实现多处理机系统的关键
• 1.1.2 Cache一致性协议验证
• 1.2 模型检验
• 1.2.1 模型检验的发展历程
• 1.2.2 模型检验的过程
• 1.2.3 模型检验的优化技术
• 1.3 Cache一致性协议模型检验研究现状及存在的问题
• 1.4 本文主要工作
• 1.5 论文组织结构
• 第二章 显式模型检验中的状态空间分析
• 2.1 显式模型检验工具Murphi
• 2.1.1 Murphi语法组成
• 2.1.2 Murphi模型检验过程
• 2.1.3 Murphi执行模式
• 2.1.4 Murphi压缩技术
• 2.2 Murphi状态空间分析
• 2.2.1 状态空间爆炸分析
• 2.2.2 Murphi的状态空间分配规律
• 2.2.3 各种压缩方法的比较
• 2.3 本章小结
• 第三章 基于SMT求解器的谓词抽象技术
• 3.1 谓词抽象
• 3.1.1 抽象算子和精化算子
• 3.1.2 谓词抽象算法
• 3.1.3 谓词抽象举例
• 3.2 基于SMT求解器的谓词抽象
• 3.2.1 SMT求解器
• 3.2.2 BDD建模
• 3.2.3 基于cvc3的谓词抽象算法
• 3.3 实验结果
• 3.3.1 经典互斥协议简介
• 3.3.2 实验结果
• 3.4 本章小结
• 第四章 抽象算法改进与Cache一致性协议模型检验
• 4.1 关键算法及算法分析
• 4.1.1 计算下一抽象状态的公式与算法
• 4.1.2 基于递归的一种改进实现
• 4.1.3 H函数递归实现算法分析
• 4.2 关键算法的改进
• 4.2.1 递归与非递归的比较
• 4.2.2 H函数的非递归实现
• 4.3 Cache一致性协议建模
• 4.3.1 Cache一致性协议模型
• 4.3.2 Cache一致性协议流程
• 4.4 Cache一致性协议的模型检验分析
• 4.4.1 Cache一致性协议的模型检验测试
• 4.4.2 Cache一致性协议的基于谓词抽象的模型检验测试
• 4.4.3 对比分析
• 4.5 本章小结
• 第五章 结束语
• 5.1 主要工作和创新点
• 5.2 下一步研究展望
• 致谢
• 参考文献
• 作者在学期间取得的学术成果