Re: KCSAN: data-race in __alloc_file / __alloc_file

[Marco Elver]

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