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

[Alan Stern]

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!)

> 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).

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