linux-kernel - Re: [PATCH v2 2/2] 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]

Date:   Sun, 29 Jan 2023 17:10:49 -0500
From:   Alan Stern <stern@...land.harvard.edu>
To:     Andrea Parri <parri.andrea@...il.com>
Cc:     Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
        paulmck@...nel.org, 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
Subject: Re: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po

On Sun, Jan 29, 2023 at 06:11:12PM +0100, Andrea Parri wrote:
> > The reason why Wx=1 ->ww-vis Wx=2:
> > 
> > 	0:Wx=1 ->po-rel 0:Wy=1 and po-rel < fence < ww-post-bounded.
> > 
> > 	0:Wy=1 ->rfe 1:Ry=1 ->(hb* & int) 1:Rdy=1 and
> > 		(rfe ; hb* & int) <= (rfe ; xbstar & int) <= vis.
> > 
> > 	1:Rdy=1 ->po 1:unlock ->rfe 3:lock ->po 3:Wx=2
> > 		so 1:Rdy=1 ->po-unlock-lock-po 3:Wx=2
> > 		and po-unlock-lock-po <= mb <= fence <= w-pre-bounded.
> > 
> > Finally, w-post-bounded ; vis ; w-pre-bounded <= ww-vis.
> 
> To clarify, po-unlock-lock-po is not a subrelation of mb; see what
> happens without the smp_mb__after_unlock_lock().

Ah, thank you again.  That was what I got wrong, and it explains why the 
data race appears with Jonas's patch.

This also points out an important unstated fact: All of the inter-CPU 
extended fences in the memory model are A-cumulative.  In this case the 
fence links Rdy=1 on P1 to Wx=3 on P3.  We know that 0:Wx=1 is visible 
to P1 before the Rdy executes, but what we need is that it is visible to 
P3 before Wx=3 executes.  The fact that the extended fence is strong 
(and therefore A-cumulative) provides this extra guarantee.

Alan