基于符号执行的并发程序分析与验证研究

With the wide spread and application of parallel computing and heterogeneous multi-core platforms, the quality of concurrent software has been paid with more and more attention. Usually, a concurrent system is non-deterministic. In the result of the non-determinism, a concurrent program is unpredictable and complex, and has a huge state space, which makes it a great challenge to ensure the trustworthy of a concurrent system. Therefore, it is important to study the formal verification of a concurrent system for improving the reliability and security. This project will carry out the research as follows: first, with respect to the features and the trustworthy requirements of concurrent programs, we will investigate the bug features and the formal specification method of concurrent programs, which will result a multi-dimensional specification method that can support specifying the interleaving of a concurrent program; second, based on the specification method, we will research the analysis and verification techniques by leveraging symbolic execution, and the result is supposed to support the verification of concurrent programs with a high efficiency; third, we will study environment support and the abstraction of data structures for improving the feasibility and completeness of symbolic execution; last, we will implement a symbolic execution engine and a source-oriented verification tool with a high automation. We hope this project can improve the ability of verifying concurrent programs, and contribute the state of art of symbolic execution-based verification techniques. The result of this project can directly contribute to improving the reliability of concurrent systems.

随着并行计算和异构多核平台的应用越来越广泛，并发软件的质量引起了广泛关注。由于并发系统自身的非确定性，使得并发程序呈现出不可预测性、状态空间巨大、复杂性等特征,为并发系统的可信保障带来了巨大挑战。因此，研究并发程序的形式验证技术，对提高并发系统的可靠性与安全性具有重要意义。本项目将首先从并发程序的特点和可信需求出发，研究并发程序的错误特征和关键性质规约方法，得到能够支持并发程序交叠执行规约的多维形式规约方法；然后在规约方法的基础上，结合符号执行技术的最新进展，研究基于符号执行的分析验证技术及其优化，支持高效的并发程序验证；进一步研究符号执行的环境支持和数据结构抽象技术，提高验证方法可行性和完全性；最终建立自动化程度高、直接面向源代码的并发程序符号执行和验证工具。本项目的研究能显著提高并发程序的验证能力，能丰富和发展基于符号执行的程序分析与验证方法，为提高并发系统的可靠性提供有力支持。

随着并行计算和异构多核平台的应用越来越广泛，并发软件的质量引起了广泛关注。由于并发系统自身的非确定性，使得并发程序呈现出不可预测性、状态空间巨大、复杂性等特征，为并发系统的可信保障带来了巨大挑战。从目前看，对于并发软件，符合其特点的形式规约方法、验证方法以及有效的验证工具都有待于进一步研究。对此，本项目针对具有典型特征的并行程序，对其可信保证理论基础和关键技术进行了深入研究。本项目的主要研究成果包括： . （1）在现有程序分析理论和方法的基础上，研究了基础了的符号执行方法，提出了猜测符号执行方法、正规性质引导的符号执行方法以及浮点及复杂数据类型程序的符号执行方法，以提高符号执行的可行性和可扩展性。. （2）研究提出了MPI程序的符号执行方法，能系统探索含阻塞和非阻塞通讯MPI程序的行为空间；基于符号执行方法，提出了MPI程序符号化验证方法，有机结合目前的模型检验技术，可验证MPI程序的关键性质；同时，提出了基于符号执行的MPI程序同步错缺陷检测方法，以发现非阻塞通讯MPI程序中的同步错缺陷；. （3）研究了基于请求路径的并发系统性能问题诊断方法，提出了基于路径分割的性能异常诊断方法，以降低数据维度、增大样本容量，从而提高诊断方法的效率和结果的准确度。. 根据上述理论和方法，项目设计实现了MPI C程序的符号化分析验证工具，并在多个实际的MPI程序上开展了实验应用；同时，也设计开发了基于请求路径的并发系统性能问题检测及诊断工具。