[PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Boqun Feng]

A recent discussion raises up the requirement for having test cases for
atomic APIs:

	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/

, and since we already have a way to generate a test module from a
litmus test with klitmus[1]. It makes sense that we add more litmus
tests for atomic APIs. And based on the previous discussion, I create a
new directory Documentation/atomic-tests and put these litmus tests
here.

This patchset starts the work by adding the litmus tests which are
already used in atomic_t.txt, and also improve the atomic_t.txt to make
it consistent with the litmus tests.

Previous version:
v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/

Changes since v3:

*	Merge two patches on atomic-set litmus test into one as per
	Alan. (Alan, you have acked only one of the two patches, so I
	don't add you acked-by for the combined patch).

*	Move the atomic litmus tests into litmus-tests/atomic to align
	with Joel's recent patches on RCU litmus tests.

I think we still haven't reach to a conclusion for the difference of
atomic_add_unless() in herdtools, and I'm currently reading the source
code of herd to resovle this. This is just an updated version to resolve
ealier comments and react on Joel's RCU litmus tests.

Regards,
Boqun

[1]: http://diy.inria.fr/doc/litmus.html#klitmus

Boqun Feng (4):
  tools/memory-model: Add an exception for limitations on _unless()
    family
  Documentation/litmus-tests: Introduce atomic directory
  Documentation/litmus-tests/atomic: Add a test for atomic_set()
  Documentation/litmus-tests/atomic: Add a test for
    smp_mb__after_atomic()

 Documentation/atomic_t.txt                    | 24 +++++++-------
 ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
 ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
 Documentation/litmus-tests/atomic/README      | 16 ++++++++++
 tools/memory-model/README                     | 10 ++++--
 5 files changed, 91 insertions(+), 15 deletions(-)
 create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
 create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
 create mode 100644 Documentation/litmus-tests/atomic/README

-- 
2.25.1

[PATCH v4 1/4] tools/memory-model: Add an exception for limitations on _unless() family

[Boqun Feng]

According to Luc, atomic_add_unless() is directly provided by herd7,
therefore it can be used in litmus tests. So change the limitation
section in README to unlimit the use of atomic_add_unless().

Cc: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
---
 tools/memory-model/README | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/tools/memory-model/README b/tools/memory-model/README
index fc07b52f2028..b9c562e92981 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -207,11 +207,15 @@ The Linux-kernel memory model (LKMM) has the following limitations:
 		case as a store release.
 
 	b.	The "unless" RMW operations are not currently modeled:
-		atomic_long_add_unless(), atomic_add_unless(),
-		atomic_inc_unless_negative(), and
-		atomic_dec_unless_positive().  These can be emulated
+		atomic_long_add_unless(), atomic_inc_unless_negative(),
+		and atomic_dec_unless_positive().  These can be emulated
 		in litmus tests, for example, by using atomic_cmpxchg().
 
+		One exception of this limitation is atomic_add_unless(),
+		which is provided directly by herd7 (so no corresponding
+		definition in linux-kernel.def).  atomic_add_unless() is
+		modeled by herd7 therefore it can be used in litmus tests.
+
 	c.	The call_rcu() function is not modeled.  It can be
 		emulated in litmus tests by adding another process that
 		invokes synchronize_rcu() and the body of the callback
-- 
2.25.1

[PATCH v4 2/4] Documentation/litmus-tests: Introduce atomic directory

[Boqun Feng]

Although we have atomic_t.txt and its friends to describe the semantics
of atomic APIs and lib/atomic64_test.c for build testing and testing in
UP mode, the tests for our atomic APIs in real SMP mode are still
missing. Since now we have the LKMM tool in kernel and litmus tests can
be used to generate kernel modules for testing purpose with "klitmus" (a
tool from the LKMM toolset), it makes sense to put a few typical litmus
tests into kernel so that

1)	they are the examples to describe the conceptual mode of the
	semantics of atomic APIs, and

2)	they can be used to generate kernel test modules for anyone
	who is interested to test the atomic APIs implementation (in
	most cases, is the one who implements the APIs for a new arch)

Therefore, introduce the atomic directory for this purpose. The
directory is maintained by the LKMM group to make sure the litmus tests
are always aligned with our memory model.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
---
 Documentation/litmus-tests/atomic/README | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 Documentation/litmus-tests/atomic/README

diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README
new file mode 100644
index 000000000000..ae61201a4271
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/README
@@ -0,0 +1,4 @@
+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.
-- 
2.25.1

[PATCH v4 3/4] Documentation/litmus-tests/atomic: Add a test for atomic_set()

[Boqun Feng]

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.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
---
 Documentation/atomic_t.txt                    | 14 +++++------
 ...c-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 0ab747e0d5ac..67d1d99f8589 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 000000000000..49385314d911
--- /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 ae61201a4271..a1b72410b539 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.25.1

Re: [PATCH v4 3/4] Documentation/litmus-tests/atomic: Add a test for atomic_set()

[Alan Stern]

On Thu, 26 Mar 2020, Boqun Feng wrote:

> 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.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> Acked-by: Andrea Parri <parri.andrea@gmail.com>
> ---

Acked-by: Alan Stern <stern@rowland.harvard.edu>

>  Documentation/atomic_t.txt                    | 14 +++++------
>  ...c-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 0ab747e0d5ac..67d1d99f8589 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 000000000000..49385314d911
> --- /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 ae61201a4271..a1b72410b539 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.
> 

[PATCH v4 4/4] Documentation/litmus-tests/atomic: Add a test for smp_mb__after_atomic()

[Boqun Feng]

We already use a litmus test in atomic_t.txt to describe atomic RMW +
smp_mb__after_atomic() is stronger than acquire (both the read and the
write parts are ordered). So make it a litmus test in atomic-tests
directory, so that people can access the litmus easily.

Additionally, change the processor numbers "P1, P2" to "P0, P1" in
atomic_t.txt for the consistency with the processor numbers in the
litmus test, which herd can handle.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
---
 Documentation/atomic_t.txt                    | 10 +++---
 ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
 Documentation/litmus-tests/atomic/README      |  5 +++
 3 files changed, 42 insertions(+), 5 deletions(-)
 create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index 67d1d99f8589..0f1fdedf36bb 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -233,19 +233,19 @@ as well. Similarly, something like:
 is an ACQUIRE pattern (though very much not typical), but again the barrier is
 strictly stronger than ACQUIRE. As illustrated:
 
-  C strong-acquire
+  C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire
 
   {
   }
 
-  P1(int *x, atomic_t *y)
+  P0(int *x, atomic_t *y)
   {
     r0 = READ_ONCE(*x);
     smp_rmb();
     r1 = atomic_read(y);
   }
 
-  P2(int *x, atomic_t *y)
+  P1(int *x, atomic_t *y)
   {
     atomic_inc(y);
     smp_mb__after_atomic();
@@ -253,14 +253,14 @@ strictly stronger than ACQUIRE. As illustrated:
   }
 
   exists
-  (r0=1 /\ r1=0)
+  (0:r0=1 /\ 0:r1=0)
 
 This should not happen; but a hypothetical atomic_inc_acquire() --
 (void)atomic_fetch_inc_acquire() for instance -- would allow the outcome,
 because it would not order the W part of the RMW against the following
 WRITE_ONCE.  Thus:
 
-  P1			P2
+  P0			P1
 
 			t = LL.acq *y (0)
 			t++;
diff --git a/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus b/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
new file mode 100644
index 000000000000..9a8e31a44b28
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
@@ -0,0 +1,32 @@
+C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire
+
+(*
+ * Result: Never
+ *
+ * Test that an atomic RMW followed by a smp_mb__after_atomic() is
+ * stronger than a normal acquire: both the read and write parts of
+ * the RMW are ordered before the subsequential memory accesses.
+ *)
+
+{
+}
+
+P0(int *x, atomic_t *y)
+{
+	int r0;
+	int r1;
+
+	r0 = READ_ONCE(*x);
+	smp_rmb();
+	r1 = atomic_read(y);
+}
+
+P1(int *x, atomic_t *y)
+{
+	atomic_inc(y);
+	smp_mb__after_atomic();
+	WRITE_ONCE(*x, 1);
+}
+
+exists
+(0:r0=1 /\ 0:r1=0)
diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README
index a1b72410b539..714cf93816ea 100644
--- a/Documentation/litmus-tests/atomic/README
+++ b/Documentation/litmus-tests/atomic/README
@@ -7,5 +7,10 @@ tools/memory-model/README.
 LITMUS TESTS
 ============
 
+Atomic-RMW+mb__after_atomic-is-stronger-than-acquire
+	Test that an atomic RMW followed by a smp_mb__after_atomic() is
+	stronger than a normal acquire: both the read and write parts of
+	the RMW are ordered before the subsequential memory accesses.
+
 Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
 	Test that atomic_set() cannot break the atomicity of atomic RMWs.
-- 
2.25.1

Re: [PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Joel Fernandes]

On Thu, Mar 26, 2020 at 10:40:18AM +0800, Boqun Feng wrote:
> A recent discussion raises up the requirement for having test cases for
> atomic APIs:
> 
> 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> 
> , and since we already have a way to generate a test module from a
> litmus test with klitmus[1]. It makes sense that we add more litmus
> tests for atomic APIs. And based on the previous discussion, I create a
> new directory Documentation/atomic-tests and put these litmus tests
> here.
> 
> This patchset starts the work by adding the litmus tests which are
> already used in atomic_t.txt, and also improve the atomic_t.txt to make
> it consistent with the litmus tests.
> 
> Previous version:
> v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
> v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
> v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/

For full series:

Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

One question I had was in the existing atomic_set() documentation, it talks
about atomic_add_unless() implementation based on locking could have issues.
It says the way to fix such cases is:

Quote:
    the typical solution is to then implement atomic_set{}() with
    atomic_xchg().

I didn't get how using atomic_xchg() fixes it. Is the assumption there that
atomic_xchg() would be implemented using locking to avoid atomic_set() having
issues? If so, we could clarify that in the document.

thanks,

 - Joel

> 
> Changes since v3:
> 
> *	Merge two patches on atomic-set litmus test into one as per
> 	Alan. (Alan, you have acked only one of the two patches, so I
> 	don't add you acked-by for the combined patch).
> 
> *	Move the atomic litmus tests into litmus-tests/atomic to align
> 	with Joel's recent patches on RCU litmus tests.
> 
> I think we still haven't reach to a conclusion for the difference of
> atomic_add_unless() in herdtools, and I'm currently reading the source
> code of herd to resovle this. This is just an updated version to resolve
> ealier comments and react on Joel's RCU litmus tests.
> 
> Regards,
> Boqun
> 
> [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> 
> Boqun Feng (4):
>   tools/memory-model: Add an exception for limitations on _unless()
>     family
>   Documentation/litmus-tests: Introduce atomic directory
>   Documentation/litmus-tests/atomic: Add a test for atomic_set()
>   Documentation/litmus-tests/atomic: Add a test for
>     smp_mb__after_atomic()
> 
>  Documentation/atomic_t.txt                    | 24 +++++++-------
>  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
>  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
>  Documentation/litmus-tests/atomic/README      | 16 ++++++++++
>  tools/memory-model/README                     | 10 ++++--
>  5 files changed, 91 insertions(+), 15 deletions(-)
>  create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
>  create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
>  create mode 100644 Documentation/litmus-tests/atomic/README
> 
> -- 
> 2.25.1
> 

Re: [PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Boqun Feng]

On Fri, Mar 27, 2020 at 06:18:43PM -0400, Joel Fernandes wrote:
> On Thu, Mar 26, 2020 at 10:40:18AM +0800, Boqun Feng wrote:
> > A recent discussion raises up the requirement for having test cases for
> > atomic APIs:
> > 
> > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > 
> > , and since we already have a way to generate a test module from a
> > litmus test with klitmus[1]. It makes sense that we add more litmus
> > tests for atomic APIs. And based on the previous discussion, I create a
> > new directory Documentation/atomic-tests and put these litmus tests
> > here.
> > 
> > This patchset starts the work by adding the litmus tests which are
> > already used in atomic_t.txt, and also improve the atomic_t.txt to make
> > it consistent with the litmus tests.
> > 
> > Previous version:
> > v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
> > v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
> > v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/
> 
> For full series:
> 
> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> 
> One question I had was in the existing atomic_set() documentation, it talks
> about atomic_add_unless() implementation based on locking could have issues.
> It says the way to fix such cases is:
> 
> Quote:
>     the typical solution is to then implement atomic_set{}() with
>     atomic_xchg().
> 
> I didn't get how using atomic_xchg() fixes it. Is the assumption there that
> atomic_xchg() would be implemented using locking to avoid atomic_set() having

Right, I think that's the intent of the sentence.

> issues? If so, we could clarify that in the document.
> 

Patches are welcome ;-)

Regards,
Boqun

> thanks,
> 
>  - Joel
> 
> > 
> > Changes since v3:
> > 
> > *	Merge two patches on atomic-set litmus test into one as per
> > 	Alan. (Alan, you have acked only one of the two patches, so I
> > 	don't add you acked-by for the combined patch).
> > 
> > *	Move the atomic litmus tests into litmus-tests/atomic to align
> > 	with Joel's recent patches on RCU litmus tests.
> > 
> > I think we still haven't reach to a conclusion for the difference of
> > atomic_add_unless() in herdtools, and I'm currently reading the source
> > code of herd to resovle this. This is just an updated version to resolve
> > ealier comments and react on Joel's RCU litmus tests.
> > 
> > Regards,
> > Boqun
> > 
> > [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> > 
> > Boqun Feng (4):
> >   tools/memory-model: Add an exception for limitations on _unless()
> >     family
> >   Documentation/litmus-tests: Introduce atomic directory
> >   Documentation/litmus-tests/atomic: Add a test for atomic_set()
> >   Documentation/litmus-tests/atomic: Add a test for
> >     smp_mb__after_atomic()
> > 
> >  Documentation/atomic_t.txt                    | 24 +++++++-------
> >  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
> >  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
> >  Documentation/litmus-tests/atomic/README      | 16 ++++++++++
> >  tools/memory-model/README                     | 10 ++++--
> >  5 files changed, 91 insertions(+), 15 deletions(-)
> >  create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
> >  create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> >  create mode 100644 Documentation/litmus-tests/atomic/README
> > 
> > -- 
> > 2.25.1
> > 

Re: [PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Joel Fernandes]

On Tue, Mar 31, 2020 at 09:40:37AM +0800, Boqun Feng wrote:
> On Fri, Mar 27, 2020 at 06:18:43PM -0400, Joel Fernandes wrote:
> > On Thu, Mar 26, 2020 at 10:40:18AM +0800, Boqun Feng wrote:
> > > A recent discussion raises up the requirement for having test cases for
> > > atomic APIs:
> > > 
> > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > 
> > > , and since we already have a way to generate a test module from a
> > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > tests for atomic APIs. And based on the previous discussion, I create a
> > > new directory Documentation/atomic-tests and put these litmus tests
> > > here.
> > > 
> > > This patchset starts the work by adding the litmus tests which are
> > > already used in atomic_t.txt, and also improve the atomic_t.txt to make
> > > it consistent with the litmus tests.
> > > 
> > > Previous version:
> > > v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
> > > v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
> > > v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/
> > 
> > For full series:
> > 
> > Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > 
> > One question I had was in the existing atomic_set() documentation, it talks
> > about atomic_add_unless() implementation based on locking could have issues.
> > It says the way to fix such cases is:
> > 
> > Quote:
> >     the typical solution is to then implement atomic_set{}() with
> >     atomic_xchg().
> > 
> > I didn't get how using atomic_xchg() fixes it. Is the assumption there that
> > atomic_xchg() would be implemented using locking to avoid atomic_set() having
> 
> Right, I think that's the intent of the sentence.
> 
> > issues? If so, we could clarify that in the document.
> > 
> 
> Patches are welcome ;-)


---8<-----------------------

Like this? I'll add it to my tree and send it to Paul during my next
series, unless you disagree ;-)

Subject: [PATCH] doc: atomic_t: Document better about the locking within
 atomic_xchg()

It is not fully clear how the atomic_set() would not cause an issue with
preservation of the atomicity of RMW in this example. Make it clear that
locking within atomic_xchg() would save the day.

Suggested-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
---
 Documentation/atomic_t.txt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index 0f1fdedf36bbb..1d9c307c73a7c 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -129,6 +129,8 @@ with a lock:
     unlock();
 
 the typical solution is to then implement atomic_set{}() with atomic_xchg().
+The locking within the atomic_xchg() in CPU1 would ensure that the value read
+in CPU0 would not be overwritten.
 
 
 RMW ops:
-- 
2.26.0.292.g33ef6b2f38-goog

Re: [PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Boqun Feng]

On Wed, Apr 01, 2020 at 11:58:16PM -0400, Joel Fernandes wrote:
> On Tue, Mar 31, 2020 at 09:40:37AM +0800, Boqun Feng wrote:
> > On Fri, Mar 27, 2020 at 06:18:43PM -0400, Joel Fernandes wrote:
> > > On Thu, Mar 26, 2020 at 10:40:18AM +0800, Boqun Feng wrote:
> > > > A recent discussion raises up the requirement for having test cases for
> > > > atomic APIs:
> > > > 
> > > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > > 
> > > > , and since we already have a way to generate a test module from a
> > > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > > tests for atomic APIs. And based on the previous discussion, I create a
> > > > new directory Documentation/atomic-tests and put these litmus tests
> > > > here.
> > > > 
> > > > This patchset starts the work by adding the litmus tests which are
> > > > already used in atomic_t.txt, and also improve the atomic_t.txt to make
> > > > it consistent with the litmus tests.
> > > > 
> > > > Previous version:
> > > > v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
> > > > v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
> > > > v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/
> > > 
> > > For full series:
> > > 
> > > Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > > 
> > > One question I had was in the existing atomic_set() documentation, it talks
> > > about atomic_add_unless() implementation based on locking could have issues.
> > > It says the way to fix such cases is:
> > > 
> > > Quote:
> > >     the typical solution is to then implement atomic_set{}() with
> > >     atomic_xchg().
> > > 
> > > I didn't get how using atomic_xchg() fixes it. Is the assumption there that
> > > atomic_xchg() would be implemented using locking to avoid atomic_set() having
> > 
> > Right, I think that's the intent of the sentence.
> > 
> > > issues? If so, we could clarify that in the document.
> > > 
> > 
> > Patches are welcome ;-)
> 
> 
> ---8<-----------------------
> 
> Like this? I'll add it to my tree and send it to Paul during my next
> series, unless you disagree ;-)
> 
> Subject: [PATCH] doc: atomic_t: Document better about the locking within
>  atomic_xchg()
> 
> It is not fully clear how the atomic_set() would not cause an issue with
> preservation of the atomicity of RMW in this example. Make it clear that
> locking within atomic_xchg() would save the day.
> 
> Suggested-by: Boqun Feng <boqun.feng@gmail.com>
> Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>

