{"ID":2841581,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.11055","arxiv_id":"2511.11055","title":"Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)","abstract":"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.","short_abstract":"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 abs...","url_abs":"https://arxiv.org/abs/2511.11055","url_pdf":"https://arxiv.org/pdf/2511.11055v2","authors":"[\"Michael Schwarz\",\"Julian Erhard\"]","published":"2025-11-14T08:11:31Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.SE\"]","methods":"[]","has_code":false}