Received-SPF: pass (google.com: domain of linux-kernel+bounces-182347-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.199.223 as permitted sender) client-ip=147.75.199.223;
Date: Fri, 17 May 2024 18:27:12 +0200
From: Andrea Parri <parri.andrea@gmail.com>
To: Frederic Weisbecker <frederic@kernel.org>
Cc: Valentin Schneider <vschneid@redhat.com>,
	LKML <linux-kernel@vger.kernel.org>,
	"Paul E . McKenney" <paulmck@kernel.org>,
	Boqun Feng <boqun.feng@gmail.com>,
	Joel Fernandes <joel@joelfernandes.org>,
	Neeraj Upadhyay <neeraj.upadhyay@amd.com>,
	Uladzislau Rezki <urezki@gmail.com>,
	Zqiang <qiang.zhang1211@gmail.com>, rcu <rcu@vger.kernel.org>
Subject: Re: [PATCH 2/6] rcu: Remove superfluous full memory barrier upon
 first EQS snapshot
Message-ID: <ZkeFYJ1saaMWPUON@andrea>
References: <20240515125332.9306-1-frederic@kernel.org>
 <20240515125332.9306-3-frederic@kernel.org>
 <xhsmhfruhhixv.mognet@vschneid-thinkpadt14sgen2i.remote.csb>
 <ZkYvemdrEOVFNtVu@lothringen>
 <xhsmha5kphefq.mognet@vschneid-thinkpadt14sgen2i.remote.csb>
 <ZkcHSnvn0TZX6YzV@andrea>
 <ZkdCG28qNha2vUSo@localhost.localdomain>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <ZkdCG28qNha2vUSo@localhost.localdomain>

> Z6.0+pooncelock+poonceLock+pombonce.litmus shows an example of
> how full ordering is subtely incomplete without smp_mb__after_spinlock().
> 
> But still, smp_mb__after_unlock_lock() is supposed to be weaker than
> smp_mb__after_spinlock() and yet I'm failing to produce a litmus test
> that is successfull with the latter and fails with the former.

smp_mb__after_unlock_lock() is a nop without a matching unlock-lock;
smp_mb__after_spinlock() not quite...

C after_spinlock__vs__after_unlock_lock

{ }

P0(int *x, int *y, spinlock_t *s)
{
	int r0;

	WRITE_ONCE(*x, 1);
	spin_lock(s);
	smp_mb__after_spinlock();
	r0 = READ_ONCE(*y);
	spin_unlock(s);
}

P1(int *x, int *y)
{
	int r1;

	WRITE_ONCE(*y, 1);
	smp_mb();
	r1 = READ_ONCE(*x);
}

exists (0:r0=0 /\ 1:r1=0)


> For example, and assuming smp_mb__after_unlock_lock() is expected to be
> chained across locking, here is a litmus test inspired by
> Z6.0+pooncelock+poonceLock+pombonce.litmus that never observes the condition
> even though I would expect it should, as opposed to using
> smp_mb__after_spinlock():
> 
> C smp_mb__after_unlock_lock
> 
> {}
> 
> P0(int *w, int *x, spinlock_t *mylock)
> {
> 	spin_lock(mylock);
> 	WRITE_ONCE(*w, 1);
> 	WRITE_ONCE(*x, 1);
> 	spin_unlock(mylock);
> }
> 
> P1(int *x, int *y, spinlock_t *mylock)
> {
> 	int r0;
> 
> 	spin_lock(mylock);
> 	smp_mb__after_unlock_lock();
> 	r0 = READ_ONCE(*x);
> 	WRITE_ONCE(*y, 1);
> 	spin_unlock(mylock);
> }
> 
> P2(int *y, int *z, spinlock_t *mylock)
> {
> 	int r0;
> 
> 	spin_lock(mylock);
> 	r0 = READ_ONCE(*y);
> 	WRITE_ONCE(*z, 1);
> 	spin_unlock(mylock);
> }
> 
> P3(int *w, int *z)
> {
> 	int r1;
> 
> 	WRITE_ONCE(*z, 2);
> 	smp_mb();
> 	r1 = READ_ONCE(*w);
> }
> 
> exists (1:r0=1 /\ 2:r0=1 /\ z=2 /\ 3:r1=0)

Here's an informal argument to explain this outcome.  It is not the only
according to the LKMM, but the first that came to my mind.  And this is
longer than I wished.  TL; DR:  Full barriers are strong, really strong.

Remark full memory barriers share the following "strong-fence property":

  A ->full-barrier B

implies

  (SFP) A propagates (aka, is visible) to _every CPU before B executes

(cf. tools/memory-model/Documentation/explanation.txt for details about
the concepts of "propagation" and "execution").

For example, in the snippet above,

  P0:WRITE_ONCE(*w, 1) ->full-barrier P1:spin_unlock(mylock)

since

  P0:spin_unlock(mylock) ->reads-from P1:spin_lock(mylock) ->program-order P1:smp_mb__after_unlock_lock()

acts as a full memory barrier.   (1:r0=1 and 2:r0=1 together determine
the so called critical-sections' order (CSO).)

By contradiction,

  1) P0:WRITE_ONCE(*w, 1) propagates to P3 before P1:spin_unlock(mylock) executes   (SFP)

  2) P1:spin_unlock(mylock) executes before P2:spin_lock(mylock) executes   (CSO)

  3) P2:spin_lock(mylock) executes before P2:WRITE_ONCE(*z, 1) executes  (P2:spin_lock() is an ACQUIRE op)

  4) P2:WRITE_ONCE(*z, 1) executes before P2:WRITE_ONCE(*z, 1) propagates P3  (intuitively, a store is visible to the local CPU before being visible to a remote CPU)

  5) P2:WRITE_ONCE(*z, 1) propagates to P3 before P3:WRITE_ONCE(*z, 2) executes   (z=2)

  6) P3:WRITE_ONCE(*z, 2) executes before P3:WRITE_ONCE(*z, 2) propagates to P0    (a store is visible to the local CPU before being visible to a remote CPU)

  7) P3:WRITE_ONCE(*z, 2) propagates to P0 before P3:READ_ONCE(*w) executes   (SFP)

  8) P3:READ_ONCE(*w) executes before P0:WRITE_ONCE(*w, 1) propagates to P3   (3:r1=0)

Put together, (1-8) gives:

  P0:WRITE_ONCE(*w, 1) propagates to P3 before P0:WRITE_ONCE(*w, 1) propagates to P3

an absurd.

  Andrea