c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
13 stars 1 forks source link

Fuzzer bug: looped compare exchanges #212

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 3 years ago

Consider the Litmus snippet:

{ obj = 42 }

void P0(atomic_int *obj) {
  int i = 0;
  int exp = 42;
  bool b = false;

  for (i = 0; i < 2; i++) {
    b = atomic_compare_exchange(obj, &exp, 2);
  }
}

forall (0:b == true)

This snippet will fail, as we see if we step through the loop (values being those at the point of i taking the given value):

i obj exp b
0 42 42 false
1 2 42 true
2 2 2 false

The reason this fails is because the cmpxchg-always-succeed action always assumed that the value of obj would not be depended on by anything after the compare-exchange had occurred, which is true if and only if control flow doesn't pass back through the same compare-exchange. It's, effectively, another version of the same dependency cycle issue I thought I'd fixed yesterday; the problem is that my attempt to make sure compare-exchanges generated properly was ham-fisted.

In my head, the solution feels like this:

  1. Implement #211;
  2. Always mark compare-exchanges as loop-unsafe and impossible to generate in non-straightline loops;
  3. This then, as a corollary, lets us weaken the storelike cycle breaker (I think) so that it no longer needs to special-case 'safe' dependency cycles (turns out they're not actually safe anyway!) and need only break cycles if generating into a path that can execute multiple times. (However, I'd need to make sure the loop-unsafe mark gets added. Perhaps this can always be done on the storelike and not special-cased for compare-exchanges.)
MattWindsor91 commented 3 years ago

I believe this has been fixed (but there's a new fuzzer bug to replace it!)