Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > linux.kernel > #1493541 > unrolled thread

Re: [PATCH locking/Documentation 1/2] Add note of release-acquire store vulnerability

Back to article view | Back to linux.kernel

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-29 18:00 +0200
    Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Will Deacon <will.deacon@arm.com> - 2016-09-29 18:10 +0200
      Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-29 18:20 +0200
        Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 18:50 +0200
      Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 18:50 +0200
        Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Will Deacon <will.deacon@arm.com> - 2016-09-29 19:20 +0200
          Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 19:30 +0200
            Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 20:10 +0200
              Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 20:20 +0200
                Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-29 20:50 +0200
                  Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 21:20 +0200
                    Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Alan Stern <stern@rowland.harvard.edu> - 2016-09-29 21:40 +0200
                      Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-29 22:30 +0200
                      Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-30 11:00 +0200
                    Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-30 11:10 +0200
                    Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-30 12:00 +0200
                      Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-30 14:20 +0200
                        Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-30 15:00 +0200
                          Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-30 15:40 +0200
            Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Boqun Feng <boqun.feng@gmail.com> - 2016-09-30 08:00 +0200
              Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Will Deacon <will.deacon@arm.com> - 2016-09-30 11:30 +0200
                Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-30 13:40 +0200
        Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-30 12:30 +0200
          Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-30 14:20 +0200
            Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability Peter Zijlstra <peterz@infradead.org> - 2016-09-30 14:50 +0200
              Re: [PATCH locking/Documentation 1/2] Add note of release-acquire  store vulnerability "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2016-09-30 15:20 +0200

Page 1 of 2  [1] 2  Next page →

#1493541 — Re: [PATCH locking/Documentation 1/2] Add note of release-acquire store vulnerability

On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> broken if a third process overwrites the value written by the RELEASE
> operation before the ACQUIRE operation has a chance of reading it.
> This commit therefore updates the documentation to call this vulnerability
> out explicitly.
> 
> Reported-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

> +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> +     broken by a store by another thread that overwrites the RELEASE
> +     operation's store before the ACQUIRE operation's read.

This is the powerpc lwsync quirk, right? Where the barrier disappears
when it looses the store.

Or is there more to it? Its not entirely clear from the Changelog, which
I feel should describe the reason for the behaviour.

[toc] | [next] | [standalone]

#1493549

On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > broken if a third process overwrites the value written by the RELEASE
> > operation before the ACQUIRE operation has a chance of reading it.
> > This commit therefore updates the documentation to call this vulnerability
> > out explicitly.
> > 
> > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > +     broken by a store by another thread that overwrites the RELEASE
> > +     operation's store before the ACQUIRE operation's read.
> 
> This is the powerpc lwsync quirk, right? Where the barrier disappears
> when it looses the store.
> 
> Or is there more to it? Its not entirely clear from the Changelog, which
> I feel should describe the reason for the behaviour.

If I've groked it correctly, it's for cases like:


PO:
Wx=1
WyRel=1

P1:
Wy=2

P2:
RyAcq=2
Rx=0

Final value of y is 2.


This is permitted on arm64. If you make P1's store a store-release, then
it's forbidden, but I suspect that's not generally true of the kernel
memory model.

Will

[toc] | [prev] | [next] | [standalone]

#1493556

On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > broken if a third process overwrites the value written by the RELEASE
> > > operation before the ACQUIRE operation has a chance of reading it.
> > > This commit therefore updates the documentation to call this vulnerability
> > > out explicitly.
> > > 
> > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > +     broken by a store by another thread that overwrites the RELEASE
> > > +     operation's store before the ACQUIRE operation's read.
> > 
> > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > when it looses the store.
> > 
> > Or is there more to it? Its not entirely clear from the Changelog, which
> > I feel should describe the reason for the behaviour.
> 
> If I've groked it correctly, it's for cases like:
> 
> 
> PO:
> Wx=1
> WyRel=1
> 
> P1:
> Wy=2
> 
> P2:
> RyAcq=2
> Rx=0
> 
> Final value of y is 2.
> 
> 
> This is permitted on arm64. If you make P1's store a store-release, then
> it's forbidden, but I suspect that's not generally true of the kernel
> memory model.

Right, I think that on PowerPC, even if P1 does store-release you can
still get this, since the two stores conflict one can loose out, and the
lwsync associated with the loosing store gets removed along with it.


So yes, I think this needs more clarification.

[toc] | [prev] | [next] | [standalone]

#1493591

On Thu, Sep 29, 2016 at 06:17:38PM +0200, Peter Zijlstra wrote:
> On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> > On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > broken if a third process overwrites the value written by the RELEASE
> > > > operation before the ACQUIRE operation has a chance of reading it.
> > > > This commit therefore updates the documentation to call this vulnerability
> > > > out explicitly.
> > > > 
> > > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > 
> > > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > > +     broken by a store by another thread that overwrites the RELEASE
> > > > +     operation's store before the ACQUIRE operation's read.
> > > 
> > > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > > when it looses the store.
> > > 
> > > Or is there more to it? Its not entirely clear from the Changelog, which
> > > I feel should describe the reason for the behaviour.
> > 
> > If I've groked it correctly, it's for cases like:
> > 
> > 
> > PO:
> > Wx=1
> > WyRel=1
> > 
> > P1:
> > Wy=2
> > 
> > P2:
> > RyAcq=2
> > Rx=0
> > 
> > Final value of y is 2.
> > 
> > 
> > This is permitted on arm64. If you make P1's store a store-release, then
> > it's forbidden, but I suspect that's not generally true of the kernel
> > memory model.
> 
> Right, I think that on PowerPC, even if P1 does store-release you can
> still get this, since the two stores conflict one can loose out, and the
> lwsync associated with the loosing store gets removed along with it.
> 
> So yes, I think this needs more clarification.

Whether the store is loose or not, yes, putting an lwsync as the first
instruction in a given task has no effect.  ;-)

							Thanx, Paul

[toc] | [prev] | [next] | [standalone]

#1493586

On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > broken if a third process overwrites the value written by the RELEASE
> > > operation before the ACQUIRE operation has a chance of reading it.
> > > This commit therefore updates the documentation to call this vulnerability
> > > out explicitly.
> > > 
> > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > +     broken by a store by another thread that overwrites the RELEASE
> > > +     operation's store before the ACQUIRE operation's read.
> > 
> > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > when it looses the store.
> > 
> > Or is there more to it? Its not entirely clear from the Changelog, which
> > I feel should describe the reason for the behaviour.
> 
> If I've groked it correctly, it's for cases like:
> 
> 
> PO:
> Wx=1
> WyRel=1
> 
> P1:
> Wy=2
> 
> P2:
> RyAcq=2
> Rx=0
> 
> Final value of y is 2.
> 
> 
> This is permitted on arm64. If you make P1's store a store-release, then
> it's forbidden, but I suspect that's not generally true of the kernel
> memory model.

