Detection of data races is one of the most important tasks for verifying the correctness of OpenMP parallel codes. Two main models of analysis tools have been proposed for detecting data races: dynamic analysis and static analysis. Dynamic analysis tools such as Intel Inspector and Helgrind \(^+\) can detect data races through instrumentation of the binary of the target program. Likewise, ThreadSanitizer, a dynamic analysis tool, detects data races through the instrumentation of the target program’s LLVM-IR. However, executing an instrumented program can be quite time-consuming when analyzing a computation-intensive program. There are also static analysis tools such as LLOV, and OpenRace. These tools statically detect data races using algorithms that often do not require instrumentation of the binaries or the IR. Although both detection techniques assist programmers in analyzing the correct behavior of OpenMP programs, they still produce false positives that often defeat the purpose of deploying them for code analysis. Therefore, we present DRS-oNE (Data Race Satisfiability on aNy Element), a data race detector that detects data races on array elements by solving for race constraints with the Z3 SMT solver. DRS-oNE is available at https://github.com/JShim-CS/ompdart-DRS-extension .

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Data Race Satisfiability on Array Elements

  • Junhyung Shim,
  • Quazi Ishtiaque Mahmud,
  • Ali Jannesari

摘要

Detection of data races is one of the most important tasks for verifying the correctness of OpenMP parallel codes. Two main models of analysis tools have been proposed for detecting data races: dynamic analysis and static analysis. Dynamic analysis tools such as Intel Inspector and Helgrind \(^+\) can detect data races through instrumentation of the binary of the target program. Likewise, ThreadSanitizer, a dynamic analysis tool, detects data races through the instrumentation of the target program’s LLVM-IR. However, executing an instrumented program can be quite time-consuming when analyzing a computation-intensive program. There are also static analysis tools such as LLOV, and OpenRace. These tools statically detect data races using algorithms that often do not require instrumentation of the binaries or the IR. Although both detection techniques assist programmers in analyzing the correct behavior of OpenMP programs, they still produce false positives that often defeat the purpose of deploying them for code analysis. Therefore, we present DRS-oNE (Data Race Satisfiability on aNy Element), a data race detector that detects data races on array elements by solving for race constraints with the Z3 SMT solver. DRS-oNE is available at https://github.com/JShim-CS/ompdart-DRS-extension .