Comments (3)
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.
from sv-benchmarks.
Regarding indexer.c, it is not using any special SVCOMP functions, but TSAN detected a data race.
from sv-benchmarks.
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:
- 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 containno-data-race: false
, but nothing aboutunreach-call
(in the precedes of UB verification does not make any sense). - Fix the data race in indexer.c and add
no-data-race: true
toindexer.yml
from sv-benchmarks.
Related Issues (20)
- Tasks in seq-mthreaded wrongly marked as non-terminating HOT 2
- Task ntdrivers/floppy2 is not memory safe
- Task ntdrivers/diskperf.i.cil-1.c is not memory safe HOT 2
- ntdrivers/parport.i.cil-2 is not memory safe
- LDV tasks with undefined behaviour and/or wrong verdicts HOT 3
- cut-2 and od-1 from busy-box are not memory safe HOT 1
- Undefined behavior in two AWS benchmarks
- MemSafety - unset subproperty for false verdict
- Incorrect Verification Task
- geo1-ll.c can overflow HOT 3
- Implementation-defined behaviour HOT 3
- "Repeated" benchmarks in pthread-wmm
- why can echo-2.i overflow? HOT 2
- __builtin_unreachable() in LDV benchmarks HOT 3
- Benchmarks for weak memory models HOT 3
- Reachable error in pthread-ext/41_FreeBSD_abd_kbd_sliced
- Use of `__VERIFIER_nondet_*` functions that aren't specified in SV-COMP rules HOT 1
- Info on SV-COMP 2022? HOT 2
- Repository moved to GitLab HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sv-benchmarks.