Barrier Matching for Programs with Textually Unaligned Barriers:

Barrier Matching for Programs with Textually Unaligned Barriers Yuan Zhang and Evelyn Duesterwald
Dec. 2006

Agenda:

Agenda Motivation
Analysis overview
Multi-valued expressions analysis
Barrier expression tree
Barrier Matching
Experimental results
Conclusions and future work

Motivation:

Motivation Barriers synchronize a set of processes (threads) in an SPMD model (MPI, OpenMP, etc.).
Misplacement of barriers may cause stalls. main(){
int x = 0;
int rank = get_rank();
……
S1: if (rank ==0){
……
} else {
……
barrier; // b1
} S2: if (x andgt; 0){
……
} else {
……
barrier; // b2
}
} stall Not a stall

Barrier Analysis:

Barrier Analysis Parallel program checking tool
Inter-procedural analysis
Barrier Matching Problem: Barriers in an SPMD program are well-matched if all concurrent paths from program start to program exit contain the same number of barriers.

Analysis Overview:

Analysis Overview Step 1: (Prerequisite) Multi-valued expressions analysis
An expression is multi-valued if it evaluates differently in difference processes.
If used as a predicate, a multi-valued expression splits processes into different concurrent program paths.
Intuition: unaligned barriers in concurrent paths cause stalls
Step 2: Barrier expression trees
A barrier expression at program point P describes the sequence of barriers that may execute until a process reaches P.
Step 3: Barrier matching
- Check barrier expressions to determine whether the number of barriers along concurrent paths is the same
Output: verified or error with a counter example

Scope of Analysis:

Scope of Analysis We assume structured programs (without goto statements).
We transform every program into a structured program using goto elimination.
We assume 'structurally correct' programs.
Break down the analysis problem into a series of smaller programs, one for each structured component.
We are more conservative for structurally incorrect programs.
Conservative and safe

Structural correctness:

Structural correctness Let T be the AST (Abstract Syntax Tree) of a structured program P, P is structurally correct with respect to property Prop if each subtree of T is structurally correct with respect to Prop. rank = get_rank();
if (rank andgt; n) {
f (n);
barrier;
}
if (rank andlt;= n) {
g (n);
barrier;
} Structurally incorrect but well matched Structurally correct, and well matched rank = get_rank();
if (rank andgt; n) {
f (n);
barrier;
} else {
g (n);
barrier;
} We haven’t found any structurally incorrect but well-matched programs in practice.

Agenda:

Agenda Motivation
Analysis overview
Multi-valued expressions analysis
Barrier expression tree
Barrier Matching
Experimental results
Conclusions and future work

Multi-valued Expressions Analysis:

Multi-valued Expressions Analysis A multi-valued expression evaluates differently in different processes.
Multi-valued seed expressions: process (thread) ID (obtained by calling MPI_Comm_rank(andlt;communicatorandgt;) in MPI, or omp_get_thread_num() in OpenMP).
All multi-valued expressions are directly or indirectly dependent on multi-valued seed expressions
A forward slicing problem
Given a program point p and a variable v, determine a set of statements that are affected by the value of v at point p.
Solved based on a program dependence graph (data dependence + control dependence) [1].

Example:

Example rank andgt; 2 i = 0 i = 1 i andgt; 0 i andgt; 1 barrier barrier i andgt; 0 seed rank = 1 2 3 4 5 6 7 8 9 10 11 12 entry 1 2 11 12 3 4 5 6 7 8 9 10 Control dependence edge data dependence edge

Example:

Example Traditional forward slice covers all expressions. rank andgt; 2 i = 0 i = 1 i andgt; 0 i andgt; 1 barrier barrier i andgt; 0 seed rank = 1 2 3 4 5 6 7 8 9 10 11 12 entry 1 2 11 12 3 4 5 6 7 8 9 10 Control dependence edge data dependence edge seed

What is the problem ?:

What is the problem ? rank andgt; 2 i = 0 i = 1 i andgt; 0 i andgt; 1 barrier barrier i andgt; 0 seed rank = 1 2 3 4 5 6 7 8 9 10 11 12 entry 1 2 11 12 3 4 5 6 7 8 9 10 Control dependence edge data dependence edge seed Multi-valued after processes merge Overestimation: Single-valued for executing processes Traditional forward slicing may overestimate multi-valued expressions.

What is the problem ?:

3 What is the problem ? rank andgt; 2 i = 0 i = 1 i andgt; 0 i andgt; 1 barrier barrier Φ (i) i andgt; 0 seed rank = 1 2 3 4 5 6 7 8 9 10 11 12 data dependence edge 1 2 3 12 4 5 6 7 8 9 10 seed 11 Φ edge, from Φ-gate to Φ We need edges from multi-valued predicates to the points where the values of variables that are control dependent on the predicates merge – Φ edges

Algorithm:

Algorithm Build CFG
Insert Φ nodes and Φ gates
Build dependence graph and use Φ edges in place of control dependence edges
Mark multi-valued seed expressions
Compute the inter-procedural forward slicing[2]
flow-sensitive and context-sensitive

