From: "Paul E. McKenney" <paulmck@kernel.org>
To: 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,
hernan.poncedeleon@huaweicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA
Date: Tue, 22 Jul 2025 17:43:16 -0700 [thread overview]
Message-ID: <6fb01aea-f7b4-4f38-82b9-fd6c360514fc@paulmck-laptop> (raw)
In-Reply-To: <20250106214003.504664-1-jonas.oberhauser@huaweicloud.com>
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.
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.
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 0: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 [this message]
2025-07-23 7:26 ` Hernan Ponce de Leon
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=6fb01aea-f7b4-4f38-82b9-fd6c360514fc@paulmck-laptop \
--to=paulmck@kernel.org \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=hernan.poncedeleon@huaweicloud.com \
--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=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).