Data races and possible wrong expected results in the weaver benchmarks
Many of the newly added weaver benchmarks have data races. All parallel-misc-
have the following pattern
void* thread1() {
while (g1) {
if (d1) {
__VERIFIER_atomic_begin();
pos++;
__VERIFIER_atomic_end();
} else {
__VERIFIER_atomic_begin();
pos--;
__VERIFIER_atomic_end();
}
...
}
void* thread2() {
while (g2) {
if (d2) {
pos = pos + 2;
} else {
pos = pos - 2;
}
...
}
and thus they race on pos
. I also suspect that the expected result was generated based on the assumption that pos = pos + 2;
is atomic (which is not according to the C standard). Adding atomic blocks would solve both the atomicity and data race problem.
parallel-barrier.wvr
has a similar problem: it races on pretty much all variables. Once again I believe the expected result was generated based on the assumption that things like assume_abort_if_not( f1_8 && f2_9 )
are atomic. Notice however than just wrapping this into an atomic block would result in a violation of atomic blocks specifications as I mentioned in #1312. In that issue I propose a solution using local variables that I guess might be applicable here to.
I expect the problems I mention above to appear in many benchmarks in this folder. Since this benchmarks were automatically translated by @klumppdo, it might be easier to adapt the scripts and regenerate all benchmarks.