Short Contributions on Work in Progress
A new type of session introduced with EuroPVM/MPI 2006 are the Late and Breaking Results: 2-page abstracts on the latest results and approaches could be submitted until only a few days before the conference starts. The selected contributions were presented in a special, non-parallel session, and the contributions will be published via the conference website.
The following two contributions were selected for presentation:
Using MPI-SPIN to Model Check MPI Programs with Nonblocking Communication
Stepen F. Siegel
Formal verification techniques, such as model checking, are the subject of increasing interest in the parallel programming community. In order to apply these techniques to non-trivial MPI programs, I have developed MPI-SPIN, an extension to the model checker SPIN that supports many commonly-used MPI functions, constants, and types, including those used for nonblocking point-to-point communication. In a preliminary experiment, I have applied MPI-SPIN to the 17 examples (2.17–2.33) in MPI: The Complete Reference, Volume 1 dealing with nonblocking communication. I successfully verified many correctness properties of these examples and in two cases discovered non-trivial faults.
Implementation of a Parallel NetCDF Interface for Seamless Collective Remote I/O
In scientific applications, netCDF was developed to support a view of data as a collection of self-describing, portable, and array-oriented objects that can be accessed through a simple interface. Its parallel I/O interface, parallel netCDF, was developed with the help of an MPI-I/O library. To realize the same operations among computers which have different MPI libraries, a remote I/O mechanism of a Stampi library, which is a flexible intermediate library to realize seamless MPI operations not only inside a computer but also among computers, has been introduced in some of parallel netCDF functions. This I/O system has been evaluated on interconnected PC clusters, and sufficient performance has been achieved in collective parallel netCDF functions with huge amount of data.