Re: [PATCH 2/2] tools/memory-model: Add write ordering by release-acquire and by locks

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Fri, Jun 22, 2018 at 12:31:29PM +0200, Peter Zijlstra wrote:
> On Fri, Jun 22, 2018 at 10:55:47AM +0100, Will Deacon wrote:
> > On Fri, Jun 22, 2018 at 09:09:28AM +0100, Will Deacon wrote:
> > > On Thu, Jun 21, 2018 at 01:27:12PM -0400, Alan Stern wrote:
> > > > More than one kernel developer has expressed the opinion that the LKMM
> > > > should enforce ordering of writes by release-acquire chains and by
> > > > locking.  In other words, given the following code:
> > > > 
> > > > 	WRITE_ONCE(x, 1);
> > > > 	spin_unlock(&s):
> > > > 	spin_lock(&s);
> > > > 	WRITE_ONCE(y, 1);
> 
> So this is the one I'm relying on and really want sorted.
> 
> > > > or the following:
> > > > 
> > > > 	smp_store_release(&x, 1);
> > > > 	r1 = smp_load_acquire(&x);	// r1 = 1
> > > > 	WRITE_ONCE(y, 1);
> 
> Reading back some of the old threads [1], it seems the direct
> translation of the first into acquire-release would be:
> 
> 	WRITE_ONCE(x, 1);
> 	smp_store_release(&s, 1);
> 	r1 = smp_load_acquire(&s);
> 	WRITE_ONCE(y, 1);
> 
> Which is I think easier to make happen than the second example you give.
> 
> > > > the stores to x and y should be propagated in order to all other CPUs,
> > > > even though those other CPUs might not access the lock s or be part of
> > > > the release-acquire chain.  In terms of the memory model, this means
> > > > that rel-rf-acq-po should be part of the cumul-fence relation.
> > > > 
> > > > All the architectures supported by the Linux kernel (including RISC-V)
> > > > do behave this way, albeit for varying reasons.  Therefore this patch
> > > > changes the model in accordance with the developers' wishes.
> > > 
> > > Interesting...
> > > 
> > > I think the second example would preclude us using LDAPR for load-acquire,
> > > so I'm surprised that RISC-V is ok with this. For example, the first test
> > > below is allowed on arm64.
> > > 
> > > I also think this would break if we used DMB LD to implement load-acquire
> > > (second test below).
> > > 
> > > So I'm not a big fan of this change, and I'm surprised this works on all
> > > architectures. What's the justification?
> > 
> > I also just realised that this prevents Power from using ctrl+isync to
> > implement acquire, should they wish to do so.
> 
> They in fact do so on chips lacking LWSYNC, see how PPC_ACQUIRE_BARRIER
> (as used by atomic_*_acquire) turns into ISYNC (note however that they
> do not use PPC_ACQUIRE_BARRIER for smp_load_acquire -- because there's
> no CTRL there).

PowerPC -could- use a load-compare-branch-isync sequence to implement
smp_load_acquire(), but as you say it instead uses lwsync, falling
back to sync on CPUs not implementing lwsync.

Locking should work either way because even if lock acquisition uses isync
(leveraging the fact that the "stcwx." instruction affects condition
codes and branches back when someone else already holds the lock),
lock release still uses lwsync (or sync on systems not having lwsync).

							Thanx, Paul

> [1] https://lkml.kernel.org/r/20171128095850.rhtnx6e2qxep5npa@hirez.programming.kicks-ass.net
>