That is the one!  And to Peter's point, powerpc does the same for the
example as shown.  However, on powerpc, upgrading P1's store to release
has no effect because there is no earlier access for the resulting
lwsync to influence.  For whatever it might be worth, C11 won't guarantee
ordering in that case, either.  Nor will the current Linux-kernel memory
model.  (Yes, I did just try it to make sure.  Why do you ask?)

So you guys are fishing for an expanded commit log, for example, like
the following?  ;-)

							Thanx, Paul

------------------------------------------------------------------------

If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
broken if a third process overwrites the value written by the RELEASE
operation before the ACQUIRE operation has a chance of reading it, for
example:

	P0(int *x, int *y)
	{
		WRITE_ONCE(*x, 1);
		smp_wmb();
		smp_store_release(y, 1);
	}

	P1(int *y)
	{
		smp_store_release(y, 2);
	}

	P2(int *x, int *y)
	{
		r1 = smp_load_acquire(y);
		r2 = READ_ONCE(*x);
	}

Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
r2=0), as does the current version of the early prototype Linux-kernel
memory model.

This commit therefore updates the documentation to call this vulnerability
out explicitly.

[toc] | [prev] | [next] | [standalone]

#1493602

On Thu, Sep 29, 2016 at 09:43:53AM -0700, Paul E. McKenney wrote:
> On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> > On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > broken if a third process overwrites the value written by the RELEASE
> > > > operation before the ACQUIRE operation has a chance of reading it.
> > > > This commit therefore updates the documentation to call this vulnerability
> > > > out explicitly.
> > > > 
> > > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > 
> > > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > > +     broken by a store by another thread that overwrites the RELEASE
> > > > +     operation's store before the ACQUIRE operation's read.
> > > 
> > > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > > when it looses the store.
> > > 
> > > Or is there more to it? Its not entirely clear from the Changelog, which
> > > I feel should describe the reason for the behaviour.
> > 
> > If I've groked it correctly, it's for cases like:
> > 
> > 
> > PO:
> > Wx=1
> > WyRel=1
> > 
> > P1:
> > Wy=2
> > 
> > P2:
> > RyAcq=2
> > Rx=0
> > 
> > Final value of y is 2.
> > 
> > 
> > This is permitted on arm64. If you make P1's store a store-release, then
> > it's forbidden, but I suspect that's not generally true of the kernel
> > memory model.
> 
> That is the one!  And to Peter's point, powerpc does the same for the
> example as shown.  However, on powerpc, upgrading P1's store to release
> has no effect because there is no earlier access for the resulting
> lwsync to influence.  For whatever it might be worth, C11 won't guarantee
> ordering in that case, either.  Nor will the current Linux-kernel memory
> model.  (Yes, I did just try it to make sure.  Why do you ask?)
> 
> So you guys are fishing for an expanded commit log, for example, like
> the following?  ;-)
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> broken if a third process overwrites the value written by the RELEASE
> operation before the ACQUIRE operation has a chance of reading it, for
> example:
> 
> 	P0(int *x, int *y)
> 	{
> 		WRITE_ONCE(*x, 1);
> 		smp_wmb();
> 		smp_store_release(y, 1);
> 	}
> 
> 	P1(int *y)
> 	{
> 		smp_store_release(y, 2);
> 	}
> 
> 	P2(int *x, int *y)
> 	{
> 		r1 = smp_load_acquire(y);
> 		r2 = READ_ONCE(*x);
> 	}
> 
> Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> r2=0), as does the current version of the early prototype Linux-kernel
> memory model.

FWIW, ARM doesn't allow this and arm64 only allows it if P1 uses WRITE_ONCE
instead of store-release.

Will

[toc] | [prev] | [next] | [standalone]

#1493617

On Thu, Sep 29, 2016 at 06:10:37PM +0100, Will Deacon wrote:
> On Thu, Sep 29, 2016 at 09:43:53AM -0700, Paul E. McKenney wrote:
> > On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> > > On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > > > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > > broken if a third process overwrites the value written by the RELEASE
> > > > > operation before the ACQUIRE operation has a chance of reading it.
> > > > > This commit therefore updates the documentation to call this vulnerability
> > > > > out explicitly.
> > > > > 
> > > > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > > 
> > > > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > > > +     broken by a store by another thread that overwrites the RELEASE
> > > > > +     operation's store before the ACQUIRE operation's read.
> > > > 
> > > > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > > > when it looses the store.
> > > > 
> > > > Or is there more to it? Its not entirely clear from the Changelog, which
> > > > I feel should describe the reason for the behaviour.
> > > 
> > > If I've groked it correctly, it's for cases like:
> > > 
> > > 
> > > PO:
> > > Wx=1
> > > WyRel=1
> > > 
> > > P1:
> > > Wy=2
> > > 
> > > P2:
> > > RyAcq=2
> > > Rx=0
> > > 
> > > Final value of y is 2.
> > > 
> > > 
> > > This is permitted on arm64. If you make P1's store a store-release, then
> > > it's forbidden, but I suspect that's not generally true of the kernel
> > > memory model.
> > 
> > That is the one!  And to Peter's point, powerpc does the same for the
> > example as shown.  However, on powerpc, upgrading P1's store to release
> > has no effect because there is no earlier access for the resulting
> > lwsync to influence.  For whatever it might be worth, C11 won't guarantee
> > ordering in that case, either.  Nor will the current Linux-kernel memory
> > model.  (Yes, I did just try it to make sure.  Why do you ask?)
> > 
> > So you guys are fishing for an expanded commit log, for example, like
> > the following?  ;-)
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > broken if a third process overwrites the value written by the RELEASE
> > operation before the ACQUIRE operation has a chance of reading it, for
> > example:
> > 
> > 	P0(int *x, int *y)
> > 	{
> > 		WRITE_ONCE(*x, 1);
> > 		smp_wmb();
> > 		smp_store_release(y, 1);
> > 	}
> > 
> > 	P1(int *y)
> > 	{
> > 		smp_store_release(y, 2);
> > 	}
> > 
> > 	P2(int *x, int *y)
> > 	{
> > 		r1 = smp_load_acquire(y);
> > 		r2 = READ_ONCE(*x);
> > 	}
> > 
> > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > r2=0), as does the current version of the early prototype Linux-kernel
> > memory model.
> 
> FWIW, ARM doesn't allow this and arm64 only allows it if P1 uses WRITE_ONCE
> instead of store-release.

Good catch, apologies for the error.  The following, then?

							Thanx, Paul

------------------------------------------------------------------------

