MPI程序的符号化分析、验证与性能优化

Message Passing Interface (MPI) is the standard paradigm of programming in high performance computing. MPI programs are error-prone because of complex program features, such as non-determinism and asynchrony. To deal with the reliability issue of MPI programs, this project focuses on symbolic execution based program analysis and verification. Firstly, to improve the scalability, we study partial symbolic execution with respect to the analysis objective, i.e., selecting partial processes and program for symbolic execution and making partial input variables symbolic. Secondly, to ensure the correctness of dynamic scheduling MPI programs, we study efficient symbolic verification for MPI programs that have communications depend on messages. On the other hand, MPI library provides a large number of APIs for communication, and communication behaviors have direct effect on the performance. To cope with the performance issue of MPI programs, this project studies probabilistic symbolic execution based performance analysis for MPI programs, and performance tuning through optimizing communication behaviors. The project achievement can be used to improve the reliability and performance of MPI programs, and provide technical supports for the development of high performance computing.

消息传递接口（MPI）是高性能计算并行程序设计的标准范式。MPI程序的复杂程序特征，例如非确定性和异步性，使得程序容易出错。针对MPI程序的可靠性问题，本项目从基于符号执行的MPI程序分析与验证两个方面展开研究。首先，为了提高MPI程序符号执行的可扩展性，项目研究面向分析目标的部分符号执行技术，即符号执行部分进程、部分程序和符号化部分输入变量。其次，为了保证动态调度MPI程序的正确性，项目研究通信依赖消息MPI程序的高效符号化验证技术。另一方面，MPI库提供了大量通信接口，且通信行为直接影响MPI程序性能。针对MPI性能问题，本项目研究基于概率符号执行的MPI程序性能分析方法和基于通信行为调整的MPI程序性能优化方法。本项目的研究成果可用于提升MPI程序的可靠性和性能，为我国高性能计算领域的发展提供技术支持。

消息传递接口（MPI）是高性能计算并行程序设计的标准范式。MPI程序的复杂程序特征，例如非确定性和异步性，使得程序容易出错。考虑到高性能计算MPI程序被广泛应用于安全攸关领域，确保MPI程序的正确性具有重要意义。针对MPI程序的可靠性问题，本项目研究基于符号执行的MPI程序分析与验证。 为了确保MPI通信正确性，我们提出了一种结合符号执行和路径模型检验的符号化验证方法。在该验证框架中，符号执行自动抽取路径层面可验证的通信模型，模型检验的结果则用于裁剪符号执行冗余的状态空间。该工作发表于2020年国际软件工程大会；为了确保MPI程序在不同MPI库实现下的正确性，我们提出了一种面向非确定性同步的MPI符号化验证方法。具体而言，我们给出了一种基于通信顺序进程（CSP）的路径编码方法，能够对一条执行路径的非确定性同步行为进行编码。该工作发表于2020年可信软件工程理论、工具和应用国际研讨会；为了确保MPI通信API使用的正确性，我们提出了一种面向MPI消息签名匹配的符号化验证方法。具体而言，我们给出了一种基于通信顺序进程（CSP）的路径编码方法，能够对一条执行路径的消息签名匹配情况进行编码。为了提高可扩展性，我们给出了一种基于偏序规约的路径编码优化方法来降低路径通信模型的复杂度。该工作发表于2022年国际软件测试、验证和确认大会；为了优化MPI程序的性能，我们提出了基于聚合通信来替换功能等价的发送与接收的通信，以及通过延后非阻塞通信的完成检查来重叠通信与计算。综上所述，本项目的研究成果可用于提升MPI程序的可靠性和性能，为高性能计算领域的发展提供技术支持。