<span class="var-sub_title">Using Polyhedral Analysis to Verify OpenMP Applications Are Data Race Free</span> SC18 Proceedings

The International Conference for High Performance Computing, Networking, Storage, and Analysis

2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018)


Using Polyhedral Analysis to Verify OpenMP Applications Are Data Race Free

Authors:

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.

Archive Materials


Back to 2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018) Archive Listing

Back to Full Workshop Archive Listing