一句话：提出 MPI-SV，首个基于符号执行并可自动验证含非阻塞操作的 MPI 程序的工具。
MPI 程序验证因非确定性、非阻塞操作等复杂特性而困难。本文提出 MPI-SV，将符号执行与模型检查协同结合，以自动验证含非阻塞操作的 MPI 程序，并提升可扩展性与可验证性质范围。作者实现了工具并在 111 个真实 MPI 验证任务上评估：纯符号执行方法一小时内成功验证 61 个任务（55%），MPI-SV 验证 100 个任务（90%）。平均而言，在验证关键性质满足时 MPI-SV 获得 19 倍加速，在发现违规时获得 5 倍加速。
Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV1 and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.
DOI 原文 ·
@inproceedings{paperbot5617,
title = {Symbolic verification of message passing interface programs},
author = {Hengbiao Yu and Zhenbang Chen and Xianjin Fu and Ji Wang and Zhendong Su and Jun Sun and Chun Huang and Wei Dong},
booktitle = {ICSE},
year = {2020},
doi = {10.1145/3377811.3380419}
}