linux-kernel - Re: [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency

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] [day] [month] [year] [list]

Date:   Fri, 3 Feb 2023 17:51:44 -0800
From:   "Paul E. McKenney" <paulmck@...nel.org>
To:     Alan Stern <stern@...land.harvard.edu>
Cc:     "Joel Fernandes (Google)" <joel@...lfernandes.org>,
        linux-kernel@...r.kernel.org, Akira Yokosawa <akiyks@...il.com>,
        Andrea Parri <parri.andrea@...il.com>,
        Boqun Feng <boqun.feng@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>, linux-arch@...r.kernel.org,
        Luc Maranget <luc.maranget@...ia.fr>,
        Nicholas Piggin <npiggin@...il.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will@...nel.org>
Subject: Re: [PATCH RFC] tools/memory-model: Restrict to-r to read-read
 address dependency

On Fri, Feb 03, 2023 at 08:29:53PM -0500, Alan Stern wrote:
> On Fri, Feb 03, 2023 at 08:19:13PM +0000, Joel Fernandes (Google) wrote:
> > During a code-reading exercise of linux-kernel.cat CAT file, I generated
> > a graph to show the to-r relations. While likely not problematic for the
> > model, I found it confusing that a read-write address dependency would
> > show as a to-r edge on the graph.
> > 
> > This patch therefore restricts the to-r links derived from addr to only
> > read-read address dependencies, so that read-write address dependencies don't
> > show as to-r in the graphs. This should also prevent future users of to-r from
> > deriving incorrect relations. Note that a read-write address dep, obviously,
> > still ends up in the ppo relation via the to-w relation.
> > 
> > I verified that a read-read address dependency still shows up as a to-r
> > link in the graph, as it did before.
> > 
> > For reference, the problematic graph was generated with the following
> > command:
> > herd7 -conf linux-kernel.cfg \
> >    -doshow dep -doshow to-r -doshow to-w ./foo.litmus -show all -o OUT/
> > 
> > Signed-off-by: Joel Fernandes (Google) <joel@...lfernandes.org>
> > ---
> >  tools/memory-model/linux-kernel.cat | 2 +-
> >  1 file changed, 1 insertion(+), 1 deletion(-)
> > 
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index d70315fddef6..26e6f0968143 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -69,7 +69,7 @@ let dep = addr | data
> >  let rwdep = (dep | ctrl) ; [W]
> >  let overwrite = co | fr
> >  let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
> > -let to-r = addr | (dep ; [Marked] ; rfi)
> > +let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi)
> >  let ppo = to-r | to-w | fence | (po-unlock-lock-po & int)
> >  
> >  (* Propagation: Ordering from release operations and strong fences. *)
> > -- 
> > 2.39.1.519.gcb327c4b5f-goog
> 
> Acked-by: Alan Stern <stern@...land.harvard.edu>

Thank you both, queued for v6.4.

							Thanx, Paul