Data Race Detection by Digest-Driven Abstract Interpretation
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. We extend this idea to race detection and 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.
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 30mTalk | Data Race Detection by Digest-Driven Abstract Interpretation VMCAI 2026 Pre-print | ||
11:30 30mTalk | Termination Resilience Static Analysis VMCAI 2026 Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL | ||
12:00 30mTalk | Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification VMCAI 2026 Andreas Lindner Uppsala universitet, Karl Palmskog KTH Royal Institute of Technology, Scott Constable Intel Corporation, Mads Dam KTH, Roberto Guanciale KTH Royal Institute of Technology, Hamed Nemati KTH Royal Institute of Technology | ||