Abstract
We consider the problem of verifying MPI programs that use MPI_Probe and MPI_Iprobe. Conventional testing tools, known to be inadequate in general, are even more so for testing MPI programs containing MPI probes. A few reasons are: (i) use of the MPI_ANY_SOURCE argument can make MPI probes non-deterministic, allowing them to match multiple senders, (ii) an MPI_Recv that follows an MPI probe need not match the MPI_Send that was successfully probed, and (iii) simply re-running the MPI program, even with schedule perturbations, is insufficient to bring out all behaviors of an MPI program using probes. We develop several key insights that help develop an elegant solution: prioritizing MPI processes during dynamic verification, handling non-determinism, and safe handling of probe loops. These solutions are incorporated into a new version of our dynamic verification tool ISP. ISP is now able to efficiently and soundly verify larger MPI examples, including MPI-BLAST and ADLB.
Supported in part by Microsoft, NSF CNS-0509379, CCF-0811429, and the Mathematical, Information, and Computational Science Division subprogram of the Office of Advanced Scientific Computing Research, Office of Science, U.S. Department of Energy, under Contract DE-AC02-06CH11357.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Mpi standard 1.1., http://www.mpi-forum.org/docs/mpi-11.ps
The IRS Benchmark Code, https://asc.llnl.gov/computing_resources/purple/archive/benchmarks/irs/
Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. Technical Report UCB/EECS-2008-123, Univ. of California, Berkeley (September 2008)
Dwyer, M., Hatcliff, J., Schmidt, D.: Bandera: Tools for automated reasoning about software system behavior. In: ERCIM News, 36 (January 1999)
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL 2005 (2005)
Godefroid, P., Hanmer, B., Jagadeesan, L.: Systematic software testing using VeriSoft: An analysis of the 4ess heart-beat monitor. Bell Labs Technical Journal, 3(2), April-June (1998)
Godefroind, P., Nagappan, N.: Concurrency at microsoft - an exploratory survey, EC2 (2008)
Holzmann, G.J.: The model checker spin. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Karypis, G.: METIS and ParMETIS, http://glaros.dtc.umn.edu/gkhome/views/metis
Lusk, R., Pieper, S., Butler, R., Chan, A.: Asynchronous dynamic load balancing, http://unedf.org/content/talks/Lusk-ADLB.pdf
Sharma, S., Vakkalanka, S., Gopalakrishnan, G.C., Kirby, R.M., Thakur, R., Gropp, W.D.: A formal approach to detect functionally irrelevant barriers in MPI programs. In: Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.) EuroPVM/MPI 2008. LNCS, vol. 5205, pp. 265–273. Springer, Heidelberg (2008)
Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 286–303. Springer, Heidelberg (2004)
Siegel, S.F., Siegel, A.R.: MADRE: The Memory-Aware Data Redistribution Engine. In: Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.) EuroPVM/MPI 2008. LNCS, vol. 5205, pp. 218–226. Springer, Heidelberg (2008)
Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: Scheduling considerations for building dynamic verification tools for MPI. In: PADTAD-VI 2008 (2008)
Vakkalanka, S., DeLisi, M., Gopalakrishnan, G.C., Kirby, R.M., Thakur, R., Gropp, W.D.: Implementing efficient dynamic formal verification methods for MPI programs. In: Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.) EuroPVM/MPI 2008. LNCS, vol. 5205, pp. 248–256. Springer, Heidelberg (2008)
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., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical mpi programs. In: PPoPP 2009, pp. 261–269 (2009)
Yang, J., et al.: MODIST: Transparent Model Checking of Unmodified Distributed System. In: NSDI 2009 (to appear)
Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Efficient stateful dynamic partial order reduction. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 288–305. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vo, A., Vakkalanka, S., Williams, J., Gopalakrishnan, G., Kirby, R.M., Thakur, R. (2009). Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-determinism. In: Ropo, M., Westerholm, J., Dongarra, J. (eds) Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM/MPI 2009. Lecture Notes in Computer Science, vol 5759. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03770-2_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-03770-2_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03769-6
Online ISBN: 978-3-642-03770-2
eBook Packages: Computer ScienceComputer Science (R0)