Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 06:45:32PM +0800, Boqun Feng wrote:
> Maybe it's me who misunderstand Daniel's words. But my understanding is
> that riscv people are on a debate about whether their "RCpc" atomic
> instructions need to be more strict: release+acquire pair orders two
> writes. And I thought that atomics(including RmW atomics) in kernel only
> have purely RCpc semantics, which I needed to check with you guy. And if
> I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
> purely RCpc.
> 
> Note that even on PPC, the release+acquire pair of atomics orders writes
> before and after, and on x86, writes are ordered since it's TSO. So
> strictly speaking, I think our current implementation of atomics are a
> little more strict than purely RCpc. If we think this is an requirement
> for implementation of atomic primitives, than the current version of
> riscv's "RCpc" atomics don't suffice.


So the question is:

P0()
{
WRITE_ONCE(x, 1);
smp_store_release(, 1);
r0 = smp_load_acquire();
WRITE_ONCE(z, 1);
}

P1()
{
r1 = READ_ONCE(z);
smp_rmb();
r2 = READ_ONCE(x);
}

exists: r0 == 1 /\ r1==1 /\ r2==0

Which per the current LKMM would be forbidden? How would strict RCpc
allow that? Due to a fwd from the release to the acquire and then
defeating the ordering or something like that?

My vote would go to disallowing this. Allowing this would be rather
subtle and unexpected IMO.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 06:45:32PM +0800, Boqun Feng wrote:
> Maybe it's me who misunderstand Daniel's words. But my understanding is
> that riscv people are on a debate about whether their "RCpc" atomic
> instructions need to be more strict: release+acquire pair orders two
> writes. And I thought that atomics(including RmW atomics) in kernel only
> have purely RCpc semantics, which I needed to check with you guy. And if
> I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
> purely RCpc.
> 
> Note that even on PPC, the release+acquire pair of atomics orders writes
> before and after, and on x86, writes are ordered since it's TSO. So
> strictly speaking, I think our current implementation of atomics are a
> little more strict than purely RCpc. If we think this is an requirement
> for implementation of atomic primitives, than the current version of
> riscv's "RCpc" atomics don't suffice.


So the question is:

P0()
{
WRITE_ONCE(x, 1);
smp_store_release(, 1);
r0 = smp_load_acquire();
WRITE_ONCE(z, 1);
}

P1()
{
r1 = READ_ONCE(z);
smp_rmb();
r2 = READ_ONCE(x);
}

exists: r0 == 1 /\ r1==1 /\ r2==0

Which per the current LKMM would be forbidden? How would strict RCpc
allow that? Due to a fwd from the release to the acquire and then
defeating the ordering or something like that?

My vote would go to disallowing this. Allowing this would be rather
subtle and unexpected IMO.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Thu, Feb 22, 2018 at 11:15:04AM +0100, Peter Zijlstra wrote:
> On Thu, Feb 22, 2018 at 02:58:47PM +0800, Boqun Feng wrote:
> > > And yes, if we go with a purely RCpc interpretation of acquire and
> > > release, then I don't believe the writes in the previous critical
> > > section would be ordered with the writes in the subsequent critical
> > > section.  That's really all the argument boils down to.  We'd like
> > 
> > I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
> > Alan and Andrea? 
> > 
> > And we are not going to change it, are we?
> > 
> > If atomics in Linux kernel are purely RCpc, then it cerntainly makes
> > sense for riscv to provide purely RCpc atomics.
> 
> So there's 3 things:
> 
>   smp_load_acquire(), smp_store_release()
> 
>   atomic*_{acquire,release}()
> 
>   *_{lock,unlock}();
> 
> Which are all quite distinct.
> 
> smp_load_acquire() and smp_store_release() are RCpc, and there is no
> discussion of ever wanting to change that.
> 
> The atomics also follow this and are RCpc, in fact the RELEASE only
> applies to the STORE and the ACQUIRE only applies to the LOAD of the
> atomics.
> 
> The locking primitives OTOH we would really rather like to be RCsc, and
> everybody except PPC has them as such, PPC being the only one having
> RCpc locks.
> 
> I read the part you quoted from Daniel as being purely about spinlocks,
> the 'critical section' wording being a dead give away, so I'm then
> somewhat confused why you talk about atomics.

Maybe it's me who misunderstand Daniel's words. But my understanding is
that riscv people are on a debate about whether their "RCpc" atomic
instructions need to be more strict: release+acquire pair orders two
writes. And I thought that atomics(including RmW atomics) in kernel only
have purely RCpc semantics, which I needed to check with you guy. And if
I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
purely RCpc.

Note that even on PPC, the release+acquire pair of atomics orders writes
before and after, and on x86, writes are ordered since it's TSO. So
strictly speaking, I think our current implementation of atomics are a
little more strict than purely RCpc. If we think this is an requirement
for implementation of atomic primitives, than the current version of
riscv's "RCpc" atomics don't suffice.

Regards,
Boqun


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Thu, Feb 22, 2018 at 11:15:04AM +0100, Peter Zijlstra wrote:
> On Thu, Feb 22, 2018 at 02:58:47PM +0800, Boqun Feng wrote:
> > > And yes, if we go with a purely RCpc interpretation of acquire and
> > > release, then I don't believe the writes in the previous critical
> > > section would be ordered with the writes in the subsequent critical
> > > section.  That's really all the argument boils down to.  We'd like
> > 
> > I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
> > Alan and Andrea? 
> > 
> > And we are not going to change it, are we?
> > 
> > If atomics in Linux kernel are purely RCpc, then it cerntainly makes
> > sense for riscv to provide purely RCpc atomics.
> 
> So there's 3 things:
> 
>   smp_load_acquire(), smp_store_release()
> 
>   atomic*_{acquire,release}()
> 
>   *_{lock,unlock}();
> 
> Which are all quite distinct.
> 
> smp_load_acquire() and smp_store_release() are RCpc, and there is no
> discussion of ever wanting to change that.
> 
> The atomics also follow this and are RCpc, in fact the RELEASE only
> applies to the STORE and the ACQUIRE only applies to the LOAD of the
> atomics.
> 
> The locking primitives OTOH we would really rather like to be RCsc, and
> everybody except PPC has them as such, PPC being the only one having
> RCpc locks.
> 
> I read the part you quoted from Daniel as being purely about spinlocks,
> the 'critical section' wording being a dead give away, so I'm then
> somewhat confused why you talk about atomics.

Maybe it's me who misunderstand Daniel's words. But my understanding is
that riscv people are on a debate about whether their "RCpc" atomic
instructions need to be more strict: release+acquire pair orders two
writes. And I thought that atomics(including RmW atomics) in kernel only
have purely RCpc semantics, which I needed to check with you guy. And if
I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
purely RCpc.

Note that even on PPC, the release+acquire pair of atomics orders writes
before and after, and on x86, writes are ordered since it's TSO. So
strictly speaking, I think our current implementation of atomics are a
little more strict than purely RCpc. If we think this is an requirement
for implementation of atomic primitives, than the current version of
riscv's "RCpc" atomics don't suffice.

Regards,
Boqun


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 11:06:36AM +0100, Peter Zijlstra wrote:
> On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> > And yes, if we go with a purely RCpc interpretation of acquire and
> > release, then I don't believe the writes in the previous critical
> > section would be ordered with the writes in the subsequent critical
> > section.
> 
> Excuse my ignorance (also jumping in the middle of things), but how can
> this be?
> 
> spin_unlock() is a store-release, this means the write to the lock word
> must happen after any stores inside the critical section.
> 
> spin_lock() is a load-acquire + test-and-set-ctrl-dep, we'll only
> proceed with the critical section if we observe the lock 'unlocked',
> which also means we must observe the stores prior to the unlock.
> 
> And both the ctrl-dep and the ACQUIRE ensure future stores cannot happen
> before.
> 
> So while the lock store and subsequent critical section stores are
> unordered, I don't see how it would be possible to not be ordered
> against stores from a previous critical section.
> 

Or are we talking about a third party observing while not partaking in
the lock-chain? Then I agree, the stores can be observed out of order by
this 3rd actor.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 11:06:36AM +0100, Peter Zijlstra wrote:
> On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> > And yes, if we go with a purely RCpc interpretation of acquire and
> > release, then I don't believe the writes in the previous critical
> > section would be ordered with the writes in the subsequent critical
> > section.
> 
> Excuse my ignorance (also jumping in the middle of things), but how can
> this be?
> 
> spin_unlock() is a store-release, this means the write to the lock word
> must happen after any stores inside the critical section.
> 
> spin_lock() is a load-acquire + test-and-set-ctrl-dep, we'll only
> proceed with the critical section if we observe the lock 'unlocked',
> which also means we must observe the stores prior to the unlock.
> 
> And both the ctrl-dep and the ACQUIRE ensure future stores cannot happen
> before.
> 
> So while the lock store and subsequent critical section stores are
> unordered, I don't see how it would be possible to not be ordered
> against stores from a previous critical section.
> 

Or are we talking about a third party observing while not partaking in
the lock-chain? Then I agree, the stores can be observed out of order by
this 3rd actor.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 02:58:47PM +0800, Boqun Feng wrote:
> > And yes, if we go with a purely RCpc interpretation of acquire and
> > release, then I don't believe the writes in the previous critical
> > section would be ordered with the writes in the subsequent critical
> > section.  That's really all the argument boils down to.  We'd like
> 
> I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
> Alan and Andrea? 
> 
> And we are not going to change it, are we?
> 
> If atomics in Linux kernel are purely RCpc, then it cerntainly makes
> sense for riscv to provide purely RCpc atomics.

