Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > linux.kernel > #1700264 > unrolled thread
| Started by | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| First post | 2017-07-31 19:50 +0200 |
| Last post | 2017-08-01 15:40 +0200 |
| Articles | 20 — 4 participants |
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.
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-07-31 19:50 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Boqun Feng <boqun.feng@gmail.com> - 2017-08-01 04:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Peter Zijlstra <peterz@infradead.org> - 2017-08-01 11:10 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Will Deacon <will.deacon@arm.com> - 2017-08-01 12:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Peter Zijlstra <peterz@infradead.org> - 2017-08-01 13:50 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Will Deacon <will.deacon@arm.com> - 2017-08-01 14:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Peter Zijlstra <peterz@infradead.org> - 2017-08-01 15:00 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-01 18:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Peter Zijlstra <peterz@infradead.org> - 2017-08-01 18:50 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Will Deacon <will.deacon@arm.com> - 2017-08-01 19:00 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-02 00:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Will Deacon <will.deacon@arm.com> - 2017-08-02 10:50 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-01 20:40 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Will Deacon <will.deacon@arm.com> - 2017-08-02 11:50 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-02 18:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Boqun Feng <boqun.feng@gmail.com> - 2017-08-03 16:10 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-03 17:00 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents Will Deacon <will.deacon@arm.com> - 2017-08-03 18:20 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-03 19:10 +0200
Re: [RFC][PATCH v3]: documentation,atomic: Add new documents "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> - 2017-08-01 15:40 +0200
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-07-31 19:50 +0200 |
| Subject | Re: [RFC][PATCH v3]: documentation,atomic: Add new documents |
| Message-ID | <u9mZj-Kh-9@gated-at.bofh.it> |
On Mon, Jul 31, 2017 at 07:04:03PM +0800, Boqun Feng wrote:
> On Mon, Jul 31, 2017 at 11:05:35AM +0200, Peter Zijlstra wrote:
> > On Wed, Jul 26, 2017 at 08:47:50PM +0800, Boqun Feng wrote:
> >
> > > > +
> > > > +Further, while something like:
> > > > +
> > > > + smp_mb__before_atomic();
> > > > + atomic_dec(&X);
> > > > +
> > > > +is a 'typical' RELEASE pattern, the barrier is strictly stronger than
> > > > +a RELEASE. Similarly for something like:
> > > > +
> > >
> > > .. at here. Maybe you planned to put stronger ACQUIRE pattern?
> >
> > Yes, although I struggled to find a sensible one. The problem is that
> > ACQUIRE is on loads and value returning atomics have an ACQUIRE variant,
> > so why would you ever want to use smp_mb__after_atomic() for this.
> >
> >
> > That is, the best I could come up with is something like:
> >
> > val = atomic_fetch_or_relaxed(1, &var);
> > smp_mb__after_atomic();
> >
> > But in that case we should've just written:
> >
> > val = atomic_fetch_or_acquire(1, &var);
> >
>
> Agreed.
>
> And besides, in memory-barriers.txt, the wording is:
>
> (*) smp_mb__before_atomic();
> (*) smp_mb__after_atomic();
>
> These are for use with atomic (such as add, subtract, increment and
> decrement) functions that don't return a value, especially when used for
> reference counting.
>
> So actually, using smp_mb__after_atomic() for ACQUIRE is a misuse.
You lost me on this one.
Why wouldn't the following have ACQUIRE semantics?
atomic_inc(&var);
smp_mb__after_atomic();
Is the issue that there is no actual value returned or some such?
> > Suggestions?
>
> As a result, I think it's better we say smp_mb__{before,after}_atomic()
> are only for 1) non-value-returning RmW atomic ops, 2)
> {set,clear,change}_bit and 3) internal use of atomic primitives(e.g. the
> generic version of fully ordered atomics).
>
> 1) prevents people to use it for an ACQUIRE, but allows for a RELEASE.
> 1) & 2) makes atomic_t.txt consistent with memory-barriers.txt
> 3) explains our usage of those barriers internally.
>
> Thoughts?
So if I have something like this, the assertion really can trigger?
WRITE_ONCE(x, 1); atomic_inc(&y);
r0 = xchg_release(&y, 5); smp_mb__after_atomic();
r1 = READ_ONCE(x);
WARN_ON(r0 == 0 && r1 == 0);
I must confess that I am not seeing why we would want to allow this
outcome.
Thanx, Paul
[toc] | [next] | [standalone]
| From | Boqun Feng <boqun.feng@gmail.com> |
|---|---|
| Date | 2017-08-01 04:20 +0200 |
| Message-ID | <u9uWT-5OL-15@gated-at.bofh.it> |
| In reply to | #1700264 |
[Multipart message — attachments visible in raw view] — view raw
On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote:
> On Mon, Jul 31, 2017 at 07:04:03PM +0800, Boqun Feng wrote:
> > On Mon, Jul 31, 2017 at 11:05:35AM +0200, Peter Zijlstra wrote:
> > > On Wed, Jul 26, 2017 at 08:47:50PM +0800, Boqun Feng wrote:
> > >
> > > > > +
> > > > > +Further, while something like:
> > > > > +
> > > > > + smp_mb__before_atomic();
> > > > > + atomic_dec(&X);
> > > > > +
> > > > > +is a 'typical' RELEASE pattern, the barrier is strictly stronger than
> > > > > +a RELEASE. Similarly for something like:
> > > > > +
> > > >
> > > > .. at here. Maybe you planned to put stronger ACQUIRE pattern?
> > >
> > > Yes, although I struggled to find a sensible one. The problem is that
> > > ACQUIRE is on loads and value returning atomics have an ACQUIRE variant,
> > > so why would you ever want to use smp_mb__after_atomic() for this.
> > >
> > >
> > > That is, the best I could come up with is something like:
> > >
> > > val = atomic_fetch_or_relaxed(1, &var);
> > > smp_mb__after_atomic();
> > >
> > > But in that case we should've just written:
> > >
> > > val = atomic_fetch_or_acquire(1, &var);
> > >
> >
> > Agreed.
> >
> > And besides, in memory-barriers.txt, the wording is:
> >
> > (*) smp_mb__before_atomic();
> > (*) smp_mb__after_atomic();
> >
> > These are for use with atomic (such as add, subtract, increment and
> > decrement) functions that don't return a value, especially when used for
> > reference counting.
> >
> > So actually, using smp_mb__after_atomic() for ACQUIRE is a misuse.
>
> You lost me on this one.
>
> Why wouldn't the following have ACQUIRE semantics?
>
> atomic_inc(&var);
> smp_mb__after_atomic();
>
> Is the issue that there is no actual value returned or some such?
>
That "misuse" is a wrong word there ;-(
I actually meant "the usage is correct but we don't encourage using
smp_mb__after_atomic() *only* for an ACQUIRE, because _acquire() could
always be used in that case, as Peter said".
In fact in your case, the ordering is stronger, both the load and store
part of the atomic op are ordered with the memory ops following it.
In short, I suggested we tell users to use
smp_mb__{before,after}_atomic() only when _{release,acquire} ops don't
suffice, i.e. for an RCsc RELEASE or a smp_mb() to order ops other than
the atomic op itself(like the one you use in __call_rcu_nocb_enqueue()).
But maybe this is too strict, and Peter said he would write something
about it in IRC, so I'm not that stick to this suggestion ;-)
Regards,
Boqun
> > > Suggestions?
> >
> > As a result, I think it's better we say smp_mb__{before,after}_atomic()
> > are only for 1) non-value-returning RmW atomic ops, 2)
> > {set,clear,change}_bit and 3) internal use of atomic primitives(e.g. the
> > generic version of fully ordered atomics).
> >
> > 1) prevents people to use it for an ACQUIRE, but allows for a RELEASE.
> > 1) & 2) makes atomic_t.txt consistent with memory-barriers.txt
> > 3) explains our usage of those barriers internally.
> >
> > Thoughts?
>
> So if I have something like this, the assertion really can trigger?
>
> WRITE_ONCE(x, 1); atomic_inc(&y);
> r0 = xchg_release(&y, 5); smp_mb__after_atomic();
> r1 = READ_ONCE(x);
>
>
> WARN_ON(r0 == 0 && r1 == 0);
>
> I must confess that I am not seeing why we would want to allow this
> outcome.
>
> Thanx, Paul
>
[toc] | [prev] | [next] | [standalone]
| From | Peter Zijlstra <peterz@infradead.org> |
|---|---|
| Date | 2017-08-01 11:10 +0200 |
| Message-ID | <u9BlE-1r3-25@gated-at.bofh.it> |
| In reply to | #1700264 |
On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote: > Why wouldn't the following have ACQUIRE semantics? > > atomic_inc(&var); > smp_mb__after_atomic(); > > Is the issue that there is no actual value returned or some such? Yes, so that the inc is a load-store, and thus there is a load, we loose the value. But I see your point I think. Irrespective of still having the value, the ordering is preserved and nothing should pass across that. > So if I have something like this, the assertion really can trigger? > > WRITE_ONCE(x, 1); atomic_inc(&y); > r0 = xchg_release(&y, 5); smp_mb__after_atomic(); > r1 = READ_ONCE(x); > > > WARN_ON(r0 == 0 && r1 == 0); > > I must confess that I am not seeing why we would want to allow this > outcome. No you are indeed quite right. I just wasn't creative enough. Thanks for the inspiration.
[toc] | [prev] | [next] | [standalone]
| From | Will Deacon <will.deacon@arm.com> |
|---|---|
| Date | 2017-08-01 12:20 +0200 |
| Message-ID | <u9Cro-2tI-9@gated-at.bofh.it> |
| In reply to | #1700768 |
On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote: > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote: > > > Why wouldn't the following have ACQUIRE semantics? > > > > atomic_inc(&var); > > smp_mb__after_atomic(); > > > > Is the issue that there is no actual value returned or some such? > > Yes, so that the inc is a load-store, and thus there is a load, we loose > the value. > > But I see your point I think. Irrespective of still having the value, > the ordering is preserved and nothing should pass across that. > > > So if I have something like this, the assertion really can trigger? > > > > WRITE_ONCE(x, 1); atomic_inc(&y); > > r0 = xchg_release(&y, 5); smp_mb__after_atomic(); > > r1 = READ_ONCE(x); > > > > > > WARN_ON(r0 == 0 && r1 == 0); > > > > I must confess that I am not seeing why we would want to allow this > > outcome. > > No you are indeed quite right. I just wasn't creative enough. Thanks for > the inspiration. Just to close this out, we agree that an smp_rmb() instead of smp_mb__after_atomic() would *not* forbid this outcome, right? Will
[toc] | [prev] | [next] | [standalone]
| From | Peter Zijlstra <peterz@infradead.org> |
|---|---|
| Date | 2017-08-01 13:50 +0200 |
| Message-ID | <u9DQu-3tn-23@gated-at.bofh.it> |
| In reply to | #1700809 |
On Tue, Aug 01, 2017 at 11:19:00AM +0100, Will Deacon wrote: > On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote: > > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote: > > > > > Why wouldn't the following have ACQUIRE semantics? > > > > > > atomic_inc(&var); > > > smp_mb__after_atomic(); > > > > > > Is the issue that there is no actual value returned or some such? > > > > Yes, so that the inc is a load-store, and thus there is a load, we loose > > the value. > > > > But I see your point I think. Irrespective of still having the value, > > the ordering is preserved and nothing should pass across that. > > > > > So if I have something like this, the assertion really can trigger? > > > > > > WRITE_ONCE(x, 1); atomic_inc(&y); > > > r0 = xchg_release(&y, 5); smp_mb__after_atomic(); > > > r1 = READ_ONCE(x); > > > > > > > > > WARN_ON(r0 == 0 && r1 == 0); > > > > > > I must confess that I am not seeing why we would want to allow this > > > outcome. > > > > No you are indeed quite right. I just wasn't creative enough. Thanks for > > the inspiration. > > Just to close this out, we agree that an smp_rmb() instead of > smp_mb__after_atomic() would *not* forbid this outcome, right? So that really hurts my brain. Per the normal rules that smp_rmb() would order the read of @x against the last ll of @y and per ll/sc ordering you then still don't get to make the WARN happen. On IRC you explained that your 8.1 LSE instructions are not in fact ordered by a smp_rmb, only by smp_wmb, which is 'surprising' since you really need to load the old value to compute the new value. Not happy... :-(
[toc] | [prev] | [next] | [standalone]
| From | Will Deacon <will.deacon@arm.com> |
|---|---|
| Date | 2017-08-01 14:20 +0200 |
| Message-ID | <u9Ejw-3Ut-19@gated-at.bofh.it> |
| In reply to | #1700924 |
On Tue, Aug 01, 2017 at 01:47:44PM +0200, Peter Zijlstra wrote: > On Tue, Aug 01, 2017 at 11:19:00AM +0100, Will Deacon wrote: > > On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote: > > > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote: > > > > > > > Why wouldn't the following have ACQUIRE semantics? > > > > > > > > atomic_inc(&var); > > > > smp_mb__after_atomic(); > > > > > > > > Is the issue that there is no actual value returned or some such? > > > > > > Yes, so that the inc is a load-store, and thus there is a load, we loose > > > the value. > > > > > > But I see your point I think. Irrespective of still having the value, > > > the ordering is preserved and nothing should pass across that. > > > > > > > So if I have something like this, the assertion really can trigger? > > > > > > > > WRITE_ONCE(x, 1); atomic_inc(&y); > > > > r0 = xchg_release(&y, 5); smp_mb__after_atomic(); > > > > r1 = READ_ONCE(x); > > > > > > > > > > > > WARN_ON(r0 == 0 && r1 == 0); > > > > > > > > I must confess that I am not seeing why we would want to allow this > > > > outcome. > > > > > > No you are indeed quite right. I just wasn't creative enough. Thanks for > > > the inspiration. > > > > Just to close this out, we agree that an smp_rmb() instead of > > smp_mb__after_atomic() would *not* forbid this outcome, right? > > So that really hurts my brain. Per the normal rules that smp_rmb() would > order the read of @x against the last ll of @y and per ll/sc ordering > you then still don't get to make the WARN happen. > > On IRC you explained that your 8.1 LSE instructions are not in fact > ordered by a smp_rmb, only by smp_wmb, which is 'surprising' since you > really need to load the old value to compute the new value. To be clear, it's only the ST* variants of the LSE instructions that are treated as a write for the purposes of memory ordering, so these are the non-*_return variants. It's not unlikely that other architectures will exhibit the same behaviour (e.g. Power, RISC-V), because the CPU can treat non-return atomics as "fire-and-forget" and have them handled elsewhere in the memory subsystem, causing them to be treated similarly to posted writes. For the code snippet above, the second thread has no idea about the value of y and so smp_rmb() is the wrong thing to be using imo. It really cares about ordering the store to y before the read of x, so needs a full mb (i.e. the test is more like 'R' than 'MP'). Also, wouldn't this problem also arise if your atomics were built using a spinlock where unlock had release semantics? Will
[toc] | [prev] | [next] | [standalone]
| From | Peter Zijlstra <peterz@infradead.org> |
|---|---|
| Date | 2017-08-01 15:00 +0200 |
| Message-ID | <u9EWd-47K-9@gated-at.bofh.it> |
| In reply to | #1700954 |
On Tue, Aug 01, 2017 at 01:17:13PM +0100, Will Deacon wrote: > Also, wouldn't this problem also arise if your atomics were built using a > spinlock where unlock had release semantics? I'm hoping none of our spnilock based atomics have weak ordering. Spinlock based atomics are a little crazy to begin with, making them weak *shudder*.
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-01 18:20 +0200 |
| Message-ID | <u9I3M-6bX-15@gated-at.bofh.it> |
| In reply to | #1700954 |
On Tue, Aug 01, 2017 at 01:17:13PM +0100, Will Deacon wrote:
> On Tue, Aug 01, 2017 at 01:47:44PM +0200, Peter Zijlstra wrote:
> > On Tue, Aug 01, 2017 at 11:19:00AM +0100, Will Deacon wrote:
> > > On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote:
> > > > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote:
> > > >
> > > > > Why wouldn't the following have ACQUIRE semantics?
> > > > >
> > > > > atomic_inc(&var);
> > > > > smp_mb__after_atomic();
> > > > >
> > > > > Is the issue that there is no actual value returned or some such?
> > > >
> > > > Yes, so that the inc is a load-store, and thus there is a load, we loose
> > > > the value.
> > > >
> > > > But I see your point I think. Irrespective of still having the value,
> > > > the ordering is preserved and nothing should pass across that.
> > > >
> > > > > So if I have something like this, the assertion really can trigger?
> > > > >
> > > > > WRITE_ONCE(x, 1); atomic_inc(&y);
> > > > > r0 = xchg_release(&y, 5); smp_mb__after_atomic();
> > > > > r1 = READ_ONCE(x);
> > > > >
> > > > >
> > > > > WARN_ON(r0 == 0 && r1 == 0);
> > > > >
> > > > > I must confess that I am not seeing why we would want to allow this
> > > > > outcome.
> > > >
> > > > No you are indeed quite right. I just wasn't creative enough. Thanks for
> > > > the inspiration.
> > >
> > > Just to close this out, we agree that an smp_rmb() instead of
> > > smp_mb__after_atomic() would *not* forbid this outcome, right?
> >
> > So that really hurts my brain. Per the normal rules that smp_rmb() would
> > order the read of @x against the last ll of @y and per ll/sc ordering
> > you then still don't get to make the WARN happen.
> >
> > On IRC you explained that your 8.1 LSE instructions are not in fact
> > ordered by a smp_rmb, only by smp_wmb, which is 'surprising' since you
> > really need to load the old value to compute the new value.
>
> To be clear, it's only the ST* variants of the LSE instructions that are
> treated as a write for the purposes of memory ordering, so these are the
> non-*_return variants. It's not unlikely that other architectures will
> exhibit the same behaviour (e.g. Power, RISC-V), because the CPU can
> treat non-return atomics as "fire-and-forget" and have them handled
> elsewhere in the memory subsystem, causing them to be treated similarly
> to posted writes.
>
> For the code snippet above, the second thread has no idea about the value
> of y and so smp_rmb() is the wrong thing to be using imo. It really cares
> about ordering the store to y before the read of x, so needs a full mb (i.e.
> the test is more like 'R' than 'MP').
>
> Also, wouldn't this problem also arise if your atomics were built using a
> spinlock where unlock had release semantics?
The current Linux kernel memory model forbids this outcome with smp_rmb(),
though I did have to work around the current lack of atomic_inc() using
xchg_relaxed(), so please review my litmus tests carefully.
C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
(*
* Expected result: Never.
*
* Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
*
* WRITE_ONCE(x, 1); atomic_inc(&y);
* r0 = xchg_release(&y, 5); smp_rmb();
* r1 = READ_ONCE(x);
*
*
* WARN_ON(r0 == 0 && r1 == 0);
*)
{
}
P0(int *x, int *y)
{
WRITE_ONCE(*x, 1);
r0 = xchg_release(y, 5);
}
P1(int *x, int *y)
{
r2 = xchg_relaxed(y, 1);
smp_rmb();
r1 = READ_ONCE(*x);
}
exists
(0:r0=0 /\ 1:r1=0)
Here is what herd thinks:
$ herd7 -bell strong-kernel.bell -cat weak-kernel.cat -macros linux.def ../litmus/manual/kernel/C-WillDeacon-MP+o-r+ai-rmb-o.litmus
Test C-WillDeacon-MP+o-r+ai-rmb-o Allowed
States 3
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r0=0 /\ 1:r1=0)
Observation C-WillDeacon-MP+o-r+ai-rmb-o Never 0 3
Hash=0c3e25a94b38708a2c5ea11ff52c8077
I get the same answer from strong-kernel.cat (which is our best-guess
envelope over hardware guarantees), weak-kernel.cat (which is simplified
based on what people actually use), and proposal.cat (which is a candidate
model with further simplifications).
I converted this (possibly incorrectly) to PowerPC assembly:
PPC w-RMWl-r+w-RMWl-r.litmus
""
(*
* Does 3.0 Linux-kernel Power atomic_add_return() provide local
* barrier that orders prior stores against subsequent loads?
* Use the atomic_add_return() in both threads, but to different variables.
* And use the trailing-lwsync variant of atomic_add_return().
*)
(* 24-Aug-2011: ppcmem says "Sometimes" *)
{
0:r1=1; 0:r2=x; 0:r3=5; 0:r4=y; 0:r10=0 ; 0:r11=0;
1:r1=1; 1:r2=x; 1:r3=5; 1:r4=y; 1:r10=0 ; 1:r11=0;
}
P0 | P1 ;
stw r1,0(r2) | lwarx r11,r10,r4 ;
lwsync | stwcx. r1,r10,r4 ;
lwarx r11,r10,r4 | bne Fail1 ;
stwcx. r3,r10,r4 | lwsync ;
bne Fail0 | lwz r3,0(r2) ;
li r3,42 | Fail1: ;
Fail0: | ;
exists
(0:r11=0 /\ 0:r3=42 /\ 1:r3=0)
And ppcmem agrees with the linux-kernel memory model:
[ . . . ]
Found 82 : Prune count= 13946 seen_succs= 7453 7454 states
Found 83 : Prune count= 13997 seen_succs= 7490 7491 states
Found 84 : Prune count= 14007 seen_succs= 7506 7507 states
Found 85 : Prune count= 17229 seen_succs= 8889 8890 states
Found 86 : Prune count= 17235 seen_succs= 8897 8898 states
Test w-RMWl-r+w-RMWl-r Allowed
States 9
0:r3=5; 0:r11=0; 1:r3=0;
0:r3=5; 0:r11=0; 1:r3=1;
0:r3=5; 0:r11=0; 1:r3=5;
0:r3=5; 0:r11=1; 1:r3=0;
0:r3=5; 0:r11=1; 1:r3=1;
0:r3=42; 0:r11=0; 1:r3=1;
0:r3=42; 0:r11=0; 1:r3=5;
0:r3=42; 0:r11=1; 1:r3=0;
0:r3=42; 0:r11=1; 1:r3=1;
No (allowed not found)
Condition exists (0:r11=0 /\ 0:r3=42 /\ 1:r3=0)
Hash=58fb07516ac5697580c33e06a354f667
Observation w-RMWl-r+w-RMWl-r Never 0 9
So if ARM really needs the litmus test with smp_rmb() to be allowed,
we need to adjust the Linux-kernel memory model appropriately. Which
means that one of us needs to reach out to the usual suspects. Would
you like to do that, or would you like me to?
Thanx, Paul
[toc] | [prev] | [next] | [standalone]
| From | Peter Zijlstra <peterz@infradead.org> |
|---|---|
| Date | 2017-08-01 18:50 +0200 |
| Message-ID | <u9IwQ-6mc-25@gated-at.bofh.it> |
| In reply to | #1701207 |
On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote: > So if ARM really needs the litmus test with smp_rmb() to be allowed, > we need to adjust the Linux-kernel memory model appropriately. Which > means that one of us needs to reach out to the usual suspects. Would > you like to do that, or would you like me to? I'm really sad ARM8.1 LSE breaks this stuff.. It is rather counter intuitive (then again, we _are_ talking barriers).
[toc] | [prev] | [next] | [standalone]
| From | Will Deacon <will.deacon@arm.com> |
|---|---|
| Date | 2017-08-01 19:00 +0200 |
| Message-ID | <u9IGu-6pq-27@gated-at.bofh.it> |
| In reply to | #1701236 |
On Tue, Aug 01, 2017 at 06:42:00PM +0200, Peter Zijlstra wrote: > On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote: > > So if ARM really needs the litmus test with smp_rmb() to be allowed, > > we need to adjust the Linux-kernel memory model appropriately. Which > > means that one of us needs to reach out to the usual suspects. Would > > you like to do that, or would you like me to? > > I'm really sad ARM8.1 LSE breaks this stuff.. It is rather counter > intuitive (then again, we _are_ talking barriers). I can upgrade smp_rmb to smp_mb if I have to, but I still think that code using smp_rmb() to order an operation that doesn't return a value is weird. Will
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-02 00:20 +0200 |
| Message-ID | <u9NG9-1oh-1@gated-at.bofh.it> |
| In reply to | #1701236 |
On Tue, Aug 01, 2017 at 06:42:00PM +0200, Peter Zijlstra wrote: > On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote: > > So if ARM really needs the litmus test with smp_rmb() to be allowed, > > we need to adjust the Linux-kernel memory model appropriately. Which > > means that one of us needs to reach out to the usual suspects. Would > > you like to do that, or would you like me to? > > I'm really sad ARM8.1 LSE breaks this stuff.. It is rather counter > intuitive (then again, we _are_ talking barriers). No argument. Then again, when we said that the Linux kernel memory model would have a non-trivial rate of change, we weren't joking. Will, is this the official description? http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0557a.b/index.html If so, is B6.1 what we should be looking at? Thanx, Paul
[toc] | [prev] | [next] | [standalone]
| From | Will Deacon <will.deacon@arm.com> |
|---|---|
| Date | 2017-08-02 10:50 +0200 |
| Message-ID | <u9XvQ-7wU-27@gated-at.bofh.it> |
| In reply to | #1701538 |
On Tue, Aug 01, 2017 at 03:18:18PM -0700, Paul E. McKenney wrote:
> On Tue, Aug 01, 2017 at 06:42:00PM +0200, Peter Zijlstra wrote:
> > On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote:
> > > So if ARM really needs the litmus test with smp_rmb() to be allowed,
> > > we need to adjust the Linux-kernel memory model appropriately. Which
> > > means that one of us needs to reach out to the usual suspects. Would
> > > you like to do that, or would you like me to?
> >
> > I'm really sad ARM8.1 LSE breaks this stuff.. It is rather counter
> > intuitive (then again, we _are_ talking barriers).
>
> No argument.
>
> Then again, when we said that the Linux kernel memory model would
> have a non-trivial rate of change, we weren't joking.
>
> Will, is this the official description?
>
> http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0557a.b/index.html
>
> If so, is B6.1 what we should be looking at?
Sorry it's so tricky to find. The architecture document is here:
https://static.docs.arm.com/ddi0487/b/DDI0487B_a_armv8_arm.pdf
and in section C3.2.13 ("Atomic memory operations") it states:
| The ST<OP> instructions are not regarded as doing a read for the purpose
| of a DMB LD barrier.
Will
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-01 20:40 +0200 |
| Message-ID | <u9Kff-7x4-11@gated-at.bofh.it> |
| In reply to | #1701207 |
On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote: > On Tue, Aug 01, 2017 at 01:17:13PM +0100, Will Deacon wrote: > > On Tue, Aug 01, 2017 at 01:47:44PM +0200, Peter Zijlstra wrote: > > > On Tue, Aug 01, 2017 at 11:19:00AM +0100, Will Deacon wrote: > > > > On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote: > > > > > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote: > > > > > > > > > > > Why wouldn't the following have ACQUIRE semantics? > > > > > > > > > > > > atomic_inc(&var); > > > > > > smp_mb__after_atomic(); > > > > > > > > > > > > Is the issue that there is no actual value returned or some such? > > > > > > > > > > Yes, so that the inc is a load-store, and thus there is a load, we loose > > > > > the value. > > > > > > > > > > But I see your point I think. Irrespective of still having the value, > > > > > the ordering is preserved and nothing should pass across that. > > > > > > > > > > > So if I have something like this, the assertion really can trigger? > > > > > > > > > > > > WRITE_ONCE(x, 1); atomic_inc(&y); > > > > > > r0 = xchg_release(&y, 5); smp_mb__after_atomic(); > > > > > > r1 = READ_ONCE(x); > > > > > > > > > > > > > > > > > > WARN_ON(r0 == 0 && r1 == 0); > > > > > > > > > > > > I must confess that I am not seeing why we would want to allow this > > > > > > outcome. > > > > > > > > > > No you are indeed quite right. I just wasn't creative enough. Thanks for > > > > > the inspiration. > > > > > > > > Just to close this out, we agree that an smp_rmb() instead of > > > > smp_mb__after_atomic() would *not* forbid this outcome, right? > > > > > > So that really hurts my brain. Per the normal rules that smp_rmb() would > > > order the read of @x against the last ll of @y and per ll/sc ordering > > > you then still don't get to make the WARN happen. > > > > > > On IRC you explained that your 8.1 LSE instructions are not in fact > > > ordered by a smp_rmb, only by smp_wmb, which is 'surprising' since you > > > really need to load the old value to compute the new value. > > > > To be clear, it's only the ST* variants of the LSE instructions that are > > treated as a write for the purposes of memory ordering, so these are the > > non-*_return variants. It's not unlikely that other architectures will > > exhibit the same behaviour (e.g. Power, RISC-V), because the CPU can > > treat non-return atomics as "fire-and-forget" and have them handled > > elsewhere in the memory subsystem, causing them to be treated similarly > > to posted writes. > > > > For the code snippet above, the second thread has no idea about the value > > of y and so smp_rmb() is the wrong thing to be using imo. It really cares > > about ordering the store to y before the read of x, so needs a full mb (i.e. > > the test is more like 'R' than 'MP'). > > > > Also, wouldn't this problem also arise if your atomics were built using a > > spinlock where unlock had release semantics? And responding more directly to the bit about spinlocks after a side discussion with Alan Stern, both the xchg_release() and the atomic_inc() are operating on the same variable, namely "y". Even by the very weak "roach motel" locking semantics, this outcome would be forbidden. But if you have hardware that allows this, let's all discuss and get it hashed out... Thanx, Paul Thanx, Paul
[toc] | [prev] | [next] | [standalone]
| From | Will Deacon <will.deacon@arm.com> |
|---|---|
| Date | 2017-08-02 11:50 +0200 |
| Message-ID | <u9YrU-89Z-11@gated-at.bofh.it> |
| In reply to | #1701207 |
Hi Paul,
On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote:
> On Tue, Aug 01, 2017 at 01:17:13PM +0100, Will Deacon wrote:
> > On Tue, Aug 01, 2017 at 01:47:44PM +0200, Peter Zijlstra wrote:
> > > On Tue, Aug 01, 2017 at 11:19:00AM +0100, Will Deacon wrote:
> > > > On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote:
> > > > > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote:
> > > > > > So if I have something like this, the assertion really can trigger?
> > > > > >
> > > > > > WRITE_ONCE(x, 1); atomic_inc(&y);
> > > > > > r0 = xchg_release(&y, 5); smp_mb__after_atomic();
> > > > > > r1 = READ_ONCE(x);
> > > > > >
> > > > > >
> > > > > > WARN_ON(r0 == 0 && r1 == 0);
> > > > > >
> > > > > > I must confess that I am not seeing why we would want to allow this
> > > > > > outcome.
> > > > >
> > > > > No you are indeed quite right. I just wasn't creative enough. Thanks for
> > > > > the inspiration.
> > > >
> > > > Just to close this out, we agree that an smp_rmb() instead of
> > > > smp_mb__after_atomic() would *not* forbid this outcome, right?
> > >
> > > So that really hurts my brain. Per the normal rules that smp_rmb() would
> > > order the read of @x against the last ll of @y and per ll/sc ordering
> > > you then still don't get to make the WARN happen.
> > >
> > > On IRC you explained that your 8.1 LSE instructions are not in fact
> > > ordered by a smp_rmb, only by smp_wmb, which is 'surprising' since you
> > > really need to load the old value to compute the new value.
> >
> > To be clear, it's only the ST* variants of the LSE instructions that are
> > treated as a write for the purposes of memory ordering, so these are the
> > non-*_return variants. It's not unlikely that other architectures will
> > exhibit the same behaviour (e.g. Power, RISC-V), because the CPU can
> > treat non-return atomics as "fire-and-forget" and have them handled
> > elsewhere in the memory subsystem, causing them to be treated similarly
> > to posted writes.
> >
> > For the code snippet above, the second thread has no idea about the value
> > of y and so smp_rmb() is the wrong thing to be using imo. It really cares
> > about ordering the store to y before the read of x, so needs a full mb (i.e.
> > the test is more like 'R' than 'MP').
> >
> > Also, wouldn't this problem also arise if your atomics were built using a
> > spinlock where unlock had release semantics?
>
> The current Linux kernel memory model forbids this outcome with smp_rmb(),
> though I did have to work around the current lack of atomic_inc() using
> xchg_relaxed(), so please review my litmus tests carefully.
It's worth noting that we don't have the problem with any value-returning
atomics, so all flavours of xchg in this test would be forbidden on arm64
too.
> C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
>
> (*
> * Expected result: Never.
> *
> * Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
> *
> * WRITE_ONCE(x, 1); atomic_inc(&y);
> * r0 = xchg_release(&y, 5); smp_rmb();
> * r1 = READ_ONCE(x);
> *
> *
> * WARN_ON(r0 == 0 && r1 == 0);
> *)
>
> {
> }
>
> P0(int *x, int *y)
> {
> WRITE_ONCE(*x, 1);
> r0 = xchg_release(y, 5);
> }
>
> P1(int *x, int *y)
> {
> r2 = xchg_relaxed(y, 1);
> smp_rmb();
> r1 = READ_ONCE(*x);
> }
>
> exists
> (0:r0=0 /\ 1:r1=0)
>
> Here is what herd thinks:
>
> $ herd7 -bell strong-kernel.bell -cat weak-kernel.cat -macros linux.def ../litmus/manual/kernel/C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> Test C-WillDeacon-MP+o-r+ai-rmb-o Allowed
> States 3
> 0:r0=0; 1:r1=1;
> 0:r0=1; 1:r1=0;
> 0:r0=1; 1:r1=1;
> No
> Witnesses
> Positive: 0 Negative: 3
> Condition exists (0:r0=0 /\ 1:r1=0)
> Observation C-WillDeacon-MP+o-r+ai-rmb-o Never 0 3
> Hash=0c3e25a94b38708a2c5ea11ff52c8077
>
> I get the same answer from strong-kernel.cat (which is our best-guess
> envelope over hardware guarantees), weak-kernel.cat (which is simplified
> based on what people actually use), and proposal.cat (which is a candidate
> model with further simplifications).
>
> I converted this (possibly incorrectly) to PowerPC assembly:
>
> PPC w-RMWl-r+w-RMWl-r.litmus
> ""
> (*
> * Does 3.0 Linux-kernel Power atomic_add_return() provide local
> * barrier that orders prior stores against subsequent loads?
> * Use the atomic_add_return() in both threads, but to different variables.
> * And use the trailing-lwsync variant of atomic_add_return().
> *)
> (* 24-Aug-2011: ppcmem says "Sometimes" *)
> {
> 0:r1=1; 0:r2=x; 0:r3=5; 0:r4=y; 0:r10=0 ; 0:r11=0;
> 1:r1=1; 1:r2=x; 1:r3=5; 1:r4=y; 1:r10=0 ; 1:r11=0;
> }
> P0 | P1 ;
> stw r1,0(r2) | lwarx r11,r10,r4 ;
> lwsync | stwcx. r1,r10,r4 ;
> lwarx r11,r10,r4 | bne Fail1 ;
> stwcx. r3,r10,r4 | lwsync ;
> bne Fail0 | lwz r3,0(r2) ;
> li r3,42 | Fail1: ;
> Fail0: | ;
>
>
> exists
> (0:r11=0 /\ 0:r3=42 /\ 1:r3=0)
>
> And ppcmem agrees with the linux-kernel memory model:
>
> [ . . . ]
>
> Found 82 : Prune count= 13946 seen_succs= 7453 7454 states
> Found 83 : Prune count= 13997 seen_succs= 7490 7491 states
> Found 84 : Prune count= 14007 seen_succs= 7506 7507 states
> Found 85 : Prune count= 17229 seen_succs= 8889 8890 states
> Found 86 : Prune count= 17235 seen_succs= 8897 8898 states
> Test w-RMWl-r+w-RMWl-r Allowed
> States 9
> 0:r3=5; 0:r11=0; 1:r3=0;
> 0:r3=5; 0:r11=0; 1:r3=1;
> 0:r3=5; 0:r11=0; 1:r3=5;
> 0:r3=5; 0:r11=1; 1:r3=0;
> 0:r3=5; 0:r11=1; 1:r3=1;
> 0:r3=42; 0:r11=0; 1:r3=1;
> 0:r3=42; 0:r11=0; 1:r3=5;
> 0:r3=42; 0:r11=1; 1:r3=0;
> 0:r3=42; 0:r11=1; 1:r3=1;
> No (allowed not found)
> Condition exists (0:r11=0 /\ 0:r3=42 /\ 1:r3=0)
> Hash=58fb07516ac5697580c33e06a354f667
> Observation w-RMWl-r+w-RMWl-r Never 0 9
>
> So if ARM really needs the litmus test with smp_rmb() to be allowed,
> we need to adjust the Linux-kernel memory model appropriately. Which
> means that one of us needs to reach out to the usual suspects. Would
> you like to do that, or would you like me to?
If you don't mind doing it, then that would be great, thanks. Do shout if
you need me to help with anything, though!
Will
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-02 18:20 +0200 |
| Message-ID | <ua4xk-3Io-21@gated-at.bofh.it> |
| In reply to | #1701963 |
On Wed, Aug 02, 2017 at 10:45:32AM +0100, Will Deacon wrote:
> Hi Paul,
>
> On Tue, Aug 01, 2017 at 09:14:12AM -0700, Paul E. McKenney wrote:
> > On Tue, Aug 01, 2017 at 01:17:13PM +0100, Will Deacon wrote:
> > > On Tue, Aug 01, 2017 at 01:47:44PM +0200, Peter Zijlstra wrote:
> > > > On Tue, Aug 01, 2017 at 11:19:00AM +0100, Will Deacon wrote:
> > > > > On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote:
> > > > > > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote:
> > > > > > > So if I have something like this, the assertion really can trigger?
> > > > > > >
> > > > > > > WRITE_ONCE(x, 1); atomic_inc(&y);
> > > > > > > r0 = xchg_release(&y, 5); smp_mb__after_atomic();
> > > > > > > r1 = READ_ONCE(x);
> > > > > > >
> > > > > > >
> > > > > > > WARN_ON(r0 == 0 && r1 == 0);
> > > > > > >
> > > > > > > I must confess that I am not seeing why we would want to allow this
> > > > > > > outcome.
> > > > > >
> > > > > > No you are indeed quite right. I just wasn't creative enough. Thanks for
> > > > > > the inspiration.
> > > > >
> > > > > Just to close this out, we agree that an smp_rmb() instead of
> > > > > smp_mb__after_atomic() would *not* forbid this outcome, right?
> > > >
> > > > So that really hurts my brain. Per the normal rules that smp_rmb() would
> > > > order the read of @x against the last ll of @y and per ll/sc ordering
> > > > you then still don't get to make the WARN happen.
> > > >
> > > > On IRC you explained that your 8.1 LSE instructions are not in fact
> > > > ordered by a smp_rmb, only by smp_wmb, which is 'surprising' since you
> > > > really need to load the old value to compute the new value.
> > >
> > > To be clear, it's only the ST* variants of the LSE instructions that are
> > > treated as a write for the purposes of memory ordering, so these are the
> > > non-*_return variants. It's not unlikely that other architectures will
> > > exhibit the same behaviour (e.g. Power, RISC-V), because the CPU can
> > > treat non-return atomics as "fire-and-forget" and have them handled
> > > elsewhere in the memory subsystem, causing them to be treated similarly
> > > to posted writes.
> > >
> > > For the code snippet above, the second thread has no idea about the value
> > > of y and so smp_rmb() is the wrong thing to be using imo. It really cares
> > > about ordering the store to y before the read of x, so needs a full mb (i.e.
> > > the test is more like 'R' than 'MP').
> > >
> > > Also, wouldn't this problem also arise if your atomics were built using a
> > > spinlock where unlock had release semantics?
> >
> > The current Linux kernel memory model forbids this outcome with smp_rmb(),
> > though I did have to work around the current lack of atomic_inc() using
> > xchg_relaxed(), so please review my litmus tests carefully.
>
> It's worth noting that we don't have the problem with any value-returning
> atomics, so all flavours of xchg in this test would be forbidden on arm64
> too.
Plus after upgrading to the latest and greatest version of herd,
atomic_inc() worked just fine. (Hey, I -try- to keep up!) The updated
litmus test is here:
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-WillDeacon-MP%2Bo-r%2Bai-rmb-o.litmus
Same outcome. Alan Stern is looking into what might be adjusted.
Of course, there is no guarantee that this will turn out to be reasonable
or for that matter acceptable to the usual suspects, but if feasible we
should at least see what this does to the model.
> > C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> >
> > (*
> > * Expected result: Never.
> > *
> > * Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
> > *
> > * WRITE_ONCE(x, 1); atomic_inc(&y);
> > * r0 = xchg_release(&y, 5); smp_rmb();
> > * r1 = READ_ONCE(x);
> > *
> > *
> > * WARN_ON(r0 == 0 && r1 == 0);
> > *)
> >
> > {
> > }
> >
> > P0(int *x, int *y)
> > {
> > WRITE_ONCE(*x, 1);
> > r0 = xchg_release(y, 5);
> > }
> >
> > P1(int *x, int *y)
> > {
> > r2 = xchg_relaxed(y, 1);
> > smp_rmb();
> > r1 = READ_ONCE(*x);
> > }
> >
> > exists
> > (0:r0=0 /\ 1:r1=0)
> >
> > Here is what herd thinks:
> >
> > $ herd7 -bell strong-kernel.bell -cat weak-kernel.cat -macros linux.def ../litmus/manual/kernel/C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> > Test C-WillDeacon-MP+o-r+ai-rmb-o Allowed
> > States 3
> > 0:r0=0; 1:r1=1;
> > 0:r0=1; 1:r1=0;
> > 0:r0=1; 1:r1=1;
> > No
> > Witnesses
> > Positive: 0 Negative: 3
> > Condition exists (0:r0=0 /\ 1:r1=0)
> > Observation C-WillDeacon-MP+o-r+ai-rmb-o Never 0 3
> > Hash=0c3e25a94b38708a2c5ea11ff52c8077
> >
> > I get the same answer from strong-kernel.cat (which is our best-guess
> > envelope over hardware guarantees), weak-kernel.cat (which is simplified
> > based on what people actually use), and proposal.cat (which is a candidate
> > model with further simplifications).
> >
> > I converted this (possibly incorrectly) to PowerPC assembly:
> >
> > PPC w-RMWl-r+w-RMWl-r.litmus
> > ""
> > (*
> > * Does 3.0 Linux-kernel Power atomic_add_return() provide local
> > * barrier that orders prior stores against subsequent loads?
> > * Use the atomic_add_return() in both threads, but to different variables.
> > * And use the trailing-lwsync variant of atomic_add_return().
> > *)
> > (* 24-Aug-2011: ppcmem says "Sometimes" *)
> > {
> > 0:r1=1; 0:r2=x; 0:r3=5; 0:r4=y; 0:r10=0 ; 0:r11=0;
> > 1:r1=1; 1:r2=x; 1:r3=5; 1:r4=y; 1:r10=0 ; 1:r11=0;
> > }
> > P0 | P1 ;
> > stw r1,0(r2) | lwarx r11,r10,r4 ;
> > lwsync | stwcx. r1,r10,r4 ;
> > lwarx r11,r10,r4 | bne Fail1 ;
> > stwcx. r3,r10,r4 | lwsync ;
> > bne Fail0 | lwz r3,0(r2) ;
> > li r3,42 | Fail1: ;
> > Fail0: | ;
> >
> >
> > exists
> > (0:r11=0 /\ 0:r3=42 /\ 1:r3=0)
> >
> > And ppcmem agrees with the linux-kernel memory model:
> >
> > [ . . . ]
> >
> > Found 82 : Prune count= 13946 seen_succs= 7453 7454 states
> > Found 83 : Prune count= 13997 seen_succs= 7490 7491 states
> > Found 84 : Prune count= 14007 seen_succs= 7506 7507 states
> > Found 85 : Prune count= 17229 seen_succs= 8889 8890 states
> > Found 86 : Prune count= 17235 seen_succs= 8897 8898 states
> > Test w-RMWl-r+w-RMWl-r Allowed
> > States 9
> > 0:r3=5; 0:r11=0; 1:r3=0;
> > 0:r3=5; 0:r11=0; 1:r3=1;
> > 0:r3=5; 0:r11=0; 1:r3=5;
> > 0:r3=5; 0:r11=1; 1:r3=0;
> > 0:r3=5; 0:r11=1; 1:r3=1;
> > 0:r3=42; 0:r11=0; 1:r3=1;
> > 0:r3=42; 0:r11=0; 1:r3=5;
> > 0:r3=42; 0:r11=1; 1:r3=0;
> > 0:r3=42; 0:r11=1; 1:r3=1;
> > No (allowed not found)
> > Condition exists (0:r11=0 /\ 0:r3=42 /\ 1:r3=0)
> > Hash=58fb07516ac5697580c33e06a354f667
> > Observation w-RMWl-r+w-RMWl-r Never 0 9
> >
> > So if ARM really needs the litmus test with smp_rmb() to be allowed,
> > we need to adjust the Linux-kernel memory model appropriately. Which
> > means that one of us needs to reach out to the usual suspects. Would
> > you like to do that, or would you like me to?
>
> If you don't mind doing it, then that would be great, thanks. Do shout if
> you need me to help with anything, though!
You will be copied, just to cut out the timezone delays if nothing else.
Thanx, Paul
[toc] | [prev] | [next] | [standalone]
| From | Boqun Feng <boqun.feng@gmail.com> |
|---|---|
| Date | 2017-08-03 16:10 +0200 |
| Message-ID | <uaoZ4-12B-7@gated-at.bofh.it> |
| In reply to | #1701963 |
[Multipart message — attachments visible in raw view] — view raw
Hi Will,
On Wed, Aug 02, 2017 at 10:45:32AM +0100, Will Deacon wrote:
[...]
>
> It's worth noting that we don't have the problem with any value-returning
> atomics, so all flavours of xchg in this test would be forbidden on arm64
> too.
>
> > C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> >
> > (*
> > * Expected result: Never.
> > *
> > * Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
> > *
> > * WRITE_ONCE(x, 1); atomic_inc(&y);
> > * r0 = xchg_release(&y, 5); smp_rmb();
> > * r1 = READ_ONCE(x);
> > *
> > *
> > * WARN_ON(r0 == 0 && r1 == 0);
> > *)
> >
> > {
> > }
> >
> > P0(int *x, int *y)
> > {
> > WRITE_ONCE(*x, 1);
> > r0 = xchg_release(y, 5);
> > }
> >
> > P1(int *x, int *y)
> > {
> > r2 = xchg_relaxed(y, 1);
> > smp_rmb();
> > r1 = READ_ONCE(*x);
> > }
> >
> > exists
> > (0:r0=0 /\ 1:r1=0)
> >
How about a litmus test like this?
C C-AMO-global-transitivity.litmus
{
}
P0(int *x, int *y)
{
WRITE_ONCE(*x, 1);
r0 = xchg_release(y, 5);
}
P1(int *y, int *z)
{
atomic_inc(y);
smp_mb();
r1 = READ_ONCE(*z);
}
P2(int *x, int *z)
{
WRITE_ONCE(*z, 1);
smp_mb();
r2 = READ_ONCE(*x);
}
exists
(0:r0=0 /\ 1:r1=0 /\ 2:r2=0 )
Should we forbid the outcome in the exists-clause? I ask because I want
to know whether we can just treat atomic_inc() as a store, because if I
replace atomic_inc() with a WRITE(*y, 6), IIUC, the current model says
this could happen.
Thoughts?
Regards,
Boqun
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-03 17:00 +0200 |
| Message-ID | <uapLr-1ol-17@gated-at.bofh.it> |
| In reply to | #1703150 |
On Thu, Aug 03, 2017 at 10:05:16PM +0800, Boqun Feng wrote:
> Hi Will,
>
> On Wed, Aug 02, 2017 at 10:45:32AM +0100, Will Deacon wrote:
> [...]
> >
> > It's worth noting that we don't have the problem with any value-returning
> > atomics, so all flavours of xchg in this test would be forbidden on arm64
> > too.
> >
> > > C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> > >
> > > (*
> > > * Expected result: Never.
> > > *
> > > * Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
> > > *
> > > * WRITE_ONCE(x, 1); atomic_inc(&y);
> > > * r0 = xchg_release(&y, 5); smp_rmb();
> > > * r1 = READ_ONCE(x);
> > > *
> > > *
> > > * WARN_ON(r0 == 0 && r1 == 0);
> > > *)
> > >
> > > {
> > > }
> > >
> > > P0(int *x, int *y)
> > > {
> > > WRITE_ONCE(*x, 1);
> > > r0 = xchg_release(y, 5);
> > > }
> > >
> > > P1(int *x, int *y)
> > > {
> > > r2 = xchg_relaxed(y, 1);
> > > smp_rmb();
> > > r1 = READ_ONCE(*x);
> > > }
> > >
> > > exists
> > > (0:r0=0 /\ 1:r1=0)
> > >
>
> How about a litmus test like this?
>
> C C-AMO-global-transitivity.litmus
>
> {
> }
>
> P0(int *x, int *y)
> {
> WRITE_ONCE(*x, 1);
> r0 = xchg_release(y, 5);
> }
>
> P1(int *y, int *z)
> {
> atomic_inc(y);
> smp_mb();
I am going to guess that the smp_mb() enforces the needed ordering,
but Will will let me know. ;-)
Thanx, Paul
> r1 = READ_ONCE(*z);
> }
>
> P2(int *x, int *z)
> {
> WRITE_ONCE(*z, 1);
> smp_mb();
> r2 = READ_ONCE(*x);
> }
>
> exists
> (0:r0=0 /\ 1:r1=0 /\ 2:r2=0 )
>
> Should we forbid the outcome in the exists-clause? I ask because I want
> to know whether we can just treat atomic_inc() as a store, because if I
> replace atomic_inc() with a WRITE(*y, 6), IIUC, the current model says
> this could happen.
>
> Thoughts?
>
> Regards,
> Boqun
[toc] | [prev] | [next] | [standalone]
| From | Will Deacon <will.deacon@arm.com> |
|---|---|
| Date | 2017-08-03 18:20 +0200 |
| Message-ID | <uar0T-2qL-23@gated-at.bofh.it> |
| In reply to | #1703180 |
On Thu, Aug 03, 2017 at 07:55:14AM -0700, Paul E. McKenney wrote:
> On Thu, Aug 03, 2017 at 10:05:16PM +0800, Boqun Feng wrote:
> > Hi Will,
> >
> > On Wed, Aug 02, 2017 at 10:45:32AM +0100, Will Deacon wrote:
> > [...]
> > >
> > > It's worth noting that we don't have the problem with any value-returning
> > > atomics, so all flavours of xchg in this test would be forbidden on arm64
> > > too.
> > >
> > > > C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> > > >
> > > > (*
> > > > * Expected result: Never.
> > > > *
> > > > * Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
> > > > *
> > > > * WRITE_ONCE(x, 1); atomic_inc(&y);
> > > > * r0 = xchg_release(&y, 5); smp_rmb();
> > > > * r1 = READ_ONCE(x);
> > > > *
> > > > *
> > > > * WARN_ON(r0 == 0 && r1 == 0);
> > > > *)
> > > >
> > > > {
> > > > }
> > > >
> > > > P0(int *x, int *y)
> > > > {
> > > > WRITE_ONCE(*x, 1);
> > > > r0 = xchg_release(y, 5);
> > > > }
> > > >
> > > > P1(int *x, int *y)
> > > > {
> > > > r2 = xchg_relaxed(y, 1);
> > > > smp_rmb();
> > > > r1 = READ_ONCE(*x);
> > > > }
> > > >
> > > > exists
> > > > (0:r0=0 /\ 1:r1=0)
> > > >
> >
> > How about a litmus test like this?
> >
> > C C-AMO-global-transitivity.litmus
> >
> > {
> > }
> >
> > P0(int *x, int *y)
> > {
> > WRITE_ONCE(*x, 1);
> > r0 = xchg_release(y, 5);
> > }
> >
> > P1(int *y, int *z)
> > {
> > atomic_inc(y);
> > smp_mb();
>
> I am going to guess that the smp_mb() enforces the needed ordering,
> but Will will let me know. ;-)
Yup, that would be forbidden on arm64, and would also be forbidden if
you used WRITE_ONCE instead of atomic_inc (remember that we recently
became multi-copy atomic).
Will
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-03 19:10 +0200 |
| Message-ID | <uarNf-32O-9@gated-at.bofh.it> |
| In reply to | #1703235 |
On Thu, Aug 03, 2017 at 05:12:24PM +0100, Will Deacon wrote:
> On Thu, Aug 03, 2017 at 07:55:14AM -0700, Paul E. McKenney wrote:
> > On Thu, Aug 03, 2017 at 10:05:16PM +0800, Boqun Feng wrote:
> > > Hi Will,
> > >
> > > On Wed, Aug 02, 2017 at 10:45:32AM +0100, Will Deacon wrote:
> > > [...]
> > > >
> > > > It's worth noting that we don't have the problem with any value-returning
> > > > atomics, so all flavours of xchg in this test would be forbidden on arm64
> > > > too.
> > > >
> > > > > C C-WillDeacon-MP+o-r+ai-rmb-o.litmus
> > > > >
> > > > > (*
> > > > > * Expected result: Never.
> > > > > *
> > > > > * Desired litmus test, with atomic_inc() emulated by xchg_relaxed():
> > > > > *
> > > > > * WRITE_ONCE(x, 1); atomic_inc(&y);
> > > > > * r0 = xchg_release(&y, 5); smp_rmb();
> > > > > * r1 = READ_ONCE(x);
> > > > > *
> > > > > *
> > > > > * WARN_ON(r0 == 0 && r1 == 0);
> > > > > *)
> > > > >
> > > > > {
> > > > > }
> > > > >
> > > > > P0(int *x, int *y)
> > > > > {
> > > > > WRITE_ONCE(*x, 1);
> > > > > r0 = xchg_release(y, 5);
> > > > > }
> > > > >
> > > > > P1(int *x, int *y)
> > > > > {
> > > > > r2 = xchg_relaxed(y, 1);
> > > > > smp_rmb();
> > > > > r1 = READ_ONCE(*x);
> > > > > }
> > > > >
> > > > > exists
> > > > > (0:r0=0 /\ 1:r1=0)
> > > > >
> > >
> > > How about a litmus test like this?
> > >
> > > C C-AMO-global-transitivity.litmus
> > >
> > > {
> > > }
> > >
> > > P0(int *x, int *y)
> > > {
> > > WRITE_ONCE(*x, 1);
> > > r0 = xchg_release(y, 5);
> > > }
> > >
> > > P1(int *y, int *z)
> > > {
> > > atomic_inc(y);
> > > smp_mb();
> >
> > I am going to guess that the smp_mb() enforces the needed ordering,
> > but Will will let me know. ;-)
>
> Yup, that would be forbidden on arm64, and would also be forbidden if
> you used WRITE_ONCE instead of atomic_inc (remember that we recently
> became multi-copy atomic).
Thank you for the confirmation!
Thanx, Paul
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> |
|---|---|
| Date | 2017-08-01 15:40 +0200 |
| Message-ID | <u9FyW-4zN-21@gated-at.bofh.it> |
| In reply to | #1700768 |
On Tue, Aug 01, 2017 at 11:01:21AM +0200, Peter Zijlstra wrote: > On Mon, Jul 31, 2017 at 10:43:45AM -0700, Paul E. McKenney wrote: > > > Why wouldn't the following have ACQUIRE semantics? > > > > atomic_inc(&var); > > smp_mb__after_atomic(); > > > > Is the issue that there is no actual value returned or some such? > > Yes, so that the inc is a load-store, and thus there is a load, we loose > the value. > > But I see your point I think. Irrespective of still having the value, > the ordering is preserved and nothing should pass across that. > > > So if I have something like this, the assertion really can trigger? > > > > WRITE_ONCE(x, 1); atomic_inc(&y); > > r0 = xchg_release(&y, 5); smp_mb__after_atomic(); > > r1 = READ_ONCE(x); > > > > > > WARN_ON(r0 == 0 && r1 == 0); > > > > I must confess that I am not seeing why we would want to allow this > > outcome. > > No you are indeed quite right. I just wasn't creative enough. Thanks for > the inspiration. Whew! You guys had me worried there for a bit. ;-) Thanx, Paul
[toc] | [prev] | [standalone]
Back to top | Article view | linux.kernel
csiph-web