2025/11/14 by Michael Schwarz, Schwarz, Michael, Julian Erhard +1 · 1 citation
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2511.11055
openalex publication_date 2025/11/14 · openalex created_date 2025/11/18 · openalex updated_date 2026/07/28
Sound static analysis can prove the absence of data races by establishing that no two conflicting memory accesses can occur at the same time. We repurpose the concept of digests -- summaries of computational histories originally introduced to bring tunable concurrency-sensitivity to thread-modular value analysis by abstract interpretation, extending this idea to race detection: We use digests to capture the conditions under which conflicting accesses may not happen in parallel. To formalize this, we give a definition of data races in the thread-modular local trace semantics and show how exclusion criteria for potential conflicts can be expressed as digests. We report on our implementation of digest-driven data race detection in the static analyzer Goblint, and evaluate it on the SV-COMP benchmark suite. Combining the lockset digest with digests reasoning on thread ids and thread joins increases the number of correctly solved tasks by more than a factor of five compared to lockset reasoning alone.