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
