Title: Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software
Authors: Stephen F. Siegel and Louis F. Rossi
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.
Appearing in:
Recent Advances in Parallel Virtual Machine and Message Passing Interface, 15th European PVM/MPI User's Group Meeting, Proceedings, 2008. Spring LNS 5205, pages 274-282.
BibTeX:
@InProceedings{siegel-rossi:2008:eccsvm_pvmmpi,
author = "Stephen F. Siegel and Louis F. Rossi",
title = "Analyzing {BlobFlow}: A Case Study Using Model Checking to Verify Parallel Scientific Software",
pages = {274--282},
crossref = {pvmmpi2008}
}
@Proceedings{pvmmpi2008,
booktitle = "Recent Advances in {P}arallel {V}irtual {M}achine and {M}essage {P}assing {I}nterface, 15th {E}uropean {PVM/MPI} User's Group Meeting, Proceedings",
title = "Recent Advances in {P}arallel {V}irtual {M}achine and {M}essage {P}assing {I}nterface, 15th {E}uropean {PVM/MPI} User's Group Meeting, Proceedings",
publisher = "Springer",
series = "LNCS",
volume = {5205},
year = {2008},
editor = {Alexey Lastovetsky and Tahar Kechadi and Jack Dongarra},
note = "To appear"
}
Download:
Related Links: