Description of POE

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 j₁,j₂… j_n are the matching sends, then create the match-sets as {⟨ i, j₁⟩, ⟨ i, j₂⟩, … ⟨ i, j_n⟩}. Each element of the set is issued as a different interleaving.
   • C-Match: If i₁,i₂… i_n are the same collective operation of n processes then ⟨ i₁, i₂, …, i_n⟩ 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 atleast one process that has not issued MPI_Finalize, then there is a deadlock. Flag a deadlock and kill all the MPI processes.

ADDITIONAL DETAILS: Additional details of POE algorithm can be found here.

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