[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software

  • Conference paper
Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5205))

  • 932 Accesses

Abstract

Model checking techniques are powerful tools for the analysis and verification of concurrent systems. This paper reports on a case study applying model checking techniques to a mature, MPI-based scientific program consisting of approximately 10K lines of code. The program, BlobFlow, implements a high order vortex method for solving the two-dimensional Navier-Stokes equations. Despite the complexity of the code, we verify properties including freedom from deadlock and the functional equivalence of sequential and parallel versions of the program. This has led to new insights into the technology that will be required to automate the modeling and verification process for complex scientific software.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Chapter  Google Scholar 

  2. 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 (July 2007)

    Google Scholar 

  3. Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Combining symbolic execution with model checking to verify parallel numerical programs. Transactions on Software Engineering and Methodology 17(2), 1–34 (2008)

    Article  Google Scholar 

  4. Rossi, L.F.: Resurrecting core spreading methods: A new scheme that is both deterministic and convergent. SIAM J. Sci. Comp. 17(2), 370–397 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  5. Rossi, L.F.: Achieving high-order convergence rates with deforming basis functions. SIAM J. Sci. Comput. 26(3), 885–906 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  6. Rossi, L.F.: Evaluation of the Biot-Savart integral for deformable elliptical gaussian vortex elements. SIAM J. Sci. Comput. 28(4), 1509–1532 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  7. Siegel, S.F.: The MPI-Spin web page (2007), http://vsl.cis.udel.edu/mpi-spin

  8. 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 

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

    Google Scholar 

  10. Cottet, G.H., Koumoutsakos, P.D.: Vortex methods: Theory and Practice. Cambridge University Press, Cambridge (2000)

    Book  MATH  Google Scholar 

  11. Saffman, P.G.: Vortex Dynamics. Cambridge University Press, Cambridge (1992)

    MATH  Google Scholar 

  12. Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Model Checking of Software: 8th Intl. SPIN Workshop, pp. 103–122. Springer, Heidelberg (2001)

    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)

    Google Scholar 

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

    Chapter  Google Scholar 

  15. Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M.: Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In: Computer Aided Verification: 20th International Conference, CAV 2008, Princeton, USA, July 7–14, (to appear, 2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verified Software Laboratory, Department of Computer and Information Sciences, University of Delaware, Newark, DE 19716, USA

    Stephen F. Siegel

  2. Department of Mathematical Sciences, University of Delaware, Newark, DE 19716, USA

    Louis F. Rossi

Authors
  1. Stephen F. Siegel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Louis F. Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alexey Lastovetsky Tahar Kechadi Jack Dongarra

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Siegel, S.F., Rossi, L.F. (2008). Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software. In: Lastovetsky, A., Kechadi, T., Dongarra, J. (eds) Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM/MPI 2008. Lecture Notes in Computer Science, vol 5205. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87475-1_37

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87475-1_37

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-87474-4

  • Online ISBN: 978-3-540-87475-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics