lkml.org 
[lkml]   [2021]   [Oct]   [29]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [RFC v2 3/3] tools/memory-model: litmus: Add two tests for unlock(A)+lock(B) ordering
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

\
 
 \ /
  Last update: 2021-10-29 17:03    [W:0.092 / U:0.228 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site