Abstract
The message passing paradigm underlies many important families of programs—for instance programs in the area of high performance computing that support science and engineering research. Unfortunately, very few formal methods researchers are involved in developing formal analysis tools and techniques for message passing programs. This paper summarizes research being done in our groups in support of this area, specifically with respect to the Message Passing Interface. We emphasize the need for specialized varieties of many familiar notions such as deadlock detection, race analysis, symmetry analysis, partial order reduction, static analysis and symbolic reasoning support. Since these issues are harbingers of those being faced in multicore programming, the time is ripe to build a critical mass of researchers working in this area.
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
Armstrong, J.: Programming in Erlang: Software for a Concurrent World. Pragmatic Bookshelf (July 2007)
Asanovic, K., Bodik, R., Demmel, J., Keaveny, T., Keutzer, K., Kubiatowicz, J., Morgan, N., Patterson, D., Sen, K., Wawrzynek, J., Wessel, D., Yelick, K.: A view of the parallel computing landscape. Comm. ACM 52(10), 56–67 (2009)
Atzeni, S.: ISP takes Steve’s midterm exam, http://www.cs.utah.edu/~simone/Steve_Midterm_Exam/
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Bronevetsky, G.: Communication-sensitive static dataflow for parallel message passing applications. In: Proceedings of The Seventh International Symposium on Code Generation and Optimization, pp. 1–12. IEEE Computer Society, Los Alamitos (2009)
Cappello, F., Hérault, T., Dongarra, J. (eds.): PVM/MPI 2007. LNCS, vol. 4757. Springer, Heidelberg (2007)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Cousot, P., Cousot, R.: Semantic analysis of communicating sequential processes. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 119–133. Springer, Heidelberg (1980)
DeLisi, M.: Test results comparing ISP, Marmot, and mpirun, http://www.cs.utah.edu/fv/ISP_Tests
Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Inst., pp. 43–112. Academic Press, London (1968)
Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 174–186. ACM, New York (1997)
Gopalakrishnan, G.L., Kirby, R.M.: Top ten ways to make formal methods for HPC practical. In: 2010 FSE/SDP Workshop on the Future of Software Engineering Research. ACM, New York (to appear, 2010)
Gropp, W., Lusk, E., Skjellum, A.: Using MPI: portable parallel programming with the Message-Passing Interface. MIT Press, Cambridge (1999)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Intl. J. on Software Tools for Technology Transfer 2(4) (April 2000)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall Intl., Englewood Cliffs (1985)
Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)
Humphrey, A., Derrick, C., Gopalakrishnan, G., Tibbitts, B.R.: GEM: Graphical explorer for MPI programs. In: Parallel Software Tools and Tool Infrastructures, ICPP Workshop (2010), http://www.cs.utah.edu/fv/GEM
Jones, G., Goldsmith, M.: Programming in occam2. Prentice Hall Intl. Series in Computer Science (1988), http://www.comlab.ox.ac.uk/geraint.jones/publications/book/Pio2/
King, J.C.: Symbolic execution and program testing. Comm. ACM 19(7), 385–394 (1976)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.): EuroPVM/MPI 2008. LNCS, vol. 5205. Springer, Heidelberg (2008)
Li, G., Palmer, R., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API. Science of Computer Programming (2010), http://dx.doi.org/10.1016/j.scico.2010.03.007
Matlin, O.S., Lusk, E., McCune, W.: SPINning parallel systems software. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 213–220. Springer, Heidelberg (2002)
Mattson, T., Wijngaart, R.V.: The 48-core SCC processor: the programmers view. In: SC10 [30] (to appear)
Multicore association, http://www.multicore-association.org
Message Passing Interface Forum: MPI: A Message-Passing Interface Standard, version 2.2, September 4, (2009), http://www.mpi-forum.org/docs/
Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)
The Eclipse Parallel Tools Platform, http://www.eclipse.org/ptp
Research, M.: CHESS: Find and reproduce Heisenbugs in concurrent programs, http://research.microsoft.com/en-us/projects/chess (accessed 11/7/10)
SC 2010: The International Conference for High Performance Computing, Networking, Storage and Analysis, New Orleans, LA. ACM, New York (to appear, 2010)
Schulz, M., de Supinski, B.R.: PNMPI tools: a whole lot greater than the sum of their parts. In: Proceedings of the 2007 ACM/IEEE Conference on Supercomputing, SC 2007, pp. 30:1–30:10. ACM, New York (2007)
Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC - A runtime verification tool for MCAPI user applications. In: 9th International Conference Formal Methods in Computer Aided Design (FMCAD), pp. 41–44. IEEE, Los Alamitos (2009)
Sharma, S., Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M., Thakur, R., Gropp, W.: A formal approach to detect functionally irrelevant barriers in MPI programs. In: Lastovetsky et al. [21], pp. 265–273
Siegel, S.F.: The Toolkit for Accurate Scientific Software web page (2010), http://vsl.cis.udel.edu/tass
Siegel, S.F.: Efficient verification of halting properties for MPI programs with wildcard receives. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 413–429. Springer, Heidelberg (2005)
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.: Verifying parallel programs with MPI-Spin In: Cappello et al. [6], pp. 13–14
Siegel, S.F.: MPI-Spin web page (2008), http://vsl.cis.udel.edu/mpi-spin
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., Avrunin, G.S.: Modeling wildcard-free MPI programs for verification. In: Proceedings of the 2005 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2005), pp. 95–106. ACM Press, New York (2005)
Siegel, S.F., Avrunin, G.S.: Verification of halting properties for MPI programs using nonblocking operations. In: Cappello et al. [6], pp. 326–334
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Combining symbolic execution with model checking to verify parallel numerical programs. ACM Transactions on Software Engineering and Methodology 17, Article 10, 1–34 (2008)
Siegel, S.F., Rossi, L.F.: Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In: Lastovetsky et al. [21]
Siegel, S.F., Zirkel, T.K.: Collective assertions. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, Springer, Heidelberg (2011)
Siegel, S.F., Zirkel, T.K.: Automatic formal verification of MPI-based parallel programs. In: Proceedings of the 2011 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2011). ACM Press, New York (to appear, 2011)
Sutter, H.: The free lunch is over: A fundamental turn toward concurrency in software. Dr. Dobb’s Journal 30(3) (March 2005), http://www.drdobbs.com/architecture-and-design/184405990
Vakkalanka, S.: Efficient Dynamic Verification Algorithms for MPI Applications. Ph.D. thesis, University of Utah (2010), http://www.cs.utah.edu/formal_verification/pdf/sarvani_dissertation.pdf
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)
Vakkalanka, S., Vo, A., Gopalakrishnan, G., Kirby, R.: Precise dynamic analysis for slack elasticity: Adding buffering without adding bugs. In: Keller, R., Gabriel, E., Resch, M., Dongarra, J. (eds.) EuroMPI 2010. LNCS, vol. 6305, pp. 152–159. Springer, Heidelberg (2010)
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: SC10 [30] (to appear), http://www.cs.utah.edu/fv/DAMPI/sc10.pdf
Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. In: PPoPP, pp. 261–269 (2009)
Vuduc, R., Schulz, M., Quinlan, D., de Supinski, B., Sæbjørnsen, A.: Improving distributed memory applications testing by message perturbation. In: PADTAD 2006: Proceeding of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging, pp. 27–36. ACM, New York (2006)
Zhang, Y., Duesterwald, E.: Barrier matching for programs with textually unaligned barriers. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2007, pp. 194–204. ACM, New York (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Siegel, S.F., Gopalakrishnan, G. (2011). Formal Analysis of Message Passing. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-18275-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18274-7
Online ISBN: 978-3-642-18275-4
eBook Packages: Computer ScienceComputer Science (R0)