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

[Alan Stern]

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@xxxxxxxxxxxxxxx/
> + *)
> +
> +{
> +	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!

> +	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)

Alan