lkml.org 
[lkml]   [2015]   [Oct]   [15]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH tip/locking/core v4 1/6] powerpc: atomic: Make *xchg and *cmpxchg a full barrier
Dammit guys, it's never simple is it?

On Wed, Oct 14, 2015 at 02:44:53PM -0700, Paul E. McKenney wrote:
> To that end, the herd tool can make a diagram of what it thought
> happened, and I have attached it. I used this diagram to try and force
> this scenario at https://www.cl.cam.ac.uk/~pes20/ppcmem/index.html#PPC,
> and succeeded. Here is the sequence of events:
>
> o Commit P0's write. The model offers to propagate this write
> to the coherence point and to P1, but don't do so yet.
>
> o Commit P1's write. Similar offers, but don't take them up yet.
>
> o Commit P0's lwsync.
>
> o Execute P0's lwarx, which reads a=0. Then commit it.
>
> o Commit P0's stwcx. as successful. This stores a=1.

On arm64, this is a conditional-store-*release* and therefore cannot be
observed before the initial write to x...

> o Commit P0's branch (not taken).
>
> o Commit P0's final register-to-register move.
>
> o Commit P1's sync instruction.
>
> o There is now nothing that can happen in either processor.
> P0 is done, and P1 is waiting for its sync. Therefore,
> propagate P1's a=2 write to the coherence point and to
> the other thread.

... therefore this is illegal, because you haven't yet propagated that
prior write...

>
> o There is still nothing that can happen in either processor.
> So pick the barrier propagate, then the acknowledge sync.
>
> o P1 can now execute its read from x. Because P0's write to
> x is still waiting to propagate to P1, this still reads
> x=0. Execute and commit, and we now have both r3 registers
> equal to zero and the final value a=2.

... and P1 would have to read x == 1.

So arm64 is ok. Doesn't lwsync order store->store observability for PPC?

Will


\
 
 \ /
  Last update: 2015-10-15 13:01    [W:0.140 / U:0.528 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site