Precise Predictive Analysis for Discovering Communication
Deadlocks in MPI Programs

D 2014

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs

FOREJT, Vojtěch, Daniel KROENING, Ganesh NARAYANASWAMY and Subodh SHARMA

Basic information

Original name

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs

Authors

FOREJT, Vojtěch (203 Czech Republic, guarantor, belonging to the institution), Daniel KROENING (276 Germany), Ganesh NARAYANASWAMY (356 India) and Subodh SHARMA (356 India)

Edition

Switzerland, FM 2014: Formal Methods, p. 263-278, 16 pp. 2014

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/14:00080049

Organization unit

Faculty of Informatics

ISBN

978-3-319-06409-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-06410-9_19

UT WoS

000343040100019

Keywords in English

MPI; verification; parallel computation

Abstract

V originále

The Message Passing Interface (MPI) is the standard API for high-performance and scientific computing. Communication deadlocks are a frequent problem in MPI programs, and this paper addresses the problem of discovering such deadlocks. We begin by showing that if an MPI program is single-path, the problem of discovering communication deadlocks is NP-complete. We then present a novel propositional encoding scheme which captures the existence of communication deadlocks. The encoding is based on modelling executions with partial orders, and implemented in a tool called MOPPER. The tool executes an MPI program, collects the trace, builds a formula from the trace using the propositional encoding scheme, and checks its satisfiability. Finally, we present experimental results that quantify the benefit of the approach in comparison to a dynamic analyser and demonstrate that it offers a scalable solution.

Links

MUNI/33/IP1/2014, interní kód MU

Name: Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky (Acronym: PVT-VVPZ)

Investor: Masaryk University

Citovat

FOREJT, Vojtěch, Daniel KROENING, Ganesh NARAYANASWAMY and Subodh SHARMA. Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. In Cliff Jones, Pekka Pihlajasaari, Jun Sun. FM 2014: Formal Methods. Switzerland: Springer, 2014, p. 263-278. ISBN 978-3-319-06409-3. Available from: https://dx.doi.org/10.1007/978-3-319-06410-9_19.

@inproceedings{1297486,
   author = {Forejt, Vojtěch and Kroening, Daniel and Narayanaswamy, Ganesh and Sharma, Subodh},
   address = {Switzerland},
   booktitle = {FM 2014: Formal Methods},
   doi = {http://dx.doi.org/10.1007/978-3-319-06410-9_19},
   editor = {Cliff Jones, Pekka Pihlajasaari, Jun Sun},
   keywords = {MPI; verification; parallel computation},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Switzerland},
   isbn = {978-3-319-06409-3},
   pages = {263-278},
   publisher = {Springer},
   title = {Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs},
   year = {2014}
}

TY  - JOUR
ID  - 1297486
AU  - Forejt, Vojtěch - Kroening, Daniel - Narayanaswamy, Ganesh - Sharma, Subodh
PY  - 2014
TI  - Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
PB  - Springer
CY  - Switzerland
SN  - 9783319064093
KW  - MPI
KW  - verification
KW  - parallel computation
N2  - The Message Passing Interface (MPI) is the standard API for high-performance and scientific computing. Communication deadlocks are a frequent problem in MPI programs, and this paper addresses the problem of discovering such deadlocks. We begin by showing that if an MPI program is single-path, the problem of discovering communication deadlocks is NP-complete. We then present a novel propositional encoding scheme which captures the existence of communication deadlocks. The encoding is based on modelling executions with partial orders, and implemented in a tool called MOPPER. The tool executes an MPI program, collects the trace, builds a formula from the trace using the propositional encoding scheme, and checks its satisfiability. Finally, we present experimental results that quantify the benefit of the approach in comparison to a dynamic analyser and demonstrate that it offers a scalable solution.
ER  -

FOREJT, Vojtěch, Daniel KROENING, Ganesh NARAYANASWAMY and Subodh SHARMA. Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. In Cliff Jones, Pekka Pihlajasaari, Jun Sun. \textit{FM 2014: Formal Methods}. Switzerland: Springer, 2014, p.~263-278. ISBN~978-3-319-06409-3. Available from: https://dx.doi.org/10.1007/978-3-319-06410-9\_{}19.

Detailed Information on Publication Record