基于线程迁移系统的并发布尔程序验证

发布时间：2021-09-28 04:29

　　随着多核处理器和并发技术的快速发展,并发多线程程序设计成为了软件开发的主流模式,并发系统被逐渐应用于多个领域,为人们的生活提供了诸多便利。然而,并发系统的结构一般比较复杂,且存在多个线程相互交错执行的情况,传统的模拟和测试方法难以发现系统中的微小错误。通常采用模型检测验证并发系统的正确性,但并发系统的状态空间随着并发量的增加呈指数级增长,严重制约了模型检测的验证效率。谓词抽象技术能够有效地缓解状态空间爆炸问题,对源程序实施谓词抽象可以产生布尔程序,布尔程序作为程序验证的简单模型,在一定程度上优化了状态空间,提高了模型检测的验证效率。本文以无界线程的并发布尔程序为研究对象,分析程序中违背断言的状态是否可达,具体工作内容如下:（1）研究了后向搜索算法的基本流程,分析了算法的搜索策略和最小覆盖前驱的计算方法,并结合并发布尔程序的特点,提出一种深度优先的后向搜索算法,对最小覆盖前驱的计算方法进行优化,提高了并发布尔程序可达性分析的效率。（2）研究了并发布尔程序的线程迁移系统,在改进的算法基础上,结合计数器抽象技术和summarization方法,提出了一种基于线程迁移系统的可达性分析模型。采用... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：75 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
符号对照表
缩略语对照表
第一章 绪论
    1.1 研究背景及意义
    1.2 国内外研究现状
    1.3 研究内容及论文章节安排
        1.3.1 主要研究内容
        1.3.2 章节安排
第二章 相关基础理论
    2.1 模型检测
    2.2 抽象技术
        2.2.1 谓词抽象技术
        2.2.2 其他抽象技术
        2.2.3 基于抽象的模型检测工具
    2.3 布尔程序
        2.3.1 顺序布尔程序
        2.3.2 并发布尔程序
        2.3.3 并发布尔程序的迁移系统
    2.4 良拟序迁移系统
        2.4.1 拟序
        2.4.2 良拟序迁移系统
    2.5 可满足性问题(SAT)
    2.6 本章小结
第三章 基于后向搜索算法的并发布尔程序可达性分析
    3.1 并发布尔程序的可达性问题
    3.2 后向搜索算法
    3.3 并发布尔程序的可达性分析
        3.3.1 最小覆盖前驱
        3.3.2 可达性分析
    3.4 一种改进的BWS算法—DBWS
        3.4.1 BWS算法分析
        3.4.2 DBWS算法
        3.4.3 DBWS的扩展前驱
    3.5 本章小结
第四章 基于线程迁移系统的并发布尔程序可达性分析
    4.1 线程迁移系统
    4.2 基于线程迁移系统的可达性分析模型
    4.3 核心模块的设计与实现
        4.3.1 扩展迁移模块
        4.3.2 公式求解模块
        4.3.3 扩展算法模块
    4.4 本章小结
第五章 实验结果分析
    5.1 实验环境及测试集
    5.2 实验结果分析
    5.3 本章小结
第六章 总结与展望
    6.1 工作总结
    6.2 未来展望
参考文献
致谢
作者简介


【参考文献】：
期刊论文
[1]面向程序验证的并行程序状态空间态约简技术综述[J]. 逄龙,苏小红,马培军,赵玲玲.  智能计算机与应用. 2015(01)
[2]SMT求解器理论组合技术研究[J]. 李婧,刘万伟.  计算机工程与科学. 2011(10)



本文编号：3411242