| 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
| ||
|
Message-ID: <3e98c47c-d354-431f-851f-494df9e6bc78@huaweicloud.com>
Date: Wed, 23 Jul 2025 09:26:32 +0200
From: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
To: paulmck@...nel.org, Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: stern@...land.harvard.edu, 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
Subject: Re: [RFC] tools/memory-model: Rule out OOTA
On 7/23/2025 2:43 AM, 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.
I do not understand some of the comments in the preamble of the tests:
(*
* Result: Never
*
* But Sometimes in LKMM as of early 2025, given that 42 is a possible
* value for things like S19..
*
*
https://lore.kernel.org/all/20250106214003.504664-1-jonas.oberhauser@huaweicloud.com/
*)
I see that herd7 reports one of the states to be [b]=S16. Is this
supposed to be some kind of symbolic state (i.e., any value is possible)?
The value in the "Result" is what we would like the model to say if we
would have a perfect version of dependencies, right?
>
> 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 read the "On the other hand" from the commit log as "this fixes the
problem". However I still get the following error when running
C-JO-OOTA-7 with herd7
Warning: File "manual/oota/C-JO-OOTA-7.litmus": Non-symbolic memory
access found on '[0]' (User error)
Hernan>
> And the updated (and condensed!) version of the C++ OOTA paper may be
> found here, this time with a proposed change to the standard:
>
> https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2025/p3692r1.pdf
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit fd17e8fceb75326e159ba3aa6fdb344f74f5c7a5
> Author: Paul E. McKenney <paulmck@...nel.org>
> Date: Tue Jul 22 17:21:19 2025 -0700
>
> manual/oota: Add Jonas and Alan OOTA examples
>
> Each of these new litmus tests contains the URL of the email message
> that I took it from.
>
> Please note that I had to tweak the example leading up to
> C-JO-OOTA-4.litmus, and I might well have misinterpreted Jonas's "~"
> operator.
>
> 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.
>
> Signed-off-by: Paul E. McKenney <paulmck@...nel.org>
>
> diff --git a/manual/oota/C-AS-OOTA-1.litmus b/manual/oota/C-AS-OOTA-1.litmus
> new file mode 100644
> index 00000000..81a873a7
> --- /dev/null
> +++ b/manual/oota/C-AS-OOTA-1.litmus
> @@ -0,0 +1,40 @@
> +C C-AS-OOTA-1
> +
> +(*
> + * Result: Sometimes
> + *
> + * Because smp_rmb() combined with smp_wmb() does not order earlier
> + * reads against later writes.
> + *
> + * https://lore.kernel.org/all/a3bf910f-509a-4ad3-a1cc-4b14ef9b3259@rowland.harvard.edu
> + *)
> +
> +{}
> +
> +P0(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> +
> + r1 = READ_ONCE(*x);
> + smp_rmb();
> + if (r1 == 1) {
> + *a = *b;
> + }
> + smp_wmb();
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> +
> + r1 = READ_ONCE(*y);
> + smp_rmb();
> + if (r1 == 1) {
> + *b = *a;
> + }
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists (0:r1=1 /\ 1:r1=1)
> diff --git a/manual/oota/C-AS-OOTA-2.litmus b/manual/oota/C-AS-OOTA-2.litmus
> new file mode 100644
> index 00000000..c672b0e7
> --- /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);
> + WRITE_ONCE(*a, 2);
> +}
> +
> +exists ((0:r0=0 \/ 0:r0=2) /\ (1:r1=0 \/ 1:r1=2))
> diff --git a/manual/oota/C-JO-OOTA-1.litmus b/manual/oota/C-JO-OOTA-1.litmus
> new file mode 100644
> index 00000000..6ab437b4
> --- /dev/null
> +++ b/manual/oota/C-JO-OOTA-1.litmus
> @@ -0,0 +1,40 @@
> +C C-JO-OOTA-1
> +
> +(*
> + * Result: Never
> + *
> + * But Sometimes in LKMM as of early 2025, given that 42 is a possible
> + * value for things like S19..
> + *
> + * https://lore.kernel.org/all/20250106214003.504664-1-jonas.oberhauser@huaweicloud.com/
> + *)
> +
> +{}
> +
> +P0(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> +
> + r1 = READ_ONCE(*x);
> + smp_rmb();
> + if (r1 == 1) {
> + *a = *b;
> + }
> + smp_wmb();
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> +
> + r1 = READ_ONCE(*y);
> + smp_rmb();
> + if (r1 == 1) {
> + *b = *a;
> + }
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists (b=42)
> diff --git a/manual/oota/C-JO-OOTA-2.litmus b/manual/oota/C-JO-OOTA-2.litmus
> new file mode 100644
> index 00000000..ad708c60
> --- /dev/null
> +++ b/manual/oota/C-JO-OOTA-2.litmus
> @@ -0,0 +1,44 @@
> +C C-JO-OOTA-2
> +
> +(*
> + * Result: Never
> + *
> + * But Sometimes in LKMM as of early 2025, given that 42 is a possible
> + * value for things like S23.
> + *
> + * https://lore.kernel.org/all/1daba0ea-0dd6-4e67-923e-fd3c1a62b40b@huaweicloud.com/
> + *)
> +
> +{}
> +
> +P0(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> + int r2 = 0;
> +
> + r1 = READ_ONCE(*x);
> + smp_rmb();
> + if (r1 == 1) {
> + r2 = *b;
> + }
> + WRITE_ONCE(*a, r2);
> + smp_wmb();
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> + int r2 = 0;
> +
> + r1 = READ_ONCE(*y);
> + smp_rmb();
> + if (r1 == 1) {
> + r2 = *a;
> + }
> + WRITE_ONCE(*b, r2);
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists (b=42)
> diff --git a/manual/oota/C-JO-OOTA-3.litmus b/manual/oota/C-JO-OOTA-3.litmus
> new file mode 100644
> index 00000000..633b8334
> --- /dev/null
> +++ b/manual/oota/C-JO-OOTA-3.litmus
> @@ -0,0 +1,46 @@
> +C C-JO-OOTA-3
> +
> +(*
> + * Result: Never
> + *
> + * But LKMM finds the all-ones result, perhaps due to not tracking
> + * control dependencies out of the "if" statement.
> + *
> + * https://lore.kernel.org/all/1daba0ea-0dd6-4e67-923e-fd3c1a62b40b@huaweicloud.com/
> + *)
> +
> +{}
> +
> +P0(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> + int r2;
> +
> + r1 = READ_ONCE(*x);
> + smp_rmb();
> + r2 = READ_ONCE(*b);
> + if (r1 == 1) {
> + r2 = *b;
> + }
> + WRITE_ONCE(*a, r2);
> + 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();
> + r2 = READ_ONCE(*a);
> + if (r1 == 1) {
> + r2 = *a;
> + }
> + WRITE_ONCE(*b, r2);
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists (0:r1=1 /\ 1:r1=1)
> diff --git a/manual/oota/C-JO-OOTA-4.litmus b/manual/oota/C-JO-OOTA-4.litmus
> new file mode 100644
> index 00000000..cab7ebb6
> --- /dev/null
> +++ b/manual/oota/C-JO-OOTA-4.litmus
> @@ -0,0 +1,43 @@
> +C C-JO-OOTA-4
> +
> +(*
> + * Result: Never
> + *
> + * And LKMM agrees, which might be a surprise.
> + *
> + * https://lore.kernel.org/all/1daba0ea-0dd6-4e67-923e-fd3c1a62b40b@huaweicloud.com/
> + *)
> +
> +{}
> +
> +P0(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> + int r2;
> + int r3;
> +
> + r1 = READ_ONCE(*x);
> + smp_rmb();
> + r2 = *b;
> + r3 = r1 == 0;
> + WRITE_ONCE(*a, (r3 + 1) & r2);
> + smp_wmb();
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *a, int *b, int *x, int *y)
> +{
> + int r1;
> + int r2;
> + int r3;
> +
> + r1 = READ_ONCE(*y);
> + smp_rmb();
> + r2 = *a;
> + r3 = r1 == 0;
> + WRITE_ONCE(*b, (r3 + 1) & r2);
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists (0:r1=1 /\ 1:r1=1)
> diff --git a/manual/oota/C-JO-OOTA-5.litmus b/manual/oota/C-JO-OOTA-5.litmus
> new file mode 100644
> index 00000000..145c8378
> --- /dev/null
> +++ b/manual/oota/C-JO-OOTA-5.litmus
> @@ -0,0 +1,44 @@
> +C C-JO-OOTA-5
> +
> +(*
> + * Result: Never
> + *
> + * But LKMM finds the all-ones result, perhaps due r2 being unused.
> + *
> + * https://lore.kernel.org/all/1daba0ea-0dd6-4e67-923e-fd3c1a62b40b@huaweicloud.com/
> + *)
> +
> +{}
> +
> +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);
> + }
> + *b = 1;
> + 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);
> + }
> + *a = 1;
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +locations [0:r2;1:r2]
> +exists (0:r1=1 /\ 1:r1=1)
> diff --git a/manual/oota/C-JO-OOTA-6.litmus b/manual/oota/C-JO-OOTA-6.litmus
> new file mode 100644
> index 00000000..942e6c82
> --- /dev/null
> +++ b/manual/oota/C-JO-OOTA-6.litmus
> @@ -0,0 +1,44 @@
> +C C-JO-OOTA-6
> +
> +(*
> + * 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/
> + *)
> +
> +{}
> +
> +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);
> + }
> + *b = r2;
> + 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);
> + }
> + *a = r2;
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +locations [0:r2;1:r2]
> +exists (0:r1=1 /\ 1:r1=1)
> 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;
> +}
> +
> +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);
> + }
> + *r2 = a;
> + 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;
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +locations [0:r2;1:r2]
> +exists (0:r1=1 /\ 1:r1=1)
> diff --git a/manual/oota/C-PM-OOTA-1.litmus b/manual/oota/C-PM-OOTA-1.litmus
> new file mode 100644
> index 00000000..e771e3c9
> --- /dev/null
> +++ b/manual/oota/C-PM-OOTA-1.litmus
> @@ -0,0 +1,37 @@
> +C C-PM-OOTA-1
> +
> +(*
> + * Result: Never
> + *
> + * LKMM agrees.
> + *
> + * https://lore.kernel.org/all/9a0dccbb-bfa7-4b33-ac1a-daa9841b609a@paulmck-laptop/
> + *)
> +
> +{}
> +
> +P0(int *a, int *b, int *x, int *y) {
> + int r1;
> +
> + r1 = READ_ONCE(*x);
> + smp_rmb();
> + if (r1 == 1) {
> + WRITE_ONCE(*a, *b);
> + }
> + smp_wmb();
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *a, int *b, int *x, int *y) {
> + int r1;
> +
> + r1 = READ_ONCE(*y);
> + smp_rmb();
> + if (r1 == 1) {
> + WRITE_ONCE(*b, *a);
> + }
> + smp_wmb();
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists b=42
Powered by blists - more mailing lists