Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00080049" target="_blank" >RIV/00216224:14330/14:00080049 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-06410-9_19" target="_blank" >http://dx.doi.org/10.1007/978-3-319-06410-9_19</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-06410-9_19" target="_blank" >10.1007/978-3-319-06410-9_19</a>
Alternative languages
Result language
angličtina
Original language name
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
Original language description
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 showingthat 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
FM 2014: Formal Methods
ISBN
9783319064093
ISSN
0302-9743
e-ISSN
—
Number of pages
16
Pages from-to
263-278
Publisher name
Springer
Place of publication
Switzerland
Event location
Singapore
Event date
May 12, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000343040100019