From: "Paul E. McKenney" <paulmck@kernel.org>
To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
kernel-team@meta.com, mingo@kernel.org
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,
"Paul E. McKenney" <paulmck@kernel.org>,
Frederic Weisbecker <frederic@kernel.org>,
Daniel Lustig <dlustig@nvidia.com>,
Joel Fernandes <joel@joelfernandes.org>,
Mark Rutland <mark.rutland@arm.com>,
Jonathan Corbet <corbet@lwn.net>,
linux-doc@vger.kernel.org
Subject: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg
Date: Wed, 1 May 2024 16:21:30 -0700 [thread overview]
Message-ID: <20240501232132.1785861-2-paulmck@kernel.org> (raw)
In-Reply-To: <42a43181-a431-44bd-8aff-6b305f8111ba@paulmck-laptop>
This commit adds four litmus tests showing that a failing cmpxchg()
operation is unordered unless followed by an smp_mb__after_atomic()
operation.
Suggested-by: Frederic Weisbecker <frederic@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: Mark Rutland <mark.rutland@arm.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: <linux-arch@vger.kernel.org>
Cc: <linux-doc@vger.kernel.org>
---
Documentation/litmus-tests/README | 16 +++++++++
.../atomic/cmpxchg-fail-ordered-1.litmus | 34 +++++++++++++++++++
.../atomic/cmpxchg-fail-ordered-2.litmus | 30 ++++++++++++++++
.../atomic/cmpxchg-fail-unordered-1.litmus | 33 ++++++++++++++++++
.../atomic/cmpxchg-fail-unordered-2.litmus | 30 ++++++++++++++++
5 files changed, 143 insertions(+)
create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index 26ca56df02125..6c666f3422ea3 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -21,6 +21,22 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
Test that atomic_set() cannot break the atomicity of atomic RMWs.
NOTE: Require herd7 7.56 or later which supports "(void)expr".
+cmpxchg-fail-ordered-1.litmus
+ Demonstrate that a failing cmpxchg() operation acts as a full barrier
+ when followed by smp_mb__after_atomic().
+
+cmpxchg-fail-ordered-2.litmus
+ Demonstrate that a failing cmpxchg() operation acts as an acquire
+ operation when followed by smp_mb__after_atomic().
+
+cmpxchg-fail-unordered-1.litmus
+ Demonstrate that a failing cmpxchg() operation does not act as a
+ full barrier.
+
+cmpxchg-fail-unordered-2.litmus
+ Demonstrate that a failing cmpxchg() operation does not act as an
+ acquire operation.
+
locking (/locking directory)
----------------------------
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
new file mode 100644
index 0000000000000..3df1d140b189b
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
@@ -0,0 +1,34 @@
+C cmpxchg-fail-ordered-1
+
+(*
+ * Result: Never
+ *
+ * Demonstrate that a failing cmpxchg() operation will act as a full
+ * barrier when followed by smp_mb__after_atomic().
+ *)
+
+{}
+
+P0(int *x, int *y, int *z)
+{
+ int r0;
+ int r1;
+
+ WRITE_ONCE(*x, 1);
+ r1 = cmpxchg(z, 1, 0);
+ smp_mb__after_atomic();
+ r0 = READ_ONCE(*y);
+}
+
+P1(int *x, int *y, int *z)
+{
+ int r0;
+
+ WRITE_ONCE(*y, 1);
+ r1 = cmpxchg(z, 1, 0);
+ smp_mb__after_atomic();
+ r0 = READ_ONCE(*x);
+}
+
+locations[0:r1;1:r1]
+exists (0:r0=0 /\ 1:r0=0)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
new file mode 100644
index 0000000000000..54146044a16f6
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
@@ -0,0 +1,30 @@
+C cmpxchg-fail-ordered-2
+
+(*
+ * Result: Never
+ *
+ * Demonstrate use of smp_mb__after_atomic() to make a failing cmpxchg
+ * operation have acquire ordering.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+ int r0;
+ int r1;
+
+ WRITE_ONCE(*x, 1);
+ r1 = cmpxchg(y, 0, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r0;
+
+ r1 = cmpxchg(y, 0, 1);
+ smp_mb__after_atomic();
+ r2 = READ_ONCE(*x);
+}
+
+exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
new file mode 100644
index 0000000000000..a727ce23b1a6e
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
@@ -0,0 +1,33 @@
+C cmpxchg-fail-unordered-1
+
+(*
+ * Result: Sometimes
+ *
+ * Demonstrate that a failing cmpxchg() operation does not act as a
+ * full barrier. (In contrast, a successful cmpxchg() does act as a
+ * full barrier.)
+ *)
+
+{}
+
+P0(int *x, int *y, int *z)
+{
+ int r0;
+ int r1;
+
+ WRITE_ONCE(*x, 1);
+ r1 = cmpxchg(z, 1, 0);
+ r0 = READ_ONCE(*y);
+}
+
+P1(int *x, int *y, int *z)
+{
+ int r0;
+
+ WRITE_ONCE(*y, 1);
+ r1 = cmpxchg(z, 1, 0);
+ r0 = READ_ONCE(*x);
+}
+
+locations[0:r1;1:r1]
+exists (0:r0=0 /\ 1:r0=0)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
new file mode 100644
index 0000000000000..a245bac55b578
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
@@ -0,0 +1,30 @@
+C cmpxchg-fail-unordered-2
+
+(*
+ * Result: Sometimes
+ *
+ * Demonstrate that a failing cmpxchg() operation does not act as either
+ * an acquire release operation. (In contrast, a successful cmpxchg()
+ * does act as both an acquire and a release operation.)
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+ int r0;
+ int r1;
+
+ WRITE_ONCE(*x, 1);
+ r1 = cmpxchg(y, 0, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r0;
+
+ r1 = cmpxchg(y, 0, 1);
+ r2 = READ_ONCE(*x);
+}
+
+exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0)
--
2.40.1
next prev parent reply other threads:[~2024-05-01 23:21 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
[not found] <42a43181-a431-44bd-8aff-6b305f8111ba@paulmck-laptop>
2024-05-01 23:21 ` [PATCH memory-model 1/4] Documentation/litmus-tests: Add locking tests to README Paul E. McKenney
2024-05-01 23:21 ` Paul E. McKenney [this message]
2024-05-06 10:05 ` [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg Jonas Oberhauser
2024-05-06 16:30 ` Jonas Oberhauser
2024-05-06 18:00 ` Paul E. McKenney
2024-05-06 19:21 ` Alan Stern
2024-05-07 9:03 ` Jonas Oberhauser
2024-05-08 1:17 ` Andrea Parri
2024-05-07 9:11 ` Jonas Oberhauser
2024-05-15 6:44 ` Hernan Ponce de Leon
2024-05-15 15:01 ` Paul E. McKenney
2024-05-01 23:21 ` [PATCH memory-model 3/4] Documentation/atomic_t: Emphasize that failed atomic operations give no ordering 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=20240501232132.1785861-2-paulmck@kernel.org \
--to=paulmck@kernel.org \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=corbet@lwn.net \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=kernel-team@meta.com \
--cc=linux-arch@vger.kernel.org \
--cc=linux-doc@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mark.rutland@arm.com \
--cc=mingo@kernel.org \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--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).