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

Message-ID: <5470d186-7c75-4ead-81de-71f9d6b4c58f@paulmck-laptop>
Date: Wed, 23 Jul 2025 10:27:49 -0700
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
	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,
	hernan.poncedeleon@...weicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA

On Wed, Jul 23, 2025 at 01:13:35PM -0400, Alan Stern wrote:
> On Tue, Jul 22, 2025 at 05:43:16PM -0700, 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.
> > 
> > It is quite likely that I have incorrectly intuited the missing portions
> > of the litmus tests, especially the two called out in the commit log
> > below.  If you have time, please do double-check.
> 
> I didn't look very closely when this first came out...
> 
> > --- /dev/null
> > +++ b/manual/oota/C-AS-OOTA-2.litmus
> > @@ -0,0 +1,33 @@
> > +C C-AS-OOTA-2
> > +
> > +(*
> > + * Result: Always
> > + *
> > + * If we were using C-language relaxed atomics instead of volatiles,
> > + * the compiler *could* eliminate the first WRITE_ONCE() in each process,
> > + * then also each process's local variable, thus having an undefined value
> > + * for each of those local variables.  But this cannot happen given that
> > + * we are using Linux-kernel _ONCE() primitives.
> > + *
> > + * https://lore.kernel.org/all/c2ae9bca-8526-425e-b9b5-135004ad59ad@rowland.harvard.edu/
> > + *)
> > +
> > +{}
> > +
> > +P0(int *a, int *b)
> > +{
> > +	int r0 = READ_ONCE(*a);
> > +
> > +	WRITE_ONCE(*b, r0);
> > +	WRITE_ONCE(*b, 2);
> > +}
> > +
> > +P1(int *a, int *b)
> > +{
> > +	int r1 = READ_ONCE(*b);
> > +
> > +	WRITE_ONCE(*a, r0);
> 
> This should be r1 instead of r0.

Ah, good eyes, thank you!

With that change, I still get "Always" as shown below.  Which I believe
makes sense, given that LKMM deals with volatile atomics in contrast to
the C++ relaxed atomics that you were discussing in the email.

Please let me know if I am still missing something.

> > +	WRITE_ONCE(*a, 2);
> > +}
> > +
> > +exists ((0:r0=0 \/ 0:r0=2) /\ (1:r1=0 \/ 1:r1=2))
> 
> Alan

------------------------------------------------------------------------

$ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/oota/C-AS-OOTA-2.litmus
Test C-AS-OOTA-2 Allowed
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=2;
0:r0=2; 1:r1=0;
Ok
Witnesses
Positive: 5 Negative: 0
Condition exists ((0:r0=0 \/ 0:r0=2) /\ (1:r1=0 \/ 1:r1=2))
Observation C-AS-OOTA-2 Always 5 0
Time C-AS-OOTA-2 0.01
Hash=7b4c046bc861c102997a87e32907fa80