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 a Subodh SHARMA

Základní údaje

Originální název

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs

Autoři

FOREJT, Vojtěch (203 Česká republika, garant, domácí); Daniel KROENING (276 Německo); Ganesh NARAYANASWAMY (356 Indie) a Subodh SHARMA (356 Indie)

Vydání

Switzerland, FM 2014: Formal Methods, od s. 263-278, 16 s. 2014

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00080049

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-06409-3

ISSN

DOI

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

UT WoS

000343040100019

EID Scopus

2-s2.0-84958552935

Klíčová slova anglicky

MPI; verification; parallel computation

Štítky

core_A, firank_A

Změněno: 11. 4. 2015 15:12, RNDr. Vojtěch Forejt, Ph.D., LL.B. (Hons)

Anotace

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.

Návaznosti

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

Název: 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 (Akronym: PVT-VVPZ)

Investor: Masarykova univerzita, 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

Citovat

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. FM 2014: Formal Methods. Switzerland: Springer, 2014, s. 263-278. ISBN 978-3-319-06409-3. Dostupné z: https://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 = {https://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  - CONF
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://doi.org/10.1007/978-3-319-06410-9\_{}19.

Přehled o publikaci