Verification of Halting Properties for MPI Programs Using Nonblocking Operations

1. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

   Google Scholar 

2. Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)

   Google Scholar 

3. Matlin, O.S., Lusk, E., McCune, W.: SPINning parallel systems software. In: Bošnački, D., Leue, S. (eds.) Model Checking Software. LNCS, vol. 2318, pp. 213–220. Springer, Heidelberg (2002)

   Google Scholar 

4. Message Passing Interface Forum: MPI: A Message-Passing Interface standard, version 1.1 (1995), http://www.mpi-forum.org/docs/

5. Palmer, R., Delisi, M., Gopalakrishnan, G., Kirby, R.M.: An approach to formalization and analysis of message passing libraries. In: Proceedings of the 12th Intl. Workshop on Formal Methods for Industrial Critical Systems (FMICS), Springer, Heidelberg (to appear, 2007)

   Google Scholar 

6. Palmer, R., Gopalakrishnan, G., Kirby, R.M.: Semantics driven partial-order reduction of MPI-based parallel programs. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD V), London (to appear, 2007)

   Google Scholar 

7. Pervez, S., Gopalakrishnan, G., Kirby, R.M., Palmer, R., Thakur, R., Gropp, W.: Practical model checking method for verifying correctness of MPI programs. In: Proceedings of the 14th European PVM/MPI Users’ Group Meeting, Springer, Heidelberg (2007)

   Google Scholar 

8. Pervez, S., Gopalakrishnan, G., Kirby, R.M., Thakur, R., Gropp, W.: Formal verification of programs that use MPI one-sided communication. In: Mohr, B., Träff, J.L., Worringen, J., Dongarra, J. (eds.) Recent Advances in Parallel Virtual Machine and Message Passing Interface. LNCS, vol. 4192, pp. 30–39. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

9. 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)

   Google Scholar 

10. 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)

    Chapter  Google Scholar 

11. Siegel, S.F., Avrunin, G.S.: Modeling MPI programs for verification. Technical Report UM-CS-2004-75, Department of Computer Science, University of Massachusetts (2004)

    Google Scholar 

12. Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol. 2989, pp. 286–303. Springer, Heidelberg (2004)

    Google Scholar 

13. 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)

    Chapter  Google Scholar 

14. Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Pollock, L.L., Pezzé, M. (eds.) Proceedings of the ACM SIGSOFT Intl. Symposium on Software Testing and Analysis (ISSTA 2006), pp. 157–168. ACM Press, New York (2006)

    Chapter  Google Scholar 

15. Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI—The Complete Reference, The MPI Core, 2nd edn. MIT Press, Cambridge (1998)

    Google Scholar 

Download references