Data Race Satisfiability on Array Elements
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910880343523328 |
|---|---|
| author | Shim, Junhyung Mahmud, Quazi Ishtiaque Jannesari, Ali |
| author_facet | Shim, Junhyung Mahmud, Quazi Ishtiaque Jannesari, Ali |
| contents | 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, ThreadSanitizer, and Helgrind+ can detect data races through the execution of the source code. However, source code execution can be quite time-consuming when analyzing computation-intensive programs. There are also static analysis tools such as LLOV, and OpenRace. These tools statically detect data races using algorithms that often do not require the execution of the source code. 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 applying automatic 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_13864 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Data Race Satisfiability on Array Elements Shim, Junhyung Mahmud, Quazi Ishtiaque Jannesari, Ali Distributed, Parallel, and Cluster Computing D.2.4 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, ThreadSanitizer, and Helgrind+ can detect data races through the execution of the source code. However, source code execution can be quite time-consuming when analyzing computation-intensive programs. There are also static analysis tools such as LLOV, and OpenRace. These tools statically detect data races using algorithms that often do not require the execution of the source code. 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 applying automatic 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. |
| title | Data Race Satisfiability on Array Elements |
| topic | Distributed, Parallel, and Cluster Computing D.2.4 |
| url | https://arxiv.org/abs/2503.13864 |