Re: [PATCH] tools/memory-model: Make ppo a subrelation of po

From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: paulmck@kernel.org, parri.andrea@gmail.com, will@kernel.org,
	peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
	dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
	akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
	urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
	linux-kernel@vger.kernel.org, viktor@mpi-sws.org
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po
Date: Mon, 23 Jan 2023 15:25:00 -0500	[thread overview]
Message-ID: <Y87tHNcvb5E+t3da@rowland.harvard.edu> (raw)
In-Reply-To: <1180fe22-5e1d-ec8b-8012-b6578b1ca7c0@huaweicloud.com>

On Mon, Jan 23, 2023 at 07:25:48PM +0100, Jonas Oberhauser wrote:
> Alright, after some synchronization in the other parts of this thread I am
> beginning to prepare the next iteration of the patch.
> 
> On 1/19/2023 4:13 AM, Alan Stern wrote:
> > On Wed, Jan 18, 2023 at 10:38:11PM +0100, Jonas Oberhauser wrote:
> > > 
> > > On 1/18/2023 8:52 PM, Alan Stern wrote:
> > > > On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote:
> > > > > -	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> > > > > -	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> > > > > -		fencerel(After-unlock-lock) ; [M])
> > > > > +	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
> > > > Shouldn't the po case of (co | po) remain intact here?
> > > You can leave it here, but it is already covered by two other parts: the
> > > ordering given through ppo/hb is covered by the po-unlock-lock-po & int in
> > > ppo, and the ordering given through pb is covered by its inclusion in
> > > strong-order.
> > What about the ordering given through
> > A-cumul(strong-fence)/cumul-fence/prop/hb?  I suppose that might be
> > superseded by pb as well, but it seems odd not to have it in hb.
> 
> How should we resolve this?
> My current favorite (compromise :D) solution would be to
> 1. still eliminate both po and co cases from first definition of
> strong-fence which is used in ppo,
> 2. define a relation equal to the strong-order in this patch (with po|rf)

Wouldn't it need to have po|co?  Consider:

	Wx=1	Rx=1		Ry=1		Rz=1
		lock(s)		lock(s)		lock(s)
		unlock(s)	unlock(s)	unlock(s)
		Wy=1		Wz=1		smp_mb__after_unlock_lock
						Rx=0

With the co term this is forbidden.  With only the rf term it is 
allowed, because po-unlock-lock-po isn't A-cumulative.

> but call it strong-fence for now (in response to Andrea's valid criticism
> that this patch is doing maybe more than just fix ppo)
> 3. use the extended strong-fence in the definition of cumul-fence and pb
> 
> So I'd still simplify po|co to po|rf and drop the po case from ppo, but
> return both of those cases in cumul-fence, to be consistent with the idea
> that cumul-fence should deal with the weak properties of the fences
> including this after-unlock-lock fence.
> 
> 
> Would that be acceptable?

Subject to the point mentioned above, yes.

Alan