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