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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013)
Carter, J.D., Gardner, W.B., Grewal, G.: The Pilot library for novice MPI programmers. In: PPoPP, pp. 351–352. ACM (2010)
Chen, F., Serbanuta, T.F., Rosu, G.: jPredictor: A predictive runtime analysis tool for Java. In: ICSE, pp. 221–230. ACM (2008)
Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Deniz, E., Sen, A., Holt, J.: Verification and coverage of message passing multicore applications. ACM Trans. Design Autom. Electr. Syst. 17(3), 23 (2012)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Elwakil, M., Yang, Z.: Debugging support tool for MCAPI applications. In: PDATAD, pp. 20–25. ACM (2010)
Gradara, S., Santone, A., Villani, M.L.: DELFIN + : An efficient deadlock detection tool for CCS processes. J. Comput. Syst. Sci. 72(8), 1397–1412 (2006)
Gropp, W., Lusk, E., Skjellum, A.: Using MPI. MIT Press (1999)
Haque, W.: Concurrent deadlock detection in parallel programs. Int. J. Comput. Appl. 28(1), 19–25 (2006)
Hilbrich, T., Protze, J., Schulz, M., de Supinski, B.R., Müller, M.S.: MPI runtime error detection with MUST: advances in deadlock detection. In: SC, p. 30 (2012)
Holt, J., Agarwal, A., Brehmer, S., Domeika, M., Griffin, P., Schirrmeister, F.: Software standards for the multicore era. IEEE Micro 29(3), 40–51 (2009)
Huang, Y., Mercer, E., McCarthy, J.: Proving MCAPI executions are correct using SMT. In: ASE, pp. 26–36. IEEE (2013)
Krammer, B., Bidmon, K., Müller, M.S., Resch, M.M.: MARMOT: An MPI analysis and checking tool. In: PARCO. Advances in Parallel Computing, vol. 13, pp. 493–500. Elsevier (2003)
Leung, A., Gupta, M., Agarwal, Y., Gupta, R., Jhala, R., Lerner, S.: Verifying GPU kernels by test amplification. In: PLDI, pp. 383–394. ACM (2012)
Luecke, G.R., Zou, Y., Coyle, J., Hoekstra, J., Kraeva, M.: Deadlock detection in MPI programs. Concurrency and Computation: Practice and Experience 14(11), 911–932 (2002)
Message Passing Interface, http://www.mpi-forum.org/docs/mpi-2.2
Mueller, M.S., Gopalakrishnan, G., de Supinski, B.R., Lecomber, D., Hilbrich, T.: Dealing with MPI bugs at scale: Best practices, automatic detection, debugging, and formal verification, http://sc11.supercomputing.org/schedule/event_detail.php?evid=tut131
Natarajan, N.: A distributed algorithm for detecting communication deadlocks. In: Joseph, M., Shyamasundar, R.K. (eds.) FSTTCS 1984. LNCS, vol. 181, pp. 119–135. Springer, Heidelberg (1984)
Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC: A runtime verification tool for MCAPI user applications. In: FMCAD, pp. 41–44 (2009)
Siegel, S.F.: Model checking nonblocking MPI programs. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 44–58. Springer, Heidelberg (2007)
Siegel, S.F., Zirkel, T.K.: FEVS: A functional equivalence verification suite for high-performance scientific computing. Mathematics in Computer Science 5(4), 427–435 (2011)
Siegel, S.F., Zirkel, T.K.: The Toolkit for Accurate Scientific Software. Technical Report UDEL-CIS-2011/01, Department of Computer and Information Sciences, University of Delaware (2011)
Vakkalanka, S.: Efficient dynamic verification algorithms for MPI applications. PhD thesis, University of Utah, Salt Lake City, UT, USA, AAI3413092 (2010)
Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M.: Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 66–79. Springer, Heidelberg (2008)
Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., de Supinski, B.R., Schulz, M., Bronevetsky, G.: A scalable and distributed dynamic formal verifier for MPI programs. In: SC, pp. 1–10. IEEE (2010)
Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 256–272. Springer, Heidelberg (2009)
Xue, R., Liu, X., Wu, M., Guo, Z., Chen, W., Zheng, W., Zhang, Z., Voelker, G.: MPIWiz: subgroup reproducible replay of MPI applications. In: PPoPP, pp. 251–260. ACM (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Forejt, V., Kroening, D., Narayanaswamy, G., Sharma, S. (2014). Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_19
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)