[PATCH memory-model 0/14] LKMM updates for v5.9

[PATCH memory-model 0/14] LKMM updates for v5.9

[Paul E. McKenney]

Hello!

This series contains updates to the Linux-kernel memory model:

1.	tools/memory-model: Add recent references.

2.	tools/memory-model: Fix "conflict" definition, courtesy of
	Marco Elver.

3.	Documentation: LKMM: Add litmus test for RCU GP guarantee where
	updater frees object, courtesy of Joel Fernandes.

4.	Documentation: LKMM: Add litmus test for RCU GP guarantee where
	reader stores, courtesy of Joel Fernandes.

5.	MAINTAINERS: Update maintainers for new Documentation/litmus-tests,
	courtesy of Joel Fernandes.

6.	tools/memory-model: Add an exception for limitations on _unless()
	family, courtesy of Boqun Feng.

7.	Documentation/litmus-tests: Introduce atomic directory, courtesy of
	Boqun Feng.

8.	Documentation/litmus-tests/atomic: Add a test for atomic_set()
	courtesy of Boqun Feng.

9.	Documentation/litmus-tests/atomic: Add a test for
	smp_mb__after_atomic(), courtesy of Boqun Feng.

10.	tools/memory-model: Fix reference to litmus test in recipes.txt
	courtesy of Akira Yokosawa.

11.	Documentation/litmus-tests: Merge atomic's README into top-level
	one, courtesy of Akira Yokosawa.

12.	Documentation/litmus-tests: Cite an RCU litmus test, courtesy of
	Joel Fernandes.

13.	tools/memory-model/README: Expand dependency of klitmus7, courtesy
	of Akira Yokosawa.

14.	fix references for DMA*.txt files, courtesy of Mauro Carvalho Chehab.

							Thanx, Paul

------------------------------------------------------------------------

 /Documentation/litmus-tests/atomic/README                                                       |   16 -
 b/Documentation/atomic_t.txt                                                                    |   24 +-
 b/Documentation/litmus-tests/README                                                             |   34 ++++
 b/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus |   32 +++
 b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus             |   24 ++
 b/Documentation/litmus-tests/atomic/README                                                      |   16 +
 b/Documentation/litmus-tests/rcu/RCU+sync+free.litmus                                           |   42 +++++
 b/Documentation/litmus-tests/rcu/RCU+sync+read.litmus                                           |   37 ++++
 b/Documentation/memory-barriers.txt                                                             |    6 
 b/MAINTAINERS                                                                                   |    2 
 b/tools/memory-model/Documentation/explanation.txt                                              |   83 +++++-----
 b/tools/memory-model/Documentation/recipes.txt                                                  |    2 
 b/tools/memory-model/Documentation/references.txt                                               |   21 ++
 b/tools/memory-model/README                                                                     |   40 ++++
 14 files changed, 302 insertions(+), 77 deletions(-)

[PATCH tip/core/rcu 01/14] tools/memory-model: Add recent references

[paulmck]

From: "Paul E. McKenney" <paulmck@kernel.org>

This commit updates the list of LKMM-related publications in
Documentation/references.txt.

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
---
 tools/memory-model/Documentation/references.txt | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/tools/memory-model/Documentation/references.txt b/tools/memory-model/Documentation/references.txt
index b177f3e..ecbbaa5 100644
--- a/tools/memory-model/Documentation/references.txt
+++ b/tools/memory-model/Documentation/references.txt
@@ -73,6 +73,18 @@ o	Christopher Pulte, Shaked Flur, Will Deacon, Jon French,
 Linux-kernel memory model
 =========================
 
+o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
+	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
+	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
+	2019. "Calibrating your fear of big bad optimizing compilers"
+	Linux Weekly News.  https://lwn.net/Articles/799218/
+
+o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
+	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
+	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
+	2019. "Who's afraid of a big bad optimizing compiler?"
+	Linux Weekly News.  https://lwn.net/Articles/793253/
+
 o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
 	Alan Stern.  2018. "Frightening small children and disconcerting
 	grown-ups: Concurrency in the Linux kernel". In Proceedings of
@@ -88,6 +100,11 @@ o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
 	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 2)"
 	Linux Weekly News.  https://lwn.net/Articles/720550/
 
+o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
+	Alan Stern.  2017-2019.  "A Formal Model of Linux-Kernel Memory
+	Ordering" (backup material for the LWN articles)
+	https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
+
 
 Memory-model tooling
 ====================
@@ -110,5 +127,5 @@ Memory-model comparisons
 ========================
 
 o	Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
-	Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016).
-	http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html.
+	Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
+	http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
-- 
2.9.5

[PATCH tip/core/rcu 02/14] tools/memory-model: Fix "conflict" definition

[paulmck]

From: Marco Elver <elver@google.com>

The definition of "conflict" should not include the type of access nor
whether the accesses are concurrent or not, which this patch addresses.
The definition of "data race" remains unchanged.

The definition of "conflict" as we know it and is cited by various
papers on memory consistency models appeared in [1]: "Two accesses to
the same variable conflict if at least one is a write; two operations
conflict if they execute conflicting accesses."

