[PATCH v3 0/5] Documentation/locking/atomic: Add litmus tests for atomic APIs

[PATCH v3 0/5] Documentation/locking/atomic: 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/

Changes since v2:

*	Change from "RFC" to "PATCH".

*	Wording improvement in atomic_t.txt as per Alan's suggestion.

*	Add a new patch describing the usage of atomic_add_unless() is
	not limited anymore for LKMM litmus tests.

My PR on supporting "(void) expr;" statement has been merged by Luc
(Thank you, Luc). So all the litmus tests in this patchset can be
handled by the herdtools compiled from latest master branch of the
source code.

Comments and suggestions are welcome!

Regards,
Boqun

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

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

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

-- 
2.25.0

[PATCH v3 1/5] 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>
---
 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..409211b1c544 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.0

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

[Alan Stern]

On Thu, 27 Feb 2020, Boqun Feng wrote:

> 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().

Is this really true?  Why does herd treat atomic_add_unless() different
from all the other atomic RMS ops?  All the other ones we support do
have entries in linux-kernel.def.

Alan

PS: It seems strange to support atomic_add_unless but not 
atomic_long_add_unless.  The difference between the two is trivial.

> 
> Cc: Luc Maranget <luc.maranget@inria.fr>
> Signed-off-by: Boqun Feng <boqun.feng@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..409211b1c544 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
> 

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

[Luc Maranget]

> On Thu, 27 Feb 2020, Boqun Feng wrote:
> 
> > 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().
> 
> Is this really true?  Why does herd treat atomic_add_unless() different
> from all the other atomic RMS ops?  All the other ones we support do
> have entries in linux-kernel.def.

I think this to be true :)

As far as I remember atomic_add_unless is quite different fron other atomic
RMW ops and called for a specific all-OCaml implementation, without an
entry in linux-kernel.def. As to  atomic_long_add_unless, I was not aware
of its existence.

--Luc

> 
> Alan
> 
> PS: It seems strange to support atomic_add_unless but not 
> atomic_long_add_unless.  The difference between the two is trivial.
> 
> > 
> > Cc: Luc Maranget <luc.maranget@inria.fr>
> > Signed-off-by: Boqun Feng <boqun.feng@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..409211b1c544 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
> > 

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

[Alan Stern]

On Thu, 27 Feb 2020, Luc Maranget wrote:

> > On Thu, 27 Feb 2020, Boqun Feng wrote:
> > 
> > > 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().
> > 
> > Is this really true?  Why does herd treat atomic_add_unless() different
> > from all the other atomic RMS ops?  All the other ones we support do
> > have entries in linux-kernel.def.
> 
> I think this to be true :)
> 
> As far as I remember atomic_add_unless is quite different fron other atomic
> RMW ops and called for a specific all-OCaml implementation, without an
> entry in linux-kernel.def. As to  atomic_long_add_unless, I was not aware
> of its existence.

Can you explain what is so different about atomic_add_unless?

Alan

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

[Andrea Parri]

On Thu, Feb 27, 2020 at 08:40:45AM +0800, Boqun Feng wrote:
> 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>
> ---
>  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..409211b1c544 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

Nit: Two spaces after period?

  Andrea


> +		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.0
> 

[PATCH v3 2/5] Documentation/locking/atomic: Fix atomic-set litmus test

[Boqun Feng]

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.

Therefore fix these and this is the preparation for adding the litmus
test into memory-model litmus-tests directory so that people can
understand better about our requirements of atomic APIs and klitmus tool
can be used to generate tests.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
 Documentation/atomic_t.txt | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index 0ab747e0d5ac..ceb85ada378e 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -91,15 +91,15 @@ ops. That is:
   C 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);
   }
-- 
2.25.0

Re: [PATCH v3 2/5] Documentation/locking/atomic: Fix atomic-set litmus test

[Alan Stern]

On Thu, 27 Feb 2020, Boqun Feng wrote:

> 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.
> 
> Therefore fix these and this is the preparation for adding the litmus
> test into memory-model litmus-tests directory so that people can
> understand better about our requirements of atomic APIs and klitmus tool
> can be used to generate tests.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>

Patch 5/5 in this series does basically the same thing for 
Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.  How come you 
used one patch for that, but this is split into two patches (2/5 and 
4/5)?

Alan

> ---
>  Documentation/atomic_t.txt | 8 ++++----
>  1 file changed, 4 insertions(+), 4 deletions(-)
> 
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index 0ab747e0d5ac..ceb85ada378e 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -91,15 +91,15 @@ ops. That is:
>    C 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);
>    }
> 

Re: [PATCH v3 2/5] Documentation/locking/atomic: Fix atomic-set litmus test

[Boqun Feng]

On Thu, Feb 27, 2020 at 11:34:55AM -0500, Alan Stern wrote:
> On Thu, 27 Feb 2020, Boqun Feng wrote:
> 
> > 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.
> > 
> > Therefore fix these and this is the preparation for adding the litmus
> > test into memory-model litmus-tests directory so that people can
> > understand better about our requirements of atomic APIs and klitmus tool
> > can be used to generate tests.
> > 
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> 
> Patch 5/5 in this series does basically the same thing for 
> Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.  How come you 
> used one patch for that, but this is split into two patches (2/5 and 
> 4/5)?
> 

When I was working one the first version, I wasn't so sure that we would
reach the agreement of where to put the litmus tests, and the litmus
test in the atomic_t.txt obviously needs a fix, so I separated the fix
and the adding of a litmus test to make my rebase easier ;-). But you're
right, the separation is not needed now. 

I will merge those two patches into one in the next version, also with
the name adjustment you and Andrea have pointed out. Thanks!

Regards,
Boqun

> Alan
> 
> > ---
> >  Documentation/atomic_t.txt | 8 ++++----
> >  1 file changed, 4 insertions(+), 4 deletions(-)
> > 
> > diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> > index 0ab747e0d5ac..ceb85ada378e 100644
> > --- a/Documentation/atomic_t.txt
> > +++ b/Documentation/atomic_t.txt
> > @@ -91,15 +91,15 @@ ops. That is:
> >    C 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);
> >    }
> > 
> 
> 

[PATCH v3 3/5] Documentation/locking/atomic: Introduce atomic-tests 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-tests 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>
---
 Documentation/atomic-tests/README | 4 ++++
 MAINTAINERS                       | 1 +
 2 files changed, 5 insertions(+)
 create mode 100644 Documentation/atomic-tests/README

diff --git a/Documentation/atomic-tests/README b/Documentation/atomic-tests/README
new file mode 100644
index 000000000000..ae61201a4271
--- /dev/null
+++ b/Documentation/atomic-tests/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.
diff --git a/MAINTAINERS b/MAINTAINERS
index ffc7d5712735..ebca5f6263bb 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -9718,6 +9718,7 @@ T:	git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git dev
 F:	tools/memory-model/
 F:	Documentation/atomic_bitops.txt
 F:	Documentation/atomic_t.txt
+F:	Documentation/atomic-tests/
 F:	Documentation/core-api/atomic_ops.rst
 F:	Documentation/core-api/refcount-vs-atomic.rst
 F:	Documentation/memory-barriers.txt
-- 
2.25.0

Re: [PATCH v3 3/5] Documentation/locking/atomic: Introduce atomic-tests directory

[Alan Stern]

On Thu, 27 Feb 2020, Boqun Feng wrote:

> 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-tests 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>