If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
broken if a third process overwrites the value written by the RELEASE
operation before the ACQUIRE operation has a chance of reading it, for
example:

	P0(int *x, int *y)
	{
		WRITE_ONCE(*x, 1);
		smp_wmb();
		smp_store_release(y, 1);
	}

	P1(int *y)
	{
		WRITE_ONCE(*y, 2);
	}

	P2(int *x, int *y)
	{
		r1 = smp_load_acquire(y);
		r2 = READ_ONCE(*x);
	}

Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
r2=0), as does the current version of the early prototype Linux-kernel
memory model.

[toc] | [prev] | [next] | [standalone]

#1493630

On Thu, Sep 29, 2016 at 10:23:22AM -0700, Paul E. McKenney wrote:
> On Thu, Sep 29, 2016 at 06:10:37PM +0100, Will Deacon wrote:
> > On Thu, Sep 29, 2016 at 09:43:53AM -0700, Paul E. McKenney wrote:
> > > On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> > > > On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > > > > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > > > broken if a third process overwrites the value written by the RELEASE
> > > > > > operation before the ACQUIRE operation has a chance of reading it.
> > > > > > This commit therefore updates the documentation to call this vulnerability
> > > > > > out explicitly.
> > > > > > 
> > > > > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > > > 
> > > > > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > > > > +     broken by a store by another thread that overwrites the RELEASE
> > > > > > +     operation's store before the ACQUIRE operation's read.
> > > > > 
> > > > > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > > > > when it looses the store.
> > > > > 
> > > > > Or is there more to it? Its not entirely clear from the Changelog, which
> > > > > I feel should describe the reason for the behaviour.
> > > > 
> > > > If I've groked it correctly, it's for cases like:
> > > > 
> > > > 
> > > > PO:
> > > > Wx=1
> > > > WyRel=1
> > > > 
> > > > P1:
> > > > Wy=2
> > > > 
> > > > P2:
> > > > RyAcq=2
> > > > Rx=0
> > > > 
> > > > Final value of y is 2.
> > > > 
> > > > 
> > > > This is permitted on arm64. If you make P1's store a store-release, then
> > > > it's forbidden, but I suspect that's not generally true of the kernel
> > > > memory model.
> > > 
> > > That is the one!  And to Peter's point, powerpc does the same for the
> > > example as shown.  However, on powerpc, upgrading P1's store to release
> > > has no effect because there is no earlier access for the resulting
> > > lwsync to influence.  For whatever it might be worth, C11 won't guarantee
> > > ordering in that case, either.  Nor will the current Linux-kernel memory
> > > model.  (Yes, I did just try it to make sure.  Why do you ask?)
> > > 
> > > So you guys are fishing for an expanded commit log, for example, like
> > > the following?  ;-)
> > > 
> > > 							Thanx, Paul
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > broken if a third process overwrites the value written by the RELEASE
> > > operation before the ACQUIRE operation has a chance of reading it, for
> > > example:
> > > 
> > > 	P0(int *x, int *y)
> > > 	{
> > > 		WRITE_ONCE(*x, 1);
> > > 		smp_wmb();
> > > 		smp_store_release(y, 1);
> > > 	}
> > > 
> > > 	P1(int *y)
> > > 	{
> > > 		smp_store_release(y, 2);
> > > 	}
> > > 
> > > 	P2(int *x, int *y)
> > > 	{
> > > 		r1 = smp_load_acquire(y);
> > > 		r2 = READ_ONCE(*x);
> > > 	}
> > > 
> > > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > > r2=0), as does the current version of the early prototype Linux-kernel
> > > memory model.
> > 
> > FWIW, ARM doesn't allow this and arm64 only allows it if P1 uses WRITE_ONCE
> > instead of store-release.
> 
> Good catch, apologies for the error.  The following, then?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> broken if a third process overwrites the value written by the RELEASE
> operation before the ACQUIRE operation has a chance of reading it, for
> example:
> 
> 	P0(int *x, int *y)
> 	{
> 		WRITE_ONCE(*x, 1);
> 		smp_wmb();
> 		smp_store_release(y, 1);
> 	}
> 
> 	P1(int *y)
> 	{
> 		WRITE_ONCE(*y, 2);
> 	}
> 
> 	P2(int *x, int *y)
> 	{
> 		r1 = smp_load_acquire(y);
> 		r2 = READ_ONCE(*x);
> 	}
> 
> Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> r2=0), as does the current version of the early prototype Linux-kernel

And the above needs to be (r1!=2 || r2 != 0)...  Sigh!

							Thanx, Paul

> memory model.

[toc] | [prev] | [next] | [standalone]

#1493640

On Thu, Sep 29, 2016 at 11:04:44AM -0700, Paul E. McKenney wrote:
> On Thu, Sep 29, 2016 at 10:23:22AM -0700, Paul E. McKenney wrote:
> > On Thu, Sep 29, 2016 at 06:10:37PM +0100, Will Deacon wrote:
> > > On Thu, Sep 29, 2016 at 09:43:53AM -0700, Paul E. McKenney wrote:
> > > > On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> > > > > On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > > > > > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > > > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > > > > broken if a third process overwrites the value written by the RELEASE
> > > > > > > operation before the ACQUIRE operation has a chance of reading it.
> > > > > > > This commit therefore updates the documentation to call this vulnerability
> > > > > > > out explicitly.
> > > > > > > 
> > > > > > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > > > > 
> > > > > > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > > > > > +     broken by a store by another thread that overwrites the RELEASE
> > > > > > > +     operation's store before the ACQUIRE operation's read.
> > > > > > 
> > > > > > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > > > > > when it looses the store.
> > > > > > 
> > > > > > Or is there more to it? Its not entirely clear from the Changelog, which
> > > > > > I feel should describe the reason for the behaviour.
> > > > > 
> > > > > If I've groked it correctly, it's for cases like:
> > > > > 
> > > > > 
> > > > > PO:
> > > > > Wx=1
> > > > > WyRel=1
> > > > > 
> > > > > P1:
> > > > > Wy=2
> > > > > 
> > > > > P2:
> > > > > RyAcq=2
> > > > > Rx=0
> > > > > 
> > > > > Final value of y is 2.
> > > > > 
> > > > > 
> > > > > This is permitted on arm64. If you make P1's store a store-release, then
> > > > > it's forbidden, but I suspect that's not generally true of the kernel
> > > > > memory model.
> > > > 
> > > > That is the one!  And to Peter's point, powerpc does the same for the
> > > > example as shown.  However, on powerpc, upgrading P1's store to release
> > > > has no effect because there is no earlier access for the resulting
> > > > lwsync to influence.  For whatever it might be worth, C11 won't guarantee
> > > > ordering in that case, either.  Nor will the current Linux-kernel memory
> > > > model.  (Yes, I did just try it to make sure.  Why do you ask?)
> > > > 
> > > > So you guys are fishing for an expanded commit log, for example, like
> > > > the following?  ;-)
> > > > 
> > > > 							Thanx, Paul
> > > > 
> > > > ------------------------------------------------------------------------
> > > > 
> > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > broken if a third process overwrites the value written by the RELEASE
> > > > operation before the ACQUIRE operation has a chance of reading it, for
> > > > example:
> > > > 
> > > > 	P0(int *x, int *y)
> > > > 	{
> > > > 		WRITE_ONCE(*x, 1);
> > > > 		smp_wmb();
> > > > 		smp_store_release(y, 1);
> > > > 	}
> > > > 
> > > > 	P1(int *y)
> > > > 	{
> > > > 		smp_store_release(y, 2);
> > > > 	}
> > > > 
> > > > 	P2(int *x, int *y)
> > > > 	{
> > > > 		r1 = smp_load_acquire(y);
> > > > 		r2 = READ_ONCE(*x);
> > > > 	}
> > > > 
> > > > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > > > r2=0), as does the current version of the early prototype Linux-kernel
> > > > memory model.
> > > 
> > > FWIW, ARM doesn't allow this and arm64 only allows it if P1 uses WRITE_ONCE
> > > instead of store-release.
> > 
> > Good catch, apologies for the error.  The following, then?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > broken if a third process overwrites the value written by the RELEASE
> > operation before the ACQUIRE operation has a chance of reading it, for
> > example:
> > 
> > 	P0(int *x, int *y)
> > 	{
> > 		WRITE_ONCE(*x, 1);
> > 		smp_wmb();
> > 		smp_store_release(y, 1);
> > 	}
> > 
> > 	P1(int *y)
> > 	{
> > 		WRITE_ONCE(*y, 2);
> > 	}
> > 
> > 	P2(int *x, int *y)
> > 	{
> > 		r1 = smp_load_acquire(y);
> > 		r2 = READ_ONCE(*x);
> > 	}
> > 
> > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > r2=0), as does the current version of the early prototype Linux-kernel
> 
> And the above needs to be (r1!=2 || r2 != 0)...  Sigh!