The LKMM as well as the C11 memory model are adaptations of
data-race-free, which are based on the work in [2]. Necessarily, we need
both conflicting data operations (plain) and synchronization operations
(marked). For example, C11's definition is based on [3], which defines a
"data race" as: "Two memory operations conflict if they access the same
memory location, and at least one of them is a store, atomic store, or
atomic read-modify-write operation. In a sequentially consistent
execution, two memory operations from different threads form a type 1
data race if they conflict, at least one of them is a data operation,
and they are adjacent in <T (i.e., they may be executed concurrently)."

[1] D. Shasha, M. Snir, "Efficient and Correct Execution of Parallel
    Programs that Share Memory", 1988.
	URL: http://snir.cs.illinois.edu/listed/J21.pdf

[2] S. Adve, "Designing Memory Consistency Models for Shared-Memory
    Multiprocessors", 1993.
	URL: http://sadve.cs.illinois.edu/Publications/thesis.pdf

[3] H.-J. Boehm, S. Adve, "Foundations of the C++ Concurrency Memory
    Model", 2008.
	URL: https://www.hpl.hp.com/techreports/2008/HPL-2008-56.pdf

Signed-off-by: Marco Elver <elver@google.com>
Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 tools/memory-model/Documentation/explanation.txt | 83 +++++++++++++-----------
 1 file changed, 45 insertions(+), 38 deletions(-)

diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index e91a2eb..993f800 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -1987,28 +1987,36 @@ outcome undefined.
 
 In technical terms, the compiler is allowed to assume that when the
 program executes, there will not be any data races.  A "data race"
-occurs when two conflicting memory accesses execute concurrently;
-two memory accesses "conflict" if:
+occurs when there are two memory accesses such that:
 
-	they access the same location,
+1.	they access the same location,
 
-	they occur on different CPUs (or in different threads on the
-	same CPU),
+2.	at least one of them is a store,
 
-	at least one of them is a plain access,
+3.	at least one of them is plain,
 
-	and at least one of them is a store.
+4.	they occur on different CPUs (or in different threads on the
+	same CPU), and
 
-The LKMM tries to determine whether a program contains two conflicting
-accesses which may execute concurrently; if it does then the LKMM says
-there is a potential data race and makes no predictions about the
-program's outcome.
+5.	they execute concurrently.
 
-Determining whether two accesses conflict is easy; you can see that
-all the concepts involved in the definition above are already part of
-the memory model.  The hard part is telling whether they may execute
-concurrently.  The LKMM takes a conservative attitude, assuming that
-accesses may be concurrent unless it can prove they cannot.
+In the literature, two accesses are said to "conflict" if they satisfy
+1 and 2 above.  We'll go a little farther and say that two accesses
+are "race candidates" if they satisfy 1 - 4.  Thus, whether or not two
+race candidates actually do race in a given execution depends on
+whether they are concurrent.
+
+The LKMM tries to determine whether a program contains race candidates
+which may execute concurrently; if it does then the LKMM says there is
+a potential data race and makes no predictions about the program's
+outcome.
+
+Determining whether two accesses are race candidates is easy; you can
+see that all the concepts involved in the definition above are already
+part of the memory model.  The hard part is telling whether they may
+execute concurrently.  The LKMM takes a conservative attitude,
+assuming that accesses may be concurrent unless it can prove they
+are not.
 
 If two memory accesses aren't concurrent then one must execute before
 the other.  Therefore the LKMM decides two accesses aren't concurrent
@@ -2171,8 +2179,8 @@ again, now using plain accesses for buf:
 	}
 
 This program does not contain a data race.  Although the U and V
-accesses conflict, the LKMM can prove they are not concurrent as
-follows:
+accesses are race candidates, the LKMM can prove they are not
+concurrent as follows:
 
 	The smp_wmb() fence in P0 is both a compiler barrier and a
 	cumul-fence.  It guarantees that no matter what hash of
@@ -2326,12 +2334,11 @@ could now perform the load of x before the load of ptr (there might be
 a control dependency but no address dependency at the machine level).
 
 Finally, it turns out there is a situation in which a plain write does
-not need to be w-post-bounded: when it is separated from the
-conflicting access by a fence.  At first glance this may seem
-impossible.  After all, to be conflicting the second access has to be
-on a different CPU from the first, and fences don't link events on
-different CPUs.  Well, normal fences don't -- but rcu-fence can!
-Here's an example:
+not need to be w-post-bounded: when it is separated from the other
+race-candidate access by a fence.  At first glance this may seem
+impossible.  After all, to be race candidates the two accesses must
+be on different CPUs, and fences don't link events on different CPUs.
+Well, normal fences don't -- but rcu-fence can!  Here's an example:
 
 	int x, y;
 
@@ -2367,7 +2374,7 @@ concurrent and there is no race, even though P1's plain store to y
 isn't w-post-bounded by any marked accesses.
 
 Putting all this material together yields the following picture.  For
-two conflicting stores W and W', where W ->co W', the LKMM says the
+race-candidate stores W and W', where W ->co W', the LKMM says the
 stores don't race if W can be linked to W' by a
 
 	w-post-bounded ; vis ; w-pre-bounded
