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: <9963f6a6-9da9-4120-b1fe-e4a1df9edda1@paulmck-laptop>
Date: Wed, 23 Jul 2025 12:57:13 -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 03:25:13PM -0400, Alan Stern wrote:
> On Tue, Jul 22, 2025 at 05:43:16PM -0700, Paul E. McKenney wrote:
> >     Also, C-JO-OOTA-7.litmus includes a "*r2 = a" statement that makes herd7
> >     very unhappy.  On the other hand, initializing registers to the address
> >     of a variable is straight forward, as shown in the resulting litmus test.
> 
> ...
> 
> > diff --git a/manual/oota/C-JO-OOTA-7.litmus b/manual/oota/C-JO-OOTA-7.litmus
> > new file mode 100644
> > index 00000000..31c0b8ae
> > --- /dev/null
> > +++ b/manual/oota/C-JO-OOTA-7.litmus
> > @@ -0,0 +1,47 @@
> > +C C-JO-OOTA-7
> > +
> > +(*
> > + * Result: Never
> > + *
> > + * But LKMM finds the all-ones result, due to OOTA on r2.
> > + *
> > + * https://lore.kernel.org/all/1147ad3e-e3ad-4fa1-9a63-772ba136ea9a@huaweicloud.com/
> > + *)
> > +
> > +{
> > +	0:r2=a;
> > +	1:r2=b;
> > +}
> 
> In this litmus test a and b are never assigned any values, so they
> always contain 0.
> 
> > +
> > +P0(int *a, int *b, int *x, int *y)
> > +{
> > +	int r1;
> > +	int r2;
> > +
> > +	r1 = READ_ONCE(*x);
> > +	smp_rmb();
> > +	if (r1 == 1) {
> > +		r2 = READ_ONCE(*a);
> 
> If this executes then r2 now contains 0.
> 
> > +	}
> > +	*r2 = a;
> 
> And so what is supposed to happen here?  No wonder herd7 is unhappy!

Nothing good, I will admit!  Good eyes, and thank you!

> > +	smp_wmb();
> > +	WRITE_ONCE(*y, 1);
> > +}
> > +
> > +P1(int *a, int *b, int *x, int *y)
> > +{
> > +	int r1;
> > +	int r2;
> > +
> > +	r1 = READ_ONCE(*y);
> > +	smp_rmb();
> > +	if (r1 == 1) {
> > +		r2 = READ_ONCE(*b);
> > +	}
> > +	*r2 = b;
> 
> Same here.
> 
> > +	smp_wmb();
> > +	WRITE_ONCE(*x, 1);
> > +}
> > +
> > +locations [0:r2;1:r2]
> > +exists (0:r1=1 /\ 1:r1=1)

Yes, I did misinterpret Jonas's initialization advice, which reads
as follows:  "unless you know how to initialize *a and *b to valid
addresses, you may need to add something like `if (r2 == 0) r2 = a`
to run this in herd7".

Given that there are two instances of r2, there are a number of
possible combinations of initialization.  I picked the one shown
in the patch below, and got this:

$ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/oota/C-JO-OOTA-7.litmus
Test C-JO-OOTA-7 Allowed
States 3
0:r1=0; 0:r2=a; 1:r1=0; 1:r2=b;
0:r1=0; 0:r2=a; 1:r1=1; 1:r2=b;
0:r1=1; 0:r2=a; 1:r1=0; 1:r2=b;
No
Witnesses
Positive: 0 Negative: 3
Flag mixed-accesses
Condition exists (0:r1=1 /\ 1:r1=1)
Observation C-JO-OOTA-7 Never 0 3
Time C-JO-OOTA-7 0.01
Hash=d9bb35335e45b31b1a39bab88eca837c

I get something very similar if I cross-initialize them, that is
a=b;b=a.

Thoughts?

							Thanx, Paul

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

diff --git a/manual/oota/C-JO-OOTA-7.litmus b/manual/oota/C-JO-OOTA-7.litmus
index 31c0b8ae..d7fe0f94 100644
--- a/manual/oota/C-JO-OOTA-7.litmus
+++ b/manual/oota/C-JO-OOTA-7.litmus
@@ -11,6 +11,8 @@ C C-JO-OOTA-7
 {
 	0:r2=a;
 	1:r2=b;
+	a=a;
+	b=b;
 }
 
 P0(int *a, int *b, int *x, int *y)