Make that (y==2 && r1==2 && r2 == 0).

Any further bids?  ;-)

							Thanx, Paul

> > memory model.

[toc] | [prev] | [next] | [standalone]

#1493676

On Thu, Sep 29, 2016 at 11:10:15AM -0700, Paul E. McKenney wrote:
> > > 
> > > 	P0(int *x, int *y)
> > > 	{
> > > 		WRITE_ONCE(*x, 1);
> > > 		smp_wmb();
> > > 		smp_store_release(y, 1);
> > > 	}
> > > 
> > > 	P1(int *y)
> > > 	{
> > > 		WRITE_ONCE(*y, 2);
> > > 	}
> > > 
> > > 	P2(int *x, int *y)
> > > 	{
> > > 		r1 = smp_load_acquire(y);
> > > 		r2 = READ_ONCE(*x);
> > > 	}
> > > 
> > > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > > r2=0), as does the current version of the early prototype Linux-kernel
> > 
> > And the above needs to be (r1!=2 || r2 != 0)...  Sigh!
> 
> Make that (y==2 && r1==2 && r2 == 0).
> 
> Any further bids?  ;-)

Isn't that the trivial P1,P2,P0 order again?

How about something like so on PPC?

P0(int *x, int *y)
{
	WRITE_ONCE(*x, 1);
	smp_store_release(y, 1);
}

P1(int *x, int *y)
{
	WRITE_ONCE(x, 2);
	smp_store_release(y, 2);
}

P2(int *x, int *y)
{
	r1 = smp_load_acquire(y);
	r2 = READ_ONCE(*x);
}

(((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)

If you execute P0 and P1 concurrently and one store of each 'wins' the
LWSYNC of either is null and void, and therefore P2 is unordered and can
observe r2==0.

[toc] | [prev] | [next] | [standalone]

#1493684

On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:
> On Thu, Sep 29, 2016 at 11:10:15AM -0700, Paul E. McKenney wrote:
> > > > 
> > > > 	P0(int *x, int *y)
> > > > 	{
> > > > 		WRITE_ONCE(*x, 1);
> > > > 		smp_wmb();
> > > > 		smp_store_release(y, 1);
> > > > 	}
> > > > 
> > > > 	P1(int *y)
> > > > 	{
> > > > 		WRITE_ONCE(*y, 2);
> > > > 	}
> > > > 
> > > > 	P2(int *x, int *y)
> > > > 	{
> > > > 		r1 = smp_load_acquire(y);
> > > > 		r2 = READ_ONCE(*x);
> > > > 	}
> > > > 
> > > > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > > > r2=0), as does the current version of the early prototype Linux-kernel
> > > 
> > > And the above needs to be (r1!=2 || r2 != 0)...  Sigh!
> > 
> > Make that (y==2 && r1==2 && r2 == 0).
> > 
> > Any further bids?  ;-)
> 
> Isn't that the trivial P1,P2,P0 order again?

I don't believe so.  Wouldn't the final P0 would leave y==1?

> How about something like so on PPC?
> 
> P0(int *x, int *y)
> {
> 	WRITE_ONCE(*x, 1);
> 	smp_store_release(y, 1);
> }
> 
> P1(int *x, int *y)
> {
> 	WRITE_ONCE(x, 2);

Need "WRITE_ONCE(*x, 2)" here.

> 	smp_store_release(y, 2);
> }
> 
> P2(int *x, int *y)
> {
> 	r1 = smp_load_acquire(y);
> 	r2 = READ_ONCE(*x);
> }
> 
> (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)

That exists-clause is quite dazzling...  So if each of P0 and P1
win, but on different stores, and if P2 follows one or the other
of P0 or P1, can r2 get the pre-initialization value for x?

> If you execute P0 and P1 concurrently and one store of each 'wins' the
> LWSYNC of either is null and void, and therefore P2 is unordered and can
> observe r2==0.

That vaguely resembles the infamous Z6.3, but only vaguely.  The Linux-kernel
memory model says "forbidden" to this:

	C C-WillDeacon-AcqRelStore.litmus

	{
	}

	P0(int *x, int *y)
	{
	      WRITE_ONCE(*x, 1);
	      smp_store_release(y, 1);
	}

	P1(int *x, int *y)
	{
	      WRITE_ONCE(*x, 2);
	      smp_store_release(y, 2);
	}

	P2(int *x, int *y)
	{
	      r1 = smp_load_acquire(y);
	      r2 = READ_ONCE(*x);
	}

	exists
	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)

So let's try PPCMEM.  If PPCMEM allows it, then the kernel model is
clearly broken.

	PPC PeterZijlstra+o-r+o-r+a-o-SB.litmus
	{
	0:r1=1; 0:r2=2; 0:r3=x; 0:r4=y;
	1:r1=1; 1:r2=2; 1:r3=x; 1:r4=y;
			2:r3=x; 2:r4=y;
	}
	 P0           | P1           | P2           ;
	 stw r1,0(r3) | stw r2,0(r3) | lwz r1,0(r4) ;
	 lwsync       | lwsync       | lwsync       ;
	 stw r1,0(r4) | stw r2,0(r4) | lwz r2,0(r3) ;
	exists
	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)

