linux-kernel - Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

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:   Tue, 24 Jan 2023 17:35:33 -0500
From:   Alan Stern <stern@...land.harvard.edu>
To:     "Paul E. McKenney" <paulmck@...nel.org>
Cc:     Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
        Andrea Parri <parri.andrea@...il.com>,
        Jonas Oberhauser <jonas.oberhauser@...wei.com>,
        Peter Zijlstra <peterz@...radead.org>, will <will@...nel.org>,
        "boqun.feng" <boqun.feng@...il.com>, npiggin <npiggin@...il.com>,
        dhowells <dhowells@...hat.com>,
        "j.alglave" <j.alglave@....ac.uk>,
        "luc.maranget" <luc.maranget@...ia.fr>, akiyks <akiyks@...il.com>,
        dlustig <dlustig@...dia.com>, joel <joel@...lfernandes.org>,
        urezki <urezki@...il.com>,
        quic_neeraju <quic_neeraju@...cinc.com>,
        frederic <frederic@...nel.org>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus
 test)

On Tue, Jan 24, 2023 at 02:15:24PM -0800, Paul E. McKenney wrote:
> > Ah, looking at the model now. Indeed it's forbidden, because in order to say
> > that something is in co, there must not be a (resulting) cycle of co and
> > barriers. But you'd get that here.  In the axiomatic model, this corresponds
> > to saying Power's "prop | co" is acyclic. The same isn't true in LKMM. So
> > that's probably why.
> 
> Which means that the RCU and SRCU implementations need to make (admittedly
> small) guarantees that cannot be expressed in LKMM.  Which is in fact
> what I was remembering, so I feel better now.
> 
> Not sure about the rest of you, though.  ;-)

Can you be more explicit?  Exactly what guarantees does the kernel 
implementation make that can't be expressed in LKMM?

And are these anything the memory model needs to worry about?

Alan