From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
To: paulmck@kernel.org, Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: stern@rowland.harvard.edu, parri.andrea@gmail.com,
will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com,
npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com,
joel@joelfernandes.org, urezki@gmail.com,
quic_neeraju@quicinc.com, frederic@kernel.org,
linux-kernel@vger.kernel.org, lkmm@lists.linux.dev
Subject: Re: [RFC] tools/memory-model: Rule out OOTA
Date: Wed, 23 Jul 2025 09:26:32 +0200 [thread overview]
Message-ID: <3e98c47c-d354-431f-851f-494df9e6bc78@huaweicloud.com> (raw)
In-Reply-To: <6fb01aea-f7b4-4f38-82b9-fd6c360514fc@paulmck-laptop>
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@kernel.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@kernel.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
next prev parent reply other threads:[~2025-07-23 7:43 UTC|newest]
Thread overview: 59+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-01-06 21:40 [RFC] tools/memory-model: Rule out OOTA Jonas Oberhauser
2025-01-07 10:06 ` Peter Zijlstra
2025-01-07 11:02 ` Jonas Oberhauser
2025-01-07 15:46 ` Jonas Oberhauser
2025-01-07 16:09 ` Alan Stern
2025-01-07 18:47 ` Paul E. McKenney
2025-01-08 17:39 ` Jonas Oberhauser
2025-01-08 18:09 ` Paul E. McKenney
2025-01-08 19:17 ` Jonas Oberhauser
2025-01-09 17:54 ` Paul E. McKenney
2025-01-09 18:35 ` Jonas Oberhauser
2025-01-10 14:54 ` Paul E. McKenney
2025-01-10 16:21 ` Jonas Oberhauser
2025-01-13 22:04 ` Paul E. McKenney
2025-01-16 18:40 ` Paul E. McKenney
2025-01-16 19:13 ` Jonas Oberhauser
2025-01-16 19:31 ` Paul E. McKenney
2025-01-16 20:21 ` Jonas Oberhauser
2025-01-16 19:28 ` Jonas Oberhauser
2025-01-16 19:39 ` Paul E. McKenney
2025-01-17 12:08 ` Jonas Oberhauser
2025-01-16 19:08 ` Jonas Oberhauser
2025-01-16 23:02 ` Alan Stern
2025-01-17 8:34 ` Hernan Ponce de Leon
2025-01-17 11:29 ` Jonas Oberhauser
2025-01-17 20:01 ` Alan Stern
2025-01-21 10:36 ` Jonas Oberhauser
2025-01-21 16:39 ` Alan Stern
2025-01-22 3:46 ` Jonas Oberhauser
2025-01-22 19:11 ` Alan Stern
2025-01-17 15:52 ` Alan Stern
2025-01-17 16:45 ` Jonas Oberhauser
2025-01-17 19:02 ` Alan Stern
2025-01-09 20:37 ` Peter Zijlstra
2025-01-09 21:13 ` Paul E. McKenney
2025-01-08 17:33 ` Jonas Oberhauser
2025-01-08 18:47 ` Alan Stern
2025-01-08 19:22 ` Jonas Oberhauser
2025-01-09 16:17 ` Alan Stern
2025-01-09 16:44 ` Jonas Oberhauser
2025-01-09 19:27 ` Alan Stern
2025-01-09 20:09 ` Jonas Oberhauser
2025-01-10 3:12 ` Alan Stern
2025-01-10 12:21 ` Jonas Oberhauser
2025-01-10 21:51 ` Alan Stern
2025-01-11 12:46 ` Jonas Oberhauser
2025-01-11 21:19 ` Alan Stern
2025-01-12 15:55 ` Jonas Oberhauser
2025-01-13 19:43 ` Alan Stern
2025-07-23 0:43 ` Paul E. McKenney
2025-07-23 7:26 ` Hernan Ponce de Leon [this message]
2025-07-23 16:39 ` Paul E. McKenney
2025-07-24 14:14 ` Paul E. McKenney
2025-07-25 5:23 ` Hernan Ponce de Leon
2025-07-29 20:34 ` Paul E. McKenney
2025-07-23 17:13 ` Alan Stern
2025-07-23 17:27 ` Paul E. McKenney
2025-07-23 19:25 ` Alan Stern
2025-07-23 19:57 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=3e98c47c-d354-431f-851f-494df9e6bc78@huaweicloud.com \
--to=hernan.poncedeleon@huaweicloud.com \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=jonas.oberhauser@huaweicloud.com \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=quic_neeraju@quicinc.com \
--cc=stern@rowland.harvard.edu \
--cc=urezki@gmail.com \
--cc=will@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).