Now herd says that this is forbidden, but let's ask ppcmem.  Futzing with
the web site seems to say "no".  The lwsyncs insist on propagating the
change to x to P2 before the change to y.  The full-state-space search
tool might take awhile, so will get you know if it disagrees.  Just in
case I missed some odd combination of ppcmem events.

But at the moment, my guess is that your dazzling condition cannot
happen on PowerPC, and that at least this aspect of the current draft
of the kernel memory model is in fact correct.

Or did I incorrectly translate your litmus test?

							Thanx, Paul

[toc] | [prev] | [next] | [standalone]

#1493691

On Thu, 29 Sep 2016, Paul E. McKenney wrote:

> On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:

> > How about something like so on PPC?
> > 
> > P0(int *x, int *y)
> > {
> > 	WRITE_ONCE(*x, 1);
> > 	smp_store_release(y, 1);
> > }
> > 
> > P1(int *x, int *y)
> > {
> > 	WRITE_ONCE(x, 2);
> 
> Need "WRITE_ONCE(*x, 2)" here.
> 
> > 	smp_store_release(y, 2);
> > }
> > 
> > P2(int *x, int *y)
> > {
> > 	r1 = smp_load_acquire(y);
> > 	r2 = READ_ONCE(*x);
> > }
> > 
> > (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)
> 
> That exists-clause is quite dazzling...  So if each of P0 and P1
> win, but on different stores, and if P2 follows one or the other
> of P0 or P1, can r2 get the pre-initialization value for x?

In fact, this is more than you need.  It's enough to specify

exists (2:r1=1 \/ 2:r1=2) /\ 2:r2=0

This much already is forbidden.  For the sake of argument, say r1=1.  
Then P2 has read from P1's store-release.  By definition, P1's write to
x is visible to P2, so r2 will get the value from that write or from
one that is later in x's coherence order.  In other words, r2 will end
up equal to either 1 or 2, but not 0.

> > If you execute P0 and P1 concurrently and one store of each 'wins' the
> > LWSYNC of either is null and void, and therefore P2 is unordered and can
> > observe r2==0.

Not so.  lwsync instructions cannot be "voided".

> That vaguely resembles the infamous Z6.3, but only vaguely.  The Linux-kernel
> memory model says "forbidden" to this:
> 
> 	C C-WillDeacon-AcqRelStore.litmus
> 
> 	{
> 	}
> 
> 	P0(int *x, int *y)
> 	{
> 	      WRITE_ONCE(*x, 1);
> 	      smp_store_release(y, 1);
> 	}
> 
> 	P1(int *x, int *y)
> 	{
> 	      WRITE_ONCE(*x, 2);
> 	      smp_store_release(y, 2);
> 	}
> 
> 	P2(int *x, int *y)
> 	{
> 	      r1 = smp_load_acquire(y);
> 	      r2 = READ_ONCE(*x);
> 	}
> 
> 	exists
> 	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)

As above, you can leave out the part about the final values for x and 
y.  The test will still be forbidden.

On the other hand, there's no guarantee that if r1=1 at the end then r2 
will also be 1.  It's quite possible that r1=1 and r2=2, or vice versa.

Alan

[toc] | [prev] | [next] | [standalone]

#1493707

On Thu, Sep 29, 2016 at 03:36:38PM -0400, Alan Stern wrote:
> On Thu, 29 Sep 2016, Paul E. McKenney wrote:
> 
> > On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:
> 
> > > How about something like so on PPC?
> > > 
> > > P0(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	smp_store_release(y, 1);
> > > }
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(x, 2);
> > 
> > Need "WRITE_ONCE(*x, 2)" here.
> > 
> > > 	smp_store_release(y, 2);
> > > }
> > > 
> > > P2(int *x, int *y)
> > > {
> > > 	r1 = smp_load_acquire(y);
> > > 	r2 = READ_ONCE(*x);
> > > }
> > > 
> > > (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)
> > 
> > That exists-clause is quite dazzling...  So if each of P0 and P1
> > win, but on different stores, and if P2 follows one or the other
> > of P0 or P1, can r2 get the pre-initialization value for x?
> 
> In fact, this is more than you need.  It's enough to specify
> 
> exists (2:r1=1 \/ 2:r1=2) /\ 2:r2=0
> 
> This much already is forbidden.  For the sake of argument, say r1=1.  
> Then P2 has read from P1's store-release.  By definition, P1's write to
> x is visible to P2, so r2 will get the value from that write or from
> one that is later in x's coherence order.  In other words, r2 will end
> up equal to either 1 or 2, but not 0.
> 
> > > If you execute P0 and P1 concurrently and one store of each 'wins' the
> > > LWSYNC of either is null and void, and therefore P2 is unordered and can
> > > observe r2==0.
> 
> Not so.  lwsync instructions cannot be "voided".
> 
> > That vaguely resembles the infamous Z6.3, but only vaguely.  The Linux-kernel
> > memory model says "forbidden" to this:
> > 
> > 	C C-WillDeacon-AcqRelStore.litmus
> > 
> > 	{
> > 	}
> > 
> > 	P0(int *x, int *y)
> > 	{
> > 	      WRITE_ONCE(*x, 1);
> > 	      smp_store_release(y, 1);
> > 	}
> > 
> > 	P1(int *x, int *y)
> > 	{
> > 	      WRITE_ONCE(*x, 2);
> > 	      smp_store_release(y, 2);
> > 	}
> > 
> > 	P2(int *x, int *y)
> > 	{
> > 	      r1 = smp_load_acquire(y);
> > 	      r2 = READ_ONCE(*x);
> > 	}
> > 
> > 	exists
> > 	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)
> 
> As above, you can leave out the part about the final values for x and 
> y.  The test will still be forbidden.
> 
> On the other hand, there's no guarantee that if r1=1 at the end then r2 
> will also be 1.  It's quite possible that r1=1 and r2=2, or vice versa.

And herd agrees for both the kernel model and the powerpc translation.
I killed PPCMEM, which was up to 1.2G of state space.  So is this a
case where "herd -cat ppc.cat" can be trusted?  ;-)

And the web ppcmem does not allow the exists clause, from what I could
see.

							Thanx, Paul

[toc] | [prev] | [next] | [standalone]

#1493956

On Thu, Sep 29, 2016 at 03:36:38PM -0400, Alan Stern wrote:
> > > If you execute P0 and P1 concurrently and one store of each 'wins' the
> > > LWSYNC of either is null and void, and therefore P2 is unordered and can
> > > observe r2==0.
> 
> Not so.  lwsync instructions cannot be "voided".

I distinctly remember there being a case (smp_wmb()) where the lwsync
would disappear if the store was lost.

