Další formáty:
BibTeX
LaTeX
RIS
@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 a 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, s.~263-278. ISBN~978-3-319-06409-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-06410-9\_{}19.
|