@@ -2380,8 +2387,8 @@ sequence, and if W' is plain then they also have to be linked by a
 
 	w-post-bounded ; vis ; r-pre-bounded
 
-sequence.  For a conflicting load R and store W, the LKMM says the two
-accesses don't race if R can be linked to W by an
+sequence.  For race-candidate load R and store W, the LKMM says the
+two accesses don't race if R can be linked to W by an
 
 	r-post-bounded ; xb* ; w-pre-bounded
 
@@ -2413,20 +2420,20 @@ is, the rules governing the memory subsystem's choice of a store to
 satisfy a load request and its determination of where a store will
 fall in the coherence order):
 
-	If R and W conflict and it is possible to link R to W by one
-	of the xb* sequences listed above, then W ->rfe R is not
-	allowed (i.e., a load cannot read from a store that it
+	If R and W are race candidates and it is possible to link R to
+	W by one of the xb* sequences listed above, then W ->rfe R is
+	not allowed (i.e., a load cannot read from a store that it
 	executes before, even if one or both is plain).
 
-	If W and R conflict and it is possible to link W to R by one
-	of the vis sequences listed above, then R ->fre W is not
-	allowed (i.e., if a store is visible to a load then the load
-	must read from that store or one coherence-after it).
+	If W and R are race candidates and it is possible to link W to
+	R by one of the vis sequences listed above, then R ->fre W is
+	not allowed (i.e., if a store is visible to a load then the
+	load must read from that store or one coherence-after it).
 
-	If W and W' conflict and it is possible to link W to W' by one
-	of the vis sequences listed above, then W' ->co W is not
-	allowed (i.e., if one store is visible to a second then the
-	second must come after the first in the coherence order).
+	If W and W' are race candidates and it is possible to link W
+	to W' by one of the vis sequences listed above, then W' ->co W
+	is not allowed (i.e., if one store is visible to a second then
+	the second must come after the first in the coherence order).
 
 This is the extent to which the LKMM deals with plain accesses.
 Perhaps it could say more (for example, plain accesses might
-- 
2.9.5

[PATCH tip/core/rcu 03/14] Documentation: LKMM: Add litmus test for RCU GP guarantee where updater frees object

[paulmck]

From: "Joel Fernandes (Google)" <joel@joelfernandes.org>

This adds an example for the important RCU grace period guarantee, which
shows an RCU reader can never span a grace period.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 .../litmus-tests/rcu/RCU+sync+free.litmus          | 42 ++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 Documentation/litmus-tests/rcu/RCU+sync+free.litmus

diff --git a/Documentation/litmus-tests/rcu/RCU+sync+free.litmus b/Documentation/litmus-tests/rcu/RCU+sync+free.litmus
new file mode 100644
index 0000000..4ee67e1
--- /dev/null
+++ b/Documentation/litmus-tests/rcu/RCU+sync+free.litmus
@@ -0,0 +1,42 @@
+C RCU+sync+free
+
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that an RCU reader can never see a write that
+ * follows a grace period, if it did not see writes that precede that grace
+ * period.
+ *
+ * This is a typical pattern of RCU usage, where the write before the grace
+ * period assigns a pointer, and the writes following the grace period destroy
+ * the object that the pointer used to point to.
+ *
+ * This is one implication of the RCU grace-period guarantee, which says (among
+ * other things) that an RCU read-side critical section cannot span a grace period.
+ *)
+
+{
+int x = 1;
+int *y = &x;
+int z = 1;
+}
+
+P0(int *x, int *z, int **y)
+{
+	int *r0;
+	int r1;
+
+	rcu_read_lock();
+	r0 = rcu_dereference(*y);
+	r1 = READ_ONCE(*r0);
+	rcu_read_unlock();
+}
+
+P1(int *x, int *z, int **y)
+{
+	rcu_assign_pointer(*y, z);
+	synchronize_rcu();
+	WRITE_ONCE(*x, 0);
+}
+
+exists (0:r0=x /\ 0:r1=0)
-- 
2.9.5

[PATCH tip/core/rcu 04/14] Documentation: LKMM: Add litmus test for RCU GP guarantee where reader stores

[paulmck]

From: "Joel Fernandes (Google)" <joel@joelfernandes.org>

This adds an example for the important RCU grace period guarantee, which
shows an RCU reader can never span a grace period.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 Documentation/litmus-tests/README                  | 11 +++++++
 .../litmus-tests/rcu/RCU+sync+read.litmus          | 37 ++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 Documentation/litmus-tests/README
 create mode 100644 Documentation/litmus-tests/rcu/RCU+sync+read.litmus

diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
new file mode 100644
index 0000000..c4307ea
--- /dev/null
+++ b/Documentation/litmus-tests/README
@@ -0,0 +1,11 @@
+============
+LITMUS TESTS
+============
+
+RCU (/rcu directory)
+--------------------
+
+RCU+sync+read.litmus
+RCU+sync+free.litmus
+    Both the above litmus tests demonstrate the RCU grace period guarantee
+    that an RCU read-side critical section can never span a grace period.
diff --git a/Documentation/litmus-tests/rcu/RCU+sync+read.litmus b/Documentation/litmus-tests/rcu/RCU+sync+read.litmus
new file mode 100644
index 0000000..f341767
--- /dev/null
+++ b/Documentation/litmus-tests/rcu/RCU+sync+read.litmus
@@ -0,0 +1,37 @@
+C RCU+sync+read
+
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that after a grace period, an RCU updater always
+ * sees all stores done in prior RCU read-side critical sections. Such
+ * read-side critical sections would have ended before the grace period ended.
+ *
+ * This is one implication of the RCU grace-period guarantee, which says (among
+ * other things) that an RCU read-side critical section cannot span a grace period.
+ *)
+
+{
+int x = 0;
+int y = 0;
+}
+
+P0(int *x, int *y)
+{
+	rcu_read_lock();
+	WRITE_ONCE(*x, 1);
+	WRITE_ONCE(*y, 1);
+	rcu_read_unlock();
+}
+
+P1(int *x, int *y)
+{
+	int r0;
+	int r1;
+
+	r0 = READ_ONCE(*x);
+	synchronize_rcu();
+	r1 = READ_ONCE(*y);
+}
+
+exists (1:r0=1 /\ 1:r1=0)
-- 
2.9.5

