Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

5-2020

Abstract

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-SV and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 57 out of the 111 tasks (51%) within one hour, while in comparison, MPI-SV verifies 99 tasks (89%). On average, compared with pure symbolic execution, MPI-SV achieves 8x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

Discipline

Information Security

Research Areas

Cybersecurity

Publication

Proceedings of the 42nd International Conference on Software Engineering, Seoul, South Korea, 2020 October 5-11

First Page

1

Last Page

12

City or Country

Seoul, South Korea

Copyright Owner and License

Authors

Additional URL

https://conf.researchr.org/details/icse-2020/icse-2020-papers/105/Symbolic-Verification-of-Message-Passing-Interface-Programs

Download

Share

COinS