Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs

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.

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

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Switzerland
• Confidentiality degree: is not subject to a state or trade secret
• 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: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-319-06410-9_19
• UT WoS: 000343040100019
• Keywords in English: MPI; verification; parallel computation
• Tags: core_A, firank_A

Abstract

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