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

[Alan Stern <stern@rowland.harvard.edu>]

On Fri, 22 Jun 2018, Andrea Parri 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);
> > 
> > or the following:
> > 
> > 	smp_store_release(&x, 1);
> > 	r1 = smp_load_acquire(&x);	// r1 = 1
> > 	WRITE_ONCE(y, 1);
> > 
> > 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.
> > 
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 
> This patch changes the "Result" for ISA2+pooncelock+pooncelock+pombonce,
> so it should update the corresponding comment/README.

Thanks for noticing this.  The next version of this patch will update 
the comment.  The README seems to be adequate as it is now, since it 
doesn't specify the result of the litmus test.

Alan