On Thu, Oct 15, 2015 at 11:35:44AM +0100, Will Deacon wrote:
>
> So arm64 is ok. Doesn't lwsync order store->store observability for PPC?
>
I did some litmus and put the result here. My understanding might be
wrong, and I think Paul can explain the lwsync and store->store order
better ;-)
When a store->lwsync->store pairs with load->lwsync->load, according to
herd, YES.
PPC W+lwsync+W-R+lwsync+R
"
2015-10-15
herds said (1:r1=0 /\ 1:r2=2) doesn't exist,
so if P1 observe the write to 'b', it must also observe P0's write
to 'a'
"
{
0:r1=1; 0:r2=2; 0:r12=a; 0:r13=b;
1:r1=0; 1:r2=0; 1:r12=a; 1:r13=b;
}
P0 | P1 ;
stw r1, 0(r12) | lwz r2, 0(r13) ;
lwsync | lwsync ;
stw r2, 0(r13) | lwz r1, 0(r12) ;
exists
(1:r1=0 /\ 1:r2=2)
If observation also includes "a write on one CPU -override- another
write on another CPU", then
when a store->lwsync->store pairs(?) with store->sync->load, according
to herd, NO(?).
PPC W+lwsync+W-W+sync+R
"
2015-10-15
herds said (1:r1=0 /\ b=3) exists sometimes,
so if P1 observe P0's write to 'b'(by 'overriding' this write to
'b'), it may not observe P0's write to 'a'.
"
{
0:r1=1; 0:r2=2; 0:r12=a; 0:r13=b;
1:r1=0; 1:r2=3; 1:r12=a; 1:r13=b;
}
P0 | P1 ;
stw r1, 0(r12) | stw r2, 0(r13) ;
lwsync | sync ;
stw r2, 0(r13) | lwz r1, 0(r12) ;
exists
(1:r1=0 /\ b=3)
Regards,
Boqun
Attachment:
signature.asc
Description: PGP signature