Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version)

Extending the digest framework to thread barriers, pthread_once, and ancestor locksets

Daniel Bund; Julian Erhard; Michael Petter; Michael Schwarz· 2026· DOI 10.48550/arXiv.2609.00246

The core problem

Static data race detection is a cornerstone of concurrent program verification, yet existing analyses often ignore synchronization constructs that fall outside the common lock/unlock and thread-creation patterns. The authors identify a gap: maintaining an abstraction of the execution history of threads can improve precision, but current frameworks do not model thread barriers or `pthread_once`, which are widely used in practice to coordinate phases and one-time initialization. This work extends the **digest** framework—a static analysis framework for data race detection—to incorporate these constructs. The central research question is whether handling such "off the beaten path" synchronization mechanisms can be done without sacrificing soundness or scalability, and how existing state-of-the-art tools compare. The paper also proposes a suite of litmus tests to systematically evaluate analyses for these features, providing a benchmark for future work. The extended version includes additional details and proofs omitted from the conference version.

Innovation

The evaluation focuses on two aspects: (1) the ability of the extended digest framework to handle barriers and `pthread_once`, and (2) a comparison with existing state-of-the-art static race detectors. The authors implemented their extensions and ran them on the litmus test suite. Key findings include: - The extended framework successfully detects races in programs using barriers and `pthread_once`, while maintaining soundness. For example, in a test where two threads access a shared variable without proper synchronization around a barrier, the analysis reports a race; when the barrier is correctly used, it reports no race. - The ancestor lockset abstraction improves precision in cases where a child thread accesses data protected by a lock held by its parent. Without this abstraction, such accesses might be falsely flagged as races. - **Comparison with state-of-the-art tools**: The authors evaluated several popular static race detectors (e.g., based on lockset analysis, happens-before analysis, or hybrid approaches). None of them support thread barriers or `pthread_once` out of the box. When these constructs appear in the code, the tools either ignore them (leading to false positi

Static data race detection is a cornerstone of concurrent program verification, yet existing analyses often ignore synchronization constructs that fall outside the common lock/unlock and thread-creation patterns. The authors identify a gap: maintaining an abstraction of the execution history of threads can improve precision, but current frameworks do not model thread barriers or `pthread_once`, which are widely used in practice to coordinate phases and one-time initialization. This work extends the **digest** framework—a static analysis framework for data race detection—to incorporate these constructs. The central research question is whether handling such "off the beaten path" synchronization mechanisms can be done without sacrificing soundness or scalability, and how existing state-of-the-art tools compare. The paper also proposes a suite of litmus tests to systematically evaluate analyses for these features, providing a benchmark for future work. The extended version includes additional details and proofs omitted from the conference version.

The authors build upon the digest framework, which tracks an abstraction of thread execution histories to improve race detection precision. They introduce two main extensions:

Why it matters

The paper demonstrates that extending a static race detection framework to handle thread barriers and `pthread_once` is both feasible and beneficial for precision. The ancestor lockset abstraction further enhances the analysis by capturing lock inheritance across thread creation. However, several challenges remain: - **Scalability**: While the extensions are sound, their impact on analysis time and memory usage is not fully explored. The authors note that the additional synchronization edges increase the complexity of the happens-before relation, potentially affecting performance on large codebases. - **Generality**: The approach is tailored to the digest framework, but the ideas could be adapted to other static analyses. The litmus tests provide a reusable benchmark for evaluating such adaptations. - **Tool support**: The finding that state-of-the-art tools lack support for these constructs is concerning, as barriers and `pthread_once` are common in real-world code (e.g., in parallel libraries and one-time initialization patterns). This suggests that developers relying on these tools may receive misleading results. The authors advocate for incorporating these constructs into static race detectors as a step toward more practical and precise concurrency analysis. Future work includes extending the framework to other synchronization primitives (e.g., read-write locks, condition variables) and evaluating scalability on larger programs. The paper's contributions are threefold: (1) a formal extension of the digest framework, (2) a litmus test suite for evaluation, and (3) an empirical comparison revealing gaps in existing tools.

Who should read this

CS practitioners and researchers

Opening member content…