linux-arch.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: paulmck@kernel.org
To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
	kernel-team@fb.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>
Subject: [PATCH tip/core/rcu 08/14] Documentation/litmus-tests/atomic: Add a test for atomic_set()
Date: Mon, 22 Jun 2020 17:52:25 -0700	[thread overview]
Message-ID: <20200623005231.27712-8-paulmck@kernel.org> (raw)
In-Reply-To: <20200623005152.GA27459@paulmck-ThinkPad-P72>

From: Boqun Feng <boqun.feng@gmail.com>

We already use a litmus test in atomic_t.txt to describe the behavior of
an atomic_set() with the an atomic RMW, so add it into atomic-tests
directory to make it easily accessible for anyone who cares about the
semantics of our atomic APIs.

Besides currently the litmus test "atomic-set" in atomic_t.txt has a few
things to be improved:

1)	The CPU/Processor numbers "P1,P2" are not only inconsistent with
	the rest of the document, which uses "CPU0" and "CPU1", but also
	unacceptable by the herd tool, which requires processors start
	at "P0".

2)	The initialization block uses a "atomic_set()", which is OK, but
	it's better to use ATOMIC_INIT() to make clear this is an
	initialization.

3)	The return value of atomic_add_unless() is discarded
	inexplicitly, which is OK for C language, but it will be helpful
	to the herd tool if we use a void cast to make the discard
	explicit.

4)	The name and the paragraph describing the test need to be more
	accurate and aligned with our wording in LKMM.

Therefore fix these in both atomic_t.txt and the new added litmus test.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 Documentation/atomic_t.txt                         | 14 ++++++-------
 ...Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++++++++++
 Documentation/litmus-tests/atomic/README           |  7 +++++++
 3 files changed, 38 insertions(+), 7 deletions(-)
 create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index 0ab747e..67d1d99f 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -85,21 +85,21 @@ smp_store_release() respectively. Therefore, if you find yourself only using
 the Non-RMW operations of atomic_t, you do not in fact need atomic_t at all
 and are doing it wrong.
 
-A subtle detail of atomic_set{}() is that it should be observable to the RMW
-ops. That is:
+A note for the implementation of atomic_set{}() is that it must not break the
+atomicity of the RMW ops. That is:
 
-  C atomic-set
+  C Atomic-RMW-ops-are-atomic-WRT-atomic_set
 
   {
-    atomic_set(v, 1);
+    atomic_t v = ATOMIC_INIT(1);
   }
 
-  P1(atomic_t *v)
+  P0(atomic_t *v)
   {
-    atomic_add_unless(v, 1, 0);
+    (void)atomic_add_unless(v, 1, 0);
   }
 
-  P2(atomic_t *v)
+  P1(atomic_t *v)
   {
     atomic_set(v, 0);
   }
diff --git a/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
new file mode 100644
index 0000000..4938531
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
@@ -0,0 +1,24 @@
+C Atomic-RMW-ops-are-atomic-WRT-atomic_set
+
+(*
+ * Result: Never
+ *
+ * Test that atomic_set() cannot break the atomicity of atomic RMWs.
+ *)
+
+{
+	atomic_t v = ATOMIC_INIT(1);
+}
+
+P0(atomic_t *v)
+{
+	(void)atomic_add_unless(v, 1, 0);
+}
+
+P1(atomic_t *v)
+{
+	atomic_set(v, 0);
+}
+
+exists
+(v=2)
diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README
index ae61201..a1b7241 100644
--- a/Documentation/litmus-tests/atomic/README
+++ b/Documentation/litmus-tests/atomic/README
@@ -2,3 +2,10 @@ This directory contains litmus tests that are typical to describe the semantics
 of our atomic APIs. For more information about how to "run" a litmus test or
 how to generate a kernel test module based on a litmus test, please see
 tools/memory-model/README.
+
+============
+LITMUS TESTS
+============
+
+Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
+	Test that atomic_set() cannot break the atomicity of atomic RMWs.
-- 
2.9.5

  parent reply	other threads:[~2020-06-23  0:52 UTC|newest]

Thread overview: 25+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-06-23  0:51 [PATCH memory-model 0/14] LKMM updates for v5.9 Paul E. McKenney
2020-06-23  0:52 ` [PATCH tip/core/rcu 01/14] tools/memory-model: Add recent references paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 02/14] tools/memory-model: Fix "conflict" definition paulmck
2020-06-23  0:52   ` paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 03/14] Documentation: LKMM: Add litmus test for RCU GP guarantee where updater frees object paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 04/14] Documentation: LKMM: Add litmus test for RCU GP guarantee where reader stores paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 05/14] MAINTAINERS: Update maintainers for new Documentation/litmus-tests paulmck
2020-06-23  0:52   ` paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 06/14] tools/memory-model: Add an exception for limitations on _unless() family paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 07/14] Documentation/litmus-tests: Introduce atomic directory paulmck
2020-06-23  0:52 ` paulmck [this message]
2020-06-23  0:52 ` [PATCH tip/core/rcu 09/14] Documentation/litmus-tests/atomic: Add a test for smp_mb__after_atomic() paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 10/14] tools/memory-model: Fix reference to litmus test in recipes.txt paulmck
2020-06-23  0:52   ` paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 11/14] Documentation/litmus-tests: Merge atomic's README into top-level one paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 12/14] Documentation/litmus-tests: Cite an RCU litmus test paulmck
2020-06-23  0:52 ` [PATCH tip/core/rcu 13/14] tools/memory-model/README: Expand dependency of klitmus7 paulmck
2020-06-23 14:37   ` Akira Yokosawa
2020-06-23 15:54     ` Paul E. McKenney
2020-06-23 22:06       ` [PATCH 1/2] tools/memory-model/README: Mention herdtools7 7.56 in compatibility table Akira Yokosawa
2020-06-23 22:09         ` [PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test Akira Yokosawa
2020-06-23 23:24           ` Andrea Parri
2020-06-24  4:05             ` Paul E. McKenney
2020-06-23 22:57         ` [PATCH 1/2] tools/memory-model/README: Mention herdtools7 7.56 in compatibility table Andrea Parri
2020-06-23  0:52 ` [PATCH tip/core/rcu 14/14] docs: fix references for DMA*.txt files paulmck

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=20200623005231.27712-8-paulmck@kernel.org \
    --to=paulmck@kernel.org \
    --cc=akiyks@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=dhowells@redhat.com \
    --cc=j.alglave@ucl.ac.uk \
    --cc=kernel-team@fb.com \
    --cc=linux-arch@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=luc.maranget@inria.fr \
    --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 NNTP newsgroup(s).