Practical Formal Verification of MPI and Thread Programs
Organizers
Ganesh Gopalakrishnan, Robert M. Kirby, Sarvani Vakkalanka, Anh Vo, and Yu Yang
School of Computing, University of Utah, Salt Lake City, UT 84112

1  Introduction

This webpage offers the contents of a full-day hands-on tutorial on the principles of MPI as well as dynamic formal verification of MPI programs. It is offered using our dynamic formal verifier for MPI programs, namely ISP, which stands for In-Situ Partial order. This tutorial also has a segment on Inspect, our dynamic formal verification tool for Pthread C programs. We will also present ISP’s Eclipse-based Graphical User Interface for intuitive interactions with the tool. This tutorial was given most recently on September 7th (Full Day) at Espoo, Finland, during the EuroPVM/MPI 2009 conference. We can easily shorten this tutorial to occupy a half-day.

2  Material for the Tutorial

2.1  Slides

The latest slides for the ISP tutorial are found in these files

2.2  Tutorial Notes

A report covering the tutorial is given in this PDF document.

You will find the following supportive material also:

2.3  LiveDVD

At the tutorial, we will provide you with a complete bootable disk (called LiveDVD) containing the entire ISP and Eclipse code, and all our exercises. You may download the ISO from HERE and burn your own DVDs before you come in. After you get your DVD containing this ISO, here is how you boot into Windows or MAC (and get back to your machine once done!):

Windows:
MacBook:

3  Other Material

3.1  Eclipse Code

The Eclipse plug-in for ISP and associated download instructions and documentation are available from this site.

3.2  Email Help

Send an email to isp-dev@cs.utah.edu for any sort of help with ISP.

3.3  ISP Case Studies

A number of case studies are available at our ISP Examples site.

Also, please also check out these studies by Simone Atzeni of how our tool ISP “took a midterm-exam and passed it well!” It also took on some challenge problems!

4  Detailed Description of the Tutorial

With the increased use of parallelism in the design of shared memory and distributed message passing programs, designers needs verification tools that can increase their productivity and help them converge on efficient and correct concurrent programs faster. This can be achieved by providing designers a debugger-like design environment that can analyze the runs of a given program and obtain formal guarantees against classes of bugs such as deadlocks, assertion violations, resource leaks, and races. In a practical sense, the kind of guarantees that one can hope for in a concurrent program are: for a given test harness, it does not have any of these bugs. Even to achieve such guarantees, verification tools must intelligently, and parsimoniously, enumerate the concurrent schedules of the program, and be able to manifest a schedule that is possible on some platform (not necessarily the one on which verification is being run). This is because (i) even a simple five-process program with five ‘steps’ can interleave in over 10 Billion ways, and (ii) a testing tool can get stuck in a subset of these interleavings.

This tutorial presents two tools that help achieve this for shared memory thread programs and MPI (message passing) programs. The emphasis of this tutorial (about 70% time-wise) will be on MPI – the lingua franca for distributed high performance computing. However, given the increasing use of threading along with message passing, we will cover that category also for the remaining time. Our MPI formal verification tool is called ISP and the thread formal verification tool is called Inspect. We use the term formal verification in the most practical connotation possible: run the code under the mercy of a verification scheduler such that it can issue rigorous guarantees when the run finishes without errors.

Previous tools have employed various methods for bounding the number of interleavings as well as enforcing interleavings that would not naturally occur on a testing platform. In our research, we employ less ‘chancy’ versions of these techniques. We directly run (instrumented versions of) the user’s code using a verification scheduler. Specifically, the scheduler of Inspect (our dynamic program verifier) tracks operation dependencies in each execution, and replays an execution in order to enforce a different interleaving if it contains one interleaving where two globals are concurrently accessed in a non-commuting fashion. The ISP scheduler delays operations that may complete out-of-order (according to the MPI standard) in order to discover the maximal extent of non-deterministic commnications possible. It then makes sure that the runtime will carry out all these non-deterministic commnications. It omits communications that commute. The tutorial will cover these algorithms at a high level and demonstrate the workings of these tools on real examples to lend further insights. It will also point out the capacity limits of ISP and Inspect, how they may be overcome, and how these tools naturally blend into existing semi-formal and conventional verification flows.

4.1  Topics

See the slides for the latest overview:

ISP for MPI (Message Passing):
Inspect for shared memory threads:

4.2  Audience Background Assumed

We have successfully taught the above material in an undergraduate (senior) computer science and electrical engineering class. Thus, no special background besides knowledge of concurrency and familiarity with debugging is being assumed.

5  Students behind ISP and Inspect

The ISP effort was spearheaded by our PhD student Sarvani Vakkalanka. Under her leadership, ISP and all its formalization and dynamic verification algorithms took shape. Anh Vo and Michael DeLisi joined forces with Sarvani and significantly advanced ISP, really making it and its distribution and use into a reality. Other students who have played a significant role in ISP’s development include: Subodh Sharma, Sriram Aananthakrishnan, Simone Atzeni, Alan Humphrey, Chris Derrick, Jason Williams, Grzegorz Szubzda, Geof Sawaya, and Guodong Li. We also acknowledge Robert Palmer and Salman Pervez for their contributions toward our getting started on MPI Formal Verification. ISP could never have become a reality without their work, and ISP continues to advance thanks to them. Sincere thanks to Rajeev Thakur, Bill Gropp, Rusty Lusk, and Steve Siegel for their constant encouragement. ISP’s Eclipse GUI is thanks to Beth Tibbits’s (IBM) constant help and encouragement.

All versions of Inspect were created by Yu Yang for his PhD. Yu works for Microsoft now. We also acknowledge Xiaofang Chen and Grzegorz Szubzda’s help with Inspect. We thank Chao Wang, Vineet Kahlon, and Aarti Gupta of NEC Research for their support.

6  Organizer Bios

Ganesh Gopalakrishnan received his PhD in Computer Science from Stony Brook University in 1986, and joined the faculty at the School of Computing, University of Utah, the same year. He spent a year each at the University of Calgary (1988), Stanford University (1995), and Intel, Santa Clara (2002). His 2009 sabbatical will be on developing a Concurrency Curriculum in collaboration with Microsoft Research. His interests are generally in the area of applying formal specification and verification methods to practical situations involving concurrency. Much of his recent work has been on dynamic formal verification methods for MPI programs, resulting in the ISP tool. He also worked on dynamic verification of thread programs, and has recently begun a project on dynamic verification of MCAPI (multicore communications API) program. His research group continues to contribute toward formal verification of cache coherence protocols, shared memory models, partial order reduction methods, and parallel/distributed model checking. He currently advises many graduate and undergraduate students, has authored “Computation Engineering: Applied Automata Theory and Logic (Springer, 2006),” and has written over 120 research papers. His research is supported by Microsoft, NSF, and SRC under various grants.

Robert M. (Mike) Kirby is an Associate Professor of Computer Science, Adjunct Associate Professor of Mathematics and Adjunct Associate Professor of Bioengineering at the University of Utah. He is both a faculty member in the School of Computing and the Scientific Computing and Imaging Institute at Utah. He received the Sc.M. degree in Applied Mathematics, the Sc.M. degree in Computer Science, and the Ph.D. degree in Applied Mathematics from Brown University, Providence, RI, in 1999, 2001, and 2002, respectively. His research focus is on large-scale scientific computing and visualization, with an emphasis on the scientific cycle of mathematical modeling, computation, visualization, evaluation, and understanding. His primary research interests include: Computational Science and Engineering Applications, Algorithm Development and Application of High-Order Methods, Scientific Visualization, Verification and Application of Concurrent Programming, and High Performance Computing.

The organizer’s approach to this tutorial will be to emphasize the problem to be solved (namely hunt bugs) and introduce just enough formal methods to appreciate how the tools are able to effect searches that are parsimonious. The attendees will be able to take the LiveDVDs with them (as well as download the full sources of our tools later).

7  Funding Acknowledgements

This research was supported by Microsoft, NSF “CSR-SMA: Toward Reliable and Efficient Message Passing Software Through Formal Analysis,” “CPA-DA: Formal Methods for Multi-core Shared Memory Protocol Design,” and “MCDA: Formal Analysis of Multicore Communication APIs and Applications,” and by SRC Task ID TJ 1847.001 “Formal Specification, Verification, and Test Generation for Multi-core CPUs,” August 2008, and and Task ID TJ 1993, “MCDA: Formal Analysis of Multicore Communication APIs and Applications.”


This document was translated from LATEX by HEVEA.