So there's 3 things:

  smp_load_acquire(), smp_store_release()

  atomic*_{acquire,release}()

  *_{lock,unlock}();

Which are all quite distinct.

smp_load_acquire() and smp_store_release() are RCpc, and there is no
discussion of ever wanting to change that.

The atomics also follow this and are RCpc, in fact the RELEASE only
applies to the STORE and the ACQUIRE only applies to the LOAD of the
atomics.

The locking primitives OTOH we would really rather like to be RCsc, and
everybody except PPC has them as such, PPC being the only one having
RCpc locks.

I read the part you quoted from Daniel as being purely about spinlocks,
the 'critical section' wording being a dead give away, so I'm then
somewhat confused why you talk about atomics.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 02:58:47PM +0800, Boqun Feng wrote:
> > And yes, if we go with a purely RCpc interpretation of acquire and
> > release, then I don't believe the writes in the previous critical
> > section would be ordered with the writes in the subsequent critical
> > section.  That's really all the argument boils down to.  We'd like
> 
> I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
> Alan and Andrea? 
> 
> And we are not going to change it, are we?
> 
> If atomics in Linux kernel are purely RCpc, then it cerntainly makes
> sense for riscv to provide purely RCpc atomics.

So there's 3 things:

  smp_load_acquire(), smp_store_release()

  atomic*_{acquire,release}()

  *_{lock,unlock}();

Which are all quite distinct.

smp_load_acquire() and smp_store_release() are RCpc, and there is no
discussion of ever wanting to change that.

The atomics also follow this and are RCpc, in fact the RELEASE only
applies to the STORE and the ACQUIRE only applies to the LOAD of the
atomics.

The locking primitives OTOH we would really rather like to be RCsc, and
everybody except PPC has them as such, PPC being the only one having
RCpc locks.

I read the part you quoted from Daniel as being purely about spinlocks,
the 'critical section' wording being a dead give away, so I'm then
somewhat confused why you talk about atomics.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> And yes, if we go with a purely RCpc interpretation of acquire and
> release, then I don't believe the writes in the previous critical
> section would be ordered with the writes in the subsequent critical
> section.

Excuse my ignorance (also jumping in the middle of things), but how can
this be?

spin_unlock() is a store-release, this means the write to the lock word
must happen after any stores inside the critical section.

spin_lock() is a load-acquire + test-and-set-ctrl-dep, we'll only
proceed with the critical section if we observe the lock 'unlocked',
which also means we must observe the stores prior to the unlock.

And both the ctrl-dep and the ACQUIRE ensure future stores cannot happen
before.

So while the lock store and subsequent critical section stores are
unordered, I don't see how it would be possible to not be ordered
against stores from a previous critical section.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> And yes, if we go with a purely RCpc interpretation of acquire and
> release, then I don't believe the writes in the previous critical
> section would be ordered with the writes in the subsequent critical
> section.

Excuse my ignorance (also jumping in the middle of things), but how can
this be?

spin_unlock() is a store-release, this means the write to the lock word
must happen after any stores inside the critical section.

spin_lock() is a load-acquire + test-and-set-ctrl-dep, we'll only
proceed with the critical section if we observe the lock 'unlocked',
which also means we must observe the stores prior to the unlock.

And both the ctrl-dep and the ACQUIRE ensure future stores cannot happen
before.

So while the lock store and subsequent critical section stores are
unordered, I don't see how it would be possible to not be ordered
against stores from a previous critical section.

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> On 2/21/2018 9:27 PM, Boqun Feng wrote:
> > On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
> >> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> >>> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
>  From: Alan Stern 
> 
>  This commit adds a litmus test in which P0() and P1() form a lock-based S
>  litmus test, with the addition of P2(), which observes P0()'s and P1()'s
>  accesses with a full memory barrier but without the lock.  This litmus
>  test asks whether writes carried out by two different processes under the
>  same lock will be seen in order by a third process not holding that lock.
>  The answer to this question is "yes" for all architectures supporting
> >>>
> >>> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> >>> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> >>> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> >>> Or there is an upcomming commit to switch PowerPC's lock implementation?
> >>
> >> The PowerPC lock implementation's unlock-lock pair does not order writes
> >> from the previous critical section against reads from the later critical
> >> section, but it does order other combinations of reads and writes.
> > 
> > Ah.. right! Thanks for the explanation ;-)
> > 
> >> Some have apparently said that RISC-V 's unlock-lock pair also does not
> >> order writes from the previous critical section against writes from the
> >> later critical section.  And no, I don't claim to have yet gotten my
> >> head around RISC-V memory ordering.  ;-)
> >>
> > 
> > Me neither. Now I remember this: we have a off-list(accidentally)
> > discussion about this, and IIRC at that moment riscv people confirmed
> > that riscv's unlock-lock pair doesn't order write->write, but that was
> > before their memory model draft posted for discussions, so things may
> > change now... 
> > 
> > Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
> > 
> > Regards,
> > Boqun
> > 
> >>Thanx, Paul
> >>
> 
> As a matter of fact, the RISC-V memory model committee is debating this
> exact question at the moment.  Now that I see this thread I'll have to
> go back and catch up on what I've missed, but at least I can be on cc
> from this point on to answer any RISC-V questions that come up from
> here on.
> 

Hi Daniel ;-)

> (Is there some place I should add my name as a RISC-V memory model
> contact, so I don't miss threads like this in the future?)
> 

You can submit a patch to add yourself as a Maintainer or Reviewer for
LKMM, Patch #6 in this series is a good example:

https://marc.info/?l=linux-kernel=151916916630299=2

, and "get_maintainer.pl" will help people find you for memory model
stuffs. 

> And yes, if we go with a purely RCpc interpretation of acquire and
> release, then I don't believe the writes in the previous critical
> section would be ordered with the writes in the subsequent critical
> section.  That's really all the argument boils down to.  We'd like

I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
Alan and Andrea? 

And we are not going to change it, are we?

If atomics in Linux kernel are purely RCpc, then it cerntainly makes
sense for riscv to provide purely RCpc atomics.

> to support RCpc if we can since that's all some software needs, but
> we also obviously want to make sure we can support RCsc and these
> kinds of LKMM subtleties efficiently too when needed.  So we have a

I think the problem here is that locks in Linux kernel are more strict
than RCpc but weaker than RCsc, and there is not a well-known concept
for the semantics of locks in Linux kernel AFAIK.

Regards,
Boqun

> few encoding details that we're still finalizing, because questions
> like this one are still popping up :)
> 
> Let me know if you had other RISC-V-specific questions I can help
> answer.
> 
> Dan


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> On 2/21/2018 9:27 PM, Boqun Feng wrote:
> > On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
> >> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> >>> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
>  From: Alan Stern 
> 
>  This commit adds a litmus test in which P0() and P1() form a lock-based S
>  litmus test, with the addition of P2(), which observes P0()'s and P1()'s
>  accesses with a full memory barrier but without the lock.  This litmus
>  test asks whether writes carried out by two different processes under the
>  same lock will be seen in order by a third process not holding that lock.
>  The answer to this question is "yes" for all architectures supporting
> >>>
> >>> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> >>> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> >>> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> >>> Or there is an upcomming commit to switch PowerPC's lock implementation?
> >>
> >> The PowerPC lock implementation's unlock-lock pair does not order writes
> >> from the previous critical section against reads from the later critical
> >> section, but it does order other combinations of reads and writes.
> > 
> > Ah.. right! Thanks for the explanation ;-)
> > 
> >> Some have apparently said that RISC-V 's unlock-lock pair also does not
> >> order writes from the previous critical section against writes from the
> >> later critical section.  And no, I don't claim to have yet gotten my
> >> head around RISC-V memory ordering.  ;-)
> >>
> > 
> > Me neither. Now I remember this: we have a off-list(accidentally)
> > discussion about this, and IIRC at that moment riscv people confirmed
> > that riscv's unlock-lock pair doesn't order write->write, but that was
> > before their memory model draft posted for discussions, so things may
> > change now... 
> > 
> > Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
> > 
> > Regards,
> > Boqun
> > 
> >>Thanx, Paul
> >>
> 
> As a matter of fact, the RISC-V memory model committee is debating this
> exact question at the moment.  Now that I see this thread I'll have to
> go back and catch up on what I've missed, but at least I can be on cc
> from this point on to answer any RISC-V questions that come up from
> here on.
> 

Hi Daniel ;-)

> (Is there some place I should add my name as a RISC-V memory model
> contact, so I don't miss threads like this in the future?)
> 

You can submit a patch to add yourself as a Maintainer or Reviewer for
LKMM, Patch #6 in this series is a good example:

https://marc.info/?l=linux-kernel=151916916630299=2

, and "get_maintainer.pl" will help people find you for memory model
stuffs. 

> And yes, if we go with a purely RCpc interpretation of acquire and
> release, then I don't believe the writes in the previous critical
> section would be ordered with the writes in the subsequent critical
> section.  That's really all the argument boils down to.  We'd like

I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
Alan and Andrea? 

And we are not going to change it, are we?

If atomics in Linux kernel are purely RCpc, then it cerntainly makes
sense for riscv to provide purely RCpc atomics.

> to support RCpc if we can since that's all some software needs, but
> we also obviously want to make sure we can support RCsc and these
> kinds of LKMM subtleties efficiently too when needed.  So we have a

I think the problem here is that locks in Linux kernel are more strict
than RCpc but weaker than RCsc, and there is not a well-known concept
for the semantics of locks in Linux kernel AFAIK.

Regards,
Boqun

> few encoding details that we're still finalizing, because questions
> like this one are still popping up :)
> 
> Let me know if you had other RISC-V-specific questions I can help
> answer.
> 
> Dan


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Daniel Lustig]