Thanks!

Acked-by: Boqun Feng <boqun.feng@gmail.com>

Regards,
Boqun

> ---
>  Documentation/atomic_t.txt | 2 ++
>  1 file changed, 2 insertions(+)
> 
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index 0f1fdedf36bbb..1d9c307c73a7c 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -129,6 +129,8 @@ with a lock:
>      unlock();
>  
>  the typical solution is to then implement atomic_set{}() with atomic_xchg().
> +The locking within the atomic_xchg() in CPU1 would ensure that the value read
> +in CPU0 would not be overwritten.
>  
>  
>  RMW ops:
> -- 
> 2.26.0.292.g33ef6b2f38-goog
> 

Re: [PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Joel Fernandes]

On Thu, Apr 02, 2020 at 04:03:58PM +0800, Boqun Feng wrote:
> On Wed, Apr 01, 2020 at 11:58:16PM -0400, Joel Fernandes wrote:
> > On Tue, Mar 31, 2020 at 09:40:37AM +0800, Boqun Feng wrote:
> > > On Fri, Mar 27, 2020 at 06:18:43PM -0400, Joel Fernandes wrote:
> > > > On Thu, Mar 26, 2020 at 10:40:18AM +0800, Boqun Feng wrote:
> > > > > A recent discussion raises up the requirement for having test cases for
> > > > > atomic APIs:
> > > > > 
> > > > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > > > 
> > > > > , and since we already have a way to generate a test module from a
> > > > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > > > tests for atomic APIs. And based on the previous discussion, I create a
> > > > > new directory Documentation/atomic-tests and put these litmus tests
> > > > > here.
> > > > > 
> > > > > This patchset starts the work by adding the litmus tests which are
> > > > > already used in atomic_t.txt, and also improve the atomic_t.txt to make
> > > > > it consistent with the litmus tests.
> > > > > 
> > > > > Previous version:
> > > > > v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
> > > > > v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
> > > > > v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/
> > > > 
> > > > For full series:
> > > > 
> > > > Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > > > 
> > > > One question I had was in the existing atomic_set() documentation, it talks
> > > > about atomic_add_unless() implementation based on locking could have issues.
> > > > It says the way to fix such cases is:
> > > > 
> > > > Quote:
> > > >     the typical solution is to then implement atomic_set{}() with
> > > >     atomic_xchg().
> > > > 
> > > > I didn't get how using atomic_xchg() fixes it. Is the assumption there that
> > > > atomic_xchg() would be implemented using locking to avoid atomic_set() having
> > > 
> > > Right, I think that's the intent of the sentence.
> > > 
> > > > issues? If so, we could clarify that in the document.
> > > > 
> > > 
> > > Patches are welcome ;-)
> > 
> > 
> > ---8<-----------------------
> > 
> > Like this? I'll add it to my tree and send it to Paul during my next
> > series, unless you disagree ;-)
> > 
> > Subject: [PATCH] doc: atomic_t: Document better about the locking within
> >  atomic_xchg()
> > 
> > It is not fully clear how the atomic_set() would not cause an issue with
> > preservation of the atomicity of RMW in this example. Make it clear that
> > locking within atomic_xchg() would save the day.
> > 
> > Suggested-by: Boqun Feng <boqun.feng@gmail.com>
> > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> 
> Thanks!
> 
> Acked-by: Boqun Feng <boqun.feng@gmail.com>

