Data races pose a serious threat to the correctness of concurrent programs. Traditional model-checking-based race detection techniques typically encode race detection as assertion verification, but this introduces substantial overhead due to numerous auxiliary variables and statements. In this paper, we present a precise modeling of data races based on event-level ordering constraints, which avoids any instrumentation while capturing the exact semantics and covering all potential race occurrences within the given bounded scope. We integrate it into a concurrent program verification framework and prove its correctness. Moreover, we enhance the existing theory solvers for ordering consistency theory with two new components, enabling effective reasoning about data races. Finally, we introduce an encoding optimization that leverages the novel concept of value-critical events to eliminate redundant value constraints. We implement our approach in a prototype tool, Deagle-DR, and compare it against state-of-the-art tools, including Dartagnan, Ugemcutter, Cseq-DR, LaDR, and Iekke. Experiments show that our approach is competitive with state-of-the-art methods.

@inproceedings{paperbot12581,
  title = {Precise and Efficient Static Data Race Detection},
  author = {Pei Wang and Zhihang Sun and Fei He},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3837438}
}