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]
Date:   Mon, 23 Jan 2023 19:25:48 +0100
From:   Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To:     Alan Stern <stern@...land.harvard.edu>
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

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) 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?
jonas

Powered by blists - more mailing lists

Powered by Openwall GNU/*/Linux Powered by OpenVZ