search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
183 stars 170 forks source link

SV-COMP concurrency benchmarks with data races #1291

Open fatimahkj opened 3 years ago

fatimahkj commented 3 years ago

Dear SV-COMP community,

I tested some benchmarks in the concurrency safety category using a thread sanitizer (TSAN). Some of the benchmarks marked as true, TSAN found a data race bug.

My question is if some of the benchmarks marked as true have a data race?

For example: fib_bench-1.c and indexer.c in pthread subcargory.

Best, Fatimah

hernanponcedeleon commented 3 years ago

Hi Fatimah,

when you say "some benchmarks are marked as true", what property do you refer to? For example, fib_bench-1.yml has two properties, no-data-race and unreach-call. no-data-race: true Means the program has no data races according to the SVCOMP semantics.

Notice that SVCOMP has special functions __VERIFIER_atomic_begin() and __VERIFIER_atomic_end() which can be used for synchronisation purposes like avoiding data races. The semantics of these two functions in only defined in the context of SVCOMP (they are not standard C) and thus tools outside the community will not understand them. This is probably the reason why TSAN mark the benchmarks as having data races.

There has been some discussion (see #657) in trying to minimise the use of this SVCOMP specific functions and opt for standard synchronisation mechanisms (C11 atomics of pthreads), but we are not there yet. I was hoping to push in this direction for next year SVCOMP.

fatimahkj commented 3 years ago

Regarding indexer.c, it is not using any special SVCOMP functions, but TSAN detected a data race.

hernanponcedeleon commented 3 years ago

Notice that the yml file does not contain an entry for the no-data-race category. This suggests nobody tried to check data races in this benchmarks before.

In the past, when we found data races, we proceeded in the following way: 1) Create a new benchmark (e.g. indexer-b.c) containing the data race so when can use it for the data race category (this will be just a copy of the benchmark in its current state). The corresponding property file (indexer-b.yml) will contain no-data-race: false, but nothing about unreach-call (in the precedes of UB verification does not make any sense). 2) Fix the data race in indexer.c and add no-data-race: true to indexer.yml