Using Polyhedral Analysis to Verify OpenMP Applications are Data Race Free
Citations Over TimeTop 10% of 2018 papers
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.
Related Papers
- → Studying the advancement in debugging practice of professional software developers(2016)104 cited
- → Using submission log data to investigate novice programmers’ employment of debugging strategies(2023)9 cited
- → Studying the Advancement in Debugging Practice of Professional Software Developers(2014)14 cited
- → The Debugging of Rule Bases(2009)5 cited
- → Design of Scan Cell for System on Chip Scan Based Debugging Applications(2017)1 cited