VSL Publications

Verification of MPI programs using CIVL

Cite
Ziqing Luo, Manchun Zheng, and Stephen F. Siegel. 2017. Verification of MPI programs using CIVL. In Proceedings of the 24th European MPI Users' Group Meeting (EuroMPI '17). ACM, New York, NY, USA, Article 6, 11 pages. DOI: https://doi.org/10.1145/3127024.3127032
Abstract
CIVL is a framework for verifying concurrent programs. The framework is built around a language, CIVL-C, that extends sequential C with general-purpose primitives that can be used to model a variety of concurrency dialects, including OpenMP, Pthreads, CUDA, and MPI. The framework automatically transforms programs using those dialects into CIVL-C so that static analysis and verification tools for CIVL-C can be applied. This paper describes how C/MPI programs are so transformed. The result is a verifier that can check, within finite bounds, a number of difficult properties of MPI programs, including functional correctness, deadlock-freedom, and adherence to rules specified in the MPI Standard.
Downloads
  1. Download from ACM library
  2. civl_mpi.pdf (preprint)
Related Links
  1. Experimental Archive page
BibTeX 
@inproceedings{Luo:2017:VMP:3127024.3127032,
 author = {Luo, Ziqing and Zheng, Manchun and Siegel, Stephen F.},
 title = {Verification of MPI Programs Using CIVL},
 booktitle = {Proceedings of the 24th European MPI Users' Group Meeting},
 series = {EuroMPI '17},
 year = {2017},
 isbn = {978-1-4503-4849-2},
 location = {Chicago, Illinois},
 pages = {6:1--6:11},
 articleno = {6},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/3127024.3127032},
 doi = {10.1145/3127024.3127032},
 acmid = {3127032},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {CIVL, MPI, model checking, symbolic execution, verification},
}
VSL | Publications