[PATCH tip/core/rcu 05/14] MAINTAINERS: Update maintainers for new Documentation/litmus-tests

[paulmck]

From: "Joel Fernandes (Google)" <joel@joelfernandes.org>

This commit adds Joel Fernandes as official LKMM reviewer.

Acked-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
[ paulmck: Apply Joe Perches alphabetization feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 MAINTAINERS | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/MAINTAINERS b/MAINTAINERS
index 68f21d4..696a02f 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -9960,6 +9960,7 @@ M:	Luc Maranget <luc.maranget@inria.fr>
 M:	"Paul E. McKenney" <paulmck@kernel.org>
 R:	Akira Yokosawa <akiyks@gmail.com>
 R:	Daniel Lustig <dlustig@nvidia.com>
+R:	Joel Fernandes <joel@joelfernandes.org>
 L:	linux-kernel@vger.kernel.org
 L:	linux-arch@vger.kernel.org
 S:	Supported
@@ -9968,6 +9969,7 @@ F:	Documentation/atomic_bitops.txt
 F:	Documentation/atomic_t.txt
 F:	Documentation/core-api/atomic_ops.rst
 F:	Documentation/core-api/refcount-vs-atomic.rst
+F:	Documentation/litmus-tests/
 F:	Documentation/memory-barriers.txt
 F:	tools/memory-model/
 
-- 
2.9.5

[PATCH tip/core/rcu 06/14] tools/memory-model: Add an exception for limitations on _unless() family

[paulmck]

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

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>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 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 fc07b52..b9c562e 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.9.5

[PATCH tip/core/rcu 07/14] Documentation/litmus-tests: Introduce atomic directory

[paulmck]

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

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.

Acked-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 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 0000000..ae61201
--- /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.9.5

[PATCH tip/core/rcu 08/14] Documentation/litmus-tests/atomic: Add a test for atomic_set()

[paulmck]

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

[PATCH tip/core/rcu 09/14] Documentation/litmus-tests/atomic: Add a test for smp_mb__after_atomic()

[paulmck]

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

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.

Acked-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
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                         | 10 +++----
 ...b__after_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 67d1d99f..0f1fded 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 0000000..9a8e31a
--- /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 a1b7241..714cf93 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.9.5

[PATCH tip/core/rcu 10/14] tools/memory-model: Fix reference to litmus test in recipes.txt

[paulmck]

From: Akira Yokosawa <akiyks@gmail.com>

The name of litmus test doesn't match the one described below.
Fix the name of litmus test.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 tools/memory-model/Documentation/recipes.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt
index 7fe8d7a..63c4adf 100644
--- a/tools/memory-model/Documentation/recipes.txt
+++ b/tools/memory-model/Documentation/recipes.txt
@@ -126,7 +126,7 @@ However, it is not necessarily the case that accesses ordered by
 locking will be seen as ordered by CPUs not holding that lock.
 Consider this example:
 
-	/* See Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus. */
+	/* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */
 	void CPU0(void)
 	{
 		spin_lock(&mylock);
-- 
2.9.5

[PATCH tip/core/rcu 11/14] Documentation/litmus-tests: Merge atomic's README into top-level one

[paulmck]

From: Akira Yokosawa <akiyks@gmail.com>

Where Documentation/litmus-tests/README lists RCU litmus tests,
Documentation/litmus-tests/atomic/README lists atomic litmus tests.
For symmetry, merge the latter into former, with some context
adjustment in the introduction.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Acked-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 Documentation/litmus-tests/README        | 19 +++++++++++++++++++
 Documentation/litmus-tests/atomic/README | 16 ----------------
 2 files changed, 19 insertions(+), 16 deletions(-)
 delete mode 100644 Documentation/litmus-tests/atomic/README

diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index c4307ea..ac0b270 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -2,6 +2,25 @@
 LITMUS TESTS
 ============
 
+Each subdirectory contains litmus tests that are typical to describe the
+semantics of respective kernel 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.
+
+
+atomic (/atomic derectory)
+--------------------------
+
+Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
+    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.
+
+
 RCU (/rcu directory)
 --------------------
 
diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README
deleted file mode 100644
index 714cf93..0000000
--- a/Documentation/litmus-tests/atomic/README
+++ /dev/null
@@ -1,16 +0,0 @@
-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+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.9.5

[PATCH tip/core/rcu 12/14] Documentation/litmus-tests: Cite an RCU litmus test

[paulmck]

From: "Joel Fernandes (Google)" <joel@joelfernandes.org>

This commit cites a pertinent RCU-related litmus test.

Co-developed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Co-developed-by: Akira Yokosawa <akiyks@gmail.com>
[Alan: grammar nit]
[ paulmck: Update commit log and title per Akira feedback. ]
Suggested-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 Documentation/litmus-tests/README | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index ac0b270..b79e640 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -24,6 +24,10 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
 RCU (/rcu directory)
 --------------------
 
+MP+onceassign+derefonce.litmus (under tools/memory-model/litmus-tests/)
+    Demonstrates the use of rcu_assign_pointer() and rcu_dereference() to
+    ensure that an RCU reader will not see pre-initialization garbage.
+
 RCU+sync+read.litmus
 RCU+sync+free.litmus
     Both the above litmus tests demonstrate the RCU grace period guarantee
-- 
2.9.5

[PATCH tip/core/rcu 13/14] tools/memory-model/README: Expand dependency of klitmus7

[paulmck]

From: Akira Yokosawa <akiyks@gmail.com>

klitmus7 is independent of the memory model but depends on the
build-target kernel release.
It occasionally lost compatibility due to kernel API changes [1, 2, 3].
It was remedied in a backwards-compatible manner respectively [4, 5, 6].

Reflect this fact in README.

[1]: b899a850431e ("compiler.h: Remove ACCESS_ONCE()")
[2]: 0bb95f80a38f ("Makefile: Globally enable VLA warning")
[3]: d56c0d45f0e2 ("proc: decouple proc from VFS with "struct proc_ops"")
[4]: https://github.com/herd/herdtools7/commit/e87d7f9287d1
     ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated ACCESS_ONCE")
[5]: https://github.com/herd/herdtools7/commit/a0cbb10d02be
     ("klitmus: Avoid variable length array")
[6]: https://github.com/herd/herdtools7/commit/46b9412d3a58
     ("klitmus: Linux kernel v5.6.x compat")

NOTE: [5] was ahead of herdtools7 7.53, which did not make an
official release.  Code generated by klitmus7 without [5] can still be
built targeting Linux 4.20--5.5 if you don't care VLA warnings.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 tools/memory-model/README | 30 ++++++++++++++++++++++++++++--
 1 file changed, 28 insertions(+), 2 deletions(-)

diff --git a/tools/memory-model/README b/tools/memory-model/README
index b9c562e..90af203 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -28,8 +28,34 @@ downloaded separately:
 See "herdtools7/INSTALL.md" for installation instructions.
 
 Note that although these tools usually provide backwards compatibility,
-this is not absolutely guaranteed.  Therefore, if a later version does
-not work, please try using the exact version called out above.
+this is not absolutely guaranteed.
+
+For example, a future version of herd7 might not work with the model
+in this release.  A compatible model will likely be made available in
+a later release of Linux kernel.
+
+If you absolutely need to run the model in this particular release,
+please try using the exact version called out above.
+
+klitmus7 is independent of the model provided here.  It has its own
+dependency on a target kernel release where converted code is built
+and executed.  Any change in kernel APIs essential to klitmus7 will
+necessitate an upgrade of klitmus7.
+
+If you find any compatibility issues in klitmus7, please inform the
+memory model maintainers.
+
+klitmus7 Compatibility Table
+----------------------------
+
+	============  ==========
+	target Linux  herdtools7
+	------------  ----------
+	     -- 4.18  7.48 --
+	4.15 -- 4.19  7.49 --
+	4.20 -- 5.5   7.54 --
+	5.6  --       HEAD
+	============  ==========
 
 
 ==================
-- 
2.9.5

[PATCH tip/core/rcu 14/14] docs: fix references for DMA*.txt files

[paulmck]

From: Mauro Carvalho Chehab <mchehab+huawei@kernel.org>

As we moved those files to core-api, fix references to point
to their newer locations.

Signed-off-by: Mauro Carvalho Chehab <mchehab+huawei@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
 Documentation/memory-barriers.txt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index eaabc31..0e4947a 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -546,8 +546,8 @@ There are certain things that the Linux kernel memory barriers do not guarantee:
 	[*] For information on bus mastering DMA and coherency please read:
 
 	    Documentation/driver-api/pci/pci.rst
-	    Documentation/DMA-API-HOWTO.txt
-	    Documentation/DMA-API.txt
+	    Documentation/core-api/dma-api-howto.rst
+	    Documentation/core-api/dma-api.rst
 
 
 DATA DEPENDENCY BARRIERS (HISTORICAL)
@@ -1932,7 +1932,7 @@ There are some more advanced barrier functions:
      here.
 
      See the subsection "Kernel I/O barrier effects" for more information on
-     relaxed I/O accessors and the Documentation/DMA-API.txt file for more
+     relaxed I/O accessors and the Documentation/core-api/dma-api.rst file for more
      information on consistent memory.
 
 
-- 
2.9.5

Re: [PATCH tip/core/rcu 13/14] tools/memory-model/README: Expand dependency of klitmus7

[Akira Yokosawa]

On Mon, 22 Jun 2020 17:52:30 -0700, paulmck@kernel.org wrote:
> From: Akira Yokosawa <akiyks@gmail.com>
> 
> klitmus7 is independent of the memory model but depends on the
> build-target kernel release.
> It occasionally lost compatibility due to kernel API changes [1, 2, 3].
> It was remedied in a backwards-compatible manner respectively [4, 5, 6].
> 
> Reflect this fact in README.
> 
> [1]: b899a850431e ("compiler.h: Remove ACCESS_ONCE()")
> [2]: 0bb95f80a38f ("Makefile: Globally enable VLA warning")
> [3]: d56c0d45f0e2 ("proc: decouple proc from VFS with "struct proc_ops"")
> [4]: https://github.com/herd/herdtools7/commit/e87d7f9287d1
>      ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated ACCESS_ONCE")
> [5]: https://github.com/herd/herdtools7/commit/a0cbb10d02be
>      ("klitmus: Avoid variable length array")
> [6]: https://github.com/herd/herdtools7/commit/46b9412d3a58
>      ("klitmus: Linux kernel v5.6.x compat")
> 
> NOTE: [5] was ahead of herdtools7 7.53, which did not make an
> official release.  Code generated by klitmus7 without [5] can still be
> built targeting Linux 4.20--5.5 if you don't care VLA warnings.
> 
> Acked-by: Andrea Parri <parri.andrea@gmail.com>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> ---
>  tools/memory-model/README | 30 ++++++++++++++++++++++++++++--
>  1 file changed, 28 insertions(+), 2 deletions(-)
> 
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index b9c562e..90af203 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -28,8 +28,34 @@ downloaded separately:
>  See "herdtools7/INSTALL.md" for installation instructions.
>  
>  Note that although these tools usually provide backwards compatibility,
> -this is not absolutely guaranteed.  Therefore, if a later version does
> -not work, please try using the exact version called out above.
> +this is not absolutely guaranteed.
> +
> +For example, a future version of herd7 might not work with the model
> +in this release.  A compatible model will likely be made available in
> +a later release of Linux kernel.
> +
> +If you absolutely need to run the model in this particular release,
> +please try using the exact version called out above.
> +
> +klitmus7 is independent of the model provided here.  It has its own
> +dependency on a target kernel release where converted code is built
> +and executed.  Any change in kernel APIs essential to klitmus7 will
> +necessitate an upgrade of klitmus7.
> +
> +If you find any compatibility issues in klitmus7, please inform the
> +memory model maintainers.
> +
> +klitmus7 Compatibility Table
> +----------------------------
> +
> +	============  ==========
> +	target Linux  herdtools7
> +	------------  ----------
> +	     -- 4.18  7.48 --
> +	4.15 -- 4.19  7.49 --
> +	4.20 -- 5.5   7.54 --
> +	5.6  --       HEAD
> +	============  ==========

Paul,

I was planning to send an update on this one.
herdtoolds7 7.56 will be released later this week (now tagged 7.56-rc1).

Andrea tested klitmus7 7.56-rc1 against Linux 5.7 and 5.8-rc1.
I tested it against Linux 5.7.4.
klitmus7 worked fine in all these test.

So I think we can safely update the bottom row of the table as:

> +	5.6  --       7.56 --

Can you amend this one directly?
Or do you want me to send a follow-up patch?

        Thanks, Akira

>  
>  
>  ==================
> 

Re: [PATCH tip/core/rcu 13/14] tools/memory-model/README: Expand dependency of klitmus7

[Paul E. McKenney]

On Tue, Jun 23, 2020 at 11:37:32PM +0900, Akira Yokosawa wrote:
> On Mon, 22 Jun 2020 17:52:30 -0700, paulmck@kernel.org wrote:
> > From: Akira Yokosawa <akiyks@gmail.com>
> > 
> > klitmus7 is independent of the memory model but depends on the
> > build-target kernel release.
> > It occasionally lost compatibility due to kernel API changes [1, 2, 3].
> > It was remedied in a backwards-compatible manner respectively [4, 5, 6].
> > 
> > Reflect this fact in README.
> > 
> > [1]: b899a850431e ("compiler.h: Remove ACCESS_ONCE()")
> > [2]: 0bb95f80a38f ("Makefile: Globally enable VLA warning")
> > [3]: d56c0d45f0e2 ("proc: decouple proc from VFS with "struct proc_ops"")
> > [4]: https://github.com/herd/herdtools7/commit/e87d7f9287d1
> >      ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated ACCESS_ONCE")
> > [5]: https://github.com/herd/herdtools7/commit/a0cbb10d02be
> >      ("klitmus: Avoid variable length array")
> > [6]: https://github.com/herd/herdtools7/commit/46b9412d3a58
> >      ("klitmus: Linux kernel v5.6.x compat")
> > 
> > NOTE: [5] was ahead of herdtools7 7.53, which did not make an
> > official release.  Code generated by klitmus7 without [5] can still be
> > built targeting Linux 4.20--5.5 if you don't care VLA warnings.
> > 
> > Acked-by: Andrea Parri <parri.andrea@gmail.com>
> > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > ---
> >  tools/memory-model/README | 30 ++++++++++++++++++++++++++++--
> >  1 file changed, 28 insertions(+), 2 deletions(-)
> > 
> > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > index b9c562e..90af203 100644
> > --- a/tools/memory-model/README
> > +++ b/tools/memory-model/README
> > @@ -28,8 +28,34 @@ downloaded separately:
> >  See "herdtools7/INSTALL.md" for installation instructions.
> >  
> >  Note that although these tools usually provide backwards compatibility,
> > -this is not absolutely guaranteed.  Therefore, if a later version does
> > -not work, please try using the exact version called out above.
> > +this is not absolutely guaranteed.
> > +
> > +For example, a future version of herd7 might not work with the model
> > +in this release.  A compatible model will likely be made available in
> > +a later release of Linux kernel.
> > +
> > +If you absolutely need to run the model in this particular release,
> > +please try using the exact version called out above.
> > +
> > +klitmus7 is independent of the model provided here.  It has its own
> > +dependency on a target kernel release where converted code is built
> > +and executed.  Any change in kernel APIs essential to klitmus7 will
> > +necessitate an upgrade of klitmus7.
> > +
> > +If you find any compatibility issues in klitmus7, please inform the
> > +memory model maintainers.
> > +
> > +klitmus7 Compatibility Table
> > +----------------------------
> > +
> > +	============  ==========
> > +	target Linux  herdtools7
> > +	------------  ----------
> > +	     -- 4.18  7.48 --
> > +	4.15 -- 4.19  7.49 --
> > +	4.20 -- 5.5   7.54 --
> > +	5.6  --       HEAD
> > +	============  ==========
> 
> Paul,
> 
> I was planning to send an update on this one.
> herdtoolds7 7.56 will be released later this week (now tagged 7.56-rc1).
> 
> Andrea tested klitmus7 7.56-rc1 against Linux 5.7 and 5.8-rc1.
> I tested it against Linux 5.7.4.
> klitmus7 worked fine in all these test.
> 
> So I think we can safely update the bottom row of the table as:
> 
> > +	5.6  --       7.56 --
> 
> Can you amend this one directly?
> Or do you want me to send a follow-up patch?

A follow-up patch is probably best.  This can't be the only place that
must change?  Or maybe we set this up better than I remember?  ;-)

							Thanx, Paul

[PATCH 1/2] tools/memory-model/README: Mention herdtools7 7.56 in compatibility table

[Akira Yokosawa]

From 89f96cba0db5643b1d22a0fe740f4c5cac788b29 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 24 Jun 2020 06:56:43 +0900
Subject: [PATCH 1/2] tools/memory-model/README: Mention herdtools7 7.56 in compatibility table

herdtools7 7.56 is going to be released in the week of 22 Jun 2020.
Mention the exact version in the compatibility table.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 tools/memory-model/README | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/memory-model/README b/tools/memory-model/README
index 90af203c3cf1..ecb7385376bf 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -54,7 +54,7 @@ klitmus7 Compatibility Table
 	     -- 4.18  7.48 --
 	4.15 -- 4.19  7.49 --
 	4.20 -- 5.5   7.54 --
-	5.6  --       HEAD
+	5.6  --       7.56 --
 	============  ==========
 
 
-- 
2.17.1

[PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test

[Akira Yokosawa]

From f808c371075d2f92b955da1a83ecb3828db1972e Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 24 Jun 2020 06:59:26 +0900
Subject: [PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test

herdtools 7.56 has enhanced herd7's C parser so that the "(void)expr"
construct in Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus is
accepted.

This is independent of LKMM's cat model, so mention the required
version in the header of the litmus test and its entry in README.

CC: Boqun Feng <boqun.feng@gmail.com>
Reported-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 Documentation/litmus-tests/README                                | 1 +
 .../atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus       | 1 +
 2 files changed, 2 insertions(+)

diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index b79e640214b9..7f5c6c3ed6c3 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -19,6 +19,7 @@ Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
 
 Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
     Test that atomic_set() cannot break the atomicity of atomic RMWs.
+    NOTE: Require herd7 7.56 or later which supports "(void)expr".
 
 
 RCU (/rcu directory)
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
index 49385314d911..ffd4d3e79c4a 100644
--- 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
@@ -4,6 +4,7 @@ C Atomic-RMW-ops-are-atomic-WRT-atomic_set
  * Result: Never
  *
  * Test that atomic_set() cannot break the atomicity of atomic RMWs.
+ * NOTE: This requires herd7 7.56 or later which supports "(void)expr".
  *)
 
 {
-- 
2.17.1

Re: [PATCH 1/2] tools/memory-model/README: Mention herdtools7 7.56 in compatibility table

[Andrea Parri]

On Wed, Jun 24, 2020 at 07:06:02AM +0900, Akira Yokosawa wrote:
> From 89f96cba0db5643b1d22a0fe740f4c5cac788b29 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Wed, 24 Jun 2020 06:56:43 +0900
> Subject: [PATCH 1/2] tools/memory-model/README: Mention herdtools7 7.56 in compatibility table
> 
> herdtools7 7.56 is going to be released in the week of 22 Jun 2020.
> Mention the exact version in the compatibility table.
> 
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>

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

  Andrea


> ---
>  tools/memory-model/README | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index 90af203c3cf1..ecb7385376bf 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -54,7 +54,7 @@ klitmus7 Compatibility Table
>  	     -- 4.18  7.48 --
>  	4.15 -- 4.19  7.49 --
>  	4.20 -- 5.5   7.54 --
> -	5.6  --       HEAD
> +	5.6  --       7.56 --
>  	============  ==========
>  
>  
> -- 
> 2.17.1
> 
> 

Re: [PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test

[Andrea Parri]

On Wed, Jun 24, 2020 at 07:09:01AM +0900, Akira Yokosawa wrote:
> From f808c371075d2f92b955da1a83ecb3828db1972e Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Wed, 24 Jun 2020 06:59:26 +0900
> Subject: [PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test
> 
> herdtools 7.56 has enhanced herd7's C parser so that the "(void)expr"
> construct in Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus is
> accepted.
> 
> This is independent of LKMM's cat model, so mention the required
> version in the header of the litmus test and its entry in README.
> 
> CC: Boqun Feng <boqun.feng@gmail.com>
> Reported-by: Andrea Parri <parri.andrea@gmail.com>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>

Frankly, I was hoping that we could simply bump the herd7 version in
tools/memory-model/README; I understand your point, but I admit that
I haven't being playing with 7.52 for a while now...

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

  Andrea


> ---
>  Documentation/litmus-tests/README                                | 1 +
>  .../atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus       | 1 +
>  2 files changed, 2 insertions(+)
> 
> diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
> index b79e640214b9..7f5c6c3ed6c3 100644
> --- a/Documentation/litmus-tests/README
> +++ b/Documentation/litmus-tests/README
> @@ -19,6 +19,7 @@ Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
>  
>  Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
>      Test that atomic_set() cannot break the atomicity of atomic RMWs.
> +    NOTE: Require herd7 7.56 or later which supports "(void)expr".
>  
>  
>  RCU (/rcu directory)
> 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
> index 49385314d911..ffd4d3e79c4a 100644
> --- 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
> @@ -4,6 +4,7 @@ C Atomic-RMW-ops-are-atomic-WRT-atomic_set
>   * Result: Never
>   *
>   * Test that atomic_set() cannot break the atomicity of atomic RMWs.
> + * NOTE: This requires herd7 7.56 or later which supports "(void)expr".
>   *)
>  
>  {
> -- 
> 2.17.1
> 
> 

Re: [PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test

[Paul E. McKenney]

On Wed, Jun 24, 2020 at 01:24:25AM +0200, Andrea Parri wrote:
> On Wed, Jun 24, 2020 at 07:09:01AM +0900, Akira Yokosawa wrote:
> > From f808c371075d2f92b955da1a83ecb3828db1972e Mon Sep 17 00:00:00 2001
> > From: Akira Yokosawa <akiyks@gmail.com>
> > Date: Wed, 24 Jun 2020 06:59:26 +0900
> > Subject: [PATCH 2/2] Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test
> > 
> > herdtools 7.56 has enhanced herd7's C parser so that the "(void)expr"
> > construct in Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus is
> > accepted.
> > 
> > This is independent of LKMM's cat model, so mention the required
> > version in the header of the litmus test and its entry in README.
> > 
> > CC: Boqun Feng <boqun.feng@gmail.com>
> > Reported-by: Andrea Parri <parri.andrea@gmail.com>
> > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> 
> Frankly, I was hoping that we could simply bump the herd7 version in
> tools/memory-model/README; I understand your point, but I admit that
> I haven't being playing with 7.52 for a while now...

Maybe in a few years it will no longer be relevant, and could then
be removed?

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

I queued both, thank you both!

						Thanx, Paul

>   Andrea
> 
> 
> > ---
> >  Documentation/litmus-tests/README                                | 1 +
> >  .../atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus       | 1 +
> >  2 files changed, 2 insertions(+)
> > 
> > diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
> > index b79e640214b9..7f5c6c3ed6c3 100644
> > --- a/Documentation/litmus-tests/README
> > +++ b/Documentation/litmus-tests/README
> > @@ -19,6 +19,7 @@ Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
> >  
> >  Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
> >      Test that atomic_set() cannot break the atomicity of atomic RMWs.
> > +    NOTE: Require herd7 7.56 or later which supports "(void)expr".
> >  
> >  
> >  RCU (/rcu directory)
> > 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
> > index 49385314d911..ffd4d3e79c4a 100644
> > --- 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
> > @@ -4,6 +4,7 @@ C Atomic-RMW-ops-are-atomic-WRT-atomic_set
> >   * Result: Never
> >   *
> >   * Test that atomic_set() cannot break the atomicity of atomic RMWs.
> > + * NOTE: This requires herd7 7.56 or later which supports "(void)expr".
> >   *)
> >  
> >  {
> > -- 
> > 2.17.1
> > 
> >