On Mon, 11 Nov 2019 at 19:50, Linus Torvalds <torvalds@xxxxxxxxxxxxxxxxxxxx> wrote: > > On Mon, Nov 11, 2019 at 10:31 AM Eric Dumazet <edumazet@xxxxxxxxxx> wrote: > > > > Problem is that KASAN/KCSAN stops as soon as one issue is hit, > > regardless of it being a false positive or not. > > So mayb e that - together with the known huge base of false positives > - just means that KCSAN needs some more work before it can be used as > a basis for sending out patches. > > Maybe the reporting needs to create a hash of the location, and report > once per location? Or something like that. > > Maybe KCSAN needs a way to filter out known false positives on a KCSAN > side, without having to change the source for a tool that gives too > much noise? > > > If we do not annotate the false positive, the real issues might be > > hidden for years. > > I don't think "change the kernel source for a tool that isn't good > enough" is the solution. > > > There is no pattern really, only a lot of noise (small ' bugs' that > > have no real impact) > > Yeah, if it hasn't shown any real bugs so far, that just strengthens > the "it needs much fewer false positives to be useful". > > KASAN and lockdep can afford to stop after the first problem, because > the problems they report - and the additional annotations you might > want to add - are quality problems and annotations. There is a fundamental limitation here. As I understand, in an ideal world we'd only find true logic bugs, *race conditions*, first, and *data races* later. Some data races are also race conditions, which a tool like KCSAN can report. However, not all race conditions are data races and vice-versa. The intent is to report data races according to the LKMM. KCSAN currently does that. On syzbot, we do not even report all data races because we use a very conservative config, to filter things like data races between plain and ONCE/atomic accesses, etc. A data race detector can only work at the memory model/language level. Deeper analysis, to find only race conditions, requires conveying the intended logic and patterns to a tool. This requires 1) the developer either writing a spec or model of their code, and then 2) the tool verifying that the implementation matches. People have done this for small bits of code using model checkers (and other formal methods), but this just doesn't scale! KCSAN finds real problems today. Maybe not all of them are race conditions, but they are data races. We already have several options to filter data races, and will keep adding more. However, a tool that magically proves that there are no concurrency related logic bugs is an entirely different beast. Thanks, -- Marco
