linux-kernel - Re: [RFC] tools/memory-model: Rule out OOTA

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]

Message-ID: <c47d74ef-5eb9-4994-8b73-fbb6eb6bfa8e@paulmck-laptop>
Date: Tue, 29 Jul 2025 13:34:24 -0700
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
	stern@...land.harvard.edu, 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, lkmm@...ts.linux.dev
Subject: Re: [RFC] tools/memory-model: Rule out OOTA

On Fri, Jul 25, 2025 at 07:23:23AM +0200, Hernan Ponce de Leon wrote:
> On 7/24/2025 4:14 PM, Paul E. McKenney wrote:
> > On Wed, Jul 23, 2025 at 09:39:05AM -0700, Paul E. McKenney wrote:
> > > On Wed, Jul 23, 2025 at 09:26:32AM +0200, Hernan Ponce de Leon wrote:
> > > > On 7/23/2025 2:43 AM, Paul E. McKenney wrote:
> > > > > On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote:
> > > > > > The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following
> > > > > > example shared on this list a few years ago:
> > > > > 
> > > > > Apologies for being slow, but I have finally added the litmus tests in
> > > > > this email thread to the https://github.com/paulmckrcu/litmus repo.
> > > > 
> > > > I do not understand some of the comments in the preamble of the tests:
> > > > 
> > > > (*
> > > >   * Result: Never
> > > >   *
> > > >   * But Sometimes in LKMM as of early 2025, given that 42 is a possible
> > > >   * value for things like S19..
> > > >   *
> > > >   * https://lore.kernel.org/all/20250106214003.504664-1-jonas.oberhauser@huaweicloud.com/
> > > >   *)
> > > > 
> > > > I see that herd7 reports one of the states to be [b]=S16. Is this supposed
> > > > to be some kind of symbolic state (i.e., any value is possible)?
> > > 
> > > Exactly!
> > > 
> > > > The value in the "Result" is what we would like the model to say if we would
> > > > have a perfect version of dependencies, right?
> > > 
> > > In this case, yes.
> > 
> > I should hasten to add that, compiler optimizations being what they are,
> > "perfect" may or may not be attainable, and even if attainable, might
> > not be maintainable.
> 
> Yes, I just wanted to clarify if this is what herd7 + the current model are
> saying or what developers should expect.

Good point, and I added explicit words to this effect in the comments
of those aspirational OOTA litmus tests, so thank you!

							Thanx, Paul

> Hernan
> 
> > 
> > I am pretty sure that you all already understood that, but I felt the
> > need to make it explicit.  ;-)
> > 
> > 							Thanx, Paul
>