基于符号计数器抽象的并发布尔程序验证研究

摘要

随着计算机技术的快速发展和应用需求，多线程并发程序成为现代程序设计的重要目标。由于线程之间的相互交错执行，可能会产生许多难以发现的微小错误，因此，并发软件验证成为备受关注的研究领域。然而，模型检测并发软件面临严重的状态空间爆炸问题，即可达状态数随着并发线程的增加而呈指数增长，对并发软件直接采用模型检测方法进行验证的效率非常低，甚至无法在实际应用中实现。
　　推动模型检测发展的一个有效方法是谓词抽象，对源程序实施谓词抽象技术产生布尔程序，布尔程序作为软件验证的常用模型，虽缩减了状态空间，但仍是谓词抽象精化技术的瓶颈。为解决状态空间爆炸问题，本文围绕并发布尔程序的线程状态的可达性问题进行分析，为其提出了一些算法，并以一组布尔程序基准测试集证明了算法的有效性。主要工作与贡献如下：
　　（1）研究了带有有界线程创建的非递归并发布尔程序的可达性问题，结合on-the-fly技术提出了一种基于符号计数器抽象的判定方法。在计数器抽象方法中，计数器记录每个局部状态的执行线程数，由其构成的向量表示系统的全局状态。然而，在实际应用中，难以实现为每个局部状态引入一个计数器。本文的方法是仅为可达的局部状态引入计数器，同时在全局状态中保留局部状态至少有一个线程执行的计数器,去掉零值的计数器及其对应的局部状态，从而节省大量的存储空间。
　　（2）研究了带有无界线程创建的非递归并发布尔程序的可达性问题，在上一个方法的基础上进行了扩展，提出了一种基于Karp-Miller可覆盖树的判定方法。由于由未知个线程执行的有限状态并发程序，在任何程序状态都允许动态创建线程，从而会使线程总数增加，由此可能产生无限的状态空间，此种程序的验证问题是不可判定的。本文的方法是为布尔程序直接构建Karp-Miller可覆盖树，将线程状态的可达性问题简化为状态向量加系统的可覆盖性问题，从而证明可达性问题的可判定性，其优点是避免布尔程序静态转化为状态向量加系统时面临的状态空间爆炸问题。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1.1 研究背景及意义

§1.2 国内外研究现状

§1.3 研究内容与主要贡献

§1.4 结构安排

第二章 布尔程序

§2.1 顺序布尔程序

§2.2 并发布尔程序

§2.3 本章小结

第三章 基于符号计数器抽象的并发布尔程序验证

§3.1 执行模型

§3.2 对称化简

§3.3 计数器抽象

§3.4 符号计数器抽象

§3.5 关键实现技术

§3.6 实验分析及对比

§3.7 本章小结

第四章 基于Karp-Miller可覆盖树的并发布尔程序验证

§4.1 计算模型

§4.2 Karp-Miller可覆盖树

§4.3 线程状态的可达性分析

§4.4 本章小结

第五章 结束与展望

§5.1 主要研究工作

§5.2 下一步有待研究的问题

参考文献

致谢

作者在攻读硕士期间主要研究成果