Scheduling Considerations for Building Dynamic Verication Tools for MPI?

Abstract. Dynamic verication methods are the natural choice for for-mally verifying real world programs when model extraction and mainte-nance are expensive. Message passing programs written using the MPI library often fall under this category, especially when these programs have to be veried after being ported to new platforms and iteratively optimized. However, implementing dynamic verication tools for MPI requires solving many problems pertaining to the scheduling realities of the MPI runtime. In this paper, we describe the progression of our ideas during the development of our dynamic verication tool for MPI pro-grams, called in-situ partial order (ISP). Each idea developed in this progression relates to our dual goals of ensuring full coverage of all rep-resentative interleavings (in the sense of partial order reduction) among MPI processes, and forcing the MPI runtime to eect these interleavings. We brie y examine similar issued faced by other builders of dynamic ver-i cation tools. We conclude with observations backing the growing im-portance of addressing scheduling issues in future dynamic verication tools for various concurrency APIs.