Abstract
Formal dynamic analysis of Message Passing Interface (MPI) programs is crucially important in the context of developing HPC applications. Existing dynamic verification tools for MPI programs suffer from exponential schedule explosion, especially when multiple non-deterministic receive statements are issued by a process. In this paper, we focus on detecting message-orphaning deadlocks within MPI programs. For this analysis target, we describe a sound heuristic that helps avoid schedule explosion in most practical cases while not missing deadlocks in practice. Our method hinges on initially computing the potential non-deterministic matches as conventional dynamic analyzers do, but then including only the entries which are found relevant to cause a refusal deadlock (essentially a macroscopic-view persistent-set reduction technique). Experimental results are encouraging.
This research has been supported by NSF OCI 1148127 and EPSRC project EP/G026254/1.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bronevetsky, G.: Communication-Sensitive Static Dataflow for Parallel Message Passing Applications. In: CGO: Proceedings of the 7th annual IEEE/ACM International Symposium on Code Generation and Optimization (2009) ISBN: 978-0-7695-3576-0
FEVS Benchmark, http://vsl.cis.udel.edu/fevs/index.html
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 110–121. ACM (2005)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)
Godefroid, P., Levin, M., Molnar, D.: Whitebox fuzzing for security testing. Communications of the ACM (March 2012)
Gopalakrishnan, G., Kirby, R.M., Siegel, S., Thakur, R., Gropp, W., Lusk, E., de Supinski, B.R., Schulz, M., Bronevetsky, G.: Formal analysis of mpi-based parallel programs: Present and future. Communications of the ACM (December 2011)
Karypis, G., Kumar, V.: Parallel multilevel k-way partitioning scheme for irregular graphs. In: SuperComputing, SC (1996)
Message Passing Interface, http://www.mpi-forum.org/docs/mpi-2.2
Sarkar, V., Harrod, W., Snavely, A.: Software challenges in extreme scale systems. SciDAC Review Special Issue on Advanced Computing: The Roadmap to Exascale, 60–65 (January 2010)
Siegel, S.F.: The MADRE web page (2008), http://vsl.cis.udel.edu/madre
Siegel, S.F.: MPI-Spin web page (2008), http://vsl.cis.udel.edu/mpi-spin
Vakkalanka, S.: Efficient dynamic verification algorithms for MPI applications. PhD thesis, University of Utah, Salt Lake City, Ut, USA (2010)
Vakkalanka, S., Gopalakrishnan, G.C., 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: Proceedings of the ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2010, pp. 1–10. IEEE Computer Society, Washington, DC (2010)
Vo, A., Gopalakrishnan, G., Kirby, R.M., de Supinski, B.R., Schulz, M., Bronevetsky, G.: Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update. In: PACT, pp. 330–339 (2011), http://doi.ieeecomputersociety.org/10.1109/PACT.2011.64
Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. In: Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2009, pp. 261–270. ACM, New York (2009)
Vuduc, R., Schulz, M., Quinlan, D., de Supinski, B., Sornsen, A.: Improving distributed memory applications testing by message perturbation. In: Proceedings of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging, PADTAD 2006, pp. 27–36. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sharma, S., Gopalakrishnan, G., Bronevetsky, G. (2012). A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications. In: Gheyi, R., Naumann, D. (eds) Formal Methods: Foundations and Applications. SBMF 2012. Lecture Notes in Computer Science, vol 7498. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33296-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-33296-8_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33295-1
Online ISBN: 978-3-642-33296-8
eBook Packages: Computer ScienceComputer Science (R0)