Formal analysis of MPI-based parallel programs

Abstract

The goal is reliable parallel simulations, helping scientists understand nature, from how foams compress to how ribosomes construct proteins.

References

1. Ahn, D.H., de Supinski, B.R., Laguna, I., Lee, G.L., Liblit, B., Miller, B.P., and schulz, M. scalable temporal order analysis for large-scale debugging. In Proceedings of the ACM/IEEE Conference on Supercomputing (Portland, OR, Nov. 14--20). ACM Press, New York, 2009.
2. Arnold, D.C., Ahn, D.H., de supinski, B.R., Lee, G.L., Miller, B.P., and schulz, M. stack trace analysis for large-scale debugging. In Proceedings of the IEEE International Parallel & Distributed Processing Symposium (Long Beach, CA, Mar. 26--30). IEEE Computer Society, 2007, 1--10.
3. Balay, S., Gropp, W.D., McInnes, L.C., and Smith, B.F. Efficient management of parallelism in object-oriented numerical software libraries. In Modern Software Tools in Scientific Computing, E. Arge, A.M. Bruaset, and H.P. Langtangen, Eds. Birkhauser Press, 1997, 163--202.
4. Barrett, C. and Tinelli, C. CVC3. In Proceedings of the 19 ^th International Conference on Computer Aided Verification, Vol. 4590 LNCS (Berlin, July 3--7). Springer, Berlin, 2007, 298--302.
5. Blackford, L. Scalapack User's Guide. Society for Industrial and Applied Mathematics. Philadelphia, PA, 1997.
6. Bronevetsky, G. Communication-sensitive static dataflow for parallel message passing applications. In Proceedings of the International Symposium on Code Generation and Optimization (Seattle, Mar. 22--25, 2009), 1--12.
7. Butenhof, D.R. Programming with POSIX Threads. Addison-Wesley, Boston, 2006.
8. Cadar, C., Dunbar, D., and Engler, D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the Eighth USENIX Symposium on Operating Systems Design and Implementation (San Diego, Dec. 7--10). USENIX Association, 2008, 209--224.
9. Eclipse Foundation, Inc. Parallel Tools Platform. Ottawa, Ontario, Canada; http://www.eclipse.org/ptp
10. Godefroid, P. Model checking for programming languages using Verisoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Paris, Jan. 15--17). ACM Press, New York, 1997, 174--186.
11. Goldberg, D. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys 23, 1 (Mar. 1991), 5--48.
12. Graphical Explorer of MPI Programs. ISP Eclipse plug-in; University of Utah, School of Computing; http://www.cs.utah.edu/formal_verification/GEM
13. Gropp, W., Lusk, E., and Thakur, R. Using MPI-2: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge, MA, 1999.
14. Hilbrich, T., Schulz, M., de Supinski, B., and Müller, M.S. MUST: A scalable approach to runtime error detection in MPI programs. In Tools for High Performance Computing. Springer, Berlin, 2009, 53--66.
15. International Exascale Software Project; http://www.exascale.org/iesp/Main_Page
16. Karypis Lab. ParMETIS: Parallel Graph Partitioning and Fill-Reducing Matrix Ordering. Minneapolis, MN; http://glaros.dtc.umn.edu/gkhome/metis/parmetis/overview
17. Khurshid, S., Pasareanu, C.S., and Visser, W. Generalized symbolic execution for model checking and testing. In Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Vol. 2619 LNCS, H. Garavel and J. Hatcliff, Eds. (Warsaw, Apr. 7--11). Springer, 2003, 553--568.
18. King, J.C. Symbolic execution and program testing. Commun. ACM 19, 7 (July 1976), 385--394.
19. Krammer, B., Bidmon, K., Müjller, M.S., and Resch, M.M. MARMOT: An MPI analysis and checking tool. In Proceedings of the Parallel Computing Conference (Dresden, Sept. 2--5, 2003), 493--500.
20. Lamport, L. Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 7 (July 1978), 558--565.
21. Message Passing Interface Forum. MPI: A Message-Passing Interface Standard, Version 2.2, Sept. 4, 2009; http://www.mpi-forum.org/docs/
22. MPICH2: High performance and widely portable MPI; http://www.mcs.anl.gov/mpi/mpich
23. Multicore Association. Multicore Communications API, El Dorado Hills, CA; http://www.multicore-association.org
24. NASA Advanced Supercomputing Division. Parallel Benchmarks; http://www.nas.nasa.gov/Resources/Software/npb.html
25. Open MPI: Open Source High Performance MPI. Indiana University, Bloomington, IN; http://www.open-mpi.org/
26. Pacheco, P. Parallel Programming with MPI. Morgan Kaufmann, San Francisco, 1996.
27. Siegel, S.F. et al. The Toolkit for Accurate Scientific Software. Verified Software Laboratory, University of Delaware, 2010; http://vsl.cis.udel.edu/tass
28. Siegel, S.F., Mironova, A., Avrunin, G.S., and Clarke, L.A. Combining symbolic execution with model checking to verify parallel numerical programs. ACM Transactions on Software Engineering and Methodology 17, 2 (Apr. 2008), 1--34.
29. Strout, M.M., Kreaseck, B., and Hovland, P.D. Data-flow analysis for MPI programs. In Proceedings of the 2006 International Conference on Parallel Processing (Columbus, OH, Aug. 14--18). IEEE Computer Society, 2006, 175--184.
30. Vakkalanka, S. Efficient Dynamic Verification Algorithms for MPI Applications. Ph.D. dissertation, University of Utah, 2010; http://www.cs.utah.edu/fv
31. Vakkalanka, S., Vo, A., Gopalakrishnan, G., and Kirby, R. M. Reduced Execution Semantics of MPI: From Theory to Practice. In Proceedings of Formal Methods, Second World Congress Lecture Notes in Computer Science 5850 (Eindhoven, The Netherlands, Nov. 2--6). Springer 2009. 724--740.
32. Vetter, J.S. and de Supinski, B.R. Dynamic software testing of MPI applications with Umpire. In Proceedings of the 2000 ACM/IEEE Conference on Supercomputing (Dallas, Nov. 4--10). IEEE Computer Society Press, 2000.
33. Vo, A., Gopalakrishnan, G., Kirby, R.M., de Supinski, B.R., Schulz, M., and Bronevetsky, G. Large-scale verification of MPI programs using Lamport clocks with lazy updates. In Proceedings of the 20 ^th International Conference on Parallel Architectures and Compilation Techniques (Galveston, TX, Oct. 10--14). IEEE Computer Society Press, 2011. 329--338.
34. Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., de Supinski, B.R., Schulz, M., and Bronevetsky, G. A scalable and distributed dynamic formal verifier for MPI programs. In Proceedings of the ACM/IEEE Conference on Supercomputing (New Orleans, Nov. 13--19). IEEE Computer Society Press, 2010.
35. Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., and Thakur, R. Formal verification of practical MPI programs. In Proceedings of the 14 ^th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Raleigh, NC, Feb. 14--18). ACM Press, New York, 2009, 261--269.

Index Terms

• Computer systems organization

  • Architectures

    • Distributed architectures

• Computing methodologies

  • Concurrent computing methodologies

    • Concurrent programming languages

• Hardware

  • Communication hardware, interfaces and storage

  • Robustness

• Networks

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging

  • Software notations and tools

    • General programming languages

      • Language types

        • Concurrent programming languages

  • Software organization and properties

    • Software system structures

      • Distributed systems organizing principles