On 2/21/2018 9:27 PM, Boqun Feng wrote:
> On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
>> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
>>> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
 From: Alan Stern 

 This commit adds a litmus test in which P0() and P1() form a lock-based S
 litmus test, with the addition of P2(), which observes P0()'s and P1()'s
 accesses with a full memory barrier but without the lock.  This litmus
 test asks whether writes carried out by two different processes under the
 same lock will be seen in order by a third process not holding that lock.
 The answer to this question is "yes" for all architectures supporting
>>>
>>> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
>>> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
>>> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
>>> Or there is an upcomming commit to switch PowerPC's lock implementation?
>>
>> The PowerPC lock implementation's unlock-lock pair does not order writes
>> from the previous critical section against reads from the later critical
>> section, but it does order other combinations of reads and writes.
> 
> Ah.. right! Thanks for the explanation ;-)
> 
>> Some have apparently said that RISC-V 's unlock-lock pair also does not
>> order writes from the previous critical section against writes from the
>> later critical section.  And no, I don't claim to have yet gotten my
>> head around RISC-V memory ordering.  ;-)
>>
> 
> Me neither. Now I remember this: we have a off-list(accidentally)
> discussion about this, and IIRC at that moment riscv people confirmed
> that riscv's unlock-lock pair doesn't order write->write, but that was
> before their memory model draft posted for discussions, so things may
> change now... 
> 
> Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
> 
> Regards,
> Boqun
> 
>>  Thanx, Paul
>>

As a matter of fact, the RISC-V memory model committee is debating this
exact question at the moment.  Now that I see this thread I'll have to
go back and catch up on what I've missed, but at least I can be on cc
from this point on to answer any RISC-V questions that come up from
here on.

(Is there some place I should add my name as a RISC-V memory model
contact, so I don't miss threads like this in the future?)

And yes, if we go with a purely RCpc interpretation of acquire and
release, then I don't believe the writes in the previous critical
section would be ordered with the writes in the subsequent critical
section.  That's really all the argument boils down to.  We'd like
to support RCpc if we can since that's all some software needs, but
we also obviously want to make sure we can support RCsc and these
kinds of LKMM subtleties efficiently too when needed.  So we have a
few encoding details that we're still finalizing, because questions
like this one are still popping up :)

Let me know if you had other RISC-V-specific questions I can help
answer.

Dan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Daniel Lustig]

On 2/21/2018 9:27 PM, Boqun Feng wrote:
> On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
>> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
>>> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
 From: Alan Stern 

 This commit adds a litmus test in which P0() and P1() form a lock-based S
 litmus test, with the addition of P2(), which observes P0()'s and P1()'s
 accesses with a full memory barrier but without the lock.  This litmus
 test asks whether writes carried out by two different processes under the
 same lock will be seen in order by a third process not holding that lock.
 The answer to this question is "yes" for all architectures supporting
>>>
>>> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
>>> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
>>> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
>>> Or there is an upcomming commit to switch PowerPC's lock implementation?
>>
>> The PowerPC lock implementation's unlock-lock pair does not order writes
>> from the previous critical section against reads from the later critical
>> section, but it does order other combinations of reads and writes.
> 
> Ah.. right! Thanks for the explanation ;-)
> 
>> Some have apparently said that RISC-V 's unlock-lock pair also does not
>> order writes from the previous critical section against writes from the
>> later critical section.  And no, I don't claim to have yet gotten my
>> head around RISC-V memory ordering.  ;-)
>>
> 
> Me neither. Now I remember this: we have a off-list(accidentally)
> discussion about this, and IIRC at that moment riscv people confirmed
> that riscv's unlock-lock pair doesn't order write->write, but that was
> before their memory model draft posted for discussions, so things may
> change now... 
> 
> Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
> 
> Regards,
> Boqun
> 
>>  Thanx, Paul
>>

As a matter of fact, the RISC-V memory model committee is debating this
exact question at the moment.  Now that I see this thread I'll have to
go back and catch up on what I've missed, but at least I can be on cc
from this point on to answer any RISC-V questions that come up from
here on.

(Is there some place I should add my name as a RISC-V memory model
contact, so I don't miss threads like this in the future?)

And yes, if we go with a purely RCpc interpretation of acquire and
release, then I don't believe the writes in the previous critical
section would be ordered with the writes in the subsequent critical
section.  That's really all the argument boils down to.  We'd like
to support RCpc if we can since that's all some software needs, but
we also obviously want to make sure we can support RCsc and these
kinds of LKMM subtleties efficiently too when needed.  So we have a
few encoding details that we're still finalizing, because questions
like this one are still popping up :)

Let me know if you had other RISC-V-specific questions I can help
answer.

Dan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> > On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> > > From: Alan Stern 
> > > 
> > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > accesses with a full memory barrier but without the lock.  This litmus
> > > test asks whether writes carried out by two different processes under the
> > > same lock will be seen in order by a third process not holding that lock.
> > > The answer to this question is "yes" for all architectures supporting
> > 
> > Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> > spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> > why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> > Or there is an upcomming commit to switch PowerPC's lock implementation?
> 
> The PowerPC lock implementation's unlock-lock pair does not order writes
> from the previous critical section against reads from the later critical
> section, but it does order other combinations of reads and writes.

Ah.. right! Thanks for the explanation ;-)

> Some have apparently said that RISC-V 's unlock-lock pair also does not
> order writes from the previous critical section against writes from the
> later critical section.  And no, I don't claim to have yet gotten my
> head around RISC-V memory ordering.  ;-)
> 

Me neither. Now I remember this: we have a off-list(accidentally)
discussion about this, and IIRC at that moment riscv people confirmed
that riscv's unlock-lock pair doesn't order write->write, but that was
before their memory model draft posted for discussions, so things may
change now... 

Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?

Regards,
Boqun

>   Thanx, Paul
> 
> > [Cc ppc maintainers]
> > 
> > Regards,
> > Boqun
> > 
> > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > 
> > > A patch to LKMM is under development.
> > > 
> > > Signed-off-by: Alan Stern 
> > > Signed-off-by: Paul E. McKenney 
> > > ---
> > >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > > ++
> > >  1 file changed, 41 insertions(+)
> > >  create mode 100644 
> > > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > 
> > > diff --git 
> > > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > >  
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > new file mode 100644
> > > index ..7a39a0aaa976
> > > --- /dev/null
> > > +++ 
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > @@ -0,0 +1,41 @@
> > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > +
> > > +(*
> > > + * Result: Sometimes
> > > + *
> > > + * This test shows that the ordering provided by a lock-protected S
> > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > + * This is likely to change soon.
> > > + *)
> > > +
> > > +{}
> > > +
> > > +P0(int *x, int *y, spinlock_t *mylock)
> > > +{
> > > + spin_lock(mylock);
> > > + WRITE_ONCE(*x, 1);
> > > + WRITE_ONCE(*y, 1);
> > > + spin_unlock(mylock);
> > > +}
> > > +
> > > +P1(int *y, int *z, spinlock_t *mylock)
> > > +{
> > > + int r0;
> > > +
> > > + spin_lock(mylock);
> > > + r0 = READ_ONCE(*y);
> > > + WRITE_ONCE(*z, 1);
> > > + spin_unlock(mylock);
> > > +}
> > > +
> > > +P2(int *x, int *z)
> > > +{
> > > + int r1;
> > > + int r2;
> > > +
> > > + r2 = READ_ONCE(*z);
> > > + smp_mb();
> > > + r1 = READ_ONCE(*x);
> > > +}
> > > +
> > > +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > > -- 
> > > 2.5.2
> > > 
> 
> 


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> > On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> > > From: Alan Stern 
> > > 
> > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > accesses with a full memory barrier but without the lock.  This litmus
> > > test asks whether writes carried out by two different processes under the
> > > same lock will be seen in order by a third process not holding that lock.
> > > The answer to this question is "yes" for all architectures supporting
> > 
> > Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> > spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> > why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> > Or there is an upcomming commit to switch PowerPC's lock implementation?
> 
> The PowerPC lock implementation's unlock-lock pair does not order writes
> from the previous critical section against reads from the later critical
> section, but it does order other combinations of reads and writes.

Ah.. right! Thanks for the explanation ;-)

> Some have apparently said that RISC-V 's unlock-lock pair also does not
> order writes from the previous critical section against writes from the
> later critical section.  And no, I don't claim to have yet gotten my
> head around RISC-V memory ordering.  ;-)
> 

Me neither. Now I remember this: we have a off-list(accidentally)
discussion about this, and IIRC at that moment riscv people confirmed
that riscv's unlock-lock pair doesn't order write->write, but that was
before their memory model draft posted for discussions, so things may
change now... 

Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?

Regards,
Boqun

