Abstract
Among the most common and hardest to debug types of bugs in concurrent systems are data races. In this paper, we present an approach for verifying that an OpenMP program is data race free. We use polyhedral analysis to verify those parts of the program where we detect parallel affine loop nests. We show the applicability of polyhedral analysis with analysis-enabling program transformations for data race detection in HPC applications. We evaluate our approach with the dedicated data race benchmark suite DataRaceBench and the LLNL Proxy Application AMG2013 which consists of 75,000 LOC. Our evaluation shows that polyhedral analysis can classify 40% of the DataRaceBench 1.2.0 benchmarks as either data race free or having data races and verify that 41 of the 114 (36%) loop nests of AMG2013 are data race free.
