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 <stern@xxxxxxxxxxxxxxxxxxx>
> >>>>
> >>>> 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&m=151916916630299&w=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

Attachment: signature.asc
Description: PGP signature