>   Thanx, Paul
> 
> > [Cc ppc maintainers]
> > 
> > Regards,
> > Boqun
> > 
> > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > 
> > > A patch to LKMM is under development.
> > > 
> > > Signed-off-by: Alan Stern 
> > > Signed-off-by: Paul E. McKenney 
> > > ---
> > >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > > ++
> > >  1 file changed, 41 insertions(+)
> > >  create mode 100644 
> > > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > 
> > > diff --git 
> > > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > >  
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > new file mode 100644
> > > index ..7a39a0aaa976
> > > --- /dev/null
> > > +++ 
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > @@ -0,0 +1,41 @@
> > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > +
> > > +(*
> > > + * Result: Sometimes
> > > + *
> > > + * This test shows that the ordering provided by a lock-protected S
> > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > + * This is likely to change soon.
> > > + *)
> > > +
> > > +{}
> > > +
> > > +P0(int *x, int *y, spinlock_t *mylock)
> > > +{
> > > + spin_lock(mylock);
> > > + WRITE_ONCE(*x, 1);
> > > + WRITE_ONCE(*y, 1);
> > > + spin_unlock(mylock);
> > > +}
> > > +
> > > +P1(int *y, int *z, spinlock_t *mylock)
> > > +{
> > > + int r0;
> > > +
> > > + spin_lock(mylock);
> > > + r0 = READ_ONCE(*y);
> > > + WRITE_ONCE(*z, 1);
> > > + spin_unlock(mylock);
> > > +}
> > > +
> > > +P2(int *x, int *z)
> > > +{
> > > + int r1;
> > > + int r2;
> > > +
> > > + r2 = READ_ONCE(*z);
> > > + smp_mb();
> > > + r1 = READ_ONCE(*x);
> > > +}
> > > +
> > > +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > > -- 
> > > 2.5.2
> > > 
> 
> 


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> > From: Alan Stern 
> > 
> > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > accesses with a full memory barrier but without the lock.  This litmus
> > test asks whether writes carried out by two different processes under the
> > same lock will be seen in order by a third process not holding that lock.
> > The answer to this question is "yes" for all architectures supporting
> 
> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> Or there is an upcomming commit to switch PowerPC's lock implementation?

The PowerPC lock implementation's unlock-lock pair does not order writes
from the previous critical section against reads from the later critical
section, but it does order other combinations of reads and writes.
Some have apparently said that RISC-V 's unlock-lock pair also does not
order writes from the previous critical section against writes from the
later critical section.  And no, I don't claim to have yet gotten my
head around RISC-V memory ordering.  ;-)

Thanx, Paul