Thanks for the Ack, will send it to Paul during next series with your tag.

 - Joel

Re: [PATCH v4 0/4] Documentation/litmus-tests: Add litmus tests for atomic APIs

[Paul E. McKenney]

On Fri, Mar 27, 2020 at 06:18:43PM -0400, Joel Fernandes wrote:
> On Thu, Mar 26, 2020 at 10:40:18AM +0800, Boqun Feng wrote:
> > A recent discussion raises up the requirement for having test cases for
> > atomic APIs:
> > 
> > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > 
> > , and since we already have a way to generate a test module from a
> > litmus test with klitmus[1]. It makes sense that we add more litmus
> > tests for atomic APIs. And based on the previous discussion, I create a
> > new directory Documentation/atomic-tests and put these litmus tests
> > here.
> > 
> > This patchset starts the work by adding the litmus tests which are
> > already used in atomic_t.txt, and also improve the atomic_t.txt to make
> > it consistent with the litmus tests.
> > 
> > Previous version:
> > v1: https://lore.kernel.org/linux-doc/20200214040132.91934-1-boqun.feng@gmail.com/
> > v2: https://lore.kernel.org/lkml/20200219062627.104736-1-boqun.feng@gmail.com/
> > v3: https://lore.kernel.org/linux-doc/20200227004049.6853-1-boqun.feng@gmail.com/
> 
> For full series:
> 
> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

Queued in place of the following commits, with Joel's and Alan's tags
added, thank you all!

							Thanx, Paul

c13c55d4 tools/memory-model: Add an exception for limitations on _unless() family
59ffd85 Documentation/locking/atomic: Fix atomic-set litmus test
23c19c8 Documentation/locking/atomic: Introduce atomic-tests directory
3bd201c Documentation/locking/atomic: Add a litmus test for atomic_set()
833f53b Documentation/locking/atomic: Add a litmus test smp_mb__after_atomic()

> One question I had was in the existing atomic_set() documentation, it talks
> about atomic_add_unless() implementation based on locking could have issues.
> It says the way to fix such cases is:
> 
> Quote:
>     the typical solution is to then implement atomic_set{}() with
>     atomic_xchg().
> 
> I didn't get how using atomic_xchg() fixes it. Is the assumption there that
> atomic_xchg() would be implemented using locking to avoid atomic_set() having
> issues? If so, we could clarify that in the document.
> 
> thanks,
> 
>  - Joel
> 
> > 
> > Changes since v3:
> > 
> > *	Merge two patches on atomic-set litmus test into one as per
> > 	Alan. (Alan, you have acked only one of the two patches, so I
> > 	don't add you acked-by for the combined patch).
> > 
> > *	Move the atomic litmus tests into litmus-tests/atomic to align
> > 	with Joel's recent patches on RCU litmus tests.
> > 
> > I think we still haven't reach to a conclusion for the difference of
> > atomic_add_unless() in herdtools, and I'm currently reading the source
> > code of herd to resovle this. This is just an updated version to resolve
> > ealier comments and react on Joel's RCU litmus tests.
> > 
> > Regards,
> > Boqun
> > 
> > [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> > 
> > Boqun Feng (4):
> >   tools/memory-model: Add an exception for limitations on _unless()
> >     family
> >   Documentation/litmus-tests: Introduce atomic directory
> >   Documentation/litmus-tests/atomic: Add a test for atomic_set()
> >   Documentation/litmus-tests/atomic: Add a test for
> >     smp_mb__after_atomic()
> > 
> >  Documentation/atomic_t.txt                    | 24 +++++++-------
> >  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
> >  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
> >  Documentation/litmus-tests/atomic/README      | 16 ++++++++++
> >  tools/memory-model/README                     | 10 ++++--
> >  5 files changed, 91 insertions(+), 15 deletions(-)
> >  create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
> >  create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> >  create mode 100644 Documentation/litmus-tests/atomic/README
> > 
> > -- 
> > 2.25.1
> >