We present a new symbolic static data race detection algorithm, which is defined as a code-to-code translation that injects code to monitor any accesses to shared memory locations. We implemented this algorithm in the LaDR tool as an extension of an existing lazy sequentialization schema which works well when used in tandem with bounded model checkers. We evaluated LaDR on the benchmarks from the data race demonstration category of SV-COMP 2024, and on safestack, a lock-free data structure that contains a rare ABA-related bug. LaDR finds more data races than all other tools participating in SV-COMP 2024, and is the only tool that can find a data race in safestack.
Static Data Race Detection via Lazy Sequentialization
Garbi G.;Parlato G.;
2024-01-01
Abstract
We present a new symbolic static data race detection algorithm, which is defined as a code-to-code translation that injects code to monitor any accesses to shared memory locations. We implemented this algorithm in the LaDR tool as an extension of an existing lazy sequentialization schema which works well when used in tandem with bounded model checkers. We evaluated LaDR on the benchmarks from the data race demonstration category of SV-COMP 2024, and on safestack, a lock-free data structure that contains a rare ABA-related bug. LaDR finds more data races than all other tools participating in SV-COMP 2024, and is the only tool that can find a data race in safestack.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
