lkml.org 
[lkml]   [2019]   [Nov]   [11]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
From
Date
SubjectRe: KCSAN: data-race in __alloc_file / __alloc_file
On Mon, Nov 11, 2019 at 8:51 AM Linus Torvalds
<torvalds@linux-foundation.org> wrote:
>
> On Mon, Nov 11, 2019 at 7:51 AM Alan Stern <stern@rowland.harvard.edu> wrote:
> >
> > I dislike the explicit annotation approach, because it shifts the
> > burden of proving correctness from the automatic verifier to the
> > programmer.
>
> Yes.
>
> However, sometimes explicit annotations are very useful as
> documentation and as showing of intent even if they might not change
> behavior or code generation.
>
> But they generally should never _replace_ checking - in fact, the
> annotations themselves should hopefully be checked for correctness
> too.
>
> So a good annotation would implicitly document intent, but it should
> also be something that we can check being true, so that we also have
> the check that reality actually _matches_ the intent too. Because
> misleading and wrong documentation is worse than no documentation at
> all.
>
> Side note: an example of a dangerous annotation is the one that Eric
> pointed out, where a 64-bit read in percpu_counter_read_positive()
> could be changed to READ_ONCE(), and we would compile it cleanly, but
> on 32-bit it wouldn't actually be atomic.
>
> We at one time tried to actually verify that READ/WRITE_ONCE() was
> done only on types that could actually be accessed atomically (always
> ignoring alpha because the pain is not worth it), but it showed too
> many problems.
>
> So now we silently accept things that aren't actually atomic. We do
> access them "once" in the sense that we don't allow the compiler to
> reload it, but it's not "once" in the LKMM sense of one single value.
>
> That's ok for some cases. But it's actually a horrid horrid thing from
> a documentation standpoint, and I hate it, and it's dangerous.
>
> Linus

I was hoping to cleanup the 'easy cases' before looking at more serious issues.

But it looks like even the ' easy cases' are not that easy.

Now I wonder what to do with the ~400 KCSAN reports sitting in
pre-moderation queue.

\
 
 \ /
  Last update: 2019-11-11 18:53    [W:0.292 / U:0.020 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site