barrier

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

Slide19: 

main(){ if (single-valued){ while (single-valued) p(); } else { if (multi-valued) barrier; // b1 else q(); } } p(){ if (multi-valued){ barrier; //b2 …… barrier; //b3 } else { barrier; //b4 …… barrier; //b5 } } q(){ if (multi-valued){ barrier; //b6 } else { barrier; //b7 } } | * || Tp b1 Tq b2 b3 b4 b5 || b6 b7 || Tmain = (Tp)* | ( b1 || Tq) Tp = (b2 . b3) || (b4 . b5) Tq = b6 || b7

Fixed Length Barrier Tree: 

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

Slide23: 

main(){ if (single-valued){ while (single-valued) p(); } else { if (multi-valued) barrier; // b1 else q(); } } p(){ if (multi-valued){ barrier; //b2 …… barrier; //b3 } else { barrier; //b4 …… barrier; //b5 } } q(){ if (multi-valued){ barrier; //b6 } else { barrier; //b7 } } | * || Tp b1 Tq b2 b3 b4 b5 || b6 b7 || Tmain = (Tp)* | ( b1 |c Tq) Tp = (b2 . b3) |c (b4 . b5) Tq = b6 |c b7 [ 1 ] [ 1 ] [ 1 ] [ 1 ] [ 1 ] [ 1 ] [ 1 ] [ 2 ] [ 2 ] [ 2 ] [ 1 ] [ 1 ] [ 2 ] [ T ] [ T ] [ 1 ]

Counter Example: 

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