Symbolic verification of message passing interface programs
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...
Saved in:
Main Authors: | , , , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2020
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4633 https://ink.library.smu.edu.sg/context/sis_research/article/5636/viewcontent/Symbolic_verification_of_Message_Passing_Interface_Programs_av.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5636 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-56362020-03-17T02:49:41Z Symbolic verification of message passing interface programs YU, Hengbiao CHEN, Zhenbang FU, Xianjin WANG, Ji SU, Zhendong SUN, Jun HUANG, Chun DONG, Wei 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. 2020-05-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4633 https://ink.library.smu.edu.sg/context/sis_research/article/5636/viewcontent/Symbolic_verification_of_Message_Passing_Interface_Programs_av.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Information Security |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Information Security |
spellingShingle |
Information Security YU, Hengbiao CHEN, Zhenbang FU, Xianjin WANG, Ji SU, Zhendong SUN, Jun HUANG, Chun DONG, Wei Symbolic verification of message passing interface programs |
description |
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. |
format |
text |
author |
YU, Hengbiao CHEN, Zhenbang FU, Xianjin WANG, Ji SU, Zhendong SUN, Jun HUANG, Chun DONG, Wei |
author_facet |
YU, Hengbiao CHEN, Zhenbang FU, Xianjin WANG, Ji SU, Zhendong SUN, Jun HUANG, Chun DONG, Wei |
author_sort |
YU, Hengbiao |
title |
Symbolic verification of message passing interface programs |
title_short |
Symbolic verification of message passing interface programs |
title_full |
Symbolic verification of message passing interface programs |
title_fullStr |
Symbolic verification of message passing interface programs |
title_full_unstemmed |
Symbolic verification of message passing interface programs |
title_sort |
symbolic verification of message passing interface programs |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2020 |
url |
https://ink.library.smu.edu.sg/sis_research/4633 https://ink.library.smu.edu.sg/context/sis_research/article/5636/viewcontent/Symbolic_verification_of_Message_Passing_Interface_Programs_av.pdf |
_version_ |
1770574944739000320 |