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

发布时间：2022-07-02 12:49

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

【文章页数】：65 页

【学位级别】：硕士

【文章目录】：
摘要
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 下一步研究展望
致谢
参考文献
作者在学期间取得的学术成果


【参考文献】：
期刊论文
[1]一种基于广播的cache一致性协议的设计和验证[J]. 李俊,袁爱东,高剑刚.  计算机科学与探索. 2008(05)
[2]谓词抽象技术研究?[J]. 屈婉霞,李暾,郭阳,杨晓东.  软件学报. 2008(01)
[3]模型检验中抽象技术研究综述[J]. 屈婉霞,李暾,郭阳,杨晓东.  计算机工程与应用. 2006(33)
[4]CMP中Cache一致性协议的验证[J]. 李崇民,王海,李兆麟.  电子技术应用. 2005(12)
[5]并发和实时系统的模型检验技术[J]. 董威,王戟,齐治昌.  计算机研究与发展. 2001(06)

硕士论文
[1]形式验证技术的应用研究[D]. 朱学仕.哈尔滨工程大学 2004



本文编号：3654392