[toc] | [prev] | [next] | [standalone]

#1493972

On Thu, Sep 29, 2016 at 12:18:58PM -0700, Paul E. McKenney wrote:
> On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:
> > On Thu, Sep 29, 2016 at 11:10:15AM -0700, Paul E. McKenney wrote:
> > > > > 
> > > > > 	P0(int *x, int *y)
> > > > > 	{
> > > > > 		WRITE_ONCE(*x, 1);
> > > > > 		smp_wmb();
> > > > > 		smp_store_release(y, 1);
> > > > > 	}
> > > > > 
> > > > > 	P1(int *y)
> > > > > 	{
> > > > > 		WRITE_ONCE(*y, 2);
> > > > > 	}
> > > > > 
> > > > > 	P2(int *x, int *y)
> > > > > 	{
> > > > > 		r1 = smp_load_acquire(y);
> > > > > 		r2 = READ_ONCE(*x);
> > > > > 	}
> > > > > 
> > > > > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > > > > r2=0), as does the current version of the early prototype Linux-kernel
> > > > 
> > > > And the above needs to be (r1!=2 || r2 != 0)...  Sigh!
> > > 
> > > Make that (y==2 && r1==2 && r2 == 0).
> > > 
> > > Any further bids?  ;-)
> > 
> > Isn't that the trivial P1,P2,P0 order again?
> 
> I don't believe so.  Wouldn't the final P0 would leave y==1?

Ah, indeed. I was forgetting to 'execute' P0 entirely.

[toc] | [prev] | [next] | [standalone]

#1494005

On Thu, Sep 29, 2016 at 12:18:58PM -0700, Paul E. McKenney wrote:
> On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:

> > How about something like so on PPC?
> > 
> > P0(int *x, int *y)
> > {
> > 	WRITE_ONCE(*x, 1);
> > 	smp_store_release(y, 1);
> > }
> > 
> > P1(int *x, int *y)
> > {
> > 	WRITE_ONCE(x, 2);
> 
> Need "WRITE_ONCE(*x, 2)" here.
> 
> > 	smp_store_release(y, 2);
> > }
> > 
> > P2(int *x, int *y)
> > {
> > 	r1 = smp_load_acquire(y);
> > 	r2 = READ_ONCE(*x);
> > }
> > 
> > (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)
> 
> That exists-clause is quite dazzling...  So if each of P0 and P1
> win, but on different stores, and if P2 follows one or the other
> of P0 or P1, can r2 get the pre-initialization value for x?
> 
> > If you execute P0 and P1 concurrently and one store of each 'wins' the
> > LWSYNC of either is null and void, and therefore P2 is unordered and can
> > observe r2==0.
> 
> That vaguely resembles the infamous Z6.3, but only vaguely.  The Linux-kernel
> memory model says "forbidden" to this:

  https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/ppc710.html

That one, right?

Hmm, I seem to remember something else.. /me goes poke through history
and comes up with:

  https://lkml.kernel.org/r/20160115215853.GC3818@linux.vnet.ibm.com

So what was that about then? I remember it being a completely
nonsensical case, but a weird one.

> So let's try PPCMEM.  If PPCMEM allows it, then the kernel model is
> clearly broken.
> 
> 	PPC PeterZijlstra+o-r+o-r+a-o-SB.litmus
> 	{
> 	0:r1=1; 0:r2=2; 0:r3=x; 0:r4=y;
> 	1:r1=1; 1:r2=2; 1:r3=x; 1:r4=y;
> 			2:r3=x; 2:r4=y;
> 	}
> 	 P0           | P1           | P2           ;
> 	 stw r1,0(r3) | stw r2,0(r3) | lwz r1,0(r4) ;
> 	 lwsync       | lwsync       | lwsync       ;
> 	 stw r1,0(r4) | stw r2,0(r4) | lwz r2,0(r3) ;
> 	exists
> 	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)

> Or did I incorrectly translate your litmus test?

Looks about right.

Still not seeing how that is prohibited though. My reasoning is as
follows:

 - P0 and P1 both store to x, one looses (say P0). Effectively only P1
   does a store.

 - P0 and P1 both store to y, one looses (say P1). Effectively only P0
   does a store.

 - P2 reads y, sees the value from P0.

 - P2 does lwsync, which constraints P2 to not issue the load of x
   before this. It also forms a (local) sync-point with P0 for having
   seen its store or y.

 - P2 reads x, sees the initial value because the store from P1 hasn't
   been propagated yet.

It will not see the store P0 did to x, since that didn't happen.

Assuming I'm wrong on that last part, is then the following possible?

(x=2 /\ y=1 /\ 2:r1=1 /\ 2:r2=1)

Where we see a store that didn't happen?

[toc] | [prev] | [next] | [standalone]

#1494065

On Fri, Sep 30, 2016 at 11:57:38AM +0200, Peter Zijlstra wrote:
> On Thu, Sep 29, 2016 at 12:18:58PM -0700, Paul E. McKenney wrote:
> > On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:
> 
> > > How about something like so on PPC?
> > > 
> > > P0(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	smp_store_release(y, 1);
> > > }
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(x, 2);
> > 
> > Need "WRITE_ONCE(*x, 2)" here.
> > 
> > > 	smp_store_release(y, 2);
> > > }
> > > 
> > > P2(int *x, int *y)
> > > {
> > > 	r1 = smp_load_acquire(y);
> > > 	r2 = READ_ONCE(*x);
> > > }
> > > 
> > > (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)
> > 
> > That exists-clause is quite dazzling...  So if each of P0 and P1
> > win, but on different stores, and if P2 follows one or the other
> > of P0 or P1, can r2 get the pre-initialization value for x?
> > 
> > > If you execute P0 and P1 concurrently and one store of each 'wins' the
> > > LWSYNC of either is null and void, and therefore P2 is unordered and can
> > > observe r2==0.
> > 
> > That vaguely resembles the infamous Z6.3, but only vaguely.  The Linux-kernel
> > memory model says "forbidden" to this:
> 
>   https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/ppc710.html
> 
> That one, right?

That is the one!  Prohibiting the cycle requires smp_mb() on both threads
0 and 1 on the one hand, or on both threads 0 and 2 on the other hand.

> Hmm, I seem to remember something else.. /me goes poke through history
> and comes up with:
> 
>   https://lkml.kernel.org/r/20160115215853.GC3818@linux.vnet.ibm.com
> 
> So what was that about then? I remember it being a completely
> nonsensical case, but a weird one.

That was an Alan Stern example where PowerPC prohibits the outcome,
and the ppcmem tool agrees, but where herd does not.  (ppcmem is giving
the correct answer.)

But this is specific to PowerPC.  I would not advise writing code that
relies on this one.  ;-)

