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 for Android: free password hash cracker in your pocket

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <b9c250b2-e4c0-4e8f-b37c-b51d93b980f0@rowland.harvard.edu>
Date: Wed, 23 Jul 2025 15:25:13 -0400
From: Alan Stern <stern@...land.harvard.edu>
To: "Paul E. McKenney" <paulmck@...nel.org>
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 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!

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