> ---
>  Documentation/atomic-tests/README | 4 ++++
>  MAINTAINERS                       | 1 +
>  2 files changed, 5 insertions(+)
>  create mode 100644 Documentation/atomic-tests/README
> 
> diff --git a/Documentation/atomic-tests/README b/Documentation/atomic-tests/README
> new file mode 100644
> index 000000000000..ae61201a4271
> --- /dev/null
> +++ b/Documentation/atomic-tests/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.
> diff --git a/MAINTAINERS b/MAINTAINERS
> index ffc7d5712735..ebca5f6263bb 100644
> --- a/MAINTAINERS
> +++ b/MAINTAINERS
> @@ -9718,6 +9718,7 @@ T:	git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git dev
>  F:	tools/memory-model/
>  F:	Documentation/atomic_bitops.txt
>  F:	Documentation/atomic_t.txt
> +F:	Documentation/atomic-tests/
>  F:	Documentation/core-api/atomic_ops.rst
>  F:	Documentation/core-api/refcount-vs-atomic.rst
>  F:	Documentation/memory-barriers.txt
> 

[PATCH v3 4/5] Documentation/locking/atomic: Add a litmus 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.

Additionally, change the sentences describing the test in atomic_t.txt
with better wording.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
 ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 +++++++++++++++++++
 Documentation/atomic-tests/README             |  7 ++++++
 Documentation/atomic_t.txt                    |  6 ++---
 3 files changed, 34 insertions(+), 3 deletions(-)
 create mode 100644 Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus

diff --git a/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus b/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
new file mode 100644
index 000000000000..5dd7f04e504a
--- /dev/null
+++ b/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
@@ -0,0 +1,24 @@
+C Atomic-set-observable-to-RMW
+
+(*
+ * 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/atomic-tests/README b/Documentation/atomic-tests/README
index ae61201a4271..a1b72410b539 100644
--- a/Documentation/atomic-tests/README
+++ b/Documentation/atomic-tests/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.
diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index ceb85ada378e..67d1d99f8589 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -85,10 +85,10 @@ 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_t v = ATOMIC_INIT(1);
-- 
2.25.0

Re: [PATCH v3 4/5] Documentation/locking/atomic: Add a litmus test for atomic_set()

[Alan Stern]

On Thu, 27 Feb 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.
> 
> Additionally, change the sentences describing the test in atomic_t.txt
> with better wording.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 +++++++++++++++++++
>  Documentation/atomic-tests/README             |  7 ++++++
>  Documentation/atomic_t.txt                    |  6 ++---
>  3 files changed, 34 insertions(+), 3 deletions(-)
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> 
> diff --git a/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus b/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> new file mode 100644
> index 000000000000..5dd7f04e504a
> --- /dev/null
> +++ b/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> @@ -0,0 +1,24 @@
> +C Atomic-set-observable-to-RMW

This line needs to match the filename.  Aside from that,

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


> +
> +(*
> + * 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/atomic-tests/README b/Documentation/atomic-tests/README
> index ae61201a4271..a1b72410b539 100644
> --- a/Documentation/atomic-tests/README
> +++ b/Documentation/atomic-tests/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.
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index ceb85ada378e..67d1d99f8589 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -85,10 +85,10 @@ 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_t v = ATOMIC_INIT(1);
> 

Re: [PATCH v3 4/5] Documentation/locking/atomic: Add a litmus test for atomic_set()

[Andrea Parri]

On Thu, Feb 27, 2020 at 08:40:48AM +0800, 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.
> 
> Additionally, change the sentences describing the test in atomic_t.txt
> with better wording.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 +++++++++++++++++++
>  Documentation/atomic-tests/README             |  7 ++++++
>  Documentation/atomic_t.txt                    |  6 ++---
>  3 files changed, 34 insertions(+), 3 deletions(-)
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> 
> diff --git a/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus b/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> new file mode 100644
> index 000000000000..5dd7f04e504a
> --- /dev/null
> +++ b/Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> @@ -0,0 +1,24 @@
> +C Atomic-set-observable-to-RMW

Nit: s/Atomic-set-observable-to-RMW/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);

Nit: spaces after commas


> +}
> +
> +P1(atomic_t *v)
> +{
> +	atomic_set(v, 0);
> +}
> +
> +exists
> +(v=2)
> diff --git a/Documentation/atomic-tests/README b/Documentation/atomic-tests/README
> index ae61201a4271..a1b72410b539 100644
> --- a/Documentation/atomic-tests/README
> +++ b/Documentation/atomic-tests/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.
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index ceb85ada378e..67d1d99f8589 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -85,10 +85,10 @@ 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_t v = ATOMIC_INIT(1);
> -- 
> 2.25.0
> 

