Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Data Race Satisfiability on Array Elements

Junhyung Shim, Quazi Ishtiaque Mahmud, Ali Jannesari

TL;DR

This work tackles data races in OpenMP programs, focusing on array-element races that are harder to detect than scalar races. It introduces DRS-oNE, a static detector that encodes race constraints and solves them with the SMT solver $z3$ to determine feasibility of conflicting accesses within a parallel loop. Building on OMPDart and an AST-CFG representation, DRS-oNE augments traditional race constraints with static information about integer variables to prune infeasible paths, thereby reducing false positives. Benchmarks on a subset of DataRaceBench show that DRS-oNE achieves high precision, offering a reliable static complement to existing dynamic and static tools and supporting use cases like verifying auto-parallelization guided by AI models.

Abstract

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.

Data Race Satisfiability on Array Elements

TL;DR

This work tackles data races in OpenMP programs, focusing on array-element races that are harder to detect than scalar races. It introduces DRS-oNE, a static detector that encodes race constraints and solves them with the SMT solver to determine feasibility of conflicting accesses within a parallel loop. Building on OMPDart and an AST-CFG representation, DRS-oNE augments traditional race constraints with static information about integer variables to prune infeasible paths, thereby reducing false positives. Benchmarks on a subset of DataRaceBench show that DRS-oNE achieves high precision, offering a reliable static complement to existing dynamic and static tools and supporting use cases like verifying auto-parallelization guided by AI models.

Abstract

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.

Paper Structure

This paper contains 19 sections, 18 figures, 3 tables, 3 algorithms.

Table of Contents

  1. INTRODUCTION
  2. RELATED WORK
  3. Race Detection using Polyhedral Model
  4. Race Detection through multiple Analyses
  5. Race Detection using LLMs
  6. Race Detection through Dynamic Analysis
  7. Race Detection through Constraint Solving and Symbolic Execution
  8. MOTIVATING EXAMPLES
  9. RACE CONSTRAINT
  10. IMPLEMENTATION
  11. Usage
  12. Workflow of DRS
  13. Locating the Target Loop
  14. SMT Variables & Constraints Encoder
  15. Z3-Python Script Writer
  16. ...and 4 more sections

Figures (18)

  • Figure 1: Data race on an array element
  • Figure 1: Workflow diagram of DRS-oNE
  • Figure 2: FP1 - False Positive Case-1 resulting from Infeasible Path
  • Figure 3: Simplified View of What OpenRace would Analyze for FP1
  • Figure 4: FP2 - False Positive Case-2 resulting from Infeasible Path
  • ...and 13 more figures