Special Issues:

Special Issues Handling pointers and Arrays
model the array as a single object
treat andamp; and * operations as multi-valued
Handling libraries
Assume thread libraries are annotated as either single- or multi-valued
Other libraries are single-valued.

Agenda:

Agenda Motivation
Analysis overview
Multi-valued expressions analysis
Barrier expression tree
Barrier Matching
Experimental results
Conclusions and future work

Barrier Expressions:

Barrier Expressions A barrier expression at a program point p represents the sequences of barriers that may execute along any path from the beginning of the program to point p.
It is represented as a binary tree
It can be built from the path expression[3]
Barrier Matching Problem (rephrased): A barrier tree t is well-matched if all concurrent barrier sequences that can be derived from t have the same number of barriers.

Barrier Expression Construction:

Barrier Expression Construction if (multi-valued){
barrier b1
} else {
barrier b2
} || b1 b2 BE = b1 || b2 if (single-valued){
barrier b1
} else {
barrier b2
} | b1 b2 BE = b1 | b2 b1 b2 Barrier b1
Barrier b2 * b1 BE = b1 * While (cond) {
barrier b1
} Example program Operator Barrier tree concatenation alternation Concurrent alternation quantification

Fixed Length Barrier Tree A barrier tree t is called a fixed length tree if all barrier sequences derivable from t have the same number of barriers.
If a tree is fixed-length then all its subtrees are fixed-length.

Barrier Matching Conditions:

Barrier Matching Conditions A barrier tree is well-matched if and only if the following two conditions are satisfied:
t contains no concurrent quantification subtrees
all concurrent alternation subtrees are fixed-length

Fixed-length Calculation Rules:

cnt (t) = 1 cnt (t) = 0 cnt (t) = cnt (Tp) cnt (t) = cnt (t1) + cnt(t2) cnt (t) = cnt (t) + T = T
If t is a concurrent tree, report warning b Ø Tp Fixed-length Calculation Rules

Counter Example || | | b1 b2 b3 b4 Ø For each subtree of an error concurrent alternation tree t, calculate the longest and shortest barrier sequences
choose two sequences with different length from t’s two subtrees [ 1, 1 ] [ 0, 0 ] [ 1, 1 ] [ 1, 1 ] [ 1, 1 ] [ 0, 1 ] [ 2, 2 ] [ 1, 2 ] Four possible sequences with length 0, 1, 1, 2

Agenda:

Agenda Motivation
Analysis overview
Multi-valued expressions analysis
Barrier expression tree
Barrier Matching
Experimental results
Conclusions and future work

Experiments:

Experiments Implemented as part of the Eclipse Parallel Tools Platform (PTP) project (www.eclipse.org/ptp).
MPI+C on top of Eclipse CDT(C Development Tool)
Special treatment for MPI
Communicator: each communicator is treated separately
Broadcast: the broadcasted value is single-valued

Benchmarks and Results:

Benchmarks and Results No Spurious Warning !

Related Work:

Related Work 'Barrier Inference' by Aiken and Gay [4]
Based on a set of inference rules
Assumes programmer annotations to describe the effect of procedures
Model checking [5]
Don’t assume the structural correctness
expensive

Future work:

Future work Extend to other collective communications (e.g. broadcast, allreduce, allgather, …)
Match send/recv in MPI
Key issue:
How to match the source and the destination?
How to handle tags?
Optimization:
transform send/recv that is executed by every process into a collective communication?

Conclusions:

Conclusions Problem: verify barrier synchronizations in SPMD programs so as to detect potential deadlocks
Approach: combination of program slicing and path expressions
Results: No spurious warning on 7 libraries/applications
Accessibility: open source to Eclipse CDT

Acknowledgment:

Acknowledgment Beth Tibbitts for her help with the Eclipse implementation

References:

References Karl J. Ottenstein and Linda M. Ottenstein. The program dependence graph in a software development environment. Software Engineering Notes, 9(3), 1984
Susan Horwitz, Thomas Reps, and David Binkley. Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems, 12(1):26-60, Jan. 1990
Robert E. Tarjan. Fast algorithms for solving path problems. Journal of the ACM, 28(3): 594-614, July 1981
Alexander Aiken and David Gay. Barrier inference. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 342-354, 1998
Stephen F. Siegel and George S. Avrunin. Modeling wildcard-free mpi programs for verification. In Proceedings of the 10th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 95-106, 2005

You do not have the permission to view this presentation. In order to view it, please
contact the author of the presentation.

Send to Blogs and Networks

Processing ....

Premium member

Use HTTPs

HTTPS (Hypertext Transfer Protocol Secure) is a protocol used by Web servers to transfer and display Web content securely. Most web browsers block content or generate a “mixed content” warning when users access web pages via HTTPS that contain embedded content loaded via HTTP. To prevent users from facing this, Use HTTPS option.