> [Cc ppc maintainers]
> 
> Regards,
> Boqun
> 
> > the Linux kernel, but is "no" according to the current version of LKMM.
> > 
> > A patch to LKMM is under development.
> > 
> > Signed-off-by: Alan Stern 
> > Signed-off-by: Paul E. McKenney 
> > ---
> >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > ++
> >  1 file changed, 41 insertions(+)
> >  create mode 100644 
> > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > 
> > diff --git 
> > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >  
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > new file mode 100644
> > index ..7a39a0aaa976
> > --- /dev/null
> > +++ 
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -0,0 +1,41 @@
> > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This test shows that the ordering provided by a lock-protected S
> > + * litmus test (P0() and P1()) are not visible to external process P2().
> > + * This is likely to change soon.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y, spinlock_t *mylock)
> > +{
> > +   spin_lock(mylock);
> > +   WRITE_ONCE(*x, 1);
> > +   WRITE_ONCE(*y, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P1(int *y, int *z, spinlock_t *mylock)
> > +{
> > +   int r0;
> > +
> > +   spin_lock(mylock);
> > +   r0 = READ_ONCE(*y);
> > +   WRITE_ONCE(*z, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P2(int *x, int *z)
> > +{
> > +   int r1;
> > +   int r2;
> > +
> > +   r2 = READ_ONCE(*z);
> > +   smp_mb();
> > +   r1 = READ_ONCE(*x);
> > +}
> > +
> > +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > -- 
> > 2.5.2
> > 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> > From: Alan Stern 
> > 
> > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > accesses with a full memory barrier but without the lock.  This litmus
> > test asks whether writes carried out by two different processes under the
> > same lock will be seen in order by a third process not holding that lock.
> > The answer to this question is "yes" for all architectures supporting
> 
> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> Or there is an upcomming commit to switch PowerPC's lock implementation?

The PowerPC lock implementation's unlock-lock pair does not order writes
from the previous critical section against reads from the later critical
section, but it does order other combinations of reads and writes.
Some have apparently said that RISC-V 's unlock-lock pair also does not
order writes from the previous critical section against writes from the
later critical section.  And no, I don't claim to have yet gotten my
head around RISC-V memory ordering.  ;-)

Thanx, Paul

> [Cc ppc maintainers]
> 
> Regards,
> Boqun
> 
> > the Linux kernel, but is "no" according to the current version of LKMM.
> > 
> > A patch to LKMM is under development.
> > 
> > Signed-off-by: Alan Stern 
> > Signed-off-by: Paul E. McKenney 
> > ---
> >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > ++
> >  1 file changed, 41 insertions(+)
> >  create mode 100644 
> > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > 
> > diff --git 
> > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >  
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > new file mode 100644
> > index ..7a39a0aaa976
> > --- /dev/null
> > +++ 
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -0,0 +1,41 @@
> > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This test shows that the ordering provided by a lock-protected S
> > + * litmus test (P0() and P1()) are not visible to external process P2().
> > + * This is likely to change soon.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y, spinlock_t *mylock)
> > +{
> > +   spin_lock(mylock);
> > +   WRITE_ONCE(*x, 1);
> > +   WRITE_ONCE(*y, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P1(int *y, int *z, spinlock_t *mylock)
> > +{
> > +   int r0;
> > +
> > +   spin_lock(mylock);
> > +   r0 = READ_ONCE(*y);
> > +   WRITE_ONCE(*z, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P2(int *x, int *z)
> > +{
> > +   int r1;
> > +   int r2;
> > +
> > +   r2 = READ_ONCE(*z);
> > +   smp_mb();
> > +   r1 = READ_ONCE(*x);
> > +}
> > +
> > +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > -- 
> > 2.5.2
> > 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> From: Alan Stern 
> 
> This commit adds a litmus test in which P0() and P1() form a lock-based S
> litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> accesses with a full memory barrier but without the lock.  This litmus
> test asks whether writes carried out by two different processes under the
> same lock will be seen in order by a third process not holding that lock.
> The answer to this question is "yes" for all architectures supporting

Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
Or there is an upcomming commit to switch PowerPC's lock implementation?

[Cc ppc maintainers]

Regards,
Boqun

> the Linux kernel, but is "no" according to the current version of LKMM.
> 
> A patch to LKMM is under development.
> 
> Signed-off-by: Alan Stern 
> Signed-off-by: Paul E. McKenney 
> ---
>  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> ++
>  1 file changed, 41 insertions(+)
>  create mode 100644 
> tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> 
> diff --git 
> a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> new file mode 100644
> index ..7a39a0aaa976
> --- /dev/null
> +++ 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -0,0 +1,41 @@
> +C ISA2+pooncelock+pooncelock+pombonce.litmus
> +
> +(*
> + * Result: Sometimes
> + *
> + * This test shows that the ordering provided by a lock-protected S
> + * litmus test (P0() and P1()) are not visible to external process P2().
> + * This is likely to change soon.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y, spinlock_t *mylock)
> +{
> + spin_lock(mylock);
> + WRITE_ONCE(*x, 1);
> + WRITE_ONCE(*y, 1);
> + spin_unlock(mylock);
> +}
> +
> +P1(int *y, int *z, spinlock_t *mylock)
> +{
> + int r0;
> +
> + spin_lock(mylock);
> + r0 = READ_ONCE(*y);
> + WRITE_ONCE(*z, 1);
> + spin_unlock(mylock);
> +}
> +
> +P2(int *x, int *z)
> +{
> + int r1;
> + int r2;
> +
> + r2 = READ_ONCE(*z);
> + smp_mb();
> + r1 = READ_ONCE(*x);
> +}
> +
> +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> -- 
> 2.5.2
> 


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Boqun Feng]

On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> From: Alan Stern 
> 
> This commit adds a litmus test in which P0() and P1() form a lock-based S
> litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> accesses with a full memory barrier but without the lock.  This litmus
> test asks whether writes carried out by two different processes under the
> same lock will be seen in order by a third process not holding that lock.
> The answer to this question is "yes" for all architectures supporting

Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
Or there is an upcomming commit to switch PowerPC's lock implementation?

[Cc ppc maintainers]

Regards,
Boqun

> the Linux kernel, but is "no" according to the current version of LKMM.
> 
> A patch to LKMM is under development.
> 
> Signed-off-by: Alan Stern 
> Signed-off-by: Paul E. McKenney 
> ---
>  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> ++
>  1 file changed, 41 insertions(+)
>  create mode 100644 
> tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> 
> diff --git 
> a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> new file mode 100644
> index ..7a39a0aaa976
> --- /dev/null
> +++ 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -0,0 +1,41 @@
> +C ISA2+pooncelock+pooncelock+pombonce.litmus
> +
> +(*
> + * Result: Sometimes
> + *
> + * This test shows that the ordering provided by a lock-protected S
> + * litmus test (P0() and P1()) are not visible to external process P2().
> + * This is likely to change soon.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y, spinlock_t *mylock)
> +{
> + spin_lock(mylock);
> + WRITE_ONCE(*x, 1);
> + WRITE_ONCE(*y, 1);
> + spin_unlock(mylock);
> +}
> +
> +P1(int *y, int *z, spinlock_t *mylock)
> +{
> + int r0;
> +
> + spin_lock(mylock);
> + r0 = READ_ONCE(*y);
> + WRITE_ONCE(*z, 1);
> + spin_unlock(mylock);
> +}
> +
> +P2(int *x, int *z)
> +{
> + int r1;
> + int r2;
> +
> + r2 = READ_ONCE(*z);
> + smp_mb();
> + r1 = READ_ONCE(*x);
> +}
> +
> +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> -- 
> 2.5.2
> 


signature.asc
Description: PGP signature

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 02:27:04PM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> 
> > > > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > +   Tests whether the ordering provided by a lock-protected S litmus
> > > 
> > > Call it an ISA2 litmus test, not an S litmus test!
> > 
> > Given the structure of the test, the relationship to S is important
> > because it helps motivate why anyone might care.  But yes, having ISA2
> > only in the filename is a bit obtuse.  How about the following?
> > 
> > ISA2+pooncelock+pooncelock+pombonce.litmus
> > Tests whether the ordering provided by a lock-protected S
> > litmus test is visible to an external process whose accesses are
> > separated by smp_mb().  This addition of an external process to
> > S is otherwise known as ISA2.
> 
> Okay, that's somewhat better.
> 
> However, I still don't understand why you think of this as a form of S.  
> In S, the first variable written by P0 is the same as the variable
> written by P1.  In this test, no variable other than the spinlock gets
> written twice.  To me that seems like a pretty fundamental difference.

There is a chain of processes connected by variables, similar to
a snap-together toy.  If you "disconnect" S at the end and snap in
a process having a pair of reads separated by a full memory barrier,
you get ISA2.  And yes, this does rename one of S's variables, but that
is OK because in this view, each variable is defined by the connection
between a given pair of pair of processes.

Unconventional perhaps, but then again remember who you are emailing
with.  ;-)

Another (perhaps more conventional) way to think of this is in terms of
Andrea's python script that identified equivalent litmus tests.  For that
script, both the variable names and process numbers are irrelevant.

Thanx, Paul

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 02:27:04PM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> 
> > > > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > +   Tests whether the ordering provided by a lock-protected S litmus
> > > 
> > > Call it an ISA2 litmus test, not an S litmus test!
> > 
> > Given the structure of the test, the relationship to S is important
> > because it helps motivate why anyone might care.  But yes, having ISA2
> > only in the filename is a bit obtuse.  How about the following?
> > 
> > ISA2+pooncelock+pooncelock+pombonce.litmus
> > Tests whether the ordering provided by a lock-protected S
> > litmus test is visible to an external process whose accesses are
> > separated by smp_mb().  This addition of an external process to
> > S is otherwise known as ISA2.
> 
> Okay, that's somewhat better.
> 
> However, I still don't understand why you think of this as a form of S.  
> In S, the first variable written by P0 is the same as the variable
> written by P1.  In this test, no variable other than the spinlock gets
> written twice.  To me that seems like a pretty fundamental difference.

There is a chain of processes connected by variables, similar to
a snap-together toy.  If you "disconnect" S at the end and snap in
a process having a pair of reads separated by a full memory barrier,
you get ISA2.  And yes, this does rename one of S's variables, but that
is OK because in this view, each variable is defined by the connection
between a given pair of pair of processes.

Unconventional perhaps, but then again remember who you are emailing
with.  ;-)

Another (perhaps more conventional) way to think of this is in terms of
Andrea's python script that identified equivalent litmus tests.  For that
script, both the variable names and process numbers are irrelevant.

Thanx, Paul

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 01:38:35PM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> 
> > On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> > > On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> > > 
> > > > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > > > 
> > > > > > From: Alan Stern 
> > > > > > 
> > > > > > This commit adds a litmus test in which P0() and P1() form a 
> > > > > > lock-based S
> > > > > > litmus test, with the addition of P2(), which observes P0()'s and 
> > > > > > P1()'s
> > > > > 
> > > > > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > > > > description?
> > > > 
> > > > Indeed, the name of the test is in fact ISA2.
> > > 
> > > Sure; and the Changelog entry should reflect this.
> > 
> > No argument.
> 
> > 
> > 
> > commit e6658d1d7fcc6391f3d00beaadc484243123a893
> > Author: Paul E. McKenney 
> > Date:   Wed Feb 21 09:49:01 2018 -0800
> > 
> > tools/memory-order: Add documentation of new litmus test
> > 
> > The litmus-tests/README file lacked any mention of then litmus test
> 
> s/lacked/lacks/
> s/then/the new/
> 
> > named ISA2+pooncelock+pooncelock+pombonce.litmus.  This commit therefore
> 
> s/named //
> 
> > adds this test.
> 
> It adds a description of the test, not the test itself.

Good catches, fixed.

> > Reported-by: Alan Stern 
> > Signed-off-by: Paul E. McKenney 
> > 
> > diff --git a/tools/memory-model/litmus-tests/README 
> > b/tools/memory-model/litmus-tests/README
> > index dca7d823ad57..aff3eb90e067 100644
> > --- a/tools/memory-model/litmus-tests/README
> > +++ b/tools/memory-model/litmus-tests/README
> > @@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
> > order of a pair of writes, where each write is to a different
> > variable by a different process?
> >  
> > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > +   Tests whether the ordering provided by a lock-protected S litmus
> 
> Call it an ISA2 litmus test, not an S litmus test!

Given the structure of the test, the relationship to S is important
because it helps motivate why anyone might care.  But yes, having ISA2
only in the filename is a bit obtuse.  How about the following?

ISA2+pooncelock+pooncelock+pombonce.litmus
Tests whether the ordering provided by a lock-protected S
litmus test is visible to an external process whose accesses are
separated by smp_mb().  This addition of an external process to
S is otherwise known as ISA2.

Thanx, Paul

> > +   test is visible to an external process whose accesses are
> > +   separated by smp_mb().
> > +
> >  ISA2+poonceonces.litmus
> > As below, but with store-release replaced with WRITE_ONCE()
> > and load-acquire replaced with READ_ONCE().
> 
> Alan
> 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 01:38:35PM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> 
> > On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> > > On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> > > 
> > > > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > > > 
> > > > > > From: Alan Stern 
> > > > > > 
> > > > > > This commit adds a litmus test in which P0() and P1() form a 
> > > > > > lock-based S
> > > > > > litmus test, with the addition of P2(), which observes P0()'s and 
> > > > > > P1()'s
> > > > > 
> > > > > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > > > > description?
> > > > 
> > > > Indeed, the name of the test is in fact ISA2.
> > > 
> > > Sure; and the Changelog entry should reflect this.
> > 
> > No argument.
> 
> > 
> > 
> > commit e6658d1d7fcc6391f3d00beaadc484243123a893
> > Author: Paul E. McKenney 
> > Date:   Wed Feb 21 09:49:01 2018 -0800
> > 
> > tools/memory-order: Add documentation of new litmus test
> > 
> > The litmus-tests/README file lacked any mention of then litmus test
> 
> s/lacked/lacks/
> s/then/the new/
> 
> > named ISA2+pooncelock+pooncelock+pombonce.litmus.  This commit therefore
> 
> s/named //
> 
> > adds this test.
> 
> It adds a description of the test, not the test itself.

Good catches, fixed.

> > Reported-by: Alan Stern 
> > Signed-off-by: Paul E. McKenney 
> > 
> > diff --git a/tools/memory-model/litmus-tests/README 
> > b/tools/memory-model/litmus-tests/README
> > index dca7d823ad57..aff3eb90e067 100644
> > --- a/tools/memory-model/litmus-tests/README
> > +++ b/tools/memory-model/litmus-tests/README
> > @@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
> > order of a pair of writes, where each write is to a different
> > variable by a different process?
> >  
> > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > +   Tests whether the ordering provided by a lock-protected S litmus
> 
> Call it an ISA2 litmus test, not an S litmus test!

Given the structure of the test, the relationship to S is important
because it helps motivate why anyone might care.  But yes, having ISA2
only in the filename is a bit obtuse.  How about the following?

ISA2+pooncelock+pooncelock+pombonce.litmus
Tests whether the ordering provided by a lock-protected S
litmus test is visible to an external process whose accesses are
separated by smp_mb().  This addition of an external process to
S is otherwise known as ISA2.

Thanx, Paul

> > +   test is visible to an external process whose accesses are
> > +   separated by smp_mb().
> > +
> >  ISA2+poonceonces.litmus
> > As below, but with store-release replaced with WRITE_ONCE()
> > and load-acquire replaced with READ_ONCE().
> 
> Alan
> 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Wed, 21 Feb 2018, Paul E. McKenney wrote:

> On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> > On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> > 
> > > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > > 
> > > > > From: Alan Stern 
> > > > > 
> > > > > This commit adds a litmus test in which P0() and P1() form a 
> > > > > lock-based S
> > > > > litmus test, with the addition of P2(), which observes P0()'s and 
> > > > > P1()'s
> > > > 
> > > > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > > > description?
> > > 
> > > Indeed, the name of the test is in fact ISA2.
> > 
> > Sure; and the Changelog entry should reflect this.
> 
> No argument.

> 
> 
> commit e6658d1d7fcc6391f3d00beaadc484243123a893
> Author: Paul E. McKenney 
> Date:   Wed Feb 21 09:49:01 2018 -0800
> 
> tools/memory-order: Add documentation of new litmus test
> 
> The litmus-tests/README file lacked any mention of then litmus test

s/lacked/lacks/
s/then/the new/

> named ISA2+pooncelock+pooncelock+pombonce.litmus.  This commit therefore

s/named //

> adds this test.

It adds a description of the test, not the test itself.

> 
> Reported-by: Alan Stern 
> Signed-off-by: Paul E. McKenney 
> 
> diff --git a/tools/memory-model/litmus-tests/README 
> b/tools/memory-model/litmus-tests/README
> index dca7d823ad57..aff3eb90e067 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
>   order of a pair of writes, where each write is to a different
>   variable by a different process?
>  
> +ISA2+pooncelock+pooncelock+pombonce.litmus
> + Tests whether the ordering provided by a lock-protected S litmus

Call it an ISA2 litmus test, not an S litmus test!

> + test is visible to an external process whose accesses are
> + separated by smp_mb().
> +
>  ISA2+poonceonces.litmus
>   As below, but with store-release replaced with WRITE_ONCE()
>   and load-acquire replaced with READ_ONCE().

Alan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Wed, 21 Feb 2018, Paul E. McKenney wrote:

> On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> > On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> > 
> > > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > > 
> > > > > From: Alan Stern 
> > > > > 
> > > > > This commit adds a litmus test in which P0() and P1() form a 
> > > > > lock-based S
> > > > > litmus test, with the addition of P2(), which observes P0()'s and 
> > > > > P1()'s
> > > > 
> > > > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > > > description?
> > > 
> > > Indeed, the name of the test is in fact ISA2.
> > 
> > Sure; and the Changelog entry should reflect this.
> 
> No argument.

> 
> 
> commit e6658d1d7fcc6391f3d00beaadc484243123a893
> Author: Paul E. McKenney 
> Date:   Wed Feb 21 09:49:01 2018 -0800
> 
> tools/memory-order: Add documentation of new litmus test
> 
> The litmus-tests/README file lacked any mention of then litmus test

s/lacked/lacks/
s/then/the new/

> named ISA2+pooncelock+pooncelock+pombonce.litmus.  This commit therefore

s/named //

> adds this test.

It adds a description of the test, not the test itself.

> 
> Reported-by: Alan Stern 
> Signed-off-by: Paul E. McKenney 
> 
> diff --git a/tools/memory-model/litmus-tests/README 
> b/tools/memory-model/litmus-tests/README
> index dca7d823ad57..aff3eb90e067 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
>   order of a pair of writes, where each write is to a different
>   variable by a different process?
>  
> +ISA2+pooncelock+pooncelock+pombonce.litmus
> + Tests whether the ordering provided by a lock-protected S litmus

Call it an ISA2 litmus test, not an S litmus test!

> + test is visible to an external process whose accesses are
> + separated by smp_mb().
> +
>  ISA2+poonceonces.litmus
>   As below, but with store-release replaced with WRITE_ONCE()
>   and load-acquire replaced with READ_ONCE().

Alan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Wed, 21 Feb 2018, Paul E. McKenney wrote:

> > > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > > + Tests whether the ordering provided by a lock-protected S litmus
> > 
> > Call it an ISA2 litmus test, not an S litmus test!
> 
> Given the structure of the test, the relationship to S is important
> because it helps motivate why anyone might care.  But yes, having ISA2
> only in the filename is a bit obtuse.  How about the following?
> 
> ISA2+pooncelock+pooncelock+pombonce.litmus
>   Tests whether the ordering provided by a lock-protected S
>   litmus test is visible to an external process whose accesses are
>   separated by smp_mb().  This addition of an external process to
>   S is otherwise known as ISA2.

Okay, that's somewhat better.

However, I still don't understand why you think of this as a form of S.  
In S, the first variable written by P0 is the same as the variable
written by P1.  In this test, no variable other than the spinlock gets
written twice.  To me that seems like a pretty fundamental difference.

Alan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Wed, 21 Feb 2018, Paul E. McKenney wrote:

> > > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > > + Tests whether the ordering provided by a lock-protected S litmus
> > 
> > Call it an ISA2 litmus test, not an S litmus test!
> 
> Given the structure of the test, the relationship to S is important
> because it helps motivate why anyone might care.  But yes, having ISA2
> only in the filename is a bit obtuse.  How about the following?
> 
> ISA2+pooncelock+pooncelock+pombonce.litmus
>   Tests whether the ordering provided by a lock-protected S
>   litmus test is visible to an external process whose accesses are
>   separated by smp_mb().  This addition of an external process to
>   S is otherwise known as ISA2.

Okay, that's somewhat better.

However, I still don't understand why you think of this as a form of S.  
In S, the first variable written by P0 is the same as the variable
written by P1.  In this test, no variable other than the spinlock gets
written twice.  To me that seems like a pretty fundamental difference.

Alan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> 
> > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > 
> > > > From: Alan Stern 
> > > > 
> > > > This commit adds a litmus test in which P0() and P1() form a lock-based 
> > > > S
> > > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > 
> > > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > > description?
> > 
> > Indeed, the name of the test is in fact ISA2.
> 
> Sure; and the Changelog entry should reflect this.

No argument.

> > > > accesses with a full memory barrier but without the lock.  This litmus
> > > > test asks whether writes carried out by two different processes under 
> > > > the
> > > > same lock will be seen in order by a third process not holding that 
> > > > lock.
> > > > The answer to this question is "yes" for all architectures supporting
> > > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > > 
> > > > A patch to LKMM is under development.
> > > > 
> > > > Signed-off-by: Alan Stern 
> > > > Signed-off-by: Paul E. McKenney 
> > > > ---
> > > >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > > > ++
> > > >  1 file changed, 41 insertions(+)
> > > >  create mode 100644 
> > > > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > 
> > > Aren't these tests supposed to be described in litmus-tests/README?
> 
> You apparently missed this recommendation.

I did, please accept my apologies and please see below.

> > > > diff --git 
> > > > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > >  
> > > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > new file mode 100644
> > > > index ..7a39a0aaa976
> > > > --- /dev/null
> > > > +++ 
> > > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > @@ -0,0 +1,41 @@
> > > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > +
> > > > +(*
> > > > + * Result: Sometimes
> > > > + *
> > > > + * This test shows that the ordering provided by a lock-protected S
> > > > + * litmus test (P0() and P1()) are not visible to external process 
> > > > P2().
> > > > + * This is likely to change soon.
> > > 
> > > That last line may be premature.  We haven't reached any consensus on 
> > > how RISC-V will handle this.  If RISC-V allows the test then the memory 
> > > model can't forbid it.
> > 
> > Agreed.  How about this?  If the RISC-V question is answered by the
> > end of next week, I update accordingly.  If not, I update the comment
> > to give the details.
> 
> The README also should be updated.

Agreed.

> > Hey, at least having the memory model go in at about the same time as
> > a new architecture is giving us good practice!  ;-)
> 
> Hopefully things will settle down in a week or two.

Here is hoping!

Thanx, Paul



commit e6658d1d7fcc6391f3d00beaadc484243123a893
Author: Paul E. McKenney 
Date:   Wed Feb 21 09:49:01 2018 -0800

tools/memory-order: Add documentation of new litmus test

The litmus-tests/README file lacked any mention of then litmus test
named ISA2+pooncelock+pooncelock+pombonce.litmus.  This commit therefore
adds this test.

Reported-by: Alan Stern 
Signed-off-by: Paul E. McKenney 

diff --git a/tools/memory-model/litmus-tests/README 
b/tools/memory-model/litmus-tests/README
index dca7d823ad57..aff3eb90e067 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
order of a pair of writes, where each write is to a different
variable by a different process?
 
+ISA2+pooncelock+pooncelock+pombonce.litmus
+   Tests whether the ordering provided by a lock-protected S litmus
+   test is visible to an external process whose accesses are
+   separated by smp_mb().
+
 ISA2+poonceonces.litmus
As below, but with store-release replaced with WRITE_ONCE()
and load-acquire replaced with READ_ONCE().

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> 
> > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > 
> > > > From: Alan Stern 
> > > > 
> > > > This commit adds a litmus test in which P0() and P1() form a lock-based 
> > > > S
> > > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > 
> > > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > > description?
> > 
> > Indeed, the name of the test is in fact ISA2.
> 
> Sure; and the Changelog entry should reflect this.

No argument.

> > > > accesses with a full memory barrier but without the lock.  This litmus
> > > > test asks whether writes carried out by two different processes under 
> > > > the
> > > > same lock will be seen in order by a third process not holding that 
> > > > lock.
> > > > The answer to this question is "yes" for all architectures supporting
> > > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > > 
> > > > A patch to LKMM is under development.
> > > > 
> > > > Signed-off-by: Alan Stern 
> > > > Signed-off-by: Paul E. McKenney 
> > > > ---
> > > >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > > > ++
> > > >  1 file changed, 41 insertions(+)
> > > >  create mode 100644 
> > > > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > 
> > > Aren't these tests supposed to be described in litmus-tests/README?
> 
> You apparently missed this recommendation.

I did, please accept my apologies and please see below.

> > > > diff --git 
> > > > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > >  
> > > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > new file mode 100644
> > > > index ..7a39a0aaa976
> > > > --- /dev/null
> > > > +++ 
> > > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > @@ -0,0 +1,41 @@
> > > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > +
> > > > +(*
> > > > + * Result: Sometimes
> > > > + *
> > > > + * This test shows that the ordering provided by a lock-protected S
> > > > + * litmus test (P0() and P1()) are not visible to external process 
> > > > P2().
> > > > + * This is likely to change soon.
> > > 
> > > That last line may be premature.  We haven't reached any consensus on 
> > > how RISC-V will handle this.  If RISC-V allows the test then the memory 
> > > model can't forbid it.
> > 
> > Agreed.  How about this?  If the RISC-V question is answered by the
> > end of next week, I update accordingly.  If not, I update the comment
> > to give the details.
> 
> The README also should be updated.

Agreed.

> > Hey, at least having the memory model go in at about the same time as
> > a new architecture is giving us good practice!  ;-)
> 
> Hopefully things will settle down in a week or two.

Here is hoping!

Thanx, Paul



commit e6658d1d7fcc6391f3d00beaadc484243123a893
Author: Paul E. McKenney 
Date:   Wed Feb 21 09:49:01 2018 -0800

tools/memory-order: Add documentation of new litmus test

The litmus-tests/README file lacked any mention of then litmus test
named ISA2+pooncelock+pooncelock+pombonce.litmus.  This commit therefore
adds this test.

Reported-by: Alan Stern 
Signed-off-by: Paul E. McKenney 

diff --git a/tools/memory-model/litmus-tests/README 
b/tools/memory-model/litmus-tests/README
index dca7d823ad57..aff3eb90e067 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
order of a pair of writes, where each write is to a different
variable by a different process?
 
+ISA2+pooncelock+pooncelock+pombonce.litmus
+   Tests whether the ordering provided by a lock-protected S litmus
+   test is visible to an external process whose accesses are
+   separated by smp_mb().
+
 ISA2+poonceonces.litmus
As below, but with store-release replaced with WRITE_ONCE()
and load-acquire replaced with READ_ONCE().

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Wed, 21 Feb 2018, Paul E. McKenney wrote:

> On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > 
> > > From: Alan Stern 
> > > 
> > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > 
> > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > description?
> 
> Indeed, the name of the test is in fact ISA2.

Sure; and the Changelog entry should reflect this.

> > > accesses with a full memory barrier but without the lock.  This litmus
> > > test asks whether writes carried out by two different processes under the
> > > same lock will be seen in order by a third process not holding that lock.
> > > The answer to this question is "yes" for all architectures supporting
> > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > 
> > > A patch to LKMM is under development.
> > > 
> > > Signed-off-by: Alan Stern 
> > > Signed-off-by: Paul E. McKenney 
> > > ---
> > >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > > ++
> > >  1 file changed, 41 insertions(+)
> > >  create mode 100644 
> > > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > 
> > Aren't these tests supposed to be described in litmus-tests/README?

You apparently missed this recommendation.

> > > diff --git 
> > > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > >  
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > new file mode 100644
> > > index ..7a39a0aaa976
> > > --- /dev/null
> > > +++ 
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > @@ -0,0 +1,41 @@
> > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > +
> > > +(*
> > > + * Result: Sometimes
> > > + *
> > > + * This test shows that the ordering provided by a lock-protected S
> > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > + * This is likely to change soon.
> > 
> > That last line may be premature.  We haven't reached any consensus on 
> > how RISC-V will handle this.  If RISC-V allows the test then the memory 
> > model can't forbid it.
> 
> Agreed.  How about this?  If the RISC-V question is answered by the
> end of next week, I update accordingly.  If not, I update the comment
> to give the details.

The README also should be updated.

> Hey, at least having the memory model go in at about the same time as
> a new architecture is giving us good practice!  ;-)

Hopefully things will settle down in a week or two.

Alan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Wed, 21 Feb 2018, Paul E. McKenney wrote:

> On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > 
> > > From: Alan Stern 
> > > 
> > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > 
> > Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> > description?
> 
> Indeed, the name of the test is in fact ISA2.

Sure; and the Changelog entry should reflect this.

> > > accesses with a full memory barrier but without the lock.  This litmus
> > > test asks whether writes carried out by two different processes under the
> > > same lock will be seen in order by a third process not holding that lock.
> > > The answer to this question is "yes" for all architectures supporting
> > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > 
> > > A patch to LKMM is under development.
> > > 
> > > Signed-off-by: Alan Stern 
> > > Signed-off-by: Paul E. McKenney 
> > > ---
> > >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > > ++
> > >  1 file changed, 41 insertions(+)
> > >  create mode 100644 
> > > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > 
> > Aren't these tests supposed to be described in litmus-tests/README?

You apparently missed this recommendation.

> > > diff --git 
> > > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > >  
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > new file mode 100644
> > > index ..7a39a0aaa976
> > > --- /dev/null
> > > +++ 
> > > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > @@ -0,0 +1,41 @@
> > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > +
> > > +(*
> > > + * Result: Sometimes
> > > + *
> > > + * This test shows that the ordering provided by a lock-protected S
> > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > + * This is likely to change soon.
> > 
> > That last line may be premature.  We haven't reached any consensus on 
> > how RISC-V will handle this.  If RISC-V allows the test then the memory 
> > model can't forbid it.
> 
> Agreed.  How about this?  If the RISC-V question is answered by the
> end of next week, I update accordingly.  If not, I update the comment
> to give the details.

The README also should be updated.

> Hey, at least having the memory model go in at about the same time as
> a new architecture is giving us good practice!  ;-)

Hopefully things will settle down in a week or two.

Alan

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> 
> > From: Alan Stern 
> > 
> > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> 
> Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> description?

Indeed, the name of the test is in fact ISA2.

> > accesses with a full memory barrier but without the lock.  This litmus
> > test asks whether writes carried out by two different processes under the
> > same lock will be seen in order by a third process not holding that lock.
> > The answer to this question is "yes" for all architectures supporting
> > the Linux kernel, but is "no" according to the current version of LKMM.
> > 
> > A patch to LKMM is under development.
> > 
> > Signed-off-by: Alan Stern 
> > Signed-off-by: Paul E. McKenney 
> > ---
> >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > ++
> >  1 file changed, 41 insertions(+)
> >  create mode 100644 
> > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> 
> Aren't these tests supposed to be described in litmus-tests/README?
> 
> > diff --git 
> > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >  
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > new file mode 100644
> > index ..7a39a0aaa976
> > --- /dev/null
> > +++ 
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -0,0 +1,41 @@
> > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This test shows that the ordering provided by a lock-protected S
> > + * litmus test (P0() and P1()) are not visible to external process P2().
> > + * This is likely to change soon.
> 
> That last line may be premature.  We haven't reached any consensus on 
> how RISC-V will handle this.  If RISC-V allows the test then the memory 
> model can't forbid it.

Agreed.  How about this?  If the RISC-V question is answered by the
end of next week, I update accordingly.  If not, I update the comment
to give the details.

Hey, at least having the memory model go in at about the same time as
a new architecture is giving us good practice!  ;-)

Thanx, Paul

> Alan
> 
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y, spinlock_t *mylock)
> > +{
> > +   spin_lock(mylock);
> > +   WRITE_ONCE(*x, 1);
> > +   WRITE_ONCE(*y, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P1(int *y, int *z, spinlock_t *mylock)
> > +{
> > +   int r0;
> > +
> > +   spin_lock(mylock);
> > +   r0 = READ_ONCE(*y);
> > +   WRITE_ONCE(*z, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P2(int *x, int *z)
> > +{
> > +   int r1;
> > +   int r2;
> > +
> > +   r2 = READ_ONCE(*z);
> > +   smp_mb();
> > +   r1 = READ_ONCE(*x);
> > +}
> > +
> > +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > 
> 
> 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> 
> > From: Alan Stern 
> > 
> > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> 
> Why do you call this an "S" litmus test?  Isn't ISA2 a better 
> description?

Indeed, the name of the test is in fact ISA2.

> > accesses with a full memory barrier but without the lock.  This litmus
> > test asks whether writes carried out by two different processes under the
> > same lock will be seen in order by a third process not holding that lock.
> > The answer to this question is "yes" for all architectures supporting
> > the Linux kernel, but is "no" according to the current version of LKMM.
> > 
> > A patch to LKMM is under development.
> > 
> > Signed-off-by: Alan Stern 
> > Signed-off-by: Paul E. McKenney 
> > ---
> >  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> > ++
> >  1 file changed, 41 insertions(+)
> >  create mode 100644 
> > tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> 
> Aren't these tests supposed to be described in litmus-tests/README?
> 
> > diff --git 
> > a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >  
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > new file mode 100644
> > index ..7a39a0aaa976
> > --- /dev/null
> > +++ 
> > b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -0,0 +1,41 @@
> > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This test shows that the ordering provided by a lock-protected S
> > + * litmus test (P0() and P1()) are not visible to external process P2().
> > + * This is likely to change soon.
> 
> That last line may be premature.  We haven't reached any consensus on 
> how RISC-V will handle this.  If RISC-V allows the test then the memory 
> model can't forbid it.

Agreed.  How about this?  If the RISC-V question is answered by the
end of next week, I update accordingly.  If not, I update the comment
to give the details.

Hey, at least having the memory model go in at about the same time as
a new architecture is giving us good practice!  ;-)

Thanx, Paul

> Alan
> 
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y, spinlock_t *mylock)
> > +{
> > +   spin_lock(mylock);
> > +   WRITE_ONCE(*x, 1);
> > +   WRITE_ONCE(*y, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P1(int *y, int *z, spinlock_t *mylock)
> > +{
> > +   int r0;
> > +
> > +   spin_lock(mylock);
> > +   r0 = READ_ONCE(*y);
> > +   WRITE_ONCE(*z, 1);
> > +   spin_unlock(mylock);
> > +}
> > +
> > +P2(int *x, int *z)
> > +{
> > +   int r1;
> > +   int r2;
> > +
> > +   r2 = READ_ONCE(*z);
> > +   smp_mb();
> > +   r1 = READ_ONCE(*x);
> > +}
> > +
> > +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > 
> 
> 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Tue, 20 Feb 2018, Paul E. McKenney wrote:

> From: Alan Stern 
> 
> This commit adds a litmus test in which P0() and P1() form a lock-based S
> litmus test, with the addition of P2(), which observes P0()'s and P1()'s

Why do you call this an "S" litmus test?  Isn't ISA2 a better 
description?

> accesses with a full memory barrier but without the lock.  This litmus
> test asks whether writes carried out by two different processes under the
> same lock will be seen in order by a third process not holding that lock.
> The answer to this question is "yes" for all architectures supporting
> the Linux kernel, but is "no" according to the current version of LKMM.
> 
> A patch to LKMM is under development.
> 
> Signed-off-by: Alan Stern 
> Signed-off-by: Paul E. McKenney 
> ---
>  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> ++
>  1 file changed, 41 insertions(+)
>  create mode 100644 
> tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus

Aren't these tests supposed to be described in litmus-tests/README?

> diff --git 
> a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> new file mode 100644
> index ..7a39a0aaa976
> --- /dev/null
> +++ 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -0,0 +1,41 @@
> +C ISA2+pooncelock+pooncelock+pombonce.litmus
> +
> +(*
> + * Result: Sometimes
> + *
> + * This test shows that the ordering provided by a lock-protected S
> + * litmus test (P0() and P1()) are not visible to external process P2().
> + * This is likely to change soon.

That last line may be premature.  We haven't reached any consensus on 
how RISC-V will handle this.  If RISC-V allows the test then the memory 
model can't forbid it.

Alan

> + *)
> +
> +{}
> +
> +P0(int *x, int *y, spinlock_t *mylock)
> +{
> + spin_lock(mylock);
> + WRITE_ONCE(*x, 1);
> + WRITE_ONCE(*y, 1);
> + spin_unlock(mylock);
> +}
> +
> +P1(int *y, int *z, spinlock_t *mylock)
> +{
> + int r0;
> +
> + spin_lock(mylock);
> + r0 = READ_ONCE(*y);
> + WRITE_ONCE(*z, 1);
> + spin_unlock(mylock);
> +}
> +
> +P2(int *x, int *z)
> +{
> + int r1;
> + int r2;
> +
> + r2 = READ_ONCE(*z);
> + smp_mb();
> + r1 = READ_ONCE(*x);
> +}
> +
> +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> 

Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Alan Stern]

On Tue, 20 Feb 2018, Paul E. McKenney wrote:

> From: Alan Stern 
> 
> This commit adds a litmus test in which P0() and P1() form a lock-based S
> litmus test, with the addition of P2(), which observes P0()'s and P1()'s

Why do you call this an "S" litmus test?  Isn't ISA2 a better 
description?

> accesses with a full memory barrier but without the lock.  This litmus
> test asks whether writes carried out by two different processes under the
> same lock will be seen in order by a third process not holding that lock.
> The answer to this question is "yes" for all architectures supporting
> the Linux kernel, but is "no" according to the current version of LKMM.
> 
> A patch to LKMM is under development.
> 
> Signed-off-by: Alan Stern 
> Signed-off-by: Paul E. McKenney 
> ---
>  .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 
> ++
>  1 file changed, 41 insertions(+)
>  create mode 100644 
> tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus

Aren't these tests supposed to be described in litmus-tests/README?

> diff --git 
> a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> new file mode 100644
> index ..7a39a0aaa976
> --- /dev/null
> +++ 
> b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -0,0 +1,41 @@
> +C ISA2+pooncelock+pooncelock+pombonce.litmus
> +
> +(*
> + * Result: Sometimes
> + *
> + * This test shows that the ordering provided by a lock-protected S
> + * litmus test (P0() and P1()) are not visible to external process P2().
> + * This is likely to change soon.

That last line may be premature.  We haven't reached any consensus on 
how RISC-V will handle this.  If RISC-V allows the test then the memory 
model can't forbid it.

Alan

> + *)
> +
> +{}
> +
> +P0(int *x, int *y, spinlock_t *mylock)
> +{
> + spin_lock(mylock);
> + WRITE_ONCE(*x, 1);
> + WRITE_ONCE(*y, 1);
> + spin_unlock(mylock);
> +}
> +
> +P1(int *y, int *z, spinlock_t *mylock)
> +{
> + int r0;
> +
> + spin_lock(mylock);
> + r0 = READ_ONCE(*y);
> + WRITE_ONCE(*z, 1);
> + spin_unlock(mylock);
> +}
> +
> +P2(int *x, int *z)
> +{
> + int r1;
> + int r2;
> +
> + r2 = READ_ONCE(*z);
> + smp_mb();
> + r1 = READ_ONCE(*x);
> +}
> +
> +exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> 

[PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

From: Alan Stern 

This commit adds a litmus test in which P0() and P1() form a lock-based S
litmus test, with the addition of P2(), which observes P0()'s and P1()'s
accesses with a full memory barrier but without the lock.  This litmus
test asks whether writes carried out by two different processes under the
same lock will be seen in order by a third process not holding that lock.
The answer to this question is "yes" for all architectures supporting
the Linux kernel, but is "no" according to the current version of LKMM.

A patch to LKMM is under development.

Signed-off-by: Alan Stern 
Signed-off-by: Paul E. McKenney 
---
 .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++
 1 file changed, 41 insertions(+)
 create mode 100644 
tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus

diff --git 
a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus 
b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
new file mode 100644
index ..7a39a0aaa976
--- /dev/null
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -0,0 +1,41 @@
+C ISA2+pooncelock+pooncelock+pombonce.litmus
+
+(*
+ * Result: Sometimes
+ *
+ * This test shows that the ordering provided by a lock-protected S
+ * litmus test (P0() and P1()) are not visible to external process P2().
+ * This is likely to change soon.
+ *)
+
+{}
+
+P0(int *x, int *y, spinlock_t *mylock)
+{
+   spin_lock(mylock);
+   WRITE_ONCE(*x, 1);
+   WRITE_ONCE(*y, 1);
+   spin_unlock(mylock);
+}
+
+P1(int *y, int *z, spinlock_t *mylock)
+{
+   int r0;
+
+   spin_lock(mylock);
+   r0 = READ_ONCE(*y);
+   WRITE_ONCE(*z, 1);
+   spin_unlock(mylock);
+}
+
+P2(int *x, int *z)
+{
+   int r1;
+   int r2;
+
+   r2 = READ_ONCE(*z);
+   smp_mb();
+   r1 = READ_ONCE(*x);
+}
+
+exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
-- 
2.5.2

[PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Paul E. McKenney]

From: Alan Stern 

This commit adds a litmus test in which P0() and P1() form a lock-based S
litmus test, with the addition of P2(), which observes P0()'s and P1()'s
accesses with a full memory barrier but without the lock.  This litmus
test asks whether writes carried out by two different processes under the
same lock will be seen in order by a third process not holding that lock.
The answer to this question is "yes" for all architectures supporting
the Linux kernel, but is "no" according to the current version of LKMM.

A patch to LKMM is under development.

Signed-off-by: Alan Stern 
Signed-off-by: Paul E. McKenney 
---
 .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++
 1 file changed, 41 insertions(+)
 create mode 100644 
tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus

diff --git 
a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus 
b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
new file mode 100644
index ..7a39a0aaa976
--- /dev/null
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -0,0 +1,41 @@
+C ISA2+pooncelock+pooncelock+pombonce.litmus
+
+(*
+ * Result: Sometimes
+ *
+ * This test shows that the ordering provided by a lock-protected S
+ * litmus test (P0() and P1()) are not visible to external process P2().
+ * This is likely to change soon.
+ *)
+
+{}
+
+P0(int *x, int *y, spinlock_t *mylock)
+{
+   spin_lock(mylock);
+   WRITE_ONCE(*x, 1);
+   WRITE_ONCE(*y, 1);
+   spin_unlock(mylock);
+}
+
+P1(int *y, int *z, spinlock_t *mylock)
+{
+   int r0;
+
+   spin_lock(mylock);
+   r0 = READ_ONCE(*y);
+   WRITE_ONCE(*z, 1);
+   spin_unlock(mylock);
+}
+
+P2(int *x, int *z)
+{
+   int r1;
+   int r2;
+
+   r2 = READ_ONCE(*z);
+   smp_mb();
+   r1 = READ_ONCE(*x);
+}
+
+exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
-- 
2.5.2