Using Polyhedral Analysis to Verify OpenMP Applications Are Data Race Free
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 for data race detection in HPC applications by evaluating our approach with the dedicated data race benchmark suite DataRaceBench and the LLNL Proxy Application AMG2013. 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. AMG2013 consists of 75,000 LOC.
Back to 2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018) Archive Listing
Back to Full Workshop Archive Listing