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
| ||
|
Message-ID: <Y9CL8LBz+/mbbD00@rowland.harvard.edu> Date: Tue, 24 Jan 2023 20:54:56 -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:54:49PM -0800, Paul E. McKenney wrote: > On Tue, Jan 24, 2023 at 05:35:33PM -0500, Alan Stern wrote: > > Can you be more explicit? Exactly what guarantees does the kernel > > implementation make that can't be expressed in LKMM? > > I doubt that I will be able to articulate it very well, but here goes. > > Within the Linux kernel, the rule for a given RCU "domain" is that if > an event follows a grace period in pretty much any sense of the word, > then that event sees the effects of all events in all read-side critical > sections that began prior to the start of that grace period. > > Here the senses of the word "follow" include combinations of rf, fr, > and co, combined with the various acyclic and irreflexive relations > defined in LKMM. The LKMM says pretty much the same thing. In fact, it says the event sees the effects of all events po-before the unlock of (not just inside) any read-side critical section that began prior to the start of the grace period. > > And are these anything the memory model needs to worry about? > > Given that several people, yourself included, are starting to use LKMM > to analyze the Linux-kernel RCU implementations, maybe it does. > > Me, I am happy either way. Judging from your description, I don't think we have anything to worry about. Alan
Powered by blists - more mailing lists