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/[email protected]/
> > + *)
> > +
> > +{
> > +	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)