> > So let's try PPCMEM.  If PPCMEM allows it, then the kernel model is
> > clearly broken.
> > 
> > 	PPC PeterZijlstra+o-r+o-r+a-o-SB.litmus
> > 	{
> > 	0:r1=1; 0:r2=2; 0:r3=x; 0:r4=y;
> > 	1:r1=1; 1:r2=2; 1:r3=x; 1:r4=y;
> > 			2:r3=x; 2:r4=y;
> > 	}
> > 	 P0           | P1           | P2           ;
> > 	 stw r1,0(r3) | stw r2,0(r3) | lwz r1,0(r4) ;
> > 	 lwsync       | lwsync       | lwsync       ;
> > 	 stw r1,0(r4) | stw r2,0(r4) | lwz r2,0(r3) ;
> > 	exists
> > 	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)
> 
> > Or did I incorrectly translate your litmus test?
> 
> Looks about right.
> 
> Still not seeing how that is prohibited though. My reasoning is as
> follows:
> 
>  - P0 and P1 both store to x, one looses (say P0). Effectively only P1
>    does a store.
> 
>  - P0 and P1 both store to y, one looses (say P1). Effectively only P0
>    does a store.

PowerPC does not "obscure" stores, so both stores really are there and
the lwsync really has effect on all CPUs.  From what I understand, even
CPUs that do obscure stores only do so in the case of repeated stores
by the same CPU to the same variable, and the above litmus test doesn't
have this.

So all the stores happen, and each CPU's stores are at least locally
ordered.

>  - P2 reads y, sees the value from P0.

Fair enough!

>  - P2 does lwsync, which constraints P2 to not issue the load of x
>    before this. It also forms a (local) sync-point with P0 for having
>    seen its store or y.
> 
>  - P2 reads x, sees the initial value because the store from P1 hasn't
>    been propagated yet.
> 
> It will not see the store P0 did to x, since that didn't happen.

Well, it saw the store to y, so it absolutely must see one of the other of
the stores to x in this particular litmus test.  If P1's store overwrote
P0's store, then P2 has to see P1's store, for example.

> Assuming I'm wrong on that last part, is then the following possible?
> 
> (x=2 /\ y=1 /\ 2:r1=1 /\ 2:r2=1)
> 
> Where we see a store that didn't happen?

Again, both stores really did happen.  ;-)

So with this litmus test:

	PPC PeterZijlstra+o-r+o-r+a-o-SB.litmus
	{
	0:r1=1; 0:r2=2; 0:r3=x; 0:r4=y;
	1:r1=1; 1:r2=2; 1:r3=x; 1:r4=y;
			2:r3=x; 2:r4=y;
	}
	 P0           | P1           | P2           ;
	 stw r1,0(r3) | stw r2,0(r3) | lwz r1,0(r4) ;
	 lwsync       | lwsync       | lwsync       ;
	 stw r1,0(r4) | stw r2,0(r4) | lwz r2,0(r3) ;
	exists
	(x=2 /\ y=1 /\ 2:r1=1 /\ 2:r2=1)

The herd tool says:

	Test PeterZijlstra+o-r+o-r+a-o-SB Allowed
	States 24
	2:r1=0; 2:r2=0; x=1; y=1;
	2:r1=0; 2:r2=0; x=1; y=2;
	2:r1=0; 2:r2=0; x=2; y=1;
	2:r1=0; 2:r2=0; x=2; y=2;
	2:r1=0; 2:r2=1; x=1; y=1;
	2:r1=0; 2:r2=1; x=1; y=2;
	2:r1=0; 2:r2=1; x=2; y=1;
	2:r1=0; 2:r2=1; x=2; y=2;
	2:r1=0; 2:r2=2; x=1; y=1;
	2:r1=0; 2:r2=2; x=1; y=2;
	2:r1=0; 2:r2=2; x=2; y=1;
	2:r1=0; 2:r2=2; x=2; y=2;
	2:r1=1; 2:r2=1; x=1; y=1;
	2:r1=1; 2:r2=1; x=1; y=2;
	2:r1=1; 2:r2=1; x=2; y=1;
	2:r1=1; 2:r2=1; x=2; y=2;
	2:r1=1; 2:r2=2; x=2; y=1;
	2:r1=1; 2:r2=2; x=2; y=2;
	2:r1=2; 2:r2=1; x=1; y=1;
	2:r1=2; 2:r2=1; x=1; y=2;
	2:r1=2; 2:r2=2; x=1; y=1;
	2:r1=2; 2:r2=2; x=1; y=2;
	2:r1=2; 2:r2=2; x=2; y=1;
	2:r1=2; 2:r2=2; x=2; y=2;
	Ok
	Witnesses
	Positive: 1 Negative: 23
	Condition exists (x=2 /\ y=1 /\ 2:r1=1 /\ 2:r2=1)
	Observation PeterZijlstra+o-r+o-r+a-o-SB Sometimes 1 23
	Hash=c32afd1ac8bfee7d4b23a27e783d0998

So herd believes that it can happen.  I was also able to force the web
ppcmem tool (https://www.cl.cam.ac.uk/~pes20/ppcmem/index.html) to get
into this state with the following sequence of choices:

	[0;5;4;0;0;4;4;2;2;2;4;4;1;1;1;7;6;0;0;3;4;0;1;2;5;0;0]

So, yes, this can happen, architecturally at least.

							Thanx, Paul

[toc] | [prev] | [next] | [standalone]

#1494084

On Fri, Sep 30, 2016 at 05:14:03AM -0700, Paul E. McKenney wrote:
> PowerPC does not "obscure" stores, so both stores really are there and
> the lwsync really has effect on all CPUs.  From what I understand, even
> CPUs that do obscure stores only do so in the case of repeated stores
> by the same CPU to the same variable, and the above litmus test doesn't
> have this.
> 
> So all the stores happen, and each CPU's stores are at least locally
> ordered.

OK, when I'm not sure I ever understood the case where smp_wmb() went
wonky on PPC, sadly I cannot now find the email where you mentioned
that :/

[toc] | [prev] | [next] | [standalone]

#1494115

On Fri, Sep 30, 2016 at 02:51:13PM +0200, Peter Zijlstra wrote:
> On Fri, Sep 30, 2016 at 05:14:03AM -0700, Paul E. McKenney wrote:
> > PowerPC does not "obscure" stores, so both stores really are there and
> > the lwsync really has effect on all CPUs.  From what I understand, even
> > CPUs that do obscure stores only do so in the case of repeated stores
> > by the same CPU to the same variable, and the above litmus test doesn't
> > have this.
> > 
> > So all the stores happen, and each CPU's stores are at least locally
> > ordered.
> 
> OK, when I'm not sure I ever understood the case where smp_wmb() went
> wonky on PPC, sadly I cannot now find the email where you mentioned
> that :/

First, a better explanation of your example:

	PPC PeterZijlstra+o-r+o-r+a-o-SB.litmus
	{
	0:r1=1; 0:r2=2; 0:r3=x; 0:r4=y;
	1:r1=1; 1:r2=2; 1:r3=x; 1:r4=y;
			2:r3=x; 2:r4=y;
	}
	 P0           | P1           | P2           ;
	 stw r1,0(r3) | stw r2,0(r3) | lwz r1,0(r4) ;
	 lwsync       | lwsync       | lwsync       ;
	 stw r1,0(r4) | stw r2,0(r4) | lwz r2,0(r3) ;
	exists
	(x=2 /\ y=1 /\ 2:r1=1 /\ 2:r2=1)

Given that 2:r1=1, and ignoring P1 for the moment, we have simple message
passing.  If P2 sees P0's store to y, it must also see P0's store to x.

So what happens when we include P1?  Well, we have constrained the test
to the case where P2 sees P0's store to y, so P2's load from x must
still see P0's store to x, or some later store to x.  Either way, given
that P2 sees P0's store to y, it cannot see the initial value of x.
In other words, even if P0's store to x is overwritten, it still has
effect on the ordering.

There are several changes to the litmus test that could require ordering
that lwsync does not provide, which I suppose could be considered to
introduce wonkiness.  ;-)

