Message-ID: <CANpmjNMvTbMJa+NmfD286vGVNQrxAnsujQZqaodw0VVUYdNjPw@mail.gmail.com>
Date:   Sun, 10 Nov 2019 20:10:05 +0100
From:   Marco Elver <elver@...gle.com>
To:     Alan Stern <stern@...land.harvard.edu>
Cc:     Linus Torvalds <torvalds@...ux-foundation.org>,
        Eric Dumazet <edumazet@...gle.com>,
        Eric Dumazet <eric.dumazet@...il.com>,
        syzbot <syzbot+3ef049d50587836c0606@...kaller.appspotmail.com>,
        linux-fsdevel <linux-fsdevel@...r.kernel.org>,
        Linux Kernel Mailing List <linux-kernel@...r.kernel.org>,
        syzkaller-bugs <syzkaller-bugs@...glegroups.com>,
        Al Viro <viro@...iv.linux.org.uk>,
        Andrea Parri <parri.andrea@...il.com>,
        "Paul E. McKenney" <paulmck@...nel.org>,
        LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>
Subject: Re: KCSAN: data-race in __alloc_file / __alloc_file

On Sun, 10 Nov 2019 at 17:09, Alan Stern <stern@...land.harvard.edu> wrote:
>
> On Sat, 9 Nov 2019, Linus Torvalds wrote:
>
> > On Sat, Nov 9, 2019, 15:08 Alan Stern <stern@...land.harvard.edu> wrote:
> >
> > > On Fri, 8 Nov 2019, Linus Torvalds wrote:
> > > >
> > > > Two writes to normal memory are *not* idempotent if they write
> > > > different values. The ordering very much matters, and it's racy and a
> > > > tool should complain.
> > >
> > > What you have written strongly indicates that either you think the word
> > > "idempotent" means something different from its actual meaning or else
> > > you are misusing the word in a very confusing way.
> > >
> >
> > "Idempotence is the property of certain operations in mathematics and
> > computer science whereby they can be applied multiple times without
> > changing the result beyond the initial application. "
> >
> > This is (for example) commonly used when talking about nfs operations,
> > where you can re-send the same nfs operation, and it's ok (even if it has
> > side effects) because the server remembers that it already did the
> > operation. If it's already been done, nothing changes.
> >
> > It may not match your definition in some other area, but this is very much
> > the accepted meaning of the word in computer science and operating systems.
>
> Agreed.  My point was that you were using the word in a way which did
> not match this definition.
>
> Never mind that.  You did not respond to the question at the end of my
> previous email: Should the LKMM be changed so that two writes are not
> considered to race with each other if they store the same value?
>
> That change would take care of the original issue of this email thread,
> wouldn't it?  And it would render WRITE_IDEMPOTENT unnecessary.
>
> Making that change would amount to formalizing your requirement that
> the compiler should not invent stores to shared variables.  In C11 such
> invented stores are allowed.  Given something like this:
>
>         <A complex computation which does not involve x but does
>          require a register spill>
>         x = 1234;
>
> C11 allows the compiler to store an intermediate value in x rather than
> allocating a slot on the stack for the register spill.  After all, x is
> going to be overwritten anyway, and if any other thread accessed x
> during the complex computation then it would race with the final store
> and so the behavior would be undefined in any case.
>
> If you want to specifically forbid the compiler from doing this, it
> makes sense to change the memory model accordingly.
>
> For those used to thinking in terms of litmus tests, consider this one:
>
> C equivalent-writes
>
> {}
>
> P0(int *x)
> {
>         *x = 1;
> }
>
> P1(int *x)
> {
>         *x = 1;
> }
>
> exists (~x=1)
>
> Should the LKMM say that this litmus test contains a race?
>
> This suggests that we might also want to relax the notion of a write
> racing with a read, although in that case I'm not at all sure what the
> appropriate change to the memory model would be.  Something along the
> lines of: If a write W races with a read R, but W stores the same value
> that R would have read if W were not present, then it's not really a
> race.  But of course this is far too vague to be useful.

What if you introduce to the above litmus test:

P2(int *x) { *x = 2; }

How can a developer, using the LKMM as a reference, hope to prove
their code is free from data races without having to enumerate all
possible values a variable could contain (in addition to all possible
interleavings)?

I view introducing data value dependencies, for the sake of allowing
more programs, to a language memory model as a slippery slope, and am
not aware of any precedent where this worked out. The additional
complexity in the memory model would put a burden on developers and
the compiler that is unlikely to be a real benefit (as you pointed
out, the compiler may even need to disable some transformations). From
a practical point of view, if the LKMM departs further and further
from C11's memory model, how do we ensure all compilers do the right
thing?

My vote would go to explicit annotation, not only because it reduces
hidden complexity, but also because it makes the code more
understandable, for developers and tooling. As an additional point, I
find the original suggestion to add WRITE_ONCE to be the least bad (or
some other better named WRITE_). Consider somebody changing the code,
changing the semantics and the values written to "non_rcu". With a
WRITE_ONCE, the developer would be clear about the fact that the write
can happen concurrently, and ensure new code is written with the
assumption that concurrent writes can happen.

Thanks,
-- Marco

Powered by blists - more mailing lists