On Mon, Jan 25, 2016 at 02:41:34PM +0000, Will Deacon wrote:
> On Fri, Jan 15, 2016 at 11:28:45AM -0800, Paul E. McKenney wrote:
> > On Fri, Jan 15, 2016 at 09:54:01AM -0800, Paul E. McKenney wrote:
> > > On Fri, Jan 15, 2016 at 10:24:32AM +0000, Will Deacon wrote:
> > > > See my earlier reply [1] (but also, your WRC Linux example looks more
> > > > like a variant on WWC and I couldn't really follow it).
> > >
> > > I will revisit my WRC Linux example. And yes, creating litmus tests
> > > that use non-fake dependencies is still a bit of an undertaking. :-/
> > > I am sure that it will seem more natural with time and experience...
> >
> > Hmmm... You are quite right, I did do WWC. I need to change cpu2()'s
> > last access from a store to a load to get WRC. Plus the levels of
> > indirection definitely didn't match up, did they?
>
> Nope, it was pretty baffling!
"It is a service that I provide." ;-)
> > struct foo {
> > struct foo *next;
> > };
> > struct foo a;
> > struct foo b;
> > struct foo c = { &a };
> > struct foo d = { &b };
> > struct foo x = { &c };
> > struct foo y = { &d };
> > struct foo *r1, *r2, *r3;
> >
> > void cpu0(void)
> > {
> > WRITE_ONCE(x.next, &y);
> > }
> >
> > void cpu1(void)
> > {
> > r1 = lockless_dereference(x.next);
> > WRITE_ONCE(r1->next, &x);
> > }
> >
> > void cpu2(void)
> > {
> > r2 = lockless_dereference(y.next);
> > r3 = READ_ONCE(r2->next);
> > }
> >
> > In this case, it is legal to end the run with:
> >
> > r1 == &y && r2 == &x && r3 == &c
> >
> > Please see below for a ppcmem litmus test.
> >
> > So, did I get it right this time? ;-)
>
> The code above looks correct to me (in that it matches WRC+addrs),
> but your litmus test:
>
> > PPC WRCnf+addrs
> > ""
> > {
> > 0:r2=x; 0:r3=y;
> > 1:r2=x; 1:r3=y;
> > 2:r2=x; 2:r3=y;
> > c=a; d=b; x=c; y=d;
> > }
> > P0 | P1 | P2 ;
> > stw r3,0(r2) | lwz r8,0(r2) | lwz r8,0(r3) ;
> > | stw r2,0(r3) | lwz r9,0(r8) ;
> > exists
> > (1:r8=y /\ 2:r8=x /\ 2:r9=c)
>
> Seems to be missing the address dependency on P1.
You are quite correct! How about the following?
As before, both herd and ppcmem say that the cycle is allowed, as
expected, given non-transitive ordering. To prohibit the cycle, P1
needs a suitable memory-barrier instruction.
Thanx, Paul
------------------------------------------------------------------------
PPC WRCnf+addrs
""
{
0:r2=x; 0:r3=y;
1:r2=x; 1:r3=y;
2:r2=x; 2:r3=y;
c=a; d=b; x=c; y=d;
}
P0 | P1 | P2 ;
stw r3,0(r2) | lwz r8,0(r2) | lwz r8,0(r3) ;
| stw r2,0(r8) | lwz r9,0(r8) ;
exists
(1:r8=y /\ 2:r8=x /\ 2:r9=c)
--
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
--
To unsubscribe from this list: send the line "unsubscribe linux-metag" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
