search

c4-project / c4f

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

Generate weak cmpxchgs #235

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

The fuzzer only generates strong cmpxchgs at the moment. This is mainly because it only generates known-true cmpxchgs, and weak cmpxchgs can't be used as known-true without loops (which might not terminate?). However, if we generate known-false cmpxchgs and deadcode cmpxchgs (these two probably need separate general issues), there is no reason why we shouldn't investigate weak ones.

MattWindsor91 commented 3 years ago

A data point for this one: LLVM's InstCombineCompares pass reduces == compares on the expected value of strong cmpxchgs to its Boolean output, but not weak cmpxchgs (because the output may not always be true when the cmpxchg succeeded). If, for some reason, optimisations like this accidentally targeted weak cmpxchgs, the result would be unsound.