Symbolic Analysis of Concurrency Errors in OpenMP Programs

Symbolic Analysis of Concurrency Errors in OpenMP Programs Presented by : Steve Diersen Contributors: Hongyi Ma, Liqiang Wang, Chunhua Liao, Daniel Quinlen, and Zijiang Yang University of Wyoming Department of Computer Science 1

Outline Motivation Overview Encoding Experiments Summary

Motivation To detect concurrency errors within OpenMP programs. – Specifically data race errors. To reduce the number of false positives and false negatives during detection. To reduce the analysis time in determining concurrency errors. 3

Motivation Example 1: #pragma omp parallel for for (i 1; i 1000; i) x[i] x[i] x[i-1]; Example 2: #pragma omp parallel shared(b) private(errors) { for(i 0; i 10; i) dt[i] b dt[i] * 5; errors dt[9] 1; } 4

Motivation Example 3: #pragma omp parallel { /* Obtain thread number */ tid omp get thread num(); /* Only master thread does this */ if (tid 0) { nthreads omp get num threads(); printf("Number of threads %d\n", nthreads); } printf("Thread %d is starting.\n",tid); }; 5

Motivation Example 3: #pragma omp parallel private(tid) { /* Obtain thread number */ tid omp get thread num(); /* Only master thread does this */ if (tid 0) { nthreads omp get num threads(); printf("Number of threads %d\n", nthreads); } printf("Thread %d is starting.\n",tid); }; 6

Motivation Why do we need analysis tools? Simple programming errors. Large programs with many lines of code. How should an analysis tools work? They should be automated and correct. 7

Motivation Typical Analysis is either: Static Analysis – performed without executing a program. It examines all possible execution paths and variable values in an inaccurate and conservative way. Dynamic Analysis – tests and evaluates an application during runtime. It reveals subtle defects or vulnerabilities whose causes are hard to be discovered by static analysis. 8

Overview OAT is a symbolic analysis tool for detecting data races in a shared memory model (OpenMP). 9

Overview The Benefits of the Symbolic Analysis approach: Schedule order simulation Simulated stack traces Reduces false positives and false negatives 10

Encoding Encoding is only done for OpenMP parallel constructs. Static Single Assignment (SSA) is used to track variables involved in multiple assignments. Dynamic scheduling is simulated using a timing order encoding. Loops can be encoded with loop bound or without loop bound. 11

Encoding A typical variable encoding looks like: The timing order is encoded by is the variable is the SSA subscript is the thread Then represents the value of index in thread at SSA 12

Encoding Schedule order in OpenMP int i, j; #pragma omp parallel for for( i 0; i N; i ) for( j 0; j N; j ) a[i][j] foo(i, j ); 13

Encoding Schedule order in OpenMP i is private int i, j; #pragma omp parallel for for( i 0; i N; i ) for( j 0; j N; j ) a[i][j] foo(i, j ); j is shared! 14

Encoding Schedule order in OpenMP i is private int i, j; #pragma omp parallel for for( i 0; i N; i ) for( j 0; j N; j ) a[i][j] foo(i, j ); j is shared! order Thread1 0 Load i 1 Swap out Thread2 2 Load i 3 Load j (j 0) 4 Call foo(i,j) 5 j 6 Swap out 7 load j (j 1) 15

Encoding Schedule order in OpenMP i is private int i, j; #pragma omp parallel for for( i 0; i N; i ) for( j 0; j N; j ) a[i][j] foo(i, j ); j is shared! j 0 is correct! order Thread1 0 Load i 1 Swap out Thread2 2 Load i 3 Load j (j 0) 4 Call foo(i,j) 5 j 6 Swap out 7 load j (j 1) 16

Encoding Schedule Ordering Encoding 17

Encoding Schedule Ordering Encoding 18

Encoding Schedule Ordering Encoding 19

Encoding Loops Without Loop Bound: Detects over-write conflicts and write-read conflicts Requires less analysis time than with loop bound May produce false positives and/or false negatives With Loop Bound: Detects data races that depend upon the number iterations Requires significantly more encoding; resulting in longer analysis times. 20

Encoding OpenMP For Loop Without Loop Bound Encoding 21

Experiments Experiments were run by injecting errors into some NAS parallel benchmarks and OpenMP source repository code. Experiments were also conducted on student homework assignments. The following slides show results from our experiments. 22

Experiments Data races were injected into the benchmarks in the following manner: By flipping the data-sharing attributes of variables Switching private for shared or visa versa By adding updating statements Adding a random write-read statement such as b b*2 23

Experiments CODE – test source code LOC – lines of code DR – data race injections OAT – OpenMP Analysis Toolkit PVS – Viva64 from PVS Studio ITC – Intel Thread Checker STA – Sun Thread Analyzer 24

Experiments 25

Experiments 26

Summary Our Symbolic Analysis approach was able to find all data races in our experiments. OAT had no false positives or false negatives. Our analysis time was faster than the dynamic analysis tools. For two threads our tool was faster than Viva64 27

Thank you Contact information: Hongyi Ma : [email protected] Steve Diersen : [email protected] University of Wyoming, Computer Science Department