Re: [PATCH v2 1/2] tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-po

Paul E. McKenney
2023-01-26T23:21:56Z

On Thu, Jan 26, 2023 at 12:08:28PM -0800, Paul E. McKenney wrote:
> On Thu, Jan 26, 2023 at 11:36:51AM -0500, Alan Stern wrote:
> > On Thu, Jan 26, 2023 at 02:46:03PM +0100, Jonas Oberhauser wrote:
> > > LKMM uses two relations for talking about UNLOCK+LOCK pairings:
> > >
> > > 1) po-unlock-lock-po, which handles UNLOCK+LOCK pairings
> > > on the same CPU or immediate lock handovers on the same
> > > lock variable
> > >
> > > 2) po;[UL];(co|po);[LKW];po, which handles UNLOCK+LOCK pairs
> > > literally as described in rcupdate.h#L1002, i.e., even
> > > after a sequence of handovers on the same lock variable.
> > >
> > > The latter relation is used only once, to provide the guarantee
> > > defined in rcupdate.h#L1002 by smp_mb__after_unlock_lock(), which
> > > makes any UNLOCK+LOCK pair followed by the fence behave like a full
> > > barrier.
> > >
> > > This patch drops this use in favor of using po-unlock-lock-po
> > > everywhere, which unifies the way the model talks about UNLOCK+LOCK
> > > pairings. At first glance this seems to weaken the guarantee given
> > > by LKMM: When considering a long sequence of lock handovers
> > > such as below, where P0 hands the lock to P1, which hands it to P2,
> > > which finally executes such an after_unlock_lock fence, the mb
> > > relation currently links any stores in the critical section of P0
> > > to instructions P2 executes after its fence, but not so after the
> > > patch.
> > >
> > > P0(int *x, int *y, spinlock_t *mylock)
> > > {
> > > spin_lock(mylock);
> > > WRITE_ONCE(*x, 2);
> > > spin_unlock(mylock);
> > > WRITE_ONCE(*y, 1);
> > > }
> > >
> > > P1(int *y, int *z, spinlock_t *mylock)
> > > {
> > > int r0 = READ_ONCE(*y); // reads 1
> > > spin_lock(mylock);
> > > spin_unlock(mylock);
> > > WRITE_ONCE(*z,1);
> > > }
> > >
> > > P2(int *z, int *d, spinlock_t *mylock)
> > > {
> > > int r1 = READ_ONCE(*z); // reads 1
> > > spin_lock(mylock);
> > > spin_unlock(mylock);
> > > smp_mb__after_unlock_lock();
> > > WRITE_ONCE(*d,1);
> > > }
> > >
> > > P3(int *x, int *d)
> > > {
> > > WRITE_ONCE(*d,2);
> > > smp_mb();
> > > WRITE_ONCE(*x,1);
> > > }
> > >
> > > exists (1:r0=1 /\ 2:r1=1 /\ x=2 /\ d=2)
> > >
> > > Nevertheless, the ordering guarantee given in rcupdate.h is actually
> > > not weakened. This is because the unlock operations along the
> > > sequence of handovers are A-cumulative fences. They ensure that any
> > > stores that propagate to the CPU performing the first unlock
> > > operation in the sequence must also propagate to every CPU that
> > > performs a subsequent lock operation in the sequence. Therefore any
> > > such stores will also be ordered correctly by the fence even if only
> > > the final handover is considered a full barrier.
> > >
> > > Indeed this patch does not affect the behaviors allowed by LKMM at
> > > all. The mb relation is used to define ordering through:
> > > 1) mb/.../ppo/hb, where the ordering is subsumed by hb+ where the
> > > lock-release, rfe, and unlock-acquire orderings each provide hb
> > > 2) mb/strong-fence/cumul-fence/prop, where the rfe and A-cumulative
> > > lock-release orderings simply add more fine-grained cumul-fence
> > > edges to substitute a single strong-fence edge provided by a long
> > > lock handover sequence
> > > 3) mb/strong-fence/pb and various similar uses in the definition of
> > > data races, where as discussed above any long handover sequence
> > > can be turned into a sequence of cumul-fence edges that provide
> > > the same ordering.
> > >
> > > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> > > ---
> >
> > Reviewed-by: Alan Stern <stern@rowland.harvard.edu>
>
> A quick spot check showed no change in performance, so thank you both!
>
> Queued for review and further testing.

And testing on https://github.com/paulmckrcu/litmus for litmus tests up
to ten processes and allowing 10 minutes per litmus test got this:

Exact output matches: 5208
!!! Timed out: 38
!!! Unknown primitive: 7

This test compared output with and without your patch.

For the tests with a Results clause, these failed:

manual/kernel/C-srcu-nest-7.litmus
manual/kernel/C-srcu-nest-5.litmus
manual/kernel/C-srcu-nest-6.litmus
manual/kernel/C-srcu-nest-8.litmus

But all of these will continue to fail until we get Alan's new-age SRCU
patch applied.

Therefore, this constitutes success, so good show thus far on testing! ;-)

Also, I am going to be pushing the scripts I use to mainline. They might
not be perfect, but they will be quite useful for this sort of change
to the memory model.

Thanx, Paul