One is the infamous "Z6.3" litmus test that you called out in your
earlier email.  At least one of the pairs of stores must be separated
by sync rather than lwsync.  Z6.3's third variable defeats lwsync's
local ordering.

							Thanx, Paul

[toc] | [prev] | [next] | [standalone]

#1493901

[Multipart message — attachments visible in raw view] — view raw

Hi Paul,

On Thu, Sep 29, 2016 at 10:23:22AM -0700, Paul E. McKenney wrote:
> On Thu, Sep 29, 2016 at 06:10:37PM +0100, Will Deacon wrote:
> > On Thu, Sep 29, 2016 at 09:43:53AM -0700, Paul E. McKenney wrote:
> > > On Thu, Sep 29, 2016 at 05:03:08PM +0100, Will Deacon wrote:
> > > > On Thu, Sep 29, 2016 at 05:58:17PM +0200, Peter Zijlstra wrote:
> > > > > On Thu, Sep 29, 2016 at 08:54:01AM -0700, Paul E. McKenney wrote:
> > > > > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > > > > broken if a third process overwrites the value written by the RELEASE
> > > > > > operation before the ACQUIRE operation has a chance of reading it.
> > > > > > This commit therefore updates the documentation to call this vulnerability
> > > > > > out explicitly.
> > > > > > 
> > > > > > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > > > 
> > > > > > +     However, please note that a chain of RELEASE+ACQUIRE pairs may be
> > > > > > +     broken by a store by another thread that overwrites the RELEASE
> > > > > > +     operation's store before the ACQUIRE operation's read.
> > > > > 
> > > > > This is the powerpc lwsync quirk, right? Where the barrier disappears
> > > > > when it looses the store.
> > > > > 
> > > > > Or is there more to it? Its not entirely clear from the Changelog, which
> > > > > I feel should describe the reason for the behaviour.
> > > > 
> > > > If I've groked it correctly, it's for cases like:
> > > > 
> > > > 
> > > > PO:
> > > > Wx=1
> > > > WyRel=1
> > > > 
> > > > P1:
> > > > Wy=2
> > > > 
> > > > P2:
> > > > RyAcq=2
> > > > Rx=0
> > > > 
> > > > Final value of y is 2.
> > > > 
> > > > 
> > > > This is permitted on arm64. If you make P1's store a store-release, then
> > > > it's forbidden, but I suspect that's not generally true of the kernel
> > > > memory model.
> > > 
> > > That is the one!  And to Peter's point, powerpc does the same for the
> > > example as shown.  However, on powerpc, upgrading P1's store to release
> > > has no effect because there is no earlier access for the resulting
> > > lwsync to influence.  For whatever it might be worth, C11 won't guarantee
> > > ordering in that case, either.  Nor will the current Linux-kernel memory
> > > model.  (Yes, I did just try it to make sure.  Why do you ask?)
> > > 
> > > So you guys are fishing for an expanded commit log, for example, like
> > > the following?  ;-)
> > > 
> > > 							Thanx, Paul
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> > > broken if a third process overwrites the value written by the RELEASE
> > > operation before the ACQUIRE operation has a chance of reading it, for
> > > example:
> > > 
> > > 	P0(int *x, int *y)
> > > 	{
> > > 		WRITE_ONCE(*x, 1);
> > > 		smp_wmb();
> > > 		smp_store_release(y, 1);
> > > 	}
> > > 
> > > 	P1(int *y)
> > > 	{
> > > 		smp_store_release(y, 2);
> > > 	}
> > > 
> > > 	P2(int *x, int *y)
> > > 	{
> > > 		r1 = smp_load_acquire(y);
> > > 		r2 = READ_ONCE(*x);
> > > 	}
> > > 
> > > Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> > > r2=0), as does the current version of the early prototype Linux-kernel
> > > memory model.
> > 
> > FWIW, ARM doesn't allow this and arm64 only allows it if P1 uses WRITE_ONCE
> > instead of store-release.
> 
> Good catch, apologies for the error.  The following, then?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> If two processes are related by a RELEASE+ACQUIRE pair, ordering can be
> broken if a third process overwrites the value written by the RELEASE
> operation before the ACQUIRE operation has a chance of reading it, for
> example:
> 
> 	P0(int *x, int *y)
> 	{
> 		WRITE_ONCE(*x, 1);
> 		smp_wmb();
               ^^^^^^^^^^^

What is this smp_wmb() for?

> 		smp_store_release(y, 1);
> 	}
> 
> 	P1(int *y)
> 	{
> 		WRITE_ONCE(*y, 2);

If we change this WRITE_ONCE to a relaxed atomic operation(e.g.
xchg_relaxed(y, 2)), both herd and ppcmem said the exist-clause "y = 2
/\ 2:r1 = 2 /\ 2:r2 = 0" wouldn't be triggered on PPC.

I guess we will get the same behavior on ARM/ARM64, Will?

If a normal store could break chain, while a RmW atomic won't, do we
want to call it out in the document and build our memory model around
this?

I asked because in spin_unlock_wait() fix, we kind of relied on this. So
it's good for us to clarify it?

Regards,
Boqun

> 	}
> 
> 	P2(int *x, int *y)
> 	{
> 		r1 = smp_load_acquire(y);
> 		r2 = READ_ONCE(*x);
> 	}
> 
> Both ARM and powerpc allow the "after the dust settles" outcome (r1=2 &&
> r2=0), as does the current version of the early prototype Linux-kernel
> memory model.
> 

[toc] | [prev] | [next] | [standalone]

Page 1 of 2  [1] 2  Next page →

Back to top | Article view | linux.kernel

csiph-web