弱内存程序的限界模型检验技术研究

To improve the performance of concurrent programs, most of the shared memory based multiprocessor systems employ relaxed memory consistency models. Due to the out of order semantics, the behaviors of such systems are generally much more complex than that of systems based on sequential consistency. It remains an extremely challenging problem to guarantee the correctness of relaxed memory programs. Bounded model checking (BMC) is one of the most successful techniques for concurrent program verification, but the existing work of BMC mainly focuses on sequential consistency. To improve the performance of relaxed memory program verification, this project studies those critical techniques of BMC for relaxed memory programs. The main content of this project includes 4 aspects as follows: (1) To obtain an effective encoding of the out of order semantics, we research on the semantics model of the out of order semantics; (2) To reduce the number of paths during the search of BMC, we research on the path reduction and encoding optimization techniques of relaxed memory programs; (3) To decrease the constraint size of relaxed memory programs, we research on an efficient interaction abstraction and verification technique; (4) We focus on concurrent C programs with PThreads and develop a concurrent program verification tool that supports relaxed memory consistency models such as TSO, PSO, and PowerPC, and then it will be applied to some real-world cases.

为提高并行程序的运行效率，目前的主流多处理机共享内存系统大都采用弱内存一致性模型。该模型的乱序执行语义导致弱内存程序的行为相对于顺序一致性模型更加复杂，如何保证弱内存程序的正确性是目前极具挑战性的一项前沿课题。限界模型检验是并行程序验证的主流方法之一，但该技术目前还主要局限于顺序一致性模型。项目研究弱内存程序限界模型检验的关键技术，以提高形式化方法对弱内存程序的验证能力和效率。具体研究内容包括：研究弱内存程序的乱序执行语义模型，实现乱序执行语义的高效编码；研究弱内存程序的搜索路径约减与编码优化，减少限界模型检验中的搜索路径；研究基于交互行为抽象的弱内存程序高效验证，降低限界模型检验中的约束表达式规模；以基于PThread库的并行C程序为研究对象，设计开发支持TSO、PSO和PowerPC等弱内存一致性模型的并行程序高效验证工具，并在实际案例中对项目研究方法和平台进行应用。

为提高并行程序的运行效率，目前的主流多处理机共享内存系统大都采用弱内存一致性模型。在并行程序中，由于线程之间交互顺序的非确定性，程序的可能行为随程序规模和线程数量的增加指数增长。在弱内存模型下，为充分利用硬件和编译器层面的优化，还允许所谓的“乱序执行”，导致弱内存程序的行为更加复杂。如何保证弱内存程序的正确性是极具挑战性的一项前沿课题。项目研究弱内存程序限界模型检验的关键技术，包括弱内存程序的乱序执行语义模型、弱内存程序的搜索路径约减与编码优化、基于交互行为抽象的弱内存程序高效验证、以及设计开发支持TSO、PSO等弱内存一致性模型的并行程序高效验证工具。. 根据项目研究目标的要求，首先针对导致弱内存程序的限界模型检验异常复杂的两个主要问题：线程间语句执行顺序的非确定性与线程内变量操作执行顺序的非确定性开展了深入研究。针对线程间语句执行顺序的非确定性问题，提出了一种基于调度约束抽象精化的验证方法，通过对交互行为进行抽象，避免了对整个程序空间进行精确搜索。针对线程内变量操作执行顺序的非确定性问题，提出一种优化的线程内执行顺序编码方法，将弱内存模型下的程序验证开销降低到与顺序一致性模型下的验证一个量级。为进一步提高弱内存程序的验证效率，提出一种面向弱内存程序的并行化验证方法，采用多个引擎从不同位置对抽象进行并行验证和抽象，突破了程序验证难以并行化的现状。为提高代码演化过程中的验证效率，提出了一种弱内存程序的增量式验证方法，通过利用前面版本验证生成的精化约束，有效避免后面版本验证过程中的冗余分析。考虑到数组是导致程序验证状态空间爆炸的主要因素之一，提出一种基于数组压缩的程序验证优化方法，通过降低程序中的数组规模，有效提高含有较大规模数组的程序验证效率。项目设计实现了并行程序验证工具Yogar-CBMC，并基于国际软件验证大赛SV-COMP中的案例验证了项目方法的有效性。