From: Alan Stern <stern@rowland.harvard.edu>
To: Akira Yokosawa <akiyks@gmail.com>
Cc: "Paul E. McKenney" <paulmck@kernel.org>,
parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org,
boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com,
j.alglave@ucl.ac.uk, luc.maranget@inria.fr, dlustig@nvidia.com,
joel@joelfernandes.org, viro@zeniv.linux.org.uk,
linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org
Subject: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
Date: Sat, 3 Oct 2020 13:13:38 -0400 [thread overview]
Message-ID: <20201003171338.GA323226@rowland.harvard.edu> (raw)
In-Reply-To: <045c643f-6a70-dfdf-2b1e-f369a667f709@gmail.com>
On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> Hi Alan,
>
> Just a minor nit in the litmus test.
>
> On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> > To expand on my statement about the LKMM's weakness regarding control
> > constructs, here is a litmus test to illustrate the issue. You might
> > want to add this to one of the archives.
> >
> > Alan
> >
> > C crypto-control-data
> > (*
> > * LB plus crypto-control-data plus data
> > *
> > * Expected result: allowed
> > *
> > * This is an example of OOTA and we would like it to be forbidden.
> > * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > * control-dependent on the preceding READ_ONCE. But the dependencies are
> > * hidden by the form of the conditional control construct, hence the
> > * name "crypto-control-data". The memory model doesn't recognize them.
> > *)
> >
> > {}
> >
> > P0(int *x, int *y)
> > {
> > int r1;
> >
> > r1 = 1;
> > if (READ_ONCE(*x) == 0)
> > r1 = 0;
> > WRITE_ONCE(*y, r1);
> > }
> >
> > P1(int *x, int *y)
> > {
> > WRITE_ONCE(*x, READ_ONCE(*y));
>
> Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
You're right. This is definitely a bug in herd7.
Luc, were you aware of this?
> When I changed P1 to
>
> P1(int *x, int *y)
> {
> int r1;
>
> r1 = READ_ONCE(*y);
> WRITE_ONCE(*x, r1);
> }
>
> and replaced the WRITE_ONCE() in P0 with smp_store_release(),
> I got the result of:
>
> -----
> Test crypto-control-data Allowed
> States 1
> 0:r1=0;
> No
> Witnesses
> Positive: 0 Negative: 3
> Condition exists (0:r1=1)
> Observation crypto-control-data Never 0 3
> Time crypto-control-data 0.01
> Hash=9b9aebbaf945dad8183d2be0ccb88e11
> -----
>
> Restoring the WRITE_ONCE() in P0, I got the result of:
>
> -----
> Test crypto-control-data Allowed
> States 2
> 0:r1=0;
> 0:r1=1;
> Ok
> Witnesses
> Positive: 1 Negative: 4
> Condition exists (0:r1=1)
> Observation crypto-control-data Sometimes 1 4
> Time crypto-control-data 0.01
> Hash=843eaa4974cec0efae79ce3cb73a1278
> -----
What you should have done was put smp_store_release in P0 and left P1 in
its original form. That test should not be allowed, but herd7 says that
it is.
> As this is the same as the expected result, I suppose you have missed another
> limitation of herd7 + LKMM.
It would be more accurate to say that we all missed it. :-) (And it's
a bug in herd7, not a limitation of either herd7 or LKMM.) How did you
notice it?
> By the way, I think this weakness on control dependency + data dependency
> deserves an entry in tools/memory-model/Documentation/litmus-tests.txt.
>
> In the LIMITATIONS section, item #1 mentions some situation where
> LKMM may not recognize possible losses of control-dependencies by
> compiler optimizations.
>
> What this litmus test demonstrates is a different class of mismatch.
Yes, one in which LKMM does not recognize a genuine dependency because
it can't tell that some optimizations are not valid.
This flaw is fundamental to the way herd7 works. It examines only one
execution at a time, and it doesn't consider the code in a conditional
branch while it's examining an execution where that branch wasn't taken.
Therefore it has no way to know that the code in the unexecuted branch
would prevent a certain optimization. But the compiler does consider
all the code in all branches when deciding what optimizations to apply.
Here's another trivial example:
r1 = READ_ONCE(*x);
if (r1 == 0)
smp_mb();
WRITE_ONCE(*y, 1);
The compiler can't move the WRITE_ONCE before the READ_ONCE or the "if"
statement, because it's not allowed to move shared memory accesses past
a memory barrier -- even if that memory barrier isn't always executed.
Therefore the WRITE_ONCE actually is ordered after the READ_ONCE, but
the memory model doesn't realize it.
> Alan, can you come up with an update in this regard?
I'll write something.
Alan
next prev parent reply other threads:[~2020-10-03 17:13 UTC|newest]
Thread overview: 52+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-10-01 4:51 Litmus test for question from Al Viro Paul E. McKenney
2020-10-01 16:15 ` Alan Stern
2020-10-01 16:36 ` Al Viro
2020-10-01 18:39 ` Alan Stern
2020-10-01 19:29 ` Al Viro
2020-10-01 21:30 ` Paul E. McKenney
2020-10-03 2:01 ` Alan Stern
2020-10-03 13:22 ` Alan Stern
2020-10-03 15:16 ` Akira Yokosawa
2020-10-03 17:13 ` Alan Stern [this message]
2020-10-03 22:50 ` Bug in herd7 [Was: Re: Litmus test for question from Al Viro] Akira Yokosawa
2020-10-04 1:40 ` [PATCH] tools: memory-model: Document that the LKMM can easily miss control dependencies Alan Stern
2020-10-04 21:07 ` joel
2020-10-04 23:12 ` Paul E. McKenney
2020-10-05 15:15 ` Bug in herd7 [Was: Re: Litmus test for question from Al Viro] Luc Maranget
2020-10-05 15:53 ` Alan Stern
2020-10-05 16:52 ` Paul E. McKenney
2020-10-05 18:19 ` Alan Stern
2020-10-05 19:18 ` Paul E. McKenney
2020-10-05 19:48 ` Alan Stern
2020-10-06 16:39 ` Paul E. McKenney
2020-10-06 17:05 ` Alan Stern
2020-10-07 17:50 ` Paul E. McKenney
2020-10-07 19:40 ` Alan Stern
2020-10-07 22:38 ` Paul E. McKenney
2020-10-08 2:25 ` Alan Stern
2020-10-08 2:50 ` Paul E. McKenney
2020-10-08 14:01 ` Alan Stern
2020-10-08 18:32 ` Paul E. McKenney
2020-10-05 15:54 ` Paul E. McKenney
2020-10-04 23:31 ` Litmus test for question from Al Viro Paul E. McKenney
2020-10-05 2:38 ` Alan Stern
2020-10-05 8:20 ` Will Deacon
2020-10-05 9:12 ` Will Deacon
2020-10-05 14:01 ` Paul E. McKenney
2020-10-05 14:23 ` Alan Stern
2020-10-05 15:13 ` Will Deacon
2020-10-05 15:16 ` Alan Stern
2020-10-05 15:35 ` Peter Zijlstra
2020-10-05 15:49 ` Paul E. McKenney
2020-10-05 14:16 ` Alan Stern
2020-10-05 14:03 ` Paul E. McKenney
2020-10-05 14:24 ` Alan Stern
2020-10-05 14:44 ` joel
2020-10-05 15:55 ` Paul E. McKenney
2020-10-05 8:36 ` David Laight
2020-10-05 13:59 ` Paul E. McKenney
2020-10-03 16:08 ` joel
2020-10-03 16:11 ` joel
2020-10-04 23:13 ` Paul E. McKenney
2020-10-03 2:35 ` Jon Masters
2020-10-04 23:32 ` Paul E. McKenney
Reply instructions:
You may reply publicly 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=20201003171338.GA323226@rowland.harvard.edu \
--to=stern@rowland.harvard.edu \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=viro@zeniv.linux.org.uk \
--cc=will@kernel.org \
/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
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.