EuroPVM/MPI 2006 will feature a special non-parallel session to present a selection of papers of outstanding quality. Three contributions have been selected for this session. Revised and extended versions of these and other selected papers will be given the opportunity to appear in a special issue of Parallel Computing.
The authors of the papers selected of this session have been honoured with a certificate and an award – below a picture of them together with the program chairs and general chair (front row, left to right: Fabian Kulla, Rajeev Thakur, William Gropp, Robert Kirby; back row: Jack Dongarra, Bernd Mohr, Jesper L. Träff, Joachim Worringen).
Time: Tuesday, 19th Sep 2006, 11:30 – 12:45
Formal Verification of Programs That Use MPI One-Sided Communication
We used formal-verification methods based on model checking to analyze the correctness properties of one existing and two new distributed-locking algorithms implemented by using MPI‘s one-sided communication. Model checking exposed an overlooked correctness issue with the first algorithm, which had been developed by relying only on manual reasoning. Model checking helped confirm the basic correctness properties of the two new algorithms, while also identifying the remaining problems in them. Our experience is that MPI-based programming, especially the tricky and relatively poorly understood one-sided communication features, stand to gain immensely from model checking. Considering that many other areas of concurrent hardware and software design now routinely employ model checking, our experience confirms that the MPI community can benefit greatly from the use of formal verification.
Issues in Developing a Thread-Safe MPI Implementation
The MPI-2 Standard has carefully specified the interaction between MPI and user-created threads, with the goal of enabling users to write multithreaded programs while also enabling MPI implementations to deliver high performance. In this paper, we describe and analyze what the MPI Standard says about thread safety and what it implies for an implementation. We classify the MPI functions based on their thread-safety requirements and discuss several issues to consider when implementing thread safety in MPI. We use the example of generating new context ids (required for creating new communicators) to demonstrate how a simple solution for the single-threaded case cannot be used when there are multiple threads and how a naive thread-safe algorithm can be expensive. We then present an algorithm for generating context ids that works efficiently in both single-threaded and multithreaded cases.
Scalable Parallel Suffix Array Construction
Suffix arrays are a simple and powerful data structure for text processing that can be used for full text indexes, data compression, and many other applications in particular in bioinformatics. We describe the first implementation and experimental evaluation of a scalable parallel algorithm for suffix array construction. The implementation works on distributed memory computers using MPI, Experiments with up to 128 processors show good constant factors and make it look likely that the algorithm would also scale to thousands of processors. This makes it possible to build suffix arrays for huge inputs very quickly. Our algorithm is a parallelization of the linear time DC3 algorithm.