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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <Y9ABZQ81oXTmggcY@rowland.harvard.edu>
Date:   Tue, 24 Jan 2023 11:03:49 -0500
From:   Alan Stern <stern@...land.harvard.edu>
To:     Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc:     paulmck@...nel.org, parri.andrea@...il.com, will@...nel.org,
        peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
        dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
        akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
        urezki@...il.com, quic_neeraju@...cinc.com, frederic@...nel.org,
        linux-kernel@...r.kernel.org, viktor@...-sws.org
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po

On Tue, Jan 24, 2023 at 01:54:14PM +0100, Jonas Oberhauser wrote:
> 
> 
> On 1/23/2023 9:25 PM, Alan Stern wrote:
> > 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.
> No, but unlock() is ( https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/tree/tools/memory-model/lock.cat?h=dev.2023.01.19a#n67
> ). So you get

So it is.  I had forgotten about that.  The model is getting too 
complicated to fit entirely in my mind...

>   Rx=0 ->overwrite Wx=1  ->rfe Rx1 ->po-rel  T1:unlock(s) ->rfe T2:lock(s)
> ->po-unlock-lock-po;after ... fence;po Rx=0
> which is
>   Rx=0          ->prop ;                           po-unlock-lock-po;after
> ... fence;po Rx=0
> 
> Are you ok going forward like this then?

I guess so, provided we mention somewhere in the code or documentation 
that this relation extends beyond a single rf.

Alan