# GEM - Overview and Features

Graphical Explorer of MPI Programs (GEM), is a graphical front end for In-situ Partial Order (ISP), a dynamic formal verification tool for MPI C/C++ programs, developed at the University of Utah. GEM greatly enhances the usability of ISP by providing an intuitive graphical way to track down bugs in MPI C/C++ programs, examine post-runtime results and to analyze MPI runtime behavior.

GEM can be used by anyone who can write simple MPI C/C++ programs, and requires no special training. GEM allows you to formally verify your MPI C/C++ programs automatically without any extra efforts on your part. No code instrumentation is necessary. GEM will definitively flag the following errors and warnings:

- Deadlocks
- Functionally Irrelevant Barriers
- MPI Object Leaks
- Local Assertion Violations
- MPI Type Mismatches

### Analyzer View

The Analyzer View is a unique user interface that visually displays the output from the log file that was generated at runtime (by ISP) by highlighting lines representing match sets (p2p and collective send-recv matches) in the source file. It shows both the current MPI call, and any matching point-to-point or collective operation. The Analyzer View also allows the user to examine MPI calls for a particular rank with an easy to use Rank Locking feature.

The Analyzer View offers the user the ability to "step" through execution of the code in debug fashion examining the execution of the MPI calls in the program as they happened at runtime. The user can view this in two different orderings:

- Internal Issue Order - The order in which the MPI calls were issued to the MPI runtime.
- Program Order - The order in which the MPI calls appear in the source code.

The source code analyzer also offers a feature to browse calls by rank and by interleaving as well as the ability to launch the Happens Before Viewer, another visualization tool provided by GEM.

In addition, it helps you understand as well as step through all relevant process interleavings (schedules). Notice our use of the word relevant: even a short MPI program may have too many (an "exponential number") interleavings. For example, an MPI program with five processes, each containing five MPI calls, can have well in excess of 1000 interleavings. However, ISP generates a new interleaving only when it represents a truly new (as yet unexamined) behavior in your MPI program.

### As Examples:

- If an MPI program consisting of two processes issues point-to-point sends and non-wildcard receives to each other, then there is no observable difference (apart from performance or resource consumption) whether the sends are posted before each matching receive or vice versa; in this case, ISP will generate only one interleaving;
- If an MPI program consisting of three processes is such that the second process issues a sequence of wildcard receives, and the first and third process issue point-to-point sends to process two, then the exact non-deterministic choices of matches made at each step may affect the ensuing computation (including the conditional outcomes). In such programs, it is possible to force an exponential number of interleavings. In practice, here is how the results look (these examples come with the ISP distribution).
- For Parmetis [1], a 14,000+ line MPI program that makes 56,990 MPI calls for four ranks and 171,956 calls for eight ranks, ISP needed to examine only one interleaving!
- For many tests in the Umpire test suite [2], conventional MPI testing tools missed deadlocks despite examining many schedules. ISP determined a minimal list of interleavings to examine, finding deadlocks whenever they existed (see our table of results at the URL given under [3]).
- For Madre [4], a naive algorithm can result in n! interleavings. An improved algorithm called POE B, present in the current release of ISP reduces this to one interleaving. Much like with existing partial order [5], ISP does not guarantee a minimal number of interleavings, although it comes pretty close to it.

### Browser View

The Browser View is a highly functional view that summarizes and categorically groups all errors and warnings found by GEM for a particular MPI verification run. The summary label (just above the tabs) gives the user a quick overview of problems found. Errors and warnings are mapped to the corresponding source code lines in the Eclipse editor. The Browser View's tabs help the user to quickly localize and fix MPI errors and warnings flagged by GEM within their source code.

- Deadlocks: This tab allows the user to visit all calls that did not complete due to a detected deadlock.
- Assertion Violations: This tab lists all local assertion violations found. Clicking any one of these will take the user to the line of source code with the failed assertion.
- Leaks: Clicking any of these will take the user to the line of source code where the corresponding un-freed MPI resource was allocated (these are usually MPI communicators and MPI DataTypes).
- Irrelevant Barriers: This tab is reserved for Functionally Irrelevant Barriers. Clicking any these will take the user to the corresponding MPI_Barrier call itself, which can then be safely removed without changing the runtime behavior of the MPI application. This could potentially speed the application up with the absence of unnecessary synchronization.
- Type Mismatches: These are warnings about the send type not matching the receive type. In some cases this may be intentional, but often times it is a programming mistake.

At the top left is a brief summary of the results indicating the number of errors and warnings found. In the top right are buttons provided with the ability to set the number of processes and re-run GEM on the current MPI project.

### How GEM Works:

GEM employs the use of In-situ Partial Order (ISP), the underlying dynamic formal verification tool, to verify MPI C/C++ programs. Here we describe ISP in detail to provide a better understanding of how it works.

ISP works by intercepting the MPI calls made by the target program and making decisions on when to send these MPI calls to the MPI library. This is accomplished by the two main components of ISP: the Profiler and the Scheduler. An overview of ISP’s components and their interaction with the program as well as the MPI library is provided in Figure 1 below.

Figure 1

### Profiler:

The interception of MPI calls is accomplished by compiling the ISP Profiler together with the target program’s source code. The Profiler makes use of MPI’s profiling mechanism (PMPI). Then the Profiler provides its own version of MPI f (replacing the original) for each corresponding MPI function f. Within each of these MPI f , the profiler communicates with the scheduler using TCP sockets to send information about the MPI call the process wants to make. It will then wait for the scheduler to make a decision on whether to send the MPI call to the MPI library or to postpone it until later. When the permission to fire f is given from the scheduler, the corresponding PMPI f will be issued to the MPI run-time. Since all MPI libraries come with functions such as PMPI f for every MPI function f, this approach provides a portable and light-weight instrumentation mechanism for MPI programs being verified [6].

### Scheduler:

The ISP Scheduler helps carry out the POE algorithm. As it turns out, the POE algorithm is based on exploiting MPI’s out-of-order completion semantics. In other words,

- (i) Not all MPI operations issued by a process complete in that order.
- (ii) A proper modeling of this out of-order completion semantics is essential in order to meet goals G1 and G2. For example, two MPI_Isend commands issued in succession by an MPI process P1 to the same target process (say P2) are forced to match in order, whereas if these MPI_Isends are targeted to two different MPI processes, then they may match contrary to the issue order. As another example, any operation following an MPI_Barrier must complete only after the barrier has completed, while an operation issued before the barrier may linger across the barrier, and actually complete after the barrier [6]!

### Description of POE Algorithm:

POE stands for "POR with out-of-order and elusive interleavings"

MPI programs suffer from "elusive" interleavings in the presence of MPI wildcard Receive R(*) . Issuing the MPI sends in different orders does not help as the MPI runtime provides no guarantees based on when the Send is actually issued. POE employs dynamic source re-writing in place of wildcard so that every interleaving explored by POE algorithm is deterministic. Also, the presence of collectives such as `MPI\_Barrier` can cause traditional runtime verification techniques such as "Dynamic Partial Order Reduction" to fail since it is not always possible to issue instructions in different orders in the presence of collectives. POE also addresses this issue by creating "match sets".

POE algorithm works by creating a graph structure with the MPI operations of processes as nodes and by adding Intra-Completes-Before (IntraCB) edges between these nodes. As the name suggests, IntraCB edges are only added between the MPI operations within the MPI processes. The IntraCB edges are added between the MPI operations based on the MPI semantics of the operations. MPI functions like `MPI_Barriers`, `MPI_Wait` etc have the semantics, that no later MPI operations can be issued until these MPI operations complete. We call such operations as fence operations. Note that instructions issued before the fence operations can linger even after the fence operation is complete.

The IntraCB edges are added based on the following rules: Let i and j be the MPI operations of a process P such that i < j (i.e., i comes before j in the program order. There is an IntraCB edge between i and j is one of the following is true:

- i is a fence operation.
- i and j are send operations and the destination of i and j are the same
- i and j are receive operations and the source of i and j are the same
- i is a wildcard receive operation and j is a receive operation.

If there is a path from i to j then i is called the ancestor of j. POE algorithm uses these IntraCB edges to form match-sets to be issued into the MPI runtime. The following is the (informal) algorithm:

An MPI operation is "matched" if it has been issued to the MPI runtime by the POE algorithm.

1. Run the MPI processes until they all reach fence operations.
2. Let e denote the MPI operations of all processes such that for each i ∈ e, all ancestors of i have been matched.
3. Let m denote the match-sets formed out of e as follows:
   - SR-Match: i, j ∈ e such that i and j are send and receive operations where source (destination) of i is equal to the destination (source)j, then 〈 i, j〉 form a match set.
   - SR*-Match If i is a wildcard receive and j1,j2… jn are the matching sends, then create the match-sets as {〈 i, j1〉, 〈 i, j2〉, … 〈 i, jn〉}. Each element of the set is issued as a different interleaving.
   - C-Match: If i1,i2… in are the same collective operation of n processes then 〈 i1, i2, …, in〉 form a match set.
   - W-MatchIf i is an `MPI_Wait`, then 〈 i 〉 forms a match set.
4. Issue the match sets to MPI runtime in the following priority order: C-Match > W-Match > SR-Match > SR*-Match.
5. If any of the processes issued a fence operation then goto step 1. Else, goto step 4.
6. If there are no match sets and all processes have issued `MPI_Finalize`, check if any wildcard match sets are yet to be explored. If yes, then restart the processes and goto step 1, otherwise, exit.
7. If there are no match sets and there is at least one process that has not issued `MPI_Finalize`, then there is a deadlock. Flag a deadlock and kill all the MPI processes.

### Obtaining ISP and Examples

ISP can be downloaded from the Gauss Group’s ISP Release Page.

What you will receive are the full sources as well as the following examples in the directory isp-tests:

- 12 examples pertaining to the Game of Life (in directory life, courtesy of Bill Gropp of UIIC and Rusty Lusk of Argonne from their EuroPVM/MPI 2007 tutorials)
- 74 examples of the Umpire test suite (in directory Umpire), courtesy of Bronis de Supinski from LLNL.
- 12 examples under others developed by various authors.
- 16 examples under madre-0.3 courtesy of Stephen F. Siegel (U. of Delaware) from his Madre release (see our PPoPP 2009 paper).
- The Parmetis 3.1 hypergraph partitioner (see our PPoPP 2009 paper).

### Why the Trident?

Because It is a universal symbol for "slaying the evil bug"!

### References

- [1] ParMETIS - Parallel graph partitioning and fill-reducing matrix ordering.
- [2] Jeffrey S. Vetter and Bronis R. de Supinski. Dynamic software testing of MPI applications with Umpire. In Supercomputing ’00: Proceedings of the 2000 ACM/IEEE Conference on Supercomputing (CDROM). IEEE Computer Society, 2000. Article 51.
- [3] Sarvani Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby. Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In Aarti Gupta and Sharad Malik, editors, CAV, volume 5123 of Lecture Notes in Computer Science. Springer, 2008.
- [4] Stephen F. Siegel. The MADRE web page.
- [5] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2000.
- [6] Anh Vo, Sarvani Vakkalanka, Rajeev Thakur, Michael DeLisi, Ganesh Gopalakrishnan and Robert M. Kirby. Formal Verification of Practical MPI Programs. PPoPP ’09, February 14–18, 2009, Raleigh, North Carolina, USA.

Back to Top | Back to Table of Contents

School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT 84112 * isp-dev@cs.utah.edu
License