OVERVIEW:

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.

HIGHLIGHTS:

ISP for MPI (Message Passing):

• Overview of bug classes in MPI programs (from the literature, experience)
• Overview of pedagogy of MPI (how it is taught)
• Introduction to ISP and demo of how it can help develop MPI programs, using formal verification to serve as safety net
• In-depth view of ISP including its algorithms
• LiveCD based exercise (e.g., the development of parallel matrix multiplication algorithms)
• Visualizing ``non-obvious'' behaviors of MPI construct using ISP's GUIs (including probes, wildcard non-determinism, etc.) for better debugging
• Demo of three ISP GUIs:
  • Java based,
  • Visual Studio based,
  • Eclipse-based based.

Inspect for shared memory threads:

• Overview of bug classes in Pthread programs (from the literature, experience)
• Overview of pedagogy of threading
• Introduction to Inspect and demo of how it can help develop thread programs. Use of simple text-book examples.
• LiveCD demo of Inspect on the verification of producer/consumer codes, work-stealing queues, etc.

AUDIENCE BACKGROUND:

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.

SLIDES:

For a preliminary set of our slides, please see

http://www.cs.utah.edu/formal_verification/europvm09-tutorial-mpi-threading-fv/europvm09-tutorial-mpi-threading-fv.pptx

or

http://www.cs.utah.edu/formal_verification/europvm09-tutorial-mpi-threading-fv/europvm09-tutorial-mpi-threading-fv.pdf

ORGANIZER BIO:

Ganesh Gopalakrishnan got 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 interests are generally in the area of applying formal specification and verification methods to practical situations involving concurrency. His recent work includes: formal verification of cache coherence protocols, shared memory models, model checking methods for message passing interface (MPI) programs and thread programs, partial order reduction methods, and annotation based parallelization (e.g., OpenMP). He currently advises many graduate and undergraduate students, recently authored "Computation Engineering: Applied Automata Theory and Logic (Springer)" and has written over 120 research papers. His research is supported by Microsoft, NSF, and SRC under various grants.

Robert (Mike) Kirby ...

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 LiveCDs with them (as well as download the full sources of our tools later).

This document was translated from L^AT_EX by H^EV^EA.