Re: [RFC v2 3/3] tools/memory-model: litmus: Add two tests for unlock(A)+lock(B) ordering

[Paul E. McKenney]

On Fri, Oct 29, 2021 at 10:34:42AM -0400, Alan Stern wrote:
> On Fri, Oct 29, 2021 at 07:51:39AM +0800, Boqun Feng wrote:
> > On Thu, Oct 28, 2021 at 12:11:29PM -0700, Paul E. McKenney wrote:
> > > On Tue, Oct 26, 2021 at 09:01:00AM +0200, Peter Zijlstra wrote:
> > > > On Mon, Oct 25, 2021 at 10:54:16PM +0800, Boqun Feng wrote:
> > > > > diff --git a/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
> > > > > new file mode 100644
> > > > > index 000000000000..955b9c7cdc7f
> > > > > --- /dev/null
> > > > > +++ b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
> > > > > @@ -0,0 +1,33 @@
> > > > > +C LB+unlocklockonceonce+poacquireonce
> > > > > +
> > > > > +(*
> > > > > + * Result: Never
> > > > > + *
> > > > > + * If two locked critical sections execute on the same CPU, all accesses
> > > > > + * in the first must execute before any accesses in the second, even if
> > > > > + * the critical sections are protected by different locks.
> > > > 
> > > > One small nit; the above "all accesses" reads as if:
> > > > 
> > > > 	spin_lock(s);
> > > > 	WRITE_ONCE(*x, 1);
> > > > 	spin_unlock(s);
> > > > 	spin_lock(t);
> > > > 	r1 = READ_ONCE(*y);
> > > > 	spin_unlock(t);
> > > > 
> > > > would also work, except of course that's the one reorder allowed by TSO.
> > > 
> > > I applied this series with Peter's Acked-by, and with the above comment
> > 
> > Thanks!
> > 
> > > reading as follows:
> > > 
> > > +(*
> > > + * Result: Never
> > > + *
> > > + * If two locked critical sections execute on the same CPU, all accesses
> > > + * in the first must execute before any accesses in the second, even if the
> > > + * critical sections are protected by different locks.  The one exception
> > > + * to this rule is that (consistent with TSO) a prior write can be reordered
> > > + * with a later read from the viewpoint of a process not holding both locks.
> > 
> > Just want to be accurate, in our memory model "execute" means a CPU
> > commit an memory access instruction to the Memory Subsystem, so if we
> > have a store W and a load R, where W executes before R, it doesn't mean
> > the memory effect of W is observed before the memory effect of R by
> > other CPUs, consider the following case
> > 
> > 
> > 	CPU0			Memory Subsystem		CPU1
> > 	====							====
> > 	WRITE_ONCE(*x,1); // W ---------->|
> > 	spin_unlock(s);                   |
> > 	spin_lock(t);                     |
> > 	r1 = READ_ONCE(*y); // R -------->|
> > 	// R reads 0                      |
> > 					  |<----------------WRITR_ONCE(*y, 1); // W'
> > 		 W' propagates to CPU0    |
> > 		<-------------------------|
> > 					  |                 smp_mb();
> > 					  |<----------------r1 = READ_ONCE(*x); // R' reads 0
> > 					  |
> > 					  | W progrates to CPU 1
> > 		                          |----------------->
> > 
> > The "->" from CPU0 to the Memory Subsystem shows that W executes before
> > R, however the memory effect of a store can be observed only after the
> > Memory Subsystem propagates it to another CPU, as a result CPU1 doesn't
> > observe W before R is executed. So the original version of the comments
> > is correct in our memory model terminology, at least that's how I
> > understand it, Alan can correct me if I'm wrong.
> 
> Indeed, that is correct.
> 
> It is an unfortunate inconsistency with the terminology in 
> Documentation/memory-barriers.txt.  I suspect most people think of a 
> write as executing when it is observed by another CPU, even though that 
> really isn't a coherent concept.  (For example, it could easily lead 
> somebody to think that a write observed at different times by different 
> CPUs has executed more than once!)

Agreed, the terminology is odd.  But the fact that different CPUs can
see writes in different orders is probably always going to be a bit
counter-intuitive, so it is good to avoid giving that intuition any
support.

> > Maybe it's better to replace the sentence starting with "The one
> > exception..." into:
> > 
> > One thing to notice is that even though a write executes by a read, the
> > memory effects can still be reordered from the viewpoint of a process
> > not holding both locks, similar to TSO ordering.
> > 
> > Thoughts?
> 
> Or more briefly:
> 
> 	Note: Even when a write executes before a read, their memory
> 	effects can be reordered from the viewpoint of another CPU (the 
> 	kind of reordering allowed by TSO).

Very good!  I took this verbatim in a fixup patch to be combined
with the original on my next rebase.

							Thanx, Paul

> Alan
> 
> > Apologies for responsing late...
> > 
> > ("Memory Subsystem" is an abstraction in our memory model, which doesn't
> > mean hardware implements things in the same way.).
> > 
> > Regards,
> > Boqun
> > 
> > > + *)
> > > 
> > > Thank you all!
> > > 
> > > 							Thanx, Paul