[PATCH v3 5/5] Documentation/locking/atomic: Add a litmus test 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>
---
 ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
 Documentation/atomic-tests/README             |  5 +++
 Documentation/atomic_t.txt                    | 10 +++---
 3 files changed, 42 insertions(+), 5 deletions(-)
 create mode 100644 Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus

diff --git a/Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus b/Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
new file mode 100644
index 000000000000..9a8e31a44b28
--- /dev/null
+++ b/Documentation/atomic-tests/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/atomic-tests/README b/Documentation/atomic-tests/README
index a1b72410b539..714cf93816ea 100644
--- a/Documentation/atomic-tests/README
+++ b/Documentation/atomic-tests/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.
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++;
-- 
2.25.0

Re: [PATCH v3 5/5] Documentation/locking/atomic: Add a litmus test smp_mb__after_atomic()

[Alan Stern]

On Thu, 27 Feb 2020, Boqun Feng wrote:

> 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>


>  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
>  Documentation/atomic-tests/README             |  5 +++
>  Documentation/atomic_t.txt                    | 10 +++---
>  3 files changed, 42 insertions(+), 5 deletions(-)
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
> 
> diff --git a/Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus b/Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
> new file mode 100644
> index 000000000000..9a8e31a44b28
> --- /dev/null
> +++ b/Documentation/atomic-tests/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/atomic-tests/README b/Documentation/atomic-tests/README
> index a1b72410b539..714cf93816ea 100644
> --- a/Documentation/atomic-tests/README
> +++ b/Documentation/atomic-tests/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.
> 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++;
> 

Re: [PATCH v3 0/5] Documentation/locking/atomic: Add litmus tests for atomic APIs

[Paul E. McKenney]

On Thu, Feb 27, 2020 at 08:40:44AM +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/
> 
> Changes since v2:
> 
> *	Change from "RFC" to "PATCH".
> 
> *	Wording improvement in atomic_t.txt as per Alan's suggestion.
> 
> *	Add a new patch describing the usage of atomic_add_unless() is
> 	not limited anymore for LKMM litmus tests.
> 
> My PR on supporting "(void) expr;" statement has been merged by Luc
> (Thank you, Luc). So all the litmus tests in this patchset can be
> handled by the herdtools compiled from latest master branch of the
> source code.
> 
> Comments and suggestions are welcome!
> 
> Regards,
> Boqun

Queued for further review, thank you, Boqun!

							Thanx, Paul

> [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> 
> Boqun Feng (5):
>   tools/memory-model: Add an exception for limitations on _unless()
>     family
>   Documentation/locking/atomic: Fix atomic-set litmus test
>   Documentation/locking/atomic: Introduce atomic-tests directory
>   Documentation/locking/atomic: Add a litmus test for atomic_set()
>   Documentation/locking/atomic: Add a litmus test smp_mb__after_atomic()
> 
>  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
>  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
>  Documentation/atomic-tests/README             | 16 ++++++++++
>  Documentation/atomic_t.txt                    | 24 +++++++-------
>  MAINTAINERS                                   |  1 +
>  tools/memory-model/README                     | 10 ++++--
>  6 files changed, 92 insertions(+), 15 deletions(-)
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
>  create mode 100644 Documentation/atomic-tests/README
> 
> -- 
> 2.25.0
> 

Re: [PATCH v3 0/5] Documentation/locking/atomic: Add litmus tests for atomic APIs

[Andrea Parri]

On Thu, Feb 27, 2020 at 08:40:44AM +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/
> 
> Changes since v2:
> 
> *	Change from "RFC" to "PATCH".
> 
> *	Wording improvement in atomic_t.txt as per Alan's suggestion.
> 
> *	Add a new patch describing the usage of atomic_add_unless() is
> 	not limited anymore for LKMM litmus tests.
> 
> My PR on supporting "(void) expr;" statement has been merged by Luc
> (Thank you, Luc). So all the litmus tests in this patchset can be
> handled by the herdtools compiled from latest master branch of the
> source code.
> 
> Comments and suggestions are welcome!

A few nits (see inline), but otherwise the series looks good to me;
with those fixed, please feel free to add:

Acked-by: Andrea Parri <parri.andrea@gmail.com>

to the entire series.

Thanks,
  Andrea


> 
> Regards,
> Boqun
> 
> [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> 
> Boqun Feng (5):
>   tools/memory-model: Add an exception for limitations on _unless()
>     family
>   Documentation/locking/atomic: Fix atomic-set litmus test
>   Documentation/locking/atomic: Introduce atomic-tests directory
>   Documentation/locking/atomic: Add a litmus test for atomic_set()
>   Documentation/locking/atomic: Add a litmus test smp_mb__after_atomic()
> 
>  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
>  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
>  Documentation/atomic-tests/README             | 16 ++++++++++
>  Documentation/atomic_t.txt                    | 24 +++++++-------
>  MAINTAINERS                                   |  1 +
>  tools/memory-model/README                     | 10 ++++--
>  6 files changed, 92 insertions(+), 15 deletions(-)
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
>  create mode 100644 Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
>  create mode 100644 Documentation/atomic-tests/README
> 
> -- 
> 2.25.0
> 

Re: [PATCH v3 0/5] Documentation/locking/atomic: Add litmus tests for atomic APIs

[Boqun Feng]

On Thu, Feb 27, 2020 at 06:54:41PM +0100, Andrea Parri wrote:
> On Thu, Feb 27, 2020 at 08:40:44AM +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/
> > 
> > Changes since v2:
> > 
> > *	Change from "RFC" to "PATCH".
> > 
> > *	Wording improvement in atomic_t.txt as per Alan's suggestion.
> > 
> > *	Add a new patch describing the usage of atomic_add_unless() is
> > 	not limited anymore for LKMM litmus tests.
> > 
> > My PR on supporting "(void) expr;" statement has been merged by Luc
> > (Thank you, Luc). So all the litmus tests in this patchset can be
> > handled by the herdtools compiled from latest master branch of the
> > source code.
> > 
> > Comments and suggestions are welcome!
> 
> A few nits (see inline), but otherwise the series looks good to me;
> with those fixed, please feel free to add:
> 
> Acked-by: Andrea Parri <parri.andrea@gmail.com>
> 

Thank you and Alan! I will fix those in the next version.

Regards,
Boqun

> to the entire series.
> 
> Thanks,
>   Andrea
> 
> 
> > 
> > Regards,
> > Boqun
> > 
> > [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> > 
> > Boqun Feng (5):
> >   tools/memory-model: Add an exception for limitations on _unless()
> >     family
> >   Documentation/locking/atomic: Fix atomic-set litmus test
> >   Documentation/locking/atomic: Introduce atomic-tests directory
> >   Documentation/locking/atomic: Add a litmus test for atomic_set()
> >   Documentation/locking/atomic: Add a litmus test smp_mb__after_atomic()
> > 
> >  ...ter_atomic-is-stronger-than-acquire.litmus | 32 +++++++++++++++++++
> >  ...c-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++
> >  Documentation/atomic-tests/README             | 16 ++++++++++
> >  Documentation/atomic_t.txt                    | 24 +++++++-------
> >  MAINTAINERS                                   |  1 +
> >  tools/memory-model/README                     | 10 ++++--
> >  6 files changed, 92 insertions(+), 15 deletions(-)
> >  create mode 100644 Documentation/atomic-tests/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
> >  create mode 100644 Documentation/atomic-tests/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> >  create mode 100644 Documentation/atomic-tests/README
> > 
> > -- 
> > 2.25.0
> >