Linux-Fsdevel Archive on lore.kernel.org
 help / color / Atom feed
From: Alan Stern <stern@rowland.harvard.edu>
To: Marco Elver <elver@google.com>
Cc: Linus Torvalds <torvalds@linux-foundation.org>,
	Eric Dumazet <edumazet@google.com>,
	Eric Dumazet <eric.dumazet@gmail.com>,
	syzbot <syzbot+3ef049d50587836c0606@syzkaller.appspotmail.com>,
	linux-fsdevel <linux-fsdevel@vger.kernel.org>,
	Linux Kernel Mailing List <linux-kernel@vger.kernel.org>,
	syzkaller-bugs <syzkaller-bugs@googlegroups.com>,
	Al Viro <viro@zeniv.linux.org.uk>,
	Andrea Parri <parri.andrea@gmail.com>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	LKMM Maintainers -- Akira Yokosawa <akiyks@gmail.com>
Subject: Re: KCSAN: data-race in __alloc_file / __alloc_file
Date: Mon, 11 Nov 2019 10:51:11 -0500 (EST)
Message-ID: <Pine.LNX.4.44L0.1911111030410.12295-100000@netrider.rowland.org> (raw)
In-Reply-To: <CANpmjNMvTbMJa+NmfD286vGVNQrxAnsujQZqaodw0VVUYdNjPw@mail.gmail.com>

On Sun, 10 Nov 2019, Marco Elver wrote:

> On Sun, 10 Nov 2019 at 17:09, Alan Stern <stern@rowland.harvard.edu> wrote:
...

> > 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; }

Then clearly the test _would_ contain a data race.

> 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)?

Well, for one thing the new rule doesn't say anything about all
possible values a variable could contain; it only talks about the
values of a pair of concurrent writes.  Of course, this would still
require you to be aware of (if not to fully enumerate) all possible
values a write could store, so perhaps it's not much of an improvement.

On the other hand, one way to prove your code is data-race-free under
the revised LKMM would be to show that it is data-race-free under the
original (i.e., current) LKMM.  Then you wouldn't have to enumerate any
lists of possible values.

> 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).

This may be so.  But if the resulting model is a better match to the
way kernel developers think about their code, wouldn't it be
appropriate?

>  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?

Linus has already committed to doing this.  To quote the latest example
(from a message he posted shortly after yours):

	I don't care one whit about C11. Made-up stores to shared data
	are not acceptable. Ever. We will turn that off with a compiler
	switch if the compiler thinks it can do them, the same way we
	turn off other incorrect optimizations like the type-based
	aliasing or the insane "signed integer arithmetic can have
	undefined behavior" stupidity that the standards people
	allowed.

Given that the kernel _requires_ compilers to behave this way, 
shouldn't the LKMM reflect this requirement?

> 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.

I dislike the explicit annotation approach, because it shifts the
burden of proving correctness from the automatic verifier to the
programmer.  Let's take the litmus test above as example.  I could
annotate it to read:

P0(int *x) { WRITE_IDEMPOTENT(*x, 1); }
P1(int *x) { WRITE_IDEMPOTENT(*x, 1); }

and then KCSAN would take my word for it that the two writes don't race
with each other (or if they do race, it doesn't matter).  But now if
the code was changed by adding:

P2(int *x) { WRITE_IDEMPOTENT(*x, 2); }

then KCSAN would still believe there was no race, meaning it would be
up to me to audit all possible writes to x to make sure they store the
same value.  That is not how automated tooling should work.

Alan Stern


  reply index

Thread overview: 67+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <CAHk-=wjB61GNmqpX0BLA5tpL4tsjWV7akaTc2Roth7uGgax+mw@mail.gmail.com>
2019-11-10 16:09 ` Alan Stern
2019-11-10 19:10   ` Marco Elver
2019-11-11 15:51     ` Alan Stern [this message]
2019-11-11 16:51       ` Linus Torvalds
2019-11-11 17:52         ` Eric Dumazet
2019-11-11 18:04           ` Linus Torvalds
2019-11-11 18:31             ` Eric Dumazet
2019-11-11 18:44               ` Eric Dumazet
2019-11-11 19:00                 ` Linus Torvalds
2019-11-11 19:13                   ` Eric Dumazet
2019-11-11 20:43                     ` Linus Torvalds
2019-11-11 20:46                       ` Linus Torvalds
2019-11-11 21:53                         ` Eric Dumazet
2019-11-11 23:51                   ` Linus Torvalds
2019-11-12 16:50                     ` Kirill Smelkov
2019-11-12 17:23                       ` Linus Torvalds
2019-11-12 17:36                         ` Linus Torvalds
2019-11-17 18:56                           ` Kirill Smelkov
2019-11-17 19:20                             ` Linus Torvalds
2019-11-11 18:50               ` Linus Torvalds
2019-11-11 18:59                 ` Marco Elver
2019-11-11 18:59                 ` Eric Dumazet
2019-11-10 19:12   ` Linus Torvalds
2019-11-10 19:20     ` Linus Torvalds
2019-11-10 20:44       ` Paul E. McKenney
2019-11-10 21:10         ` Linus Torvalds
2019-11-10 21:31           ` Paul E. McKenney
2019-11-11 14:17         ` Marco Elver
2019-11-11 14:31           ` Paul E. McKenney
2019-11-11 15:10             ` Marco Elver
2019-11-13  0:25               ` Paul E. McKenney
2019-11-12 19:14     ` Alan Stern
2019-11-12 19:47       ` Linus Torvalds
2019-11-12 20:29         ` Alan Stern
2019-11-12 20:58           ` Linus Torvalds
2019-11-12 21:13             ` Linus Torvalds
2019-11-12 22:05               ` Marco Elver
2019-11-12 21:48             ` Alan Stern
2019-11-12 22:07               ` Eric Dumazet
2019-11-12 22:44                 ` Alexei Starovoitov
2019-11-12 23:17                   ` Eric Dumazet
2019-11-12 23:40                     ` Linus Torvalds
2019-11-13 15:00                       ` Marco Elver
2019-11-13 16:57                         ` Linus Torvalds
2019-11-13 21:33                           ` Marco Elver
2019-11-13 21:50                             ` Alan Stern
2019-11-13 22:48                               ` Marco Elver
2019-11-08 13:16 syzbot
2019-11-08 13:28 ` Eric Dumazet
2019-11-08 17:01   ` Linus Torvalds
2019-11-08 17:22     ` Eric Dumazet
2019-11-08 17:38       ` Linus Torvalds
2019-11-08 17:53         ` Eric Dumazet
2019-11-08 17:55           ` Eric Dumazet
2019-11-08 18:02             ` Eric Dumazet
2019-11-08 18:12               ` Linus Torvalds
2019-11-08 20:30             ` Linus Torvalds
2019-11-08 20:53               ` Eric Dumazet
2019-11-08 21:36                 ` Linus Torvalds
2019-11-08 18:05           ` Linus Torvalds
2019-11-08 18:15             ` Marco Elver
2019-11-08 18:40               ` Linus Torvalds
2019-11-08 19:48                 ` Marco Elver
2019-11-08 20:26                   ` Linus Torvalds
2019-11-08 21:57                     ` Alan Stern
2019-11-08 22:06                       ` Linus Torvalds
2019-11-09 23:08                         ` Alan Stern

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=Pine.LNX.4.44L0.1911111030410.12295-100000@netrider.rowland.org \
    --to=stern@rowland.harvard.edu \
    --cc=akiyks@gmail.com \
    --cc=edumazet@google.com \
    --cc=elver@google.com \
    --cc=eric.dumazet@gmail.com \
    --cc=linux-fsdevel@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=parri.andrea@gmail.com \
    --cc=paulmck@kernel.org \
    --cc=syzbot+3ef049d50587836c0606@syzkaller.appspotmail.com \
    --cc=syzkaller-bugs@googlegroups.com \
    --cc=torvalds@linux-foundation.org \
    --cc=viro@zeniv.linux.org.uk \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Linux-Fsdevel Archive on lore.kernel.org

Archives are clonable:
	git clone --mirror https://lore.kernel.org/linux-fsdevel/0 linux-fsdevel/git/0.git

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V2 linux-fsdevel linux-fsdevel/ https://lore.kernel.org/linux-fsdevel \
		linux-fsdevel@vger.kernel.org
	public-inbox-index linux-fsdevel

Example config snippet for mirrors

Newsgroup available over NNTP:
	nntp://nntp.lore.kernel.org/org.kernel.vger.linux-fsdevel


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git