.png){kind=icon}
返回
Data Race Satisfiability on Array Elements
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-06343-4_8.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
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 DRSoNE (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/JShimCS/ompdart-DRS- extension.
期刊
O
机构
引用论文
.png){kind=icon}
分享收藏
分享收藏
查看更多内容