[PATCH RFC tools/lkmm] Miscellaneous fixes

[PATCH RFC tools/lkmm] Miscellaneous fixes

[Paul E. McKenney]

Hello!

This RFC series adds some miscellaneous updates to the Linux kernel
memory model:

1.	Clarify the origin and scope of the tool name to avoid confusion
	between "memory model" and "memory management", courtesy of
	Andrea Parri.

2.	Move the maintainer list for LKMM to the main MAINTAINERS file,
	courtesy of Andrea Parri.

3.	Add memory-barriers.txt to the LKMM MAINTAINERS entry, courtesy
	of Andrea Parri.

4.	Add comments explaining the purpose of the various litmus tests.

5.	Fix puntuation errors in litmus-tests/README.

6.	Add LKMM acronym to MAINTAINERS entry.  If there are no objections,
	this will be squashed with #3 above.

7.	Add Akira Yokosawa as an LKMM reviewer.

8-10.	Replace underscores with hyphens for smp_mb__*() workings.  Note that
	this patch leaves rb_dep alone because the underscore is set by herd7.
	If there are no objections, these will be squashed together.

							Thanx, Paul

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

 /tools/memory-model/MAINTAINERS                                                            |   15 -------
 b/MAINTAINERS                                                                              |   20 +++++++++-
 b/tools/memory-model/MAINTAINERS                                                           |    2 -
 b/tools/memory-model/README                                                                |   14 +++----
 b/tools/memory-model/linux-kernel.bell                                                     |    8 ++--
 b/tools/memory-model/linux-kernel.cat                                                      |    8 ++--
 b/tools/memory-model/linux-kernel.def                                                      |    6 +--
 b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus                              |    7 +++
 b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus                              |    7 +++
 b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus                              |    7 +++
 b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus                                   |    7 +++
 b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus                         |   10 +++++
 b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus                         |   10 +++++
 b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus                                  |    9 ++++
 b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus |   11 +++++
 b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus                        |   11 +++++
 b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus                    |    8 ++++
 b/tools/memory-model/litmus-tests/LB+poonceonces.litmus                                    |    7 +++
 b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus                           |   11 +++++
 b/tools/memory-model/litmus-tests/MP+polocks.litmus                                        |   11 +++++
 b/tools/memory-model/litmus-tests/MP+poonceonces.litmus                                    |    7 +++
 b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus                    |    8 ++++
 b/tools/memory-model/litmus-tests/MP+porevlocks.litmus                                     |   11 +++++
 b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus                        |    8 ++++
 b/tools/memory-model/litmus-tests/R+mbonceonces.litmus                                     |    9 ++++
 b/tools/memory-model/litmus-tests/R+poonceonces.litmus                                     |    8 ++++
 b/tools/memory-model/litmus-tests/README                                                   |    4 +-
 b/tools/memory-model/litmus-tests/S+poonceonces.litmus                                     |    9 ++++
 b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus                       |    7 +++
 b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus                                    |    9 ++++
 b/tools/memory-model/litmus-tests/SB+poonceonces.litmus                                    |    8 ++++
 b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus                              |    8 ++++
 b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus                |    8 ++++
 b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus               |    9 ++++
 b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus               |    8 ++++
 b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus    |   14 +++++++
 36 files changed, 286 insertions(+), 38 deletions(-)

[PATCH RFC tip/lkmm 01/10] tools/memory-model: Clarify the origin/scope of the tool name

[Paul E. McKenney]

From: Andrea Parri <parri.andrea@gmail.com>

Ingo pointed out that:

  "The "memory model" name is overly generic, ambiguous and somewhat
   misleading, as we usually mean the virtual memory layout/model
   when we say "memory model". GCC too uses it in that sense [...]"

Make it clear that tools/memory-model/ uses the term "memory model" as
shorthand for "memory consistency model" by calling out this convention
in tools/memory-model/README.

Stick to the original "memory model" term in sources' headers and for
the subsystem name.

Suggested-by: Ingo Molnar <mingo@kernel.org>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/MAINTAINERS       |  2 +-
 tools/memory-model/README            | 14 +++++++-------
 tools/memory-model/linux-kernel.bell |  2 +-
 tools/memory-model/linux-kernel.cat  |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/tools/memory-model/MAINTAINERS b/tools/memory-model/MAINTAINERS
index 711cbe72d606..db3bd3fc0435 100644
--- a/tools/memory-model/MAINTAINERS
+++ b/tools/memory-model/MAINTAINERS
@@ -1,4 +1,4 @@
-LINUX KERNEL MEMORY MODEL
+LINUX KERNEL MEMORY CONSISTENCY MODEL
 M:	Alan Stern <stern@rowland.harvard.edu>
 M:	Andrea Parri <parri.andrea@gmail.com>
 M:	Will Deacon <will.deacon@arm.com>
diff --git a/tools/memory-model/README b/tools/memory-model/README
index 43ba49492111..91414a49fac5 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -1,15 +1,15 @@
-			=========================
-			LINUX KERNEL MEMORY MODEL
-			=========================
+		=====================================
+		LINUX KERNEL MEMORY CONSISTENCY MODEL
+		=====================================
 
 ============
 INTRODUCTION
 ============
 
-This directory contains the memory model of the Linux kernel, written
-in the "cat" language and executable by the (externally provided)
-"herd7" simulator, which exhaustively explores the state space of
-small litmus tests.
+This directory contains the memory consistency model (memory model, for
+short) of the Linux kernel, written in the "cat" language and executable
+by the externally provided "herd7" simulator, which exhaustively explores
+the state space of small litmus tests.
 
 In addition, the "klitmus7" tool (also externally provided) may be used
 to convert a litmus test to a Linux kernel module, which in turn allows
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 57112505f5e0..b984bbda01a5 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -11,7 +11,7 @@
  * which is to appear in ASPLOS 2018.
  *)
 
-"Linux kernel memory model"
+"Linux-kernel memory consistency model"
 
 enum Accesses = 'once (*READ_ONCE,WRITE_ONCE,ACCESS_ONCE*) ||
 		'release (*smp_store_release*) ||
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 15b7a5dd8a9a..babe2b3b0bb3 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -11,7 +11,7 @@
  * which is to appear in ASPLOS 2018.
  *)
 
-"Linux kernel memory model"
+"Linux-kernel memory consistency model"
 
 (*
  * File "lock.cat" handles locks and is experimental.
-- 
2.5.2

[PATCH RFC tip/lkmm 02/10] MAINTAINERS: Add the Memory Consistency Model subsystem

[Paul E. McKenney]

From: Andrea Parri <parri.andrea@gmail.com>

Move the contents of tools/memory-model/MAINTAINERS into the main
MAINTAINERS file, removing tools/memory-model/MAINTAINERS. This
allows get_maintainer.pl to correctly identify the maintainers of
tools/memory-model/.

Suggested-by: Ingo Molnar <mingo@kernel.org>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 MAINTAINERS                    | 16 ++++++++++++++++
 tools/memory-model/MAINTAINERS | 15 ---------------
 2 files changed, 16 insertions(+), 15 deletions(-)
 delete mode 100644 tools/memory-model/MAINTAINERS

diff --git a/MAINTAINERS b/MAINTAINERS
index e3581413420c..ba4dc08fbe95 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8086,6 +8086,22 @@ M:	Kees Cook <keescook@chromium.org>
 S:	Maintained
 F:	drivers/misc/lkdtm*
 
+LINUX KERNEL MEMORY CONSISTENCY MODEL
+M:	Alan Stern <stern@rowland.harvard.edu>
+M:	Andrea Parri <parri.andrea@gmail.com>
+M:	Will Deacon <will.deacon@arm.com>
+M:	Peter Zijlstra <peterz@infradead.org>
+M:	Boqun Feng <boqun.feng@gmail.com>
+M:	Nicholas Piggin <npiggin@gmail.com>
+M:	David Howells <dhowells@redhat.com>
+M:	Jade Alglave <j.alglave@ucl.ac.uk>
+M:	Luc Maranget <luc.maranget@inria.fr>
+M:	"Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
+L:	linux-kernel@vger.kernel.org
+S:	Supported
+T:	git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
+F:	tools/memory-model/
+
 LINUX SECURITY MODULE (LSM) FRAMEWORK
 M:	Chris Wright <chrisw@sous-sol.org>
 L:	linux-security-module@vger.kernel.org
diff --git a/tools/memory-model/MAINTAINERS b/tools/memory-model/MAINTAINERS
deleted file mode 100644
index db3bd3fc0435..000000000000
--- a/tools/memory-model/MAINTAINERS
+++ /dev/null
@@ -1,15 +0,0 @@
-LINUX KERNEL MEMORY CONSISTENCY MODEL
-M:	Alan Stern <stern@rowland.harvard.edu>
-M:	Andrea Parri <parri.andrea@gmail.com>
-M:	Will Deacon <will.deacon@arm.com>
-M:	Peter Zijlstra <peterz@infradead.org>
-M:	Boqun Feng <boqun.feng@gmail.com>
-M:	Nicholas Piggin <npiggin@gmail.com>
-M:	David Howells <dhowells@redhat.com>
-M:	Jade Alglave <j.alglave@ucl.ac.uk>
-M:	Luc Maranget <luc.maranget@inria.fr>
-M:	"Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
-L:	linux-kernel@vger.kernel.org
-S:	Supported
-T:	git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
-F:	tools/memory-model/
-- 
2.5.2

[PATCH RFC tip/lkmm 03/10] MAINTAINERS: List file memory-barriers.txt within the LKMM entry

[Paul E. McKenney]

From: Andrea Parri <parri.andrea@gmail.com>

We now have a shiny new Linux-kernel memory model (LKMM) and the old
tried-and-true Documentation/memory-barrier.txt.  It would be good to
keep these automatically synchronized, but in the meantime we need at
least let people know that they are related.  Will suggested adding the
Documentation/memory-barrier.txt file to the LKMM maintainership list,
thus making the LKMM maintainers responsible for both the old and the new.
This commit follows Will's excellent suggestion.

Suggested-by: Will Deacon <will.deacon@arm.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 MAINTAINERS | 1 +
 1 file changed, 1 insertion(+)

diff --git a/MAINTAINERS b/MAINTAINERS
index ba4dc08fbe95..e6ad9b44e8fb 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8101,6 +8101,7 @@ L:	linux-kernel@vger.kernel.org
 S:	Supported
 T:	git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
 F:	tools/memory-model/
+F:	Documentation/memory-barriers.txt
 
 LINUX SECURITY MODULE (LSM) FRAMEWORK
 M:	Chris Wright <chrisw@sous-sol.org>
-- 
2.5.2

[PATCH RFC tip/lkmm 04/10] EXP litmus_tests: Add comments explaining tests' purposes

[Paul E. McKenney]

This commit adds comments to the litmus tests summarizing what these
tests are intended to demonstrate.

Suggested-by: Ingo Molnar <mingo@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
[ paulmck: Apply Andrea's and Alan's feedback. ]
---
 .../memory-model/litmus-tests/CoRR+poonceonce+Once.litmus  |  7 +++++++
 .../memory-model/litmus-tests/CoRW+poonceonce+Once.litmus  |  7 +++++++
 .../memory-model/litmus-tests/CoWR+poonceonce+Once.litmus  |  7 +++++++
 tools/memory-model/litmus-tests/CoWW+poonceonce.litmus     |  7 +++++++
 .../litmus-tests/IRIW+mbonceonces+OnceOnce.litmus          | 10 ++++++++++
 .../litmus-tests/IRIW+poonceonces+OnceOnce.litmus          | 10 ++++++++++
 tools/memory-model/litmus-tests/ISA2+poonceonces.litmus    |  9 +++++++++
 ...SA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 11 +++++++++++
 .../litmus-tests/LB+ctrlonceonce+mbonceonce.litmus         | 11 +++++++++++
 .../litmus-tests/LB+poacquireonce+pooncerelease.litmus     |  8 ++++++++
 tools/memory-model/litmus-tests/LB+poonceonces.litmus      |  7 +++++++
 .../litmus-tests/MP+onceassign+derefonce.litmus            | 11 ++++++++++-
 tools/memory-model/litmus-tests/MP+polocks.litmus          | 11 +++++++++++
 tools/memory-model/litmus-tests/MP+poonceonces.litmus      |  7 +++++++
 .../litmus-tests/MP+pooncerelease+poacquireonce.litmus     |  8 ++++++++
 tools/memory-model/litmus-tests/MP+porevlocks.litmus       | 11 +++++++++++
 .../litmus-tests/MP+wmbonceonce+rmbonceonce.litmus         |  8 ++++++++
 tools/memory-model/litmus-tests/R+mbonceonces.litmus       |  9 +++++++++
 tools/memory-model/litmus-tests/R+poonceonces.litmus       |  8 ++++++++
 tools/memory-model/litmus-tests/S+poonceonces.litmus       |  9 +++++++++
 .../litmus-tests/S+wmbonceonce+poacquireonce.litmus        |  7 +++++++
 tools/memory-model/litmus-tests/SB+mbonceonces.litmus      |  9 +++++++++
 tools/memory-model/litmus-tests/SB+poonceonces.litmus      |  8 ++++++++
 .../memory-model/litmus-tests/WRC+poonceonces+Once.litmus  |  8 ++++++++
 .../litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus |  8 ++++++++
 .../Z6.0+pooncelock+poonceLock+pombonce.litmus             |  9 +++++++++
 .../Z6.0+pooncelock+pooncelock+pombonce.litmus             |  8 ++++++++
 .../Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus  | 14 ++++++++++++++
 28 files changed, 246 insertions(+), 1 deletion(-)

diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
index 5b83d57f6ac5..967f9f2a6226 100644
--- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
@@ -1,5 +1,12 @@
 C CoRR+poonceonce+Once
 
+(*
+ * Result: Never
+ *
+ * Test of read-read coherence, that is, whether or not two successive
+ * reads from the same variable are ordered.
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
index fab91c13d52c..4635739f3974 100644
--- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
@@ -1,5 +1,12 @@
 C CoRW+poonceonce+Once
 
+(*
+ * Result: Never
+ *
+ * Test of read-write coherence, that is, whether or not a read from
+ * a given variable and a later write to that same variable are ordered.
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
index 6a35ec2042ea..bb068c92d8da 100644
--- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
@@ -1,5 +1,12 @@
 C CoWR+poonceonce+Once
 
+(*
+ * Result: Never
+ *
+ * Test of write-read coherence, that is, whether or not a write to a
+ * given variable and a later read from that same variable are ordered.
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
index 32a96b832021..0d9f0a958799 100644
--- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
+++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
@@ -1,5 +1,12 @@
 C CoWW+poonceonce
 
+(*
+ * Result: Never
+ *
+ * Test of write-write coherence, that is, whether or not two successive
+ * writes to the same variable are ordered.
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
index 7eba2c68992b..50d5db9ea983 100644
--- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
@@ -1,5 +1,15 @@
 C IRIW+mbonceonces+OnceOnce
 
+(*
+ * Result: Never
+ *
+ * Test of independent reads from independent writes with smp_mb()
+ * between each pairs of reads.  In other words, is smp_mb() sufficient to
+ * cause two different reading processes to agree on the order of a pair
+ * of writes, where each write is to a different variable by a different
+ * process?
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
index b0556c6c75d4..793fa8a74100 100644
--- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
@@ -1,5 +1,15 @@
 C IRIW+poonceonces+OnceOnce
 
+(*
+ * Result: Never
+ *
+ * Test of independent reads from independent writes with nothing
+ * between each pairs of reads.  In other words, is anything at all
+ * needed to cause two different reading processes to agree on the order
+ * of a pair of writes, where each write is to a different variable by a
+ * different process?
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
index 9a1a233d70c3..b321aa6f4ea5 100644
--- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
@@ -1,5 +1,14 @@
 C ISA2+poonceonces
 
+(*
+ * Result: Sometimes
+ *
+ * Given a release-acquire chain ordering the first process's store
+ * against the last process's load, is ordering preserved if all of the
+ * smp_store_release() invocations are replaced by WRITE_ONCE() and all
+ * of the smp_load_acquire() invocations are replaced by READ_ONCE()?
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
index 235195e87d4e..025b0462ec9b 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
@@ -1,5 +1,16 @@
 C ISA2+pooncerelease+poacquirerelease+poacquireonce
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that a release-acquire chain suffices
+ * to order P0()'s initial write against P2()'s final read.  The reason
+ * that the release-acquire chain suffices is because in all but one
+ * case (P2() to P0()), each process reads from the preceding process's
+ * write.  In memory-model-speak, there is only one non-reads-from
+ * (AKA non-rf) link, so release-acquire is all that is needed.
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
index dd5ac3a8974a..de6708229dd1 100644
--- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
@@ -1,5 +1,16 @@
 C LB+ctrlonceonce+mbonceonce
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that lightweight ordering suffices for
+ * the load-buffering pattern, in other words, preventing all processes
+ * reading from the preceding process's write.  In this example, the
+ * combination of a control dependency and a full memory barrier are enough
+ * to do the trick.  (But the full memory barrier could be replaced with
+ * another control dependency and order would still be maintained.)
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
index 47bd61319d93..07b9904b0e49 100644
--- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
+++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
@@ -1,5 +1,13 @@
 C LB+poacquireonce+pooncerelease
 
+(*
+ * Result: Never
+ *
+ * Does a release-acquire pair suffice for the load-buffering litmus
+ * test, where each process reads from one of two variables then writes
+ * to the other?
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
index a5cdf027e34b..74c49cb3c37b 100644
--- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
@@ -1,5 +1,12 @@
 C LB+poonceonces
 
+(*
+ * Result: Sometimes
+ *
+ * Can the counter-intuitive outcome for the load-buffering pattern
+ * be prevented even with no explicit ordering?
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index 1a2fe5830381..97731b4bbdd8 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -1,4 +1,13 @@
-C MP+onceassign+derefonce.litmus
+C MP+onceassign+derefonce
+
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that rcu_assign_pointer() and
+ * rcu_dereference() suffice to ensure that an RCU reader will not see
+ * pre-initialization garbage when it traverses an RCU-protected data
+ * structure containing a newly inserted element.
+ *)
 
 {
 y=z;
diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
index 5fe6f1e3c452..712a4fcdf6ce 100644
--- a/tools/memory-model/litmus-tests/MP+polocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
@@ -1,5 +1,16 @@
 C MP+polocks
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates how lock acquisitions and releases can
+ * stand in for smp_load_acquire() and smp_store_release(), respectively.
+ * In other words, when holding a given lock (or indeed after releasing a
+ * given lock), a CPU is not only guaranteed to see the accesses that other
+ * CPUs made while previously holding that lock, it is also guaranteed
+ * to see all prior accesses by those other CPUs.
+ *)
+
 {}
 
 P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 46e1ac7ba126..b2b60b84fb9d 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -1,5 +1,12 @@
 C MP+poonceonces
 
+(*
+ * Result: Maybe
+ *
+ * Can the counter-intuitive message-passing outcome be prevented with
+ * no ordering at all?
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index 0b00cc7293ba..d52c68429722 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -1,5 +1,13 @@
 C MP+pooncerelease+poacquireonce
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that smp_store_release() and
+ * smp_load_acquire() provide sufficient ordering for the message-passing
+ * pattern.
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
index 90d011c34f33..72c9276b363e 100644
--- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
@@ -1,5 +1,16 @@
 C MP+porevlocks
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates how lock acquisitions and releases can
+ * stand in for smp_load_acquire() and smp_store_release(), respectively.
+ * In other words, when holding a given lock (or indeed after releasing a
+ * given lock), a CPU is not only guaranteed to see the accesses that other
+ * CPUs made while previously holding that lock, it is also guaranteed to
+ * see all prior accesses by those other CPUs.
+ *)
+
 {}
 
 P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
index 604ad41ea0c2..c078f38ff27a 100644
--- a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
@@ -1,5 +1,13 @@
 C MP+wmbonceonce+rmbonceonce
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that smp_wmb() and smp_rmb() provide
+ * sufficient ordering for the message-passing pattern.  However, it
+ * is usually better to use smp_store_release() and smp_load_acquire().
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
index e69b9e3e9436..a0e884ad2132 100644
--- a/tools/memory-model/litmus-tests/R+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
@@ -1,5 +1,14 @@
 C R+mbonceonces
 
+(*
+ * Result: Never
+ *
+ * This is the fully ordered (via smp_mb()) version of one of the classic
+ * counterintuitive litmus tests that illustrates the effects of store
+ * propagation delays.  Note that weakening either of the barriers would
+ * cause the resulting test to be allowed.
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
index f7a12e00f82d..5386f128a131 100644
--- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
@@ -1,5 +1,13 @@
 C R+poonceonces
 
+(*
+ * Result: Sometimes
+ *
+ * This is the unordered (thus lacking smp_mb()) version of one of the
+ * classic counterintuitive litmus tests that illustrates the effects of
+ * store propagation delays.
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
index d0d541c8ec7d..8c9c2f81a580 100644
--- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
@@ -1,5 +1,14 @@
 C S+poonceonces
 
+(*
+ * Result: Sometimes
+ *
+ * Starting with a two-process release-acquire chain ordering P0()'s
+ * first store against P1()'s final load, if the smp_store_release()
+ * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
+ * READ_ONCE(), is ordering preserved?
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
index 1d292d0d6603..c53350205d28 100644
--- a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
@@ -1,5 +1,12 @@
 C S+wmbonceonce+poacquireonce
 
+(*
+ * Result: Never
+ *
+ * Can a smp_wmb(), instead of a release, and an acquire order a prior
+ * store against a subsequent store?
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
index b76caa5af1af..74b874ffa8da 100644
--- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
@@ -1,5 +1,14 @@
 C SB+mbonceonces
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that full memory barriers suffice to
+ * order the store-buffering pattern, where each process writes to the
+ * variable that the preceding process reads.  (Locking and RCU can also
+ * suffice, but not much else.)
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
index c1797e03807e..10d550730b25 100644
--- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
@@ -1,5 +1,13 @@
 C SB+poonceonces
 
+(*
+ * Result: Sometimes
+ *
+ * This litmus test demonstrates that at least some ordering is required
+ * to order the store-buffering pattern, where each process writes to the
+ * variable that the preceding process reads.
+ *)
+
 {}
 
 P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
index f5e7c92f61cc..6a2bc12a1af1 100644
--- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
@@ -1,5 +1,13 @@
 C WRC+poonceonces+Once
 
+(*
+ * Result: Sometimes
+ *
+ * This litmus test is an extension of the message-passing pattern,
+ * where the first write is moved to a separate process.  Note that this
+ * test has no ordering at all.
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
index e3d0018025dd..97fcbffde9a0 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
@@ -1,5 +1,13 @@
 C WRC+pooncerelease+rmbonceonce+Once
 
+(*
+ * Result: Never
+ *
+ * This litmus test is an extension of the message-passing pattern, where
+ * the first write is moved to a separate process.  Because it features
+ * a release and a read memory barrier, it should be forbidden.
+ *)
+
 {}
 
 P0(int *x)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
index 9c2cb53e6ef0..415248fb6699 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
@@ -1,5 +1,14 @@
 C Z6.0+pooncelock+poonceLock+pombonce
 
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates how smp_mb__after_spinlock() may be
+ * used to ensure that accesses in different critical sections for a
+ * given lock running on different CPUs are nevertheless seen in order
+ * by CPUs not holding that lock.
+ *)
+
 {}
 
 P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
index c9a1f1a49ae1..fad47258a3e3 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
@@ -1,5 +1,13 @@
 C Z6.0+pooncelock+pooncelock+pombonce
 
+(*
+ * Result: Never
+ *
+ * This example demonstrates that a pair of accesses made by different
+ * processes each while holding a given lock will not necessarily be
+ * seen as ordered by a third process not holding that lock.
+ *)
+
 {}
 
 P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
index 25409a033514..a20fc3fafb53 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
@@ -1,5 +1,19 @@
 C Z6.0+pooncerelease+poacquirerelease+mbonceonce
 
+(*
+ * Result: Sometimes
+ *
+ * This litmus test shows that a release-acquire chain, while sufficient
+ * when there is but one non-reads-from (AKA non-rf) link, does not suffice
+ * if there is more than one.  Of the three processes, only P1() reads from
+ * P0's write, which means that there are two non-rf links: P1() to P2()
+ * is a write-to-write link (AKA a "coherence" or just "co" link) and P2()
+ * to P0() is a read-to-write link (AKA a "from-reads" or just "fr" link).
+ * When there are two or more non-rf links, you typically will need one
+ * full barrier for each non-rf link.  (Exceptions include some cases
+ * involving locking.)
+ *)
+
 {}
 
 P0(int *x, int *y)
-- 
2.5.2

[PATCH RFC tip/lkmm 05/10] README: Fix a couple of punctuation errors

[Paul E. McKenney]

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/litmus-tests/README | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 9a3bb5949191..dca7d823ad57 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -23,14 +23,14 @@ IRIW+mbonceonces+OnceOnce.litmus
 	between each pairs of reads.  In other words, is smp_mb()
 	sufficient to cause two different reading processes to agree on
 	the order of a pair of writes, where each write is to a different
-	variable by a different process.
+	variable by a different process?
 
 IRIW+poonceonces+OnceOnce.litmus
 	Test of independent reads from independent writes with nothing
 	between each pairs of reads.  In other words, is anything at all
 	needed to cause two different reading processes to agree on the
 	order of a pair of writes, where each write is to a different
-	variable by a different process.
+	variable by a different process?
 
 ISA2+poonceonces.litmus
 	As below, but with store-release replaced with WRITE_ONCE()
-- 
2.5.2

[PATCH RFC tip/lkmm 06/10] EXP MAINTAINERS: Add the "LKMM" acronym

[Paul E. McKenney]

This commit adds "(LKMM)" to the end of the MAINTAINERS file's entry
for the Linux-kernel memory-consistency model.

If people are OK with this, it should be squashed into 12a62a1d0703
("MAINTAINERS: Add the Memory Consistency Model subsystem").

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 MAINTAINERS | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/MAINTAINERS b/MAINTAINERS
index e6ad9b44e8fb..674b35c3f28e 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8086,7 +8086,7 @@ M:	Kees Cook <keescook@chromium.org>
 S:	Maintained
 F:	drivers/misc/lkdtm*
 
-LINUX KERNEL MEMORY CONSISTENCY MODEL
+LINUX KERNEL MEMORY CONSISTENCY MODEL (LKMM)
 M:	Alan Stern <stern@rowland.harvard.edu>
 M:	Andrea Parri <parri.andrea@gmail.com>
 M:	Will Deacon <will.deacon@arm.com>
-- 
2.5.2

[PATCH RFC tip/lkmm 07/10] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer

[Paul E. McKenney]

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 MAINTAINERS | 1 +
 1 file changed, 1 insertion(+)

diff --git a/MAINTAINERS b/MAINTAINERS
index 674b35c3f28e..cc4c1ac94593 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8097,6 +8097,7 @@ M:	David Howells <dhowells@redhat.com>
 M:	Jade Alglave <j.alglave@ucl.ac.uk>
 M:	Luc Maranget <luc.maranget@inria.fr>
 M:	"Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
+R:	Akira Yokosawa <akiyks@gmail.com>
 L:	linux-kernel@vger.kernel.org
 S:	Supported
 T:	git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
-- 
2.5.2

[PATCH RFC tip/lkmm 08/10] EXP Remove understore from smp_mb__before_atomic() workings

[Paul E. McKenney]

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/linux-kernel.bell | 2 +-
 tools/memory-model/linux-kernel.cat  | 2 +-
 tools/memory-model/linux-kernel.def  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index b984bbda01a5..558bbef9e08a 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -28,7 +28,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'rcu-lock (*rcu_read_lock*)  ||
 		'rcu-unlock (*rcu_read_unlock*) ||
 		'sync-rcu (*synchronize_rcu*) ||
-		'before_atomic (*smp_mb__before_atomic*) ||
+		'before-atomic (*smp_mb__before_atomic*) ||
 		'after_atomic (*smp_mb__after_atomic*) ||
 		'after_spinlock (*smp_mb__after_spinlock*)
 instructions F[Barriers]
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index babe2b3b0bb3..31c08a44c088 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -29,7 +29,7 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
 let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
 let wmb = [W] ; fencerel(Wmb) ; [W]
 let mb = ([M] ; fencerel(Mb) ; [M]) |
-	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
+	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
 	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
 	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
 let gp = po ; [Sync-rcu] ; po?
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index a397387f77cc..ff4b756f4a44 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -21,7 +21,7 @@ smp_mb() { __fence{mb} ; }
 smp_rmb() { __fence{rmb} ; }
 smp_wmb() { __fence{wmb} ; }
 smp_read_barrier_depends() { __fence{rb_dep}; }
-smp_mb__before_atomic() { __fence{before_atomic} ; }
+smp_mb__before_atomic() { __fence{before-atomic} ; }
 smp_mb__after_atomic() { __fence{after_atomic} ; }
 smp_mb__after_spinlock() { __fence{after_spinlock} ; }
 
-- 
2.5.2

[PATCH RFC tip/lkmm 09/10] EXP Remove underscore from smp_mb__after_atomic() workings

[Paul E. McKenney]

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/linux-kernel.bell | 2 +-
 tools/memory-model/linux-kernel.cat  | 2 +-
 tools/memory-model/linux-kernel.def  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 558bbef9e08a..6fca420bc6c4 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -29,7 +29,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'rcu-unlock (*rcu_read_unlock*) ||
 		'sync-rcu (*synchronize_rcu*) ||
 		'before-atomic (*smp_mb__before_atomic*) ||
-		'after_atomic (*smp_mb__after_atomic*) ||
+		'after-atomic (*smp_mb__after_atomic*) ||
 		'after_spinlock (*smp_mb__after_spinlock*)
 instructions F[Barriers]
 
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 31c08a44c088..7b1d9ecc4b67 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -30,7 +30,7 @@ let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
 let wmb = [W] ; fencerel(Wmb) ; [W]
 let mb = ([M] ; fencerel(Mb) ; [M]) |
 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
-	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
+	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
 	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
 let gp = po ; [Sync-rcu] ; po?
 
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index ff4b756f4a44..46a9eb40323d 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -22,7 +22,7 @@ smp_rmb() { __fence{rmb} ; }
 smp_wmb() { __fence{wmb} ; }
 smp_read_barrier_depends() { __fence{rb_dep}; }
 smp_mb__before_atomic() { __fence{before-atomic} ; }
-smp_mb__after_atomic() { __fence{after_atomic} ; }
+smp_mb__after_atomic() { __fence{after-atomic} ; }
 smp_mb__after_spinlock() { __fence{after_spinlock} ; }
 
 // Exchange
-- 
2.5.2

[PATCH RFC tip/lkmm 10/10] EXP Remove underscores from smp_mb__after_spinlock() workings

[Paul E. McKenney]

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/linux-kernel.bell | 2 +-
 tools/memory-model/linux-kernel.cat  | 2 +-
 tools/memory-model/linux-kernel.def  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 6fca420bc6c4..18885ad15de9 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -30,7 +30,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'sync-rcu (*synchronize_rcu*) ||
 		'before-atomic (*smp_mb__before_atomic*) ||
 		'after-atomic (*smp_mb__after_atomic*) ||
-		'after_spinlock (*smp_mb__after_spinlock*)
+		'after-spinlock (*smp_mb__after_spinlock*)
 instructions F[Barriers]
 
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 7b1d9ecc4b67..f0d27f813ec2 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -31,7 +31,7 @@ let wmb = [W] ; fencerel(Wmb) ; [W]
 let mb = ([M] ; fencerel(Mb) ; [M]) |
 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
 	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
-	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
+	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
 let gp = po ; [Sync-rcu] ; po?
 
 let strong-fence = mb | gp
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 46a9eb40323d..f5a1eb04cb64 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -23,7 +23,7 @@ smp_wmb() { __fence{wmb} ; }
 smp_read_barrier_depends() { __fence{rb_dep}; }
 smp_mb__before_atomic() { __fence{before-atomic} ; }
 smp_mb__after_atomic() { __fence{after-atomic} ; }
-smp_mb__after_spinlock() { __fence{after_spinlock} ; }
+smp_mb__after_spinlock() { __fence{after-spinlock} ; }
 
 // Exchange
 xchg(X,V)  __xchg{mb}(X,V)
-- 
2.5.2

Re: [PATCH RFC tools/lkmm] Miscellaneous fixes

[Akira Yokosawa]

On 2018/02/09 23:18, Paul E. McKenney wrote:
> Hello!
> 
> This RFC series adds some miscellaneous updates to the Linux kernel
> memory model:
> 
> 1.	Clarify the origin and scope of the tool name to avoid confusion
> 	between "memory model" and "memory management", courtesy of
> 	Andrea Parri.
> 
> 2.	Move the maintainer list for LKMM to the main MAINTAINERS file,
> 	courtesy of Andrea Parri.
> 
> 3.	Add memory-barriers.txt to the LKMM MAINTAINERS entry, courtesy
> 	of Andrea Parri.
> 
> 4.	Add comments explaining the purpose of the various litmus tests.
> 
> 5.	Fix puntuation errors in litmus-tests/README.
> 
> 6.	Add LKMM acronym to MAINTAINERS entry.  If there are no objections,
> 	this will be squashed with #3 above.
> 
> 7.	Add Akira Yokosawa as an LKMM reviewer.
> 
> 8-10.	Replace underscores with hyphens for smp_mb__*() workings.  Note that
> 	this patch leaves rb_dep alone because the underscore is set by herd7.
> 	If there are no objections, these will be squashed together.

Paul, Patches 8-10 made the problem even worse with herd7 7.47.
I'll submit an alternative patch in reply to this message.

      Thanks, Akira

> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
>  /tools/memory-model/MAINTAINERS                                                            |   15 -------
>  b/MAINTAINERS                                                                              |   20 +++++++++-
>  b/tools/memory-model/MAINTAINERS                                                           |    2 -
>  b/tools/memory-model/README                                                                |   14 +++----
>  b/tools/memory-model/linux-kernel.bell                                                     |    8 ++--
>  b/tools/memory-model/linux-kernel.cat                                                      |    8 ++--
>  b/tools/memory-model/linux-kernel.def                                                      |    6 +--
>  b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus                              |    7 +++
>  b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus                              |    7 +++
>  b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus                              |    7 +++
>  b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus                                   |    7 +++
>  b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus                         |   10 +++++
>  b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus                         |   10 +++++
>  b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus                                  |    9 ++++
>  b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus |   11 +++++
>  b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus                        |   11 +++++
>  b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus                    |    8 ++++
>  b/tools/memory-model/litmus-tests/LB+poonceonces.litmus                                    |    7 +++
>  b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus                           |   11 +++++
>  b/tools/memory-model/litmus-tests/MP+polocks.litmus                                        |   11 +++++
>  b/tools/memory-model/litmus-tests/MP+poonceonces.litmus                                    |    7 +++
>  b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus                    |    8 ++++
>  b/tools/memory-model/litmus-tests/MP+porevlocks.litmus                                     |   11 +++++
>  b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus                        |    8 ++++
>  b/tools/memory-model/litmus-tests/R+mbonceonces.litmus                                     |    9 ++++
>  b/tools/memory-model/litmus-tests/R+poonceonces.litmus                                     |    8 ++++
>  b/tools/memory-model/litmus-tests/README                                                   |    4 +-
>  b/tools/memory-model/litmus-tests/S+poonceonces.litmus                                     |    9 ++++
>  b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus                       |    7 +++
>  b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus                                    |    9 ++++
>  b/tools/memory-model/litmus-tests/SB+poonceonces.litmus                                    |    8 ++++
>  b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus                              |    8 ++++
>  b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus                |    8 ++++
>  b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus               |    9 ++++
>  b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus               |    8 ++++
>  b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus    |   14 +++++++
>  36 files changed, 286 insertions(+), 38 deletions(-)
> 

[PATCH] tools/memory-model: Restore compat with herd7 7.47 ("-" -> "_")

[Akira Yokosawa]

>From 9a0de4d75e18ef8e25a1096f88c7a970d9d693f5 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 10 Feb 2018 00:45:25 +0900
Subject: [PATCH] tools/memory-model: Restore compat with herd7 7.47 ("-" -> "_")

As of herd7 7.47, these '-'s are not permitted and end up in
an error:

    File "./linux-kernel.def", line 44, characters 29-30:
    unexpected '-' (in macros)

Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
identifiers match ASPLOS paper") in the repository at
https://github.com/aparri/memory-model can restore the compatibility
with herd7 7.47.

Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
Suggested-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 tools/memory-model/linux-kernel.bell | 20 ++++++++++----------
 tools/memory-model/linux-kernel.cat  |  8 ++++----
 tools/memory-model/linux-kernel.def  | 14 +++++++-------
 3 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 18885ad..436791b 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -25,18 +25,18 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'rmb (*smp_rmb*) ||
 		'mb (*smp_mb*) ||
 		'rb_dep (*smp_read_barrier_depends*) ||
-		'rcu-lock (*rcu_read_lock*)  ||
-		'rcu-unlock (*rcu_read_unlock*) ||
-		'sync-rcu (*synchronize_rcu*) ||
-		'before-atomic (*smp_mb__before_atomic*) ||
-		'after-atomic (*smp_mb__after_atomic*) ||
-		'after-spinlock (*smp_mb__after_spinlock*)
+		'rcu_lock (*rcu_read_lock*)  ||
+		'rcu_unlock (*rcu_read_unlock*) ||
+		'sync_rcu (*synchronize_rcu*) ||
+		'before_atomic (*smp_mb__before_atomic*) ||
+		'after_atomic (*smp_mb__after_atomic*) ||
+		'after_spinlock (*smp_mb__after_spinlock*)
 instructions F[Barriers]
 
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
 let matched = let rec
-	    unmatched-locks = Rcu-lock \ domain(matched)
-	and unmatched-unlocks = Rcu-unlock \ range(matched)
+	    unmatched-locks = Rcu_lock \ domain(matched)
+	and unmatched-unlocks = Rcu_unlock \ range(matched)
 	and unmatched = unmatched-locks | unmatched-unlocks
 	and unmatched-po = [unmatched] ; po ; [unmatched]
 	and unmatched-locks-to-unlocks =
@@ -46,8 +46,8 @@ let matched = let rec
 	in matched
 
 (* Validate nesting *)
-flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
-flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
+flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking
+flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking
 
 (* Outermost level of nesting only *)
 let crit = matched \ (po^-1 ; matched ; po^-1)
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index f0d27f8..d0085d5 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -29,10 +29,10 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
 let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
 let wmb = [W] ; fencerel(Wmb) ; [W]
 let mb = ([M] ; fencerel(Mb) ; [M]) |
-	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
-	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
-	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
-let gp = po ; [Sync-rcu] ; po?
+	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
+	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
+	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
+let gp = po ; [Sync_rcu] ; po?
 
 let strong-fence = mb | gp
 
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index f5a1eb0..fc08371 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -21,9 +21,9 @@ smp_mb() { __fence{mb} ; }
 smp_rmb() { __fence{rmb} ; }
 smp_wmb() { __fence{wmb} ; }
 smp_read_barrier_depends() { __fence{rb_dep}; }
-smp_mb__before_atomic() { __fence{before-atomic} ; }
-smp_mb__after_atomic() { __fence{after-atomic} ; }
-smp_mb__after_spinlock() { __fence{after-spinlock} ; }
+smp_mb__before_atomic() { __fence{before_atomic} ; }
+smp_mb__after_atomic() { __fence{after_atomic} ; }
+smp_mb__after_spinlock() { __fence{after_spinlock} ; }
 
 // Exchange
 xchg(X,V)  __xchg{mb}(X,V)
@@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; }
 spin_trylock(X) __trylock(X)
 
 // RCU
-rcu_read_lock() { __fence{rcu-lock}; }
-rcu_read_unlock() { __fence{rcu-unlock};}
-synchronize_rcu() { __fence{sync-rcu}; }
-synchronize_rcu_expedited() { __fence{sync-rcu}; }
+rcu_read_lock() { __fence{rcu_lock}; }
+rcu_read_unlock() { __fence{rcu_unlock};}
+synchronize_rcu() { __fence{sync_rcu}; }
+synchronize_rcu_expedited() { __fence{sync_rcu}; }
 
 // Atomic
 atomic_read(X) READ_ONCE(*X)
-- 
2.7.4

Re: [PATCH RFC tip/lkmm 04/10] EXP litmus_tests: Add comments explaining tests' purposes

[Alan Stern]

On Fri, 9 Feb 2018, Paul E. McKenney wrote:

> This commit adds comments to the litmus tests summarizing what these
> tests are intended to demonstrate.
> 
> Suggested-by: Ingo Molnar <mingo@kernel.org>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> [ paulmck: Apply Andrea's and Alan's feedback. ]
> ---

> --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> @@ -1,5 +1,15 @@
>  C IRIW+poonceonces+OnceOnce
>  
> +(*
> + * Result: Never
> + *
> + * Test of independent reads from independent writes with nothing
> + * between each pairs of reads.  In other words, is anything at all
> + * needed to cause two different reading processes to agree on the order
> + * of a pair of writes, where each write is to a different variable by a
> + * different process?
> + *)

The result should be Sometimes.

Alan

[PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Akira Yokosawa]

>From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 9 Feb 2018 04:51:05 -0800
Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

As of herd7 7.47, these '-'s are not permitted and end up in
errors such as:

    File "./linux-kernel.def", line 44, characters 29-30:
    unexpected '-' (in macros)

Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
identifiers match ASPLOS paper") in the repository at
https://github.com/aparri/memory-model can restore the compatibility
with herd7 7.47.

Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
Suggested-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
Paul,

FWIW, this is a squashed version relative to patch 07/10 in the RFC series.

    Thanks, Akira
--
 tools/memory-model/linux-kernel.bell | 14 +++++++-------
 tools/memory-model/linux-kernel.cat  |  2 +-
 tools/memory-model/linux-kernel.def  |  8 ++++----
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index b984bbd..436791b 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'rmb (*smp_rmb*) ||
 		'mb (*smp_mb*) ||
 		'rb_dep (*smp_read_barrier_depends*) ||
-		'rcu-lock (*rcu_read_lock*)  ||
-		'rcu-unlock (*rcu_read_unlock*) ||
-		'sync-rcu (*synchronize_rcu*) ||
+		'rcu_lock (*rcu_read_lock*)  ||
+		'rcu_unlock (*rcu_read_unlock*) ||
+		'sync_rcu (*synchronize_rcu*) ||
 		'before_atomic (*smp_mb__before_atomic*) ||
 		'after_atomic (*smp_mb__after_atomic*) ||
 		'after_spinlock (*smp_mb__after_spinlock*)
@@ -35,8 +35,8 @@ instructions F[Barriers]
 
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
 let matched = let rec
-	    unmatched-locks = Rcu-lock \ domain(matched)
-	and unmatched-unlocks = Rcu-unlock \ range(matched)
+	    unmatched-locks = Rcu_lock \ domain(matched)
+	and unmatched-unlocks = Rcu_unlock \ range(matched)
 	and unmatched = unmatched-locks | unmatched-unlocks
 	and unmatched-po = [unmatched] ; po ; [unmatched]
 	and unmatched-locks-to-unlocks =
@@ -46,8 +46,8 @@ let matched = let rec
 	in matched
 
 (* Validate nesting *)
-flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
-flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
+flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking
+flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking
 
 (* Outermost level of nesting only *)
 let crit = matched \ (po^-1 ; matched ; po^-1)
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index babe2b3..d0085d5 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) |
 	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
 	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
 	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
-let gp = po ; [Sync-rcu] ; po?
+let gp = po ; [Sync_rcu] ; po?
 
 let strong-fence = mb | gp
 
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index a397387..fc08371 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; }
 spin_trylock(X) __trylock(X)
 
 // RCU
-rcu_read_lock() { __fence{rcu-lock}; }
-rcu_read_unlock() { __fence{rcu-unlock};}
-synchronize_rcu() { __fence{sync-rcu}; }
-synchronize_rcu_expedited() { __fence{sync-rcu}; }
+rcu_read_lock() { __fence{rcu_lock}; }
+rcu_read_unlock() { __fence{rcu_unlock};}
+synchronize_rcu() { __fence{sync_rcu}; }
+synchronize_rcu_expedited() { __fence{sync_rcu}; }
 
 // Atomic
 atomic_read(X) READ_ONCE(*X)
-- 
2.7.4

Re: [PATCH RFC tip/lkmm 04/10] EXP litmus_tests: Add comments explaining tests' purposes

[Paul E. McKenney]

On Fri, Feb 09, 2018 at 01:46:30PM -0500, Alan Stern wrote:
> On Fri, 9 Feb 2018, Paul E. McKenney wrote:
> 
> > This commit adds comments to the litmus tests summarizing what these
> > tests are intended to demonstrate.
> > 
> > Suggested-by: Ingo Molnar <mingo@kernel.org>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > [ paulmck: Apply Andrea's and Alan's feedback. ]
> > ---
> 
> > --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > @@ -1,5 +1,15 @@
> >  C IRIW+poonceonces+OnceOnce
> >  
> > +(*
> > + * Result: Never
> > + *
> > + * Test of independent reads from independent writes with nothing
> > + * between each pairs of reads.  In other words, is anything at all
> > + * needed to cause two different reading processes to agree on the order
> > + * of a pair of writes, where each write is to a different variable by a
> > + * different process?
> > + *)
> 
> The result should be Sometimes.

Right you are, and better yet, the memory model agrees with you.

I have fixed this, thank you for the careful review!

							Thanx, Paul

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Paul E. McKenney]

On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Fri, 9 Feb 2018 04:51:05 -0800
> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
> 
> As of herd7 7.47, these '-'s are not permitted and end up in
> errors such as:
> 
>     File "./linux-kernel.def", line 44, characters 29-30:
>     unexpected '-' (in macros)
> 
> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
> identifiers match ASPLOS paper") in the repository at
> https://github.com/aparri/memory-model can restore the compatibility
> with herd7 7.47.
> 
> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> Paul,
> 
> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.

Thank you, Akira!

I am going to hold off on this for a bit to see if we can instead get
a new release of herd7, but if we can't. this might well be a very good
way to go.

							Thanx, Paul

>     Thanks, Akira
> --
>  tools/memory-model/linux-kernel.bell | 14 +++++++-------
>  tools/memory-model/linux-kernel.cat  |  2 +-
>  tools/memory-model/linux-kernel.def  |  8 ++++----
>  3 files changed, 12 insertions(+), 12 deletions(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index b984bbd..436791b 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) ||
>  		'rmb (*smp_rmb*) ||
>  		'mb (*smp_mb*) ||
>  		'rb_dep (*smp_read_barrier_depends*) ||
> -		'rcu-lock (*rcu_read_lock*)  ||
> -		'rcu-unlock (*rcu_read_unlock*) ||
> -		'sync-rcu (*synchronize_rcu*) ||
> +		'rcu_lock (*rcu_read_lock*)  ||
> +		'rcu_unlock (*rcu_read_unlock*) ||
> +		'sync_rcu (*synchronize_rcu*) ||
>  		'before_atomic (*smp_mb__before_atomic*) ||
>  		'after_atomic (*smp_mb__after_atomic*) ||
>  		'after_spinlock (*smp_mb__after_spinlock*)
> @@ -35,8 +35,8 @@ instructions F[Barriers]
> 
>  (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
>  let matched = let rec
> -	    unmatched-locks = Rcu-lock \ domain(matched)
> -	and unmatched-unlocks = Rcu-unlock \ range(matched)
> +	    unmatched-locks = Rcu_lock \ domain(matched)
> +	and unmatched-unlocks = Rcu_unlock \ range(matched)
>  	and unmatched = unmatched-locks | unmatched-unlocks
>  	and unmatched-po = [unmatched] ; po ; [unmatched]
>  	and unmatched-locks-to-unlocks =
> @@ -46,8 +46,8 @@ let matched = let rec
>  	in matched
> 
>  (* Validate nesting *)
> -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
> -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
> +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking
> +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking
> 
>  (* Outermost level of nesting only *)
>  let crit = matched \ (po^-1 ; matched ; po^-1)
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index babe2b3..d0085d5 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) |
>  	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
>  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
>  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
> -let gp = po ; [Sync-rcu] ; po?
> +let gp = po ; [Sync_rcu] ; po?
> 
>  let strong-fence = mb | gp
> 
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index a397387..fc08371 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; }
>  spin_trylock(X) __trylock(X)
> 
>  // RCU
> -rcu_read_lock() { __fence{rcu-lock}; }
> -rcu_read_unlock() { __fence{rcu-unlock};}
> -synchronize_rcu() { __fence{sync-rcu}; }
> -synchronize_rcu_expedited() { __fence{sync-rcu}; }
> +rcu_read_lock() { __fence{rcu_lock}; }
> +rcu_read_unlock() { __fence{rcu_unlock};}
> +synchronize_rcu() { __fence{sync_rcu}; }
> +synchronize_rcu_expedited() { __fence{sync_rcu}; }
> 
>  // Atomic
>  atomic_read(X) READ_ONCE(*X)
> -- 
> 2.7.4
> 
> 

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Akira Yokosawa]

On 2018/02/10 10:07, Paul E. McKenney wrote:
> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Fri, 9 Feb 2018 04:51:05 -0800
>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
>>
>> As of herd7 7.47, these '-'s are not permitted and end up in
>> errors such as:
>>
>>     File "./linux-kernel.def", line 44, characters 29-30:
>>     unexpected '-' (in macros)
>>
>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
>> identifiers match ASPLOS paper") in the repository at
>> https://github.com/aparri/memory-model can restore the compatibility
>> with herd7 7.47.
>>
>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
>> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>> ---
>> Paul,
>>
>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> 
> Thank you, Akira!
> 
> I am going to hold off on this for a bit to see if we can instead get
> a new release of herd7, but if we can't. this might well be a very good
> way to go.

Fair enough.

   Thanks, Akira

> 
> 							Thanx, Paul
> 
>>     Thanks, Akira
>> --
>>  tools/memory-model/linux-kernel.bell | 14 +++++++-------
>>  tools/memory-model/linux-kernel.cat  |  2 +-
>>  tools/memory-model/linux-kernel.def  |  8 ++++----
>>  3 files changed, 12 insertions(+), 12 deletions(-)
>>
>> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
>> index b984bbd..436791b 100644
>> --- a/tools/memory-model/linux-kernel.bell
>> +++ b/tools/memory-model/linux-kernel.bell
>> @@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) ||
>>  		'rmb (*smp_rmb*) ||
>>  		'mb (*smp_mb*) ||
>>  		'rb_dep (*smp_read_barrier_depends*) ||
>> -		'rcu-lock (*rcu_read_lock*)  ||
>> -		'rcu-unlock (*rcu_read_unlock*) ||
>> -		'sync-rcu (*synchronize_rcu*) ||
>> +		'rcu_lock (*rcu_read_lock*)  ||
>> +		'rcu_unlock (*rcu_read_unlock*) ||
>> +		'sync_rcu (*synchronize_rcu*) ||
>>  		'before_atomic (*smp_mb__before_atomic*) ||
>>  		'after_atomic (*smp_mb__after_atomic*) ||
>>  		'after_spinlock (*smp_mb__after_spinlock*)
>> @@ -35,8 +35,8 @@ instructions F[Barriers]
>>
>>  (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
>>  let matched = let rec
>> -	    unmatched-locks = Rcu-lock \ domain(matched)
>> -	and unmatched-unlocks = Rcu-unlock \ range(matched)
>> +	    unmatched-locks = Rcu_lock \ domain(matched)
>> +	and unmatched-unlocks = Rcu_unlock \ range(matched)
>>  	and unmatched = unmatched-locks | unmatched-unlocks
>>  	and unmatched-po = [unmatched] ; po ; [unmatched]
>>  	and unmatched-locks-to-unlocks =
>> @@ -46,8 +46,8 @@ let matched = let rec
>>  	in matched
>>
>>  (* Validate nesting *)
>> -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
>> -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
>> +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking
>> +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking
>>
>>  (* Outermost level of nesting only *)
>>  let crit = matched \ (po^-1 ; matched ; po^-1)
>> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
>> index babe2b3..d0085d5 100644
>> --- a/tools/memory-model/linux-kernel.cat
>> +++ b/tools/memory-model/linux-kernel.cat
>> @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) |
>>  	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
>>  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
>>  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
>> -let gp = po ; [Sync-rcu] ; po?
>> +let gp = po ; [Sync_rcu] ; po?
>>
>>  let strong-fence = mb | gp
>>
>> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
>> index a397387..fc08371 100644
>> --- a/tools/memory-model/linux-kernel.def
>> +++ b/tools/memory-model/linux-kernel.def
>> @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; }
>>  spin_trylock(X) __trylock(X)
>>
>>  // RCU
>> -rcu_read_lock() { __fence{rcu-lock}; }
>> -rcu_read_unlock() { __fence{rcu-unlock};}
>> -synchronize_rcu() { __fence{sync-rcu}; }
>> -synchronize_rcu_expedited() { __fence{sync-rcu}; }
>> +rcu_read_lock() { __fence{rcu_lock}; }
>> +rcu_read_unlock() { __fence{rcu_unlock};}
>> +synchronize_rcu() { __fence{sync_rcu}; }
>> +synchronize_rcu_expedited() { __fence{sync_rcu}; }
>>
>>  // Atomic
>>  atomic_read(X) READ_ONCE(*X)
>> -- 
>> 2.7.4
>>
>>
> 

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Ingo Molnar]

* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:

> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
> > >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
> > From: Akira Yokosawa <akiyks@gmail.com>
> > Date: Fri, 9 Feb 2018 04:51:05 -0800
> > Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
> > 
> > As of herd7 7.47, these '-'s are not permitted and end up in
> > errors such as:
> > 
> >     File "./linux-kernel.def", line 44, characters 29-30:
> >     unexpected '-' (in macros)
> > 
> > Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
> > identifiers match ASPLOS paper") in the repository at
> > https://github.com/aparri/memory-model can restore the compatibility
> > with herd7 7.47.
> > 
> > Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
> > Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > ---
> > Paul,
> > 
> > FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> 
> Thank you, Akira!
> 
> I am going to hold off on this for a bit to see if we can instead get
> a new release of herd7, but if we can't. this might well be a very good
> way to go.

I'm wondering:

> >  // RCU
> > -rcu_read_lock() { __fence{rcu-lock}; }
> > -rcu_read_unlock() { __fence{rcu-unlock};}
> > -synchronize_rcu() { __fence{sync-rcu}; }
> > -synchronize_rcu_expedited() { __fence{sync-rcu}; }
> > +rcu_read_lock() { __fence{rcu_lock}; }
> > +rcu_read_unlock() { __fence{rcu_unlock};}
> > +synchronize_rcu() { __fence{sync_rcu}; }
> > +synchronize_rcu_expedited() { __fence{sync_rcu}; }

What's the point of using '-' instead of '_'? In a program language syntax 
environment it's easy to confuse it with a '-' operator, and it also looks 
slightly sloppy and inconsistent if we sometimes have '_' and sometimes '-'.

If it used on purpose, to separate namespaces from kernel internal API names,
then that's rather obscure IMHO and then I'd rather suggest proper prefixes 
instead.

Thanks,

	Ingo

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Paul E. McKenney]

On Sun, Feb 11, 2018 at 12:51:48PM +0100, Ingo Molnar wrote:
> 
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> 
> > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
> > > >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
> > > From: Akira Yokosawa <akiyks@gmail.com>
> > > Date: Fri, 9 Feb 2018 04:51:05 -0800
> > > Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
> > > 
> > > As of herd7 7.47, these '-'s are not permitted and end up in
> > > errors such as:
> > > 
> > >     File "./linux-kernel.def", line 44, characters 29-30:
> > >     unexpected '-' (in macros)
> > > 
> > > Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
> > > identifiers match ASPLOS paper") in the repository at
> > > https://github.com/aparri/memory-model can restore the compatibility
> > > with herd7 7.47.
> > > 
> > > Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
> > > Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> > > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > > ---
> > > Paul,
> > > 
> > > FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> > 
> > Thank you, Akira!
> > 
> > I am going to hold off on this for a bit to see if we can instead get
> > a new release of herd7, but if we can't. this might well be a very good
> > way to go.
> 
> I'm wondering:
> 
> > >  // RCU
> > > -rcu_read_lock() { __fence{rcu-lock}; }
> > > -rcu_read_unlock() { __fence{rcu-unlock};}
> > > -synchronize_rcu() { __fence{sync-rcu}; }
> > > -synchronize_rcu_expedited() { __fence{sync-rcu}; }
> > > +rcu_read_lock() { __fence{rcu_lock}; }
> > > +rcu_read_unlock() { __fence{rcu_unlock};}
> > > +synchronize_rcu() { __fence{sync_rcu}; }
> > > +synchronize_rcu_expedited() { __fence{sync_rcu}; }
> 
> What's the point of using '-' instead of '_'? In a program language syntax 
> environment it's easy to confuse it with a '-' operator, and it also looks 
> slightly sloppy and inconsistent if we sometimes have '_' and sometimes '-'.
> 
> If it used on purpose, to separate namespaces from kernel internal API names,
> then that's rather obscure IMHO and then I'd rather suggest proper prefixes 
> instead.

These lines are connecting Linux-kernel names to cat-language names.
The cat language can be thought of as a set-based constraint language,
which doesn't have subtraction (the closest analog being set difference,
which is denoted by "\").  Cat-language code has used "-" as a word
separator in names, and the model had previously had an odd mixture of
"-" and "_".  Hence, the switch to the cat-language convention.

Of course, if underscore is strongly preferred, underscore does work,
and it should be possible to move in that direction.

							Thanx, Paul

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Ingo Molnar]

* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:

> Cat-language code has used "-" as a word
> separator in names, and the model had previously had an odd mixture of
> "-" and "_".  Hence, the switch to the cat-language convention.
> 
> Of course, if underscore is strongly preferred, underscore does work,
> and it should be possible to move in that direction.

I'm fine with either of these variants, as long as it's consistent: the 
idiosynchratic seeming mixture of both '-' and '_' convention looked odd to me.

If '_' is also more compatible with installed versions of the language, then I'd 
go for that - but it's your call.

Thanks,

	Ingo

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Akira Yokosawa]

On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote:
> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Fri, 9 Feb 2018 04:51:05 -0800
>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
>>
>> As of herd7 7.47, these '-'s are not permitted and end up in
>> errors such as:
>>
>>     File "./linux-kernel.def", line 44, characters 29-30:
>>     unexpected '-' (in macros)
>>
>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
>> identifiers match ASPLOS paper") in the repository at
>> https://github.com/aparri/memory-model can restore the compatibility
>> with herd7 7.47.
>>
>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
>> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>> ---
>> Paul,
>>
>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> 
> Thank you, Akira!
> 
> I am going to hold off on this for a bit to see if we can instead get
> a new release of herd7, but if we can't. this might well be a very good
> way to go.

So, herdtools7.7.48 is now available by "opam update; opam upgrade".
Maybe mentioning the required version of herdtools7 in README would help.

One glitch I'm aware of is one of the output of klitmus7 fails to
compile on kernels prior to 4.14, because of smp_mb__after_spinlock()
used in Z6.0+pooncelock+poonceLock+pombonce.litmus.

And there is a question I want to ask.

Z6.0+pooncelock+pooncelock+pombonce.litmus, which doesn't have
smp_mb__after_spinlock(), has a comment of:

(*
 * Result: Never
 *
 * This example demonstrates that a pair of accesses made by different
 * processes each while holding a given lock will not necessarily be
 * seen as ordered by a third process not holding that lock.
 *)

The result was changed from "Sometimes" to "Never" in response to
Alan's feedback the other day, but the following comment indicates
the result should be "Sometimes". And the current model gives the
result of "Sometimes".

As I have no idea of the pending patches, I'd like to know once
the pending patches are applied, would 
Z6.0+pooncelock+pooncelock+pombonce.litmus and
Z6.0+pooncelock+poonceLock+pombonce.litmus become identical?

    Thanks, Akira

> 
> 							Thanx, Paul
[...]
d_lock*)  ||
>> +		'rcu_unlock (*rcu_read_unlock*) ||
>> +		'sync_rcu (*synchronize_rcu*) ||
>>  		'before_atomic (*smp_mb__before_atomic*) ||
>>  		'after_atomic (*smp_mb__after_atomic*) ||
>>  		'after_spinlock (*smp_mb__after_spinlock*)
>> @@ -35,8 +35,8 @@ instructions F[Barriers]
>>
>>  (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
>>  let matched = let rec
>> -	    unmatched-locks = Rcu-lock \ domain(matched)
>> -	and unmatched-unlocks = Rcu-unlock \ range(matched)
>> +	    unmatched-locks = Rcu_lock \ domain(matched)
>> +	and unmatched-unlocks = Rcu_unlock \ range(matched)
>>  	and unmatched = unmatched-locks | unmatched-unlocks
>>  	and unmatched-po = [unmatched] ; po ; [unmatched]
>>  	and unmatched-locks-to-unlocks =
>> @@ -46,8 +46,8 @@ let matched = let rec
>>  	in matched
>>
>>  (* Validate nesting *)
>> -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
>> -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
>> +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking
>> +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking
>>
>>  (* Outermost level of nesting only *)
>>  let crit = matched \ (po^-1 ; matched ; po^-1)
>> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
>> index babe2b3..d0085d5 100644
>> --- a/tools/memory-model/linux-kernel.cat
>> +++ b/tools/memory-model/linux-kernel.cat
>> @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) |
>>  	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
>>  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
>>  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
>> -let gp = po ; [Sync-rcu] ; po?
>> +let gp = po ; [Sync_rcu] ; po?
>>
>>  let strong-fence = mb | gp
>>
>> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
>> index a397387..fc08371 100644
>> --- a/tools/memory-model/linux-kernel.def
>> +++ b/tools/memory-model/linux-kernel.def
>> @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; }
>>  spin_trylock(X) __trylock(X)
>>
>>  // RCU
>> -rcu_read_lock() { __fence{rcu-lock}; }
>> -rcu_read_unlock() { __fence{rcu-unlock};}
>> -synchronize_rcu() { __fence{sync-rcu}; }
>> -synchronize_rcu_expedited() { __fence{sync-rcu}; }
>> +rcu_read_lock() { __fence{rcu_lock}; }
>> +rcu_read_unlock() { __fence{rcu_unlock};}
>> +synchronize_rcu() { __fence{sync_rcu}; }
>> +synchronize_rcu_expedited() { __fence{sync_rcu}; }
>>
>>  // Atomic
>>  atomic_read(X) READ_ONCE(*X)
>> -- 
>> 2.7.4
>>
>>
> 

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Paul E. McKenney]

On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote:
> On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote:
> > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
> >> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> Date: Fri, 9 Feb 2018 04:51:05 -0800
> >> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
> >>
> >> As of herd7 7.47, these '-'s are not permitted and end up in
> >> errors such as:
> >>
> >>     File "./linux-kernel.def", line 44, characters 29-30:
> >>     unexpected '-' (in macros)
> >>
> >> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
> >> identifiers match ASPLOS paper") in the repository at
> >> https://github.com/aparri/memory-model can restore the compatibility
> >> with herd7 7.47.
> >>
> >> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
> >> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >> ---
> >> Paul,
> >>
> >> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> > 
> > Thank you, Akira!
> > 
> > I am going to hold off on this for a bit to see if we can instead get
> > a new release of herd7, but if we can't. this might well be a very good
> > way to go.
> 
> So, herdtools7.7.48 is now available by "opam update; opam upgrade".
> Maybe mentioning the required version of herdtools7 in README would help.

Or have some way for the memory model's .cat files to state what version
they need, but in the meantime please see the patch below.  But even with
such version specification, we probably want to have the version in the
README...

> One glitch I'm aware of is one of the output of klitmus7 fails to
> compile on kernels prior to 4.14, because of smp_mb__after_spinlock()
> used in Z6.0+pooncelock+poonceLock+pombonce.litmus.

This is one advantage of having the memory model in the kernel source
itself -- the versions match.  And people can always fire up a different
kernel version (for example, within a VM) to run the output of klitmus7.

> And there is a question I want to ask.
> 
> Z6.0+pooncelock+pooncelock+pombonce.litmus, which doesn't have
> smp_mb__after_spinlock(), has a comment of:
> 
> (*
>  * Result: Never
>  *
>  * This example demonstrates that a pair of accesses made by different
>  * processes each while holding a given lock will not necessarily be
>  * seen as ordered by a third process not holding that lock.
>  *)
> 
> The result was changed from "Sometimes" to "Never" in response to
> Alan's feedback the other day, but the following comment indicates
> the result should be "Sometimes". And the current model gives the
> result of "Sometimes".
> 
> As I have no idea of the pending patches, I'd like to know once
> the pending patches are applied, would 
> Z6.0+pooncelock+pooncelock+pombonce.litmus and
> Z6.0+pooncelock+poonceLock+pombonce.litmus become identical?

Let's see, examining the Z6 litmus tests and running on herd7 version 7.48:

Z6.0+pooncelock+pooncelock+pombonce Sometimes 1 7
Z6.0+pooncelock+poonceLock+pombonce Never 0 7
Z6.0+pooncerelease+poacquirerelease+mbonceonce Sometimes 1 7

But Alan stated that the result of the test would be changed by one of
the patches in our "pending" list.  I ran with all the patches currently
applied, so I am guessing that Alan was refering to one of the changes
that we have discussed but not yet created.

Alan, enlightenment?

							Thanx, Paul

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

commit dad94d8dc78e50bab91b313a67232e85ee22a733
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Wed Feb 14 14:37:22 2018 -0800

    tools/memory-model: Add required herd7 version to README file
    
    LKMM and the herd7 tool are co-evolving, and out-of-date herd7 tools
    produce inaccurate results, often with no obvious error messages.  This
    commit therefore adds the required herd7 version to the LKMM README file.
    
    Longer term, it would be good if .cat files could specify the required
    version in a manner allowing herd7 to produce clear diagnostics.
    
    Suggested-by: Akira Yokosawa <akiyks@gmail.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/tools/memory-model/README b/tools/memory-model/README
index 91414a49fac5..ea950c566ffd 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -20,7 +20,8 @@ that litmus test to be exercised within the Linux kernel.
 REQUIREMENTS
 ============
 
-The "herd7" and "klitmus7" tools must be downloaded separately:
+Version 7.48 of the "herd7" and "klitmus7" tools must be downloaded
+separately:
 
   https://github.com/herd/herdtools7
 

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Alan Stern]

On Wed, 14 Feb 2018, Paul E. McKenney wrote:

> Let's see, examining the Z6 litmus tests and running on herd7 version 7.48:
> 
> Z6.0+pooncelock+pooncelock+pombonce Sometimes 1 7
> Z6.0+pooncelock+poonceLock+pombonce Never 0 7
> Z6.0+pooncerelease+poacquirerelease+mbonceonce Sometimes 1 7
> 
> But Alan stated that the result of the test would be changed by one of
> the patches in our "pending" list.  I ran with all the patches currently
> applied, so I am guessing that Alan was refering to one of the changes
> that we have discussed but not yet created.
> 
> Alan, enlightenment?

Here's the relevant patch.  It may need some manual adjustment, because 
it was not made against the files currently in the repository.

Alan


diff --git a/linux-kernel-hardware.cat b/linux-kernel-hardware.cat
Index: memory-model/linux-kernel-hardware.cat
===================================================================
--- memory-model.orig/linux-kernel-hardware.cat
+++ memory-model/linux-kernel-hardware.cat
@@ -31,7 +31,7 @@ let strong-fence = mb | gp
 (* Release Acquire *)
 let acq-po = [Acquire] ; po ; [M]
 let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po
 
 (**********************************)
 (* Fundamental coherence ordering *)
@@ -57,13 +57,13 @@ let to-w = rwdep | addrpo | (overwrite &
 let rdw = po-loc & (fre ; rfe)
 let detour = po-loc & (coe ; rfe)
 let rrdep = addr | (dep ; rfi)
-let to-r = rrdep | rfi-rel-acq
-let fence = strong-fence | wmb | po-rel | rmb | acq-po
+let to-r = rrdep
+let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int)
 let ppo = to-r | to-w | fence | rdw | detour
 
 (* Happens Before *)
 let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po
 
 let rec prop = (overwrite & ext)? ; cumul-fence ; hb*
     and hb = ppo | rfe | ((hb* ; prop) & int)
Index: memory-model/linux-kernel.cat
===================================================================
--- memory-model.orig/linux-kernel.cat
+++ memory-model/linux-kernel.cat
@@ -31,7 +31,7 @@ let strong-fence = mb | gp
 (* Release Acquire *)
 let acq-po = [Acquire] ; po ; [M]
 let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po
 
 (**********************************)
 (* Fundamental coherence ordering *)
@@ -54,13 +54,13 @@ let rwdep = (dep | ctrl) ; [W]
 let overwrite = co | fr
 let to-w = rwdep | (overwrite & int)
 let rrdep = addr | (dep ; rfi)
-let to-r = rrdep | rfi-rel-acq
-let fence = strong-fence | wmb | po-rel | rmb | acq-po
+let to-r = rrdep
+let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int)
 let ppo = to-r | to-w | fence
 
 (* Propagation: Ordering from release operations and strong fences. *)
 let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po
 let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
 
 (*

Trial of conflict resolution of Alan's patch

[Akira Yokosawa]

>From 81bd6374057f0d89894ead482b870e2f001d2998 Mon Sep 17 00:00:00 2001
From: Alan Stern <stern@rowland.harvard.edu>
Date: Fri, 16 Feb 2018 00:29:56 +0900
Subject: [PATCH] [TENTATIVE] Trial conflict resolution of Alan's patch

This is a trial of conflict resolution of the patch Alan provided.

Alan's message and original patch:

    Here's the relevant patch.  It may need some manual adjustment, because
    it was not made against the files currently in the repository.

    Alan

    diff --git a/linux-kernel-hardware.cat b/linux-kernel-hardware.cat
    Index: memory-model/linux-kernel-hardware.cat
    ===================================================================
    --- memory-model.orig/linux-kernel-hardware.cat
    +++ memory-model/linux-kernel-hardware.cat
    @@ -31,7 +31,7 @@ let strong-fence = mb | gp
     (* Release Acquire *)
     let acq-po = [Acquire] ; po ; [M]
     let po-rel = [M] ; po ; [Release]
    -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
    +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po

     (**********************************)
     (* Fundamental coherence ordering *)
    @@ -57,13 +57,13 @@ let to-w = rwdep | addrpo | (overwrite &
     let rdw = po-loc & (fre ; rfe)
     let detour = po-loc & (coe ; rfe)
     let rrdep = addr | (dep ; rfi)
    -let to-r = rrdep | rfi-rel-acq
    -let fence = strong-fence | wmb | po-rel | rmb | acq-po
    +let to-r = rrdep
    +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int)
     let ppo = to-r | to-w | fence | rdw | detour

     (* Happens Before *)
     let A-cumul(r) = rfe? ; r
    -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
    +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po

     let rec prop = (overwrite & ext)? ; cumul-fence ; hb*
         and hb = ppo | rfe | ((hb* ; prop) & int)
    Index: memory-model/linux-kernel.cat
    ===================================================================
    --- memory-model.orig/linux-kernel.cat
    +++ memory-model/linux-kernel.cat
    @@ -31,7 +31,7 @@ let strong-fence = mb | gp
     (* Release Acquire *)
     let acq-po = [Acquire] ; po ; [M]
     let po-rel = [M] ; po ; [Release]
    -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
    +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po

     (**********************************)
     (* Fundamental coherence ordering *)
    @@ -54,13 +54,13 @@ let rwdep = (dep | ctrl) ; [W]
     let overwrite = co | fr
     let to-w = rwdep | (overwrite & int)
     let rrdep = addr | (dep ; rfi)
    -let to-r = rrdep | rfi-rel-acq
    -let fence = strong-fence | wmb | po-rel | rmb | acq-po
    +let to-r = rrdep
    +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int)
     let ppo = to-r | to-w | fence

     (* Propagation: Ordering from release operations and strong fences. *)
     let A-cumul(r) = rfe? ; r
    -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
    +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po
     let prop = (overwrite & ext)? ; cumul-fence* ; rfe?

     (*

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
[akiyks: Rebased to current master]
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
So, I attempted to rebase the patch to current (somewhat old) master of
https://github.com/aparri/memory-model. Why? Because the lkmm branch
in Paul's -rcu tree doesn't have linux-kernel-hardware.cat.

However, after this change, Z6.0+pooncelock+pooncelock+pombonce still
has the result "Sometimes". I must have done something wrong in the
conflict resolution.

Note: I have almost no idea what this patch is doing. I'm just hoping
to give a starting point of a discussion.

    Thanks, Akira
--
 linux-kernel-hardware.cat | 9 ++++-----
 linux-kernel.cat          | 9 ++++-----
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/linux-kernel-hardware.cat b/linux-kernel-hardware.cat
index 7768bf7..6c35655 100644
--- a/linux-kernel-hardware.cat
+++ b/linux-kernel-hardware.cat
@@ -34,7 +34,7 @@ let strong-fence = mb | gp
 (* Release Acquire *)
 let acq-po = [Acquire] ; po ; [M]
 let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po
 
 (**********************************)
 (* Fundamental coherence ordering *)
@@ -60,14 +60,13 @@ let to-w = rwdep | addrpo | (overwrite & int)
 let rdw = po-loc & (fre ; rfe)
 let detour = po-loc & (coe ; rfe)
 let rrdep = addr | (dep ; rfi) | rdw
-let strong-rrdep = rrdep+ & rb-dep
-let to-r = strong-rrdep | rfi-rel-acq
-let fence = strong-fence | wmb | po-rel | rmb | acq-po
+let to-r = rrdep
+let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int)
 let ppo = (rrdep* ; (to-r | to-w | fence)) | rdw | detour
 
 (* Happens Before *)
 let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po
 
 let rec prop = (overwrite & ext)? ; cumul-fence ; hb*
     and hb = ppo | rfe | ((hb* ; prop) & int)
diff --git a/linux-kernel.cat b/linux-kernel.cat
index 15b7a5d..c6b0752 100644
--- a/linux-kernel.cat
+++ b/linux-kernel.cat
@@ -39,7 +39,7 @@ let strong-fence = mb | gp
 (* Release Acquire *)
 let acq-po = [Acquire] ; po ; [M]
 let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po
 
 (**********************************)
 (* Fundamental coherence ordering *)
@@ -62,14 +62,13 @@ let rwdep = (dep | ctrl) ; [W]
 let overwrite = co | fr
 let to-w = rwdep | (overwrite & int)
 let rrdep = addr | (dep ; rfi)
-let strong-rrdep = rrdep+ & rb-dep
-let to-r = strong-rrdep | rfi-rel-acq
-let fence = strong-fence | wmb | po-rel | rmb | acq-po
+let to-r = rrdep
+let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int)
 let ppo = rrdep* ; (to-r | to-w | fence)
 
 (* Propagation: Ordering from release operations and strong fences. *)
 let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po
 let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
 
 (*
-- 
2.7.4

Re: Trial of conflict resolution of Alan's patch

[Alan Stern]

On Fri, 16 Feb 2018, Akira Yokosawa wrote:

> So, I attempted to rebase the patch to current (somewhat old) master of
> https://github.com/aparri/memory-model. Why? Because the lkmm branch
> in Paul's -rcu tree doesn't have linux-kernel-hardware.cat.
> 
> However, after this change, Z6.0+pooncelock+pooncelock+pombonce still
> has the result "Sometimes". I must have done something wrong in the
> conflict resolution.
> 
> Note: I have almost no idea what this patch is doing. I'm just hoping
> to give a starting point of a discussion.

Yes, that litmus test gives "Sometimes" both with and without the 
patch.  But consider instead this slightly changed version of that 
test, in which P2 reads Z instead of writing it:

C Z6.0-variant

{}

P0(int *x, int *y, spinlock_t *mylock)
{
	spin_lock(mylock);
	WRITE_ONCE(*x, 1);
	WRITE_ONCE(*y, 1);
	spin_unlock(mylock);
}

P1(int *y, int *z, spinlock_t *mylock)
{
	int r0;

	spin_lock(mylock);
	r0 = READ_ONCE(*y);
	WRITE_ONCE(*z, 1);
	spin_unlock(mylock);
}

P2(int *x, int *z)
{
	int r1;
	int r2;

	r2 = READ_ONCE(*z);
	smp_mb();
	r1 = READ_ONCE(*x);
}

exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)

Without the patch, this test gives "Sometimes"; with the patch it gives 
"Never".  That is what I thought Paul was talking about originally.  

Sorry if my misunderstanding caused too much confusion for other 
people.

Alan

Re: Trial of conflict resolution of Alan's patch

[Paul E. McKenney]

On Thu, Feb 15, 2018 at 12:51:56PM -0500, Alan Stern wrote:
> On Fri, 16 Feb 2018, Akira Yokosawa wrote:
> 
> > So, I attempted to rebase the patch to current (somewhat old) master of
> > https://github.com/aparri/memory-model. Why? Because the lkmm branch
> > in Paul's -rcu tree doesn't have linux-kernel-hardware.cat.
> > 
> > However, after this change, Z6.0+pooncelock+pooncelock+pombonce still
> > has the result "Sometimes". I must have done something wrong in the
> > conflict resolution.
> > 
> > Note: I have almost no idea what this patch is doing. I'm just hoping
> > to give a starting point of a discussion.
> 
> Yes, that litmus test gives "Sometimes" both with and without the 
> patch.  But consider instead this slightly changed version of that 
> test, in which P2 reads Z instead of writing it:
> 
> C Z6.0-variant
> 
> {}
> 
> P0(int *x, int *y, spinlock_t *mylock)
> {
> 	spin_lock(mylock);
> 	WRITE_ONCE(*x, 1);
> 	WRITE_ONCE(*y, 1);
> 	spin_unlock(mylock);
> }
> 
> P1(int *y, int *z, spinlock_t *mylock)
> {
> 	int r0;
> 
> 	spin_lock(mylock);
> 	r0 = READ_ONCE(*y);
> 	WRITE_ONCE(*z, 1);
> 	spin_unlock(mylock);
> }
> 
> P2(int *x, int *z)
> {
> 	int r1;
> 	int r2;
> 
> 	r2 = READ_ONCE(*z);
> 	smp_mb();
> 	r1 = READ_ONCE(*x);
> }
> 
> exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> 
> Without the patch, this test gives "Sometimes"; with the patch it gives 
> "Never".  That is what I thought Paul was talking about originally.  
> 
> Sorry if my misunderstanding caused too much confusion for other 
> people.

Ah, I did indeed get confused.  I have changed the "Result:" for
Z6.0+pooncelock+pooncelock+pombonce.litmus back to "Never", as in
the patch below (which I merged into the patch adding all the
comments).

I have added the above test as ISA2+pooncelock+pooncelock+pombonce.litmus,
with the Result: of Sometimes with you (Alan) as author and with your
Signed-off-by -- please let me know if you would prefer some other
approach.

Please change the Result: when sending the proposed patch.  Or please let
me know if you would like me to apply the forward-port that Akira sent,
in which case I will add the Result: change to that patch.  Or for that
matter, Akira might repost his forward-port of your patch with this change.

							Thanx, Paul

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

commit b2950420e1154131c0667f1ac58666bad3a06a69
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Thu Feb 15 10:35:25 2018 -0800

    fixup! EXP litmus_tests:  Add comments explaining tests' purposes
    
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
index fad47258a3e3..95890669859b 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
@@ -1,7 +1,7 @@
 C Z6.0+pooncelock+pooncelock+pombonce
 
 (*
- * Result: Never
+ * Result: Somtimes
  *
  * This example demonstrates that a pair of accesses made by different
  * processes each while holding a given lock will not necessarily be

Re: Trial of conflict resolution of Alan's patch

[Akira Yokosawa]

On 2018/02/15 11:29:14 -0800, Paul E. McKenney wrote:
> On Thu, Feb 15, 2018 at 12:51:56PM -0500, Alan Stern wrote:
>> On Fri, 16 Feb 2018, Akira Yokosawa wrote:
>>
>>> So, I attempted to rebase the patch to current (somewhat old) master of
>>> https://github.com/aparri/memory-model. Why? Because the lkmm branch
>>> in Paul's -rcu tree doesn't have linux-kernel-hardware.cat.
>>>
>>> However, after this change, Z6.0+pooncelock+pooncelock+pombonce still
>>> has the result "Sometimes". I must have done something wrong in the
>>> conflict resolution.
>>>
>>> Note: I have almost no idea what this patch is doing. I'm just hoping
>>> to give a starting point of a discussion.
>>
>> Yes, that litmus test gives "Sometimes" both with and without the 
>> patch.  But consider instead this slightly changed version of that 
>> test, in which P2 reads Z instead of writing it:
>>
>> C Z6.0-variant
>>
>> {}
>>
>> P0(int *x, int *y, spinlock_t *mylock)
>> {
>> 	spin_lock(mylock);
>> 	WRITE_ONCE(*x, 1);
>> 	WRITE_ONCE(*y, 1);
>> 	spin_unlock(mylock);
>> }
>>
>> P1(int *y, int *z, spinlock_t *mylock)
>> {
>> 	int r0;
>>
>> 	spin_lock(mylock);
>> 	r0 = READ_ONCE(*y);
>> 	WRITE_ONCE(*z, 1);
>> 	spin_unlock(mylock);
>> }
>>
>> P2(int *x, int *z)
>> {
>> 	int r1;
>> 	int r2;
>>
>> 	r2 = READ_ONCE(*z);
>> 	smp_mb();
>> 	r1 = READ_ONCE(*x);
>> }
>>
>> exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
>>
>> Without the patch, this test gives "Sometimes"; with the patch it gives 
>> "Never".  That is what I thought Paul was talking about originally.  
>>
>> Sorry if my misunderstanding caused too much confusion for other 
>> people.
> 
> Ah, I did indeed get confused.  I have changed the "Result:" for
> Z6.0+pooncelock+pooncelock+pombonce.litmus back to "Never", as in
> the patch below (which I merged into the patch adding all the
> comments).
> 
> I have added the above test as ISA2+pooncelock+pooncelock+pombonce.litmus,
> with the Result: of Sometimes with you (Alan) as author and with your
> Signed-off-by -- please let me know if you would prefer some other
> approach.
> 
> Please change the Result: when sending the proposed patch.  Or please let
> me know if you would like me to apply the forward-port that Akira sent,
> in which case I will add the Result: change to that patch.  Or for that
> matter, Akira might repost his forward-port of your patch with this change.
> 

Hi,

My forward-port patch doesn't apply to the "lkmm" branch.
It looks like "linux-kernel-hardware.cat" is intentionally omitted there.
Am I guessing right?

If this is the case, I can prepare a patch to be applied to "lkmm".
But I can't compose a proper change log. So I'd like Alan to post
a patch with my SOB appended. Does this approach sound reasonable?

      Thanks, Akira

> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit b2950420e1154131c0667f1ac58666bad3a06a69
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date:   Thu Feb 15 10:35:25 2018 -0800
> 
>     fixup! EXP litmus_tests:  Add comments explaining tests' purposes
>     
>     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> index fad47258a3e3..95890669859b 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> @@ -1,7 +1,7 @@
>  C Z6.0+pooncelock+pooncelock+pombonce
>  
>  (*
> - * Result: Never
> + * Result: Somtimes
>   *
>   * This example demonstrates that a pair of accesses made by different
>   * processes each while holding a given lock will not necessarily be
> 

Re: Trial of conflict resolution of Alan's patch

[Andrea Parri]

On Thu, Feb 15, 2018 at 11:29:14AM -0800, Paul E. McKenney wrote:
> On Thu, Feb 15, 2018 at 12:51:56PM -0500, Alan Stern wrote:
> > On Fri, 16 Feb 2018, Akira Yokosawa wrote:
> > 
> > > So, I attempted to rebase the patch to current (somewhat old) master of
> > > https://github.com/aparri/memory-model. Why? Because the lkmm branch
> > > in Paul's -rcu tree doesn't have linux-kernel-hardware.cat.
> > > 
> > > However, after this change, Z6.0+pooncelock+pooncelock+pombonce still
> > > has the result "Sometimes". I must have done something wrong in the
> > > conflict resolution.
> > > 
> > > Note: I have almost no idea what this patch is doing. I'm just hoping
> > > to give a starting point of a discussion.
> > 
> > Yes, that litmus test gives "Sometimes" both with and without the 
> > patch.  But consider instead this slightly changed version of that 
> > test, in which P2 reads Z instead of writing it:
> > 
> > C Z6.0-variant
> > 
> > {}
> > 
> > P0(int *x, int *y, spinlock_t *mylock)
> > {
> > 	spin_lock(mylock);
> > 	WRITE_ONCE(*x, 1);
> > 	WRITE_ONCE(*y, 1);
> > 	spin_unlock(mylock);
> > }
> > 
> > P1(int *y, int *z, spinlock_t *mylock)
> > {
> > 	int r0;
> > 
> > 	spin_lock(mylock);
> > 	r0 = READ_ONCE(*y);
> > 	WRITE_ONCE(*z, 1);
> > 	spin_unlock(mylock);
> > }
> > 
> > P2(int *x, int *z)
> > {
> > 	int r1;
> > 	int r2;
> > 
> > 	r2 = READ_ONCE(*z);
> > 	smp_mb();
> > 	r1 = READ_ONCE(*x);
> > }
> > 
> > exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > 
> > Without the patch, this test gives "Sometimes"; with the patch it gives 
> > "Never".  That is what I thought Paul was talking about originally.  
> > 
> > Sorry if my misunderstanding caused too much confusion for other 
> > people.
> 
> Ah, I did indeed get confused.  I have changed the "Result:" for
> Z6.0+pooncelock+pooncelock+pombonce.litmus back to "Never", as in
> the patch below (which I merged into the patch adding all the
> comments).
> 
> I have added the above test as ISA2+pooncelock+pooncelock+pombonce.litmus,
> with the Result: of Sometimes with you (Alan) as author and with your
> Signed-off-by -- please let me know if you would prefer some other
> approach.
> 
> Please change the Result: when sending the proposed patch.  Or please let
> me know if you would like me to apply the forward-port that Akira sent,
> in which case I will add the Result: change to that patch.  Or for that
> matter, Akira might repost his forward-port of your patch with this change.
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit b2950420e1154131c0667f1ac58666bad3a06a69
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date:   Thu Feb 15 10:35:25 2018 -0800
> 
>     fixup! EXP litmus_tests:  Add comments explaining tests' purposes
>     
>     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> index fad47258a3e3..95890669859b 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> @@ -1,7 +1,7 @@
>  C Z6.0+pooncelock+pooncelock+pombonce
>  
>  (*
> - * Result: Never
> + * Result: Somtimes

nit: s/Somtimes/Sometimes

  Andrea


>   *
>   * This example demonstrates that a pair of accesses made by different
>   * processes each while holding a given lock will not necessarily be
> 

Re: [PATCH RFC tip/lkmm 08/10] EXP Remove understore from smp_mb__before_atomic() workings

[Andrea Parri]

On Fri, Feb 09, 2018 at 06:20:29AM -0800, Paul E. McKenney wrote:
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

nit: s/understore/underscore  (a very understandable lapsus, BTW ;-)

According to the cover letter, patches 8-10 of this series are intended
to be squashed together;  it could be useful to add a description then:
the motivation for these changes might appear "trivial" today;  months/
years from now?  mmh, I can't put my finger on it ;-)

IMO,  this descrition should also mention why this solution "is the way
to go" (e.g., compare with the solution recently implemented by Akira).

  Andrea


> ---
>  tools/memory-model/linux-kernel.bell | 2 +-
>  tools/memory-model/linux-kernel.cat  | 2 +-
>  tools/memory-model/linux-kernel.def  | 2 +-
>  3 files changed, 3 insertions(+), 3 deletions(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index b984bbda01a5..558bbef9e08a 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -28,7 +28,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
>  		'rcu-lock (*rcu_read_lock*)  ||
>  		'rcu-unlock (*rcu_read_unlock*) ||
>  		'sync-rcu (*synchronize_rcu*) ||
> -		'before_atomic (*smp_mb__before_atomic*) ||
> +		'before-atomic (*smp_mb__before_atomic*) ||
>  		'after_atomic (*smp_mb__after_atomic*) ||
>  		'after_spinlock (*smp_mb__after_spinlock*)
>  instructions F[Barriers]
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index babe2b3b0bb3..31c08a44c088 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -29,7 +29,7 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
>  let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
>  let wmb = [W] ; fencerel(Wmb) ; [W]
>  let mb = ([M] ; fencerel(Mb) ; [M]) |
> -	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
> +	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
>  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
>  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
>  let gp = po ; [Sync-rcu] ; po?
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index a397387f77cc..ff4b756f4a44 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -21,7 +21,7 @@ smp_mb() { __fence{mb} ; }
>  smp_rmb() { __fence{rmb} ; }
>  smp_wmb() { __fence{wmb} ; }
>  smp_read_barrier_depends() { __fence{rb_dep}; }
> -smp_mb__before_atomic() { __fence{before_atomic} ; }
> +smp_mb__before_atomic() { __fence{before-atomic} ; }
>  smp_mb__after_atomic() { __fence{after_atomic} ; }
>  smp_mb__after_spinlock() { __fence{after_spinlock} ; }
>  
> -- 
> 2.5.2
> 

Re: Trial of conflict resolution of Alan's patch

[Paul E. McKenney]

On Thu, Feb 15, 2018 at 11:05:39PM +0100, Andrea Parri wrote:
> On Thu, Feb 15, 2018 at 11:29:14AM -0800, Paul E. McKenney wrote:
> > On Thu, Feb 15, 2018 at 12:51:56PM -0500, Alan Stern wrote:
> > > On Fri, 16 Feb 2018, Akira Yokosawa wrote:
> > > 
> > > > So, I attempted to rebase the patch to current (somewhat old) master of
> > > > https://github.com/aparri/memory-model. Why? Because the lkmm branch
> > > > in Paul's -rcu tree doesn't have linux-kernel-hardware.cat.
> > > > 
> > > > However, after this change, Z6.0+pooncelock+pooncelock+pombonce still
> > > > has the result "Sometimes". I must have done something wrong in the
> > > > conflict resolution.
> > > > 
> > > > Note: I have almost no idea what this patch is doing. I'm just hoping
> > > > to give a starting point of a discussion.
> > > 
> > > Yes, that litmus test gives "Sometimes" both with and without the 
> > > patch.  But consider instead this slightly changed version of that 
> > > test, in which P2 reads Z instead of writing it:
> > > 
> > > C Z6.0-variant
> > > 
> > > {}
> > > 
> > > P0(int *x, int *y, spinlock_t *mylock)
> > > {
> > > 	spin_lock(mylock);
> > > 	WRITE_ONCE(*x, 1);
> > > 	WRITE_ONCE(*y, 1);
> > > 	spin_unlock(mylock);
> > > }
> > > 
> > > P1(int *y, int *z, spinlock_t *mylock)
> > > {
> > > 	int r0;
> > > 
> > > 	spin_lock(mylock);
> > > 	r0 = READ_ONCE(*y);
> > > 	WRITE_ONCE(*z, 1);
> > > 	spin_unlock(mylock);
> > > }
> > > 
> > > P2(int *x, int *z)
> > > {
> > > 	int r1;
> > > 	int r2;
> > > 
> > > 	r2 = READ_ONCE(*z);
> > > 	smp_mb();
> > > 	r1 = READ_ONCE(*x);
> > > }
> > > 
> > > exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
> > > 
> > > Without the patch, this test gives "Sometimes"; with the patch it gives 
> > > "Never".  That is what I thought Paul was talking about originally.  
> > > 
> > > Sorry if my misunderstanding caused too much confusion for other 
> > > people.
> > 
> > Ah, I did indeed get confused.  I have changed the "Result:" for
> > Z6.0+pooncelock+pooncelock+pombonce.litmus back to "Never", as in
> > the patch below (which I merged into the patch adding all the
> > comments).
> > 
> > I have added the above test as ISA2+pooncelock+pooncelock+pombonce.litmus,
> > with the Result: of Sometimes with you (Alan) as author and with your
> > Signed-off-by -- please let me know if you would prefer some other
> > approach.
> > 
> > Please change the Result: when sending the proposed patch.  Or please let
> > me know if you would like me to apply the forward-port that Akira sent,
> > in which case I will add the Result: change to that patch.  Or for that
> > matter, Akira might repost his forward-port of your patch with this change.
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit b2950420e1154131c0667f1ac58666bad3a06a69
> > Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > Date:   Thu Feb 15 10:35:25 2018 -0800
> > 
> >     fixup! EXP litmus_tests:  Add comments explaining tests' purposes
> >     
> >     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > index fad47258a3e3..95890669859b 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > @@ -1,7 +1,7 @@
> >  C Z6.0+pooncelock+pooncelock+pombonce
> >  
> >  (*
> > - * Result: Never
> > + * Result: Somtimes
> 
> nit: s/Somtimes/Sometimes

Good catch, fixed!

							Thanx, Paul

>   Andrea
> 
> 
> >   *
> >   * This example demonstrates that a pair of accesses made by different
> >   * processes each while holding a given lock will not necessarily be
> > 
> 

Re: [PATCH RFC tip/lkmm 08/10] EXP Remove understore from smp_mb__before_atomic() workings

[Paul E. McKenney]

On Thu, Feb 15, 2018 at 11:30:09PM +0100, Andrea Parri wrote:
> On Fri, Feb 09, 2018 at 06:20:29AM -0800, Paul E. McKenney wrote:
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> nit: s/understore/underscore  (a very understandable lapsus, BTW ;-)

;-)

Will fix when squashing.

> According to the cover letter, patches 8-10 of this series are intended
> to be squashed together;  it could be useful to add a description then:
> the motivation for these changes might appear "trivial" today;  months/
> years from now?  mmh, I can't put my finger on it ;-)

Assuming we keep these patches, agreed.  Something like this for the
aggregated single commit, perhaps:

	tools/memory-model: Convert underscores to hyphens

	Typical cat-language code uses hyphens for word separators in
	identifiers, but several LKMM identifiers use underscores instead.
	This commit therefore converts the underscores in the .bell and
	.cat files for smp_mb__before_atomic(), smp_mb__after_atomic(),
	and smp_mb__after_spinlock() to hyphens.

> IMO,  this descrition should also mention why this solution "is the way
> to go" (e.g., compare with the solution recently implemented by Akira).

You lost me here.  Or are you asking for a commit log similar to that
provided by Akira for his forward-port of Alan's unrelated patch?  If
so, please see above.

							Thanx, Paul

>   Andrea
> 
> 
> > ---
> >  tools/memory-model/linux-kernel.bell | 2 +-
> >  tools/memory-model/linux-kernel.cat  | 2 +-
> >  tools/memory-model/linux-kernel.def  | 2 +-
> >  3 files changed, 3 insertions(+), 3 deletions(-)
> > 
> > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> > index b984bbda01a5..558bbef9e08a 100644
> > --- a/tools/memory-model/linux-kernel.bell
> > +++ b/tools/memory-model/linux-kernel.bell
> > @@ -28,7 +28,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
> >  		'rcu-lock (*rcu_read_lock*)  ||
> >  		'rcu-unlock (*rcu_read_unlock*) ||
> >  		'sync-rcu (*synchronize_rcu*) ||
> > -		'before_atomic (*smp_mb__before_atomic*) ||
> > +		'before-atomic (*smp_mb__before_atomic*) ||
> >  		'after_atomic (*smp_mb__after_atomic*) ||
> >  		'after_spinlock (*smp_mb__after_spinlock*)
> >  instructions F[Barriers]
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index babe2b3b0bb3..31c08a44c088 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -29,7 +29,7 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
> >  let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
> >  let wmb = [W] ; fencerel(Wmb) ; [W]
> >  let mb = ([M] ; fencerel(Mb) ; [M]) |
> > -	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
> > +	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> >  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
> >  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
> >  let gp = po ; [Sync-rcu] ; po?
> > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > index a397387f77cc..ff4b756f4a44 100644
> > --- a/tools/memory-model/linux-kernel.def
> > +++ b/tools/memory-model/linux-kernel.def
> > @@ -21,7 +21,7 @@ smp_mb() { __fence{mb} ; }
> >  smp_rmb() { __fence{rmb} ; }
> >  smp_wmb() { __fence{wmb} ; }
> >  smp_read_barrier_depends() { __fence{rb_dep}; }
> > -smp_mb__before_atomic() { __fence{before_atomic} ; }
> > +smp_mb__before_atomic() { __fence{before-atomic} ; }
> >  smp_mb__after_atomic() { __fence{after_atomic} ; }
> >  smp_mb__after_spinlock() { __fence{after_spinlock} ; }
> >  
> > -- 
> > 2.5.2
> > 
> 

Re: [PATCH RFC tip/lkmm 08/10] EXP Remove understore from smp_mb__before_atomic() workings

[Andrea Parri]

On Thu, Feb 15, 2018 at 02:49:37PM -0800, Paul E. McKenney wrote:
> On Thu, Feb 15, 2018 at 11:30:09PM +0100, Andrea Parri wrote:
> > On Fri, Feb 09, 2018 at 06:20:29AM -0800, Paul E. McKenney wrote:
> > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > nit: s/understore/underscore  (a very understandable lapsus, BTW ;-)
> 
> ;-)
> 
> Will fix when squashing.
> 
> > According to the cover letter, patches 8-10 of this series are intended
> > to be squashed together;  it could be useful to add a description then:
> > the motivation for these changes might appear "trivial" today;  months/
> > years from now?  mmh, I can't put my finger on it ;-)
> 
> Assuming we keep these patches, agreed.  Something like this for the
> aggregated single commit, perhaps:
> 
> 	tools/memory-model: Convert underscores to hyphens
> 
> 	Typical cat-language code uses hyphens for word separators in
> 	identifiers, but several LKMM identifiers use underscores instead.
> 	This commit therefore converts the underscores in the .bell and
> 	.cat files for smp_mb__before_atomic(), smp_mb__after_atomic(),
> 	and smp_mb__after_spinlock() to hyphens.
> 
> > IMO,  this descrition should also mention why this solution "is the way
> > to go" (e.g., compare with the solution recently implemented by Akira).
> 
> You lost me here.  Or are you asking for a commit log similar to that
> provided by Akira for his forward-port of Alan's unrelated patch?  If
> so, please see above.

I was mainly thinking "but rb_dep...";  or you're also planning to
rename this annotation and, maybe, the "rb-dep" relation (in order
to avoid the conflict)?

  Andrea


> 
> 							Thanx, Paul
> 
> >   Andrea
> > 
> > 
> > > ---
> > >  tools/memory-model/linux-kernel.bell | 2 +-
> > >  tools/memory-model/linux-kernel.cat  | 2 +-
> > >  tools/memory-model/linux-kernel.def  | 2 +-
> > >  3 files changed, 3 insertions(+), 3 deletions(-)
> > > 
> > > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> > > index b984bbda01a5..558bbef9e08a 100644
> > > --- a/tools/memory-model/linux-kernel.bell
> > > +++ b/tools/memory-model/linux-kernel.bell
> > > @@ -28,7 +28,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
> > >  		'rcu-lock (*rcu_read_lock*)  ||
> > >  		'rcu-unlock (*rcu_read_unlock*) ||
> > >  		'sync-rcu (*synchronize_rcu*) ||
> > > -		'before_atomic (*smp_mb__before_atomic*) ||
> > > +		'before-atomic (*smp_mb__before_atomic*) ||
> > >  		'after_atomic (*smp_mb__after_atomic*) ||
> > >  		'after_spinlock (*smp_mb__after_spinlock*)
> > >  instructions F[Barriers]
> > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > > index babe2b3b0bb3..31c08a44c088 100644
> > > --- a/tools/memory-model/linux-kernel.cat
> > > +++ b/tools/memory-model/linux-kernel.cat
> > > @@ -29,7 +29,7 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
> > >  let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
> > >  let wmb = [W] ; fencerel(Wmb) ; [W]
> > >  let mb = ([M] ; fencerel(Mb) ; [M]) |
> > > -	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
> > > +	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> > >  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
> > >  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
> > >  let gp = po ; [Sync-rcu] ; po?
> > > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > > index a397387f77cc..ff4b756f4a44 100644
> > > --- a/tools/memory-model/linux-kernel.def
> > > +++ b/tools/memory-model/linux-kernel.def
> > > @@ -21,7 +21,7 @@ smp_mb() { __fence{mb} ; }
> > >  smp_rmb() { __fence{rmb} ; }
> > >  smp_wmb() { __fence{wmb} ; }
> > >  smp_read_barrier_depends() { __fence{rb_dep}; }
> > > -smp_mb__before_atomic() { __fence{before_atomic} ; }
> > > +smp_mb__before_atomic() { __fence{before-atomic} ; }
> > >  smp_mb__after_atomic() { __fence{after_atomic} ; }
> > >  smp_mb__after_spinlock() { __fence{after_spinlock} ; }
> > >  
> > > -- 
> > > 2.5.2
> > > 
> > 
> 

Re: [PATCH RFC tip/lkmm 08/10] EXP Remove understore from smp_mb__before_atomic() workings

[Paul E. McKenney]

On Fri, Feb 16, 2018 at 12:19:58AM +0100, Andrea Parri wrote:
> On Thu, Feb 15, 2018 at 02:49:37PM -0800, Paul E. McKenney wrote:
> > On Thu, Feb 15, 2018 at 11:30:09PM +0100, Andrea Parri wrote:
> > > On Fri, Feb 09, 2018 at 06:20:29AM -0800, Paul E. McKenney wrote:
> > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > 
> > > nit: s/understore/underscore  (a very understandable lapsus, BTW ;-)
> > 
> > ;-)
> > 
> > Will fix when squashing.
> > 
> > > According to the cover letter, patches 8-10 of this series are intended
> > > to be squashed together;  it could be useful to add a description then:
> > > the motivation for these changes might appear "trivial" today;  months/
> > > years from now?  mmh, I can't put my finger on it ;-)
> > 
> > Assuming we keep these patches, agreed.  Something like this for the
> > aggregated single commit, perhaps:
> > 
> > 	tools/memory-model: Convert underscores to hyphens
> > 
> > 	Typical cat-language code uses hyphens for word separators in
> > 	identifiers, but several LKMM identifiers use underscores instead.
> > 	This commit therefore converts the underscores in the .bell and
> > 	.cat files for smp_mb__before_atomic(), smp_mb__after_atomic(),
> > 	and smp_mb__after_spinlock() to hyphens.
> > 
> > > IMO,  this descrition should also mention why this solution "is the way
> > > to go" (e.g., compare with the solution recently implemented by Akira).
> > 
> > You lost me here.  Or are you asking for a commit log similar to that
> > provided by Akira for his forward-port of Alan's unrelated patch?  If
> > so, please see above.
> 
> I was mainly thinking "but rb_dep...";  or you're also planning to
> rename this annotation and, maybe, the "rb-dep" relation (in order
> to avoid the conflict)?

The rb_dep relation goes away completely once we catch LKMM up with
the recent changes that remove smp_read_barrier_depends() from the
core kernel.  So my current thought is hold back the "_"->"-" commit
until that catch-up happens.

							Thanx, Paul

>   Andrea
> 
> 
> > 
> > 							Thanx, Paul
> > 
> > >   Andrea
> > > 
> > > 
> > > > ---
> > > >  tools/memory-model/linux-kernel.bell | 2 +-
> > > >  tools/memory-model/linux-kernel.cat  | 2 +-
> > > >  tools/memory-model/linux-kernel.def  | 2 +-
> > > >  3 files changed, 3 insertions(+), 3 deletions(-)
> > > > 
> > > > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> > > > index b984bbda01a5..558bbef9e08a 100644
> > > > --- a/tools/memory-model/linux-kernel.bell
> > > > +++ b/tools/memory-model/linux-kernel.bell
> > > > @@ -28,7 +28,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
> > > >  		'rcu-lock (*rcu_read_lock*)  ||
> > > >  		'rcu-unlock (*rcu_read_unlock*) ||
> > > >  		'sync-rcu (*synchronize_rcu*) ||
> > > > -		'before_atomic (*smp_mb__before_atomic*) ||
> > > > +		'before-atomic (*smp_mb__before_atomic*) ||
> > > >  		'after_atomic (*smp_mb__after_atomic*) ||
> > > >  		'after_spinlock (*smp_mb__after_spinlock*)
> > > >  instructions F[Barriers]
> > > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > > > index babe2b3b0bb3..31c08a44c088 100644
> > > > --- a/tools/memory-model/linux-kernel.cat
> > > > +++ b/tools/memory-model/linux-kernel.cat
> > > > @@ -29,7 +29,7 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
> > > >  let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
> > > >  let wmb = [W] ; fencerel(Wmb) ; [W]
> > > >  let mb = ([M] ; fencerel(Mb) ; [M]) |
> > > > -	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
> > > > +	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> > > >  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
> > > >  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
> > > >  let gp = po ; [Sync-rcu] ; po?
> > > > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > > > index a397387f77cc..ff4b756f4a44 100644
> > > > --- a/tools/memory-model/linux-kernel.def
> > > > +++ b/tools/memory-model/linux-kernel.def
> > > > @@ -21,7 +21,7 @@ smp_mb() { __fence{mb} ; }
> > > >  smp_rmb() { __fence{rmb} ; }
> > > >  smp_wmb() { __fence{wmb} ; }
> > > >  smp_read_barrier_depends() { __fence{rb_dep}; }
> > > > -smp_mb__before_atomic() { __fence{before_atomic} ; }
> > > > +smp_mb__before_atomic() { __fence{before-atomic} ; }
> > > >  smp_mb__after_atomic() { __fence{after_atomic} ; }
> > > >  smp_mb__after_spinlock() { __fence{after_spinlock} ; }
> > > >  
> > > > -- 
> > > > 2.5.2
> > > > 
> > > 
> > 
> 

Re: Trial of conflict resolution of Alan's patch

[Alan Stern]

On Fri, 16 Feb 2018, Akira Yokosawa wrote:

> Hi,
> 
> My forward-port patch doesn't apply to the "lkmm" branch.
> It looks like "linux-kernel-hardware.cat" is intentionally omitted there.
> Am I guessing right?
> 
> If this is the case, I can prepare a patch to be applied to "lkmm".
> But I can't compose a proper change log. So I'd like Alan to post
> a patch with my SOB appended. Does this approach sound reasonable?

The patch is not yet ready to be merged.  At the very least, I need to
include an update to explanation.txt along with it.  When it is all 
ready, I will rebase it on Paul's repository and post it.

Which reminds me: Now that the material has been accepted into the 
kernel, do we need to keep the github repository?  It has the 
linux-kernel-hardware.cat file, but otherwise it seems to be redundant.

Alan

Re: Trial of conflict resolution of Alan's patch

[Andrea Parri]

On Fri, Feb 16, 2018 at 10:18:34AM -0500, Alan Stern wrote:
> On Fri, 16 Feb 2018, Akira Yokosawa wrote:
> 
> > Hi,
> > 
> > My forward-port patch doesn't apply to the "lkmm" branch.
> > It looks like "linux-kernel-hardware.cat" is intentionally omitted there.
> > Am I guessing right?
> > 
> > If this is the case, I can prepare a patch to be applied to "lkmm".
> > But I can't compose a proper change log. So I'd like Alan to post
> > a patch with my SOB appended. Does this approach sound reasonable?
> 
> The patch is not yet ready to be merged.  At the very least, I need to
> include an update to explanation.txt along with it.  When it is all 
> ready, I will rebase it on Paul's repository and post it.
> 
> Which reminds me: Now that the material has been accepted into the 
> kernel, do we need to keep the github repository?  It has the 
> linux-kernel-hardware.cat file, but otherwise it seems to be redundant.

If you mean "to keep up-to-date", I'd say "No, we don't..."  ;-)

My plan/hope is to add such a disclaimer together with a pointer
to Linus's tree ASAP...

  Andrea


> 
> Alan
> 

Re: Trial of conflict resolution of Alan's patch

[Paul E. McKenney]

On Fri, Feb 16, 2018 at 04:47:04PM +0100, Andrea Parri wrote:
> On Fri, Feb 16, 2018 at 10:18:34AM -0500, Alan Stern wrote:
> > On Fri, 16 Feb 2018, Akira Yokosawa wrote:
> > 
> > > Hi,
> > > 
> > > My forward-port patch doesn't apply to the "lkmm" branch.
> > > It looks like "linux-kernel-hardware.cat" is intentionally omitted there.
> > > Am I guessing right?
> > > 
> > > If this is the case, I can prepare a patch to be applied to "lkmm".
> > > But I can't compose a proper change log. So I'd like Alan to post
> > > a patch with my SOB appended. Does this approach sound reasonable?
> > 
> > The patch is not yet ready to be merged.  At the very least, I need to
> > include an update to explanation.txt along with it.  When it is all 
> > ready, I will rebase it on Paul's repository and post it.
> > 
> > Which reminds me: Now that the material has been accepted into the 
> > kernel, do we need to keep the github repository?  It has the 
> > linux-kernel-hardware.cat file, but otherwise it seems to be redundant.
> 
> If you mean "to keep up-to-date", I'd say "No, we don't..."  ;-)
> 
> My plan/hope is to add such a disclaimer together with a pointer
> to Linus's tree ASAP...

I agree that the github repository is useful as a historical reference
but that we should not try to keep it up to date.  The -rc1 release
came out last Sunday, so in 7-8 weeks we will hopefully have this in
the Linux kernel.  Fingers firmly crossed and all that...

							Thanx, Paul

[PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

Since commit 76ebbe78f739 ("locking/barriers: Add implicit
smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
kernel, it has not been necessary to use smp_read_barrier_depends().
Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
lockless_dereference()") removed lockless_dereference() from the
kernel.

Since these primitives are no longer part of the kernel, they do not
belong in the Linux Kernel Memory Consistency Model.  This patch
removes them, along with the internal rb-dep relation, and updates the
revelant documentation.

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

---

Index: usb-4.x/tools/memory-model/linux-kernel.cat
===================================================================
--- usb-4.x/tools/memory-model.orig/linux-kernel.cat
+++ usb-4.x/tools/memory-model/linux-kernel.cat
@@ -25,7 +25,6 @@ include "lock.cat"
 (*******************)
 
 (* Fences *)
-let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
 let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
 let wmb = [W] ; fencerel(Wmb) ; [W]
 let mb = ([M] ; fencerel(Mb) ; [M]) |
@@ -61,11 +60,9 @@ let dep = addr | data
 let rwdep = (dep | ctrl) ; [W]
 let overwrite = co | fr
 let to-w = rwdep | (overwrite & int)
-let rrdep = addr | (dep ; rfi)
-let strong-rrdep = rrdep+ & rb-dep
-let to-r = strong-rrdep | rfi-rel-acq
+let to-r = addr | (dep ; rfi) | rfi-rel-acq
 let fence = strong-fence | wmb | po-rel | rmb | acq-po
-let ppo = rrdep* ; (to-r | to-w | fence)
+let ppo = to-r | to-w | fence
 
 (* Propagation: Ordering from release operations and strong fences. *)
 let A-cumul(r) = rfe? ; r
Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
===================================================================
--- usb-4.x/tools/memory-model.orig/Documentation/explanation.txt
+++ usb-4.x/tools/memory-model/Documentation/explanation.txt
@@ -1,5 +1,5 @@
-Explanation of the Linux-Kernel Memory Model
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Explanation of the Linux-Kernel Memory Consistency Model
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 :Author: Alan Stern <stern@rowland.harvard.edu>
 :Created: October 2017
@@ -35,25 +35,24 @@ Explanation of the Linux-Kernel Memory M
 INTRODUCTION
 ------------
 
-The Linux-kernel memory model (LKMM) is rather complex and obscure.
-This is particularly evident if you read through the linux-kernel.bell
-and linux-kernel.cat files that make up the formal version of the
-memory model; they are extremely terse and their meanings are far from
-clear.
+The Linux-kernel memory consistency model (LKMM) is rather complex and
+obscure.  This is particularly evident if you read through the
+linux-kernel.bell and linux-kernel.cat files that make up the formal
+version of the model; they are extremely terse and their meanings are
+far from clear.
 
 This document describes the ideas underlying the LKMM.  It is meant
-for people who want to understand how the memory model was designed.
-It does not go into the details of the code in the .bell and .cat
-files; rather, it explains in English what the code expresses
-symbolically.
+for people who want to understand how the model was designed.  It does
+not go into the details of the code in the .bell and .cat files;
+rather, it explains in English what the code expresses symbolically.
 
 Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed
-toward beginners; they explain what memory models are and the basic
-notions shared by all such models.  People already familiar with these
-concepts can skim or skip over them.  Sections 6 (EVENTS) through 12
-(THE FROM_READS RELATION) describe the fundamental relations used in
-many memory models.  Starting in Section 13 (AN OPERATIONAL MODEL),
-the workings of the LKMM itself are covered.
+toward beginners; they explain what memory consistency models are and
+the basic notions shared by all such models.  People already familiar
+with these concepts can skim or skip over them.  Sections 6 (EVENTS)
+through 12 (THE FROM_READS RELATION) describe the fundamental
+relations used in many models.  Starting in Section 13 (AN OPERATIONAL
+MODEL), the workings of the LKMM itself are covered.
 
 Warning: The code examples in this document are not written in the
 proper format for litmus tests.  They don't include a header line, the
@@ -827,8 +826,8 @@ A-cumulative; they only affect the propa
 executed on C before the fence (i.e., those which precede the fence in
 program order).
 
-smp_read_barrier_depends(), rcu_read_lock(), rcu_read_unlock(), and
-synchronize_rcu() fences have other properties which we discuss later.
+read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
+other properties which we discuss later.
 
 
 PROPAGATION ORDER RELATION: cumul-fence
@@ -988,8 +987,8 @@ Another possibility, not mentioned earli
 section, is:
 
 	X and Y are both loads, X ->addr Y (i.e., there is an address
-	dependency from X to Y), and an smp_read_barrier_depends()
-	fence occurs between them.
+	dependency from X to Y), and X is a READ_ONCE() or an atomic
+	access.
 
 Dependencies can also cause instructions to be executed in program
 order.  This is uncontroversial when the second instruction is a
@@ -1015,9 +1014,9 @@ After all, a CPU cannot ask the memory s
 a particular location before it knows what that location is.  However,
 the split-cache design used by Alpha can cause it to behave in a way
 that looks as if the loads were executed out of order (see the next
-section for more details).  For this reason, the LKMM does not include
-address dependencies between read events in the ppo relation unless an
-smp_read_barrier_depends() fence is present.
+section for more details).  The kernel includes a workaround for this
+problem when the loads come from READ_ONCE(), and therefore the LKMM
+includes address dependencies to loads in the ppo relation.
 
 On the other hand, dependencies can indirectly affect the ordering of
 two loads.  This happens when there is a dependency from a load to a
@@ -1114,11 +1113,12 @@ code such as the following:
 		int *r1;
 		int r2;
 
-		r1 = READ_ONCE(ptr);
+		r1 = ptr;
 		r2 = READ_ONCE(*r1);
 	}
 
-can malfunction on Alpha systems.  It is quite possible that r1 = &x
+can malfunction on Alpha systems (notice that P1 uses an ordinary load
+to read ptr instead of READ_ONCE()).  It is quite possible that r1 = &x
 and r2 = 0 at the end, in spite of the address dependency.
 
 At first glance this doesn't seem to make sense.  We know that the
@@ -1141,11 +1141,15 @@ This could not have happened if the loca
 incoming stores in FIFO order.  In constrast, other architectures
 maintain at least the appearance of FIFO order.
 
-In practice, this difficulty is solved by inserting an
-smp_read_barrier_depends() fence between P1's two loads.  The effect
-of this fence is to cause the CPU not to execute any po-later
-instructions until after the local cache has finished processing all
-the stores it has already received.  Thus, if the code was changed to:
+In practice, this difficulty is solved by inserting a special fence
+between P1's two loads when the kernel is compiled for the Alpha
+architecture.  In fact, as of version 4.15, the kernel automatically
+adds this fence (called smp_read_barrier_depends() and defined as
+nothing at all on non-Alpha builds) after every READ_ONCE() and atomic
+load.  The effect of the fence is to cause the CPU not to execute any
+po-later instructions until after the local cache has finished
+processing all the stores it has already received.  Thus, if the code
+was changed to:
 
 	P1()
 	{
@@ -1153,13 +1157,15 @@ the stores it has already received.  Thu
 		int r2;
 
 		r1 = READ_ONCE(ptr);
-		smp_read_barrier_depends();
 		r2 = READ_ONCE(*r1);
 	}
 
 then we would never get r1 = &x and r2 = 0.  By the time P1 executed
 its second load, the x = 1 store would already be fully processed by
-the local cache and available for satisfying the read request.
+the local cache and available for satisfying the read request.  Thus
+we have yet another reason why shared data should always be read with
+READ_ONCE() or another synchronization primitive rather than accessed
+directly.
 
 The LKMM requires that smp_rmb(), acquire fences, and strong fences
 share this property with smp_read_barrier_depends(): They do not allow
@@ -1751,11 +1757,10 @@ no further involvement from the CPU.  Si
 the value of x, there is nothing for the smp_rmb() fence to act on.
 
 The LKMM defines a few extra synchronization operations in terms of
-things we have already covered.  In particular, rcu_dereference() and
-lockless_dereference() are both treated as a READ_ONCE() followed by
-smp_read_barrier_depends() -- which also happens to be how they are
-defined in include/linux/rcupdate.h and include/linux/compiler.h,
-respectively.
+things we have already covered.  In particular, rcu_dereference() is
+treated as READ_ONCE() and rcu_assign_pointer() is treated as
+smp_store_release() -- which is basically how the Linux kernel treats
+them.
 
 There are a few oddball fences which need special treatment:
 smp_mb__before_atomic(), smp_mb__after_atomic(), and
Index: usb-4.x/tools/memory-model/linux-kernel.bell
===================================================================
--- usb-4.x/tools/memory-model.orig/linux-kernel.bell
+++ usb-4.x/tools/memory-model/linux-kernel.bell
@@ -24,7 +24,6 @@ instructions RMW[{'once,'acquire,'releas
 enum Barriers = 'wmb (*smp_wmb*) ||
 		'rmb (*smp_rmb*) ||
 		'mb (*smp_mb*) ||
-		'rb_dep (*smp_read_barrier_depends*) ||
 		'rcu-lock (*rcu_read_lock*)  ||
 		'rcu-unlock (*rcu_read_unlock*) ||
 		'sync-rcu (*synchronize_rcu*) ||
Index: usb-4.x/tools/memory-model/linux-kernel.def
===================================================================
--- usb-4.x/tools/memory-model.orig/linux-kernel.def
+++ usb-4.x/tools/memory-model/linux-kernel.def
@@ -13,14 +13,12 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
 smp_store_release(X,V) { __store{release}(*X,V); }
 smp_load_acquire(X) __load{acquire}(*X)
 rcu_assign_pointer(X,V) { __store{release}(X,V); }
-lockless_dereference(X) __load{lderef}(X)
 rcu_dereference(X) __load{deref}(X)
 
 // Fences
 smp_mb() { __fence{mb} ; }
 smp_rmb() { __fence{rmb} ; }
 smp_wmb() { __fence{wmb} ; }
-smp_read_barrier_depends() { __fence{rb_dep}; }
 smp_mb__before_atomic() { __fence{before-atomic} ; }
 smp_mb__after_atomic() { __fence{after-atomic} ; }
 smp_mb__after_spinlock() { __fence{after-spinlock} ; }
Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
===================================================================
--- usb-4.x/tools/memory-model.orig/Documentation/cheatsheet.txt
+++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
@@ -6,8 +6,7 @@
 Store, e.g., WRITE_ONCE()            Y                                       Y
 Load, e.g., READ_ONCE()              Y                              Y        Y
 Unsuccessful RMW operation           Y                              Y        Y
-smp_read_barrier_depends()              Y                       Y   Y
-*_dereference()                      Y                          Y   Y        Y
+rcu_dereference()                    Y                          Y   Y        Y
 Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
 Successful *_release()         C        Y  Y    Y     W                      Y
 smp_rmb()                               Y       R        Y      Y        R

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Akira Yokosawa]

On 2018/02/16 17:22:55 -0500, Alan Stern wrote:
> Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> kernel, it has not been necessary to use smp_read_barrier_depends().
> Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> lockless_dereference()") removed lockless_dereference() from the
> kernel.
> 
> Since these primitives are no longer part of the kernel, they do not
> belong in the Linux Kernel Memory Consistency Model.  This patch
> removes them, along with the internal rb-dep relation, and updates the
> revelant documentation.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 

A few nits.  Please see inline comments below.

With those fixed,

Reviewed-by: Akira Yokosawa <akiyks@gmail.com>

     Thanks, Akira

> ---
> 
> Index: usb-4.x/tools/memory-model/linux-kernel.cat
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.cat
> +++ usb-4.x/tools/memory-model/linux-kernel.cat
> @@ -25,7 +25,6 @@ include "lock.cat"
>  (*******************)
>  
>  (* Fences *)
> -let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
>  let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
>  let wmb = [W] ; fencerel(Wmb) ; [W]
>  let mb = ([M] ; fencerel(Mb) ; [M]) |
> @@ -61,11 +60,9 @@ let dep = addr | data
>  let rwdep = (dep | ctrl) ; [W]
>  let overwrite = co | fr
>  let to-w = rwdep | (overwrite & int)
> -let rrdep = addr | (dep ; rfi)
> -let strong-rrdep = rrdep+ & rb-dep
> -let to-r = strong-rrdep | rfi-rel-acq
> +let to-r = addr | (dep ; rfi) | rfi-rel-acq
>  let fence = strong-fence | wmb | po-rel | rmb | acq-po
> -let ppo = rrdep* ; (to-r | to-w | fence)
> +let ppo = to-r | to-w | fence
>  
>  (* Propagation: Ordering from release operations and strong fences. *)
>  let A-cumul(r) = rfe? ; r
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -1,5 +1,5 @@
> -Explanation of the Linux-Kernel Memory Model
> -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> +Explanation of the Linux-Kernel Memory Consistency Model
> +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>  
>  :Author: Alan Stern <stern@rowland.harvard.edu>
>  :Created: October 2017
> @@ -35,25 +35,24 @@ Explanation of the Linux-Kernel Memory M
>  INTRODUCTION
>  ------------
>  
> -The Linux-kernel memory model (LKMM) is rather complex and obscure.
> -This is particularly evident if you read through the linux-kernel.bell
> -and linux-kernel.cat files that make up the formal version of the
> -memory model; they are extremely terse and their meanings are far from
> -clear.
> +The Linux-kernel memory consistency model (LKMM) is rather complex and
> +obscure.  This is particularly evident if you read through the
> +linux-kernel.bell and linux-kernel.cat files that make up the formal
> +version of the model; they are extremely terse and their meanings are
> +far from clear.
>  
>  This document describes the ideas underlying the LKMM.  It is meant
> -for people who want to understand how the memory model was designed.
> -It does not go into the details of the code in the .bell and .cat
> -files; rather, it explains in English what the code expresses
> -symbolically.
> +for people who want to understand how the model was designed.  It does
> +not go into the details of the code in the .bell and .cat files;
> +rather, it explains in English what the code expresses symbolically.
>  
>  Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed
> -toward beginners; they explain what memory models are and the basic
> -notions shared by all such models.  People already familiar with these
> -concepts can skim or skip over them.  Sections 6 (EVENTS) through 12
> -(THE FROM_READS RELATION) describe the fundamental relations used in
> -many memory models.  Starting in Section 13 (AN OPERATIONAL MODEL),
> -the workings of the LKMM itself are covered.
> +toward beginners; they explain what memory consistency models are and
> +the basic notions shared by all such models.  People already familiar
> +with these concepts can skim or skip over them.  Sections 6 (EVENTS)
> +through 12 (THE FROM_READS RELATION) describe the fundamental
> +relations used in many models.  Starting in Section 13 (AN OPERATIONAL
> +MODEL), the workings of the LKMM itself are covered.
>  
>  Warning: The code examples in this document are not written in the
>  proper format for litmus tests.  They don't include a header line, the
> @@ -827,8 +826,8 @@ A-cumulative; they only affect the propa
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
>  
> -smp_read_barrier_depends(), rcu_read_lock(), rcu_read_unlock(), and
> -synchronize_rcu() fences have other properties which we discuss later.
> +read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have

   rcu_read_lock()

> +other properties which we discuss later.
>  
>  
>  PROPAGATION ORDER RELATION: cumul-fence
> @@ -988,8 +987,8 @@ Another possibility, not mentioned earli
>  section, is:
>  
>  	X and Y are both loads, X ->addr Y (i.e., there is an address
> -	dependency from X to Y), and an smp_read_barrier_depends()
> -	fence occurs between them.
> +	dependency from X to Y), and X is a READ_ONCE() or an atomic
> +	access.
>  
>  Dependencies can also cause instructions to be executed in program
>  order.  This is uncontroversial when the second instruction is a
> @@ -1015,9 +1014,9 @@ After all, a CPU cannot ask the memory s
>  a particular location before it knows what that location is.  However,
>  the split-cache design used by Alpha can cause it to behave in a way
>  that looks as if the loads were executed out of order (see the next
> -section for more details).  For this reason, the LKMM does not include
> -address dependencies between read events in the ppo relation unless an
> -smp_read_barrier_depends() fence is present.
> +section for more details).  The kernel includes a workaround for this
> +problem when the loads come from READ_ONCE(), and therefore the LKMM
> +includes address dependencies to loads in the ppo relation.
>  
>  On the other hand, dependencies can indirectly affect the ordering of
>  two loads.  This happens when there is a dependency from a load to a
> @@ -1114,11 +1113,12 @@ code such as the following:
>  		int *r1;
>  		int r2;
>  
> -		r1 = READ_ONCE(ptr);
> +		r1 = ptr;
>  		r2 = READ_ONCE(*r1);
>  	}
>  
> -can malfunction on Alpha systems.  It is quite possible that r1 = &x
> +can malfunction on Alpha systems (notice that P1 uses an ordinary load
> +to read ptr instead of READ_ONCE()).  It is quite possible that r1 = &x
>  and r2 = 0 at the end, in spite of the address dependency.
>  
>  At first glance this doesn't seem to make sense.  We know that the
> @@ -1141,11 +1141,15 @@ This could not have happened if the loca
>  incoming stores in FIFO order.  In constrast, other architectures

                                      contrast

>  maintain at least the appearance of FIFO order.
>  
> -In practice, this difficulty is solved by inserting an
> -smp_read_barrier_depends() fence between P1's two loads.  The effect
> -of this fence is to cause the CPU not to execute any po-later
> -instructions until after the local cache has finished processing all
> -the stores it has already received.  Thus, if the code was changed to:
> +In practice, this difficulty is solved by inserting a special fence
> +between P1's two loads when the kernel is compiled for the Alpha
> +architecture.  In fact, as of version 4.15, the kernel automatically
> +adds this fence (called smp_read_barrier_depends() and defined as
> +nothing at all on non-Alpha builds) after every READ_ONCE() and atomic
> +load.  The effect of the fence is to cause the CPU not to execute any
> +po-later instructions until after the local cache has finished
> +processing all the stores it has already received.  Thus, if the code
> +was changed to:
>  
>  	P1()
>  	{
> @@ -1153,13 +1157,15 @@ the stores it has already received.  Thu
>  		int r2;
>  
>  		r1 = READ_ONCE(ptr);
> -		smp_read_barrier_depends();
>  		r2 = READ_ONCE(*r1);
>  	}
>  
>  then we would never get r1 = &x and r2 = 0.  By the time P1 executed
>  its second load, the x = 1 store would already be fully processed by
> -the local cache and available for satisfying the read request.
> +the local cache and available for satisfying the read request.  Thus
> +we have yet another reason why shared data should always be read with
> +READ_ONCE() or another synchronization primitive rather than accessed
> +directly.
>  
>  The LKMM requires that smp_rmb(), acquire fences, and strong fences
>  share this property with smp_read_barrier_depends(): They do not allow
> @@ -1751,11 +1757,10 @@ no further involvement from the CPU.  Si
>  the value of x, there is nothing for the smp_rmb() fence to act on.
>  
>  The LKMM defines a few extra synchronization operations in terms of
> -things we have already covered.  In particular, rcu_dereference() and
> -lockless_dereference() are both treated as a READ_ONCE() followed by
> -smp_read_barrier_depends() -- which also happens to be how they are
> -defined in include/linux/rcupdate.h and include/linux/compiler.h,
> -respectively.
> +things we have already covered.  In particular, rcu_dereference() is
> +treated as READ_ONCE() and rcu_assign_pointer() is treated as
> +smp_store_release() -- which is basically how the Linux kernel treats
> +them.
>  
>  There are a few oddball fences which need special treatment:
>  smp_mb__before_atomic(), smp_mb__after_atomic(), and
> Index: usb-4.x/tools/memory-model/linux-kernel.bell
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.bell
> +++ usb-4.x/tools/memory-model/linux-kernel.bell
> @@ -24,7 +24,6 @@ instructions RMW[{'once,'acquire,'releas
>  enum Barriers = 'wmb (*smp_wmb*) ||
>  		'rmb (*smp_rmb*) ||
>  		'mb (*smp_mb*) ||
> -		'rb_dep (*smp_read_barrier_depends*) ||
>  		'rcu-lock (*rcu_read_lock*)  ||
>  		'rcu-unlock (*rcu_read_unlock*) ||
>  		'sync-rcu (*synchronize_rcu*) ||
> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,14 +13,12 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -lockless_dereference(X) __load{lderef}(X)
>  rcu_dereference(X) __load{deref}(X)
>  
>  // Fences
>  smp_mb() { __fence{mb} ; }
>  smp_rmb() { __fence{rmb} ; }
>  smp_wmb() { __fence{wmb} ; }
> -smp_read_barrier_depends() { __fence{rb_dep}; }
>  smp_mb__before_atomic() { __fence{before-atomic} ; }
>  smp_mb__after_atomic() { __fence{after-atomic} ; }
>  smp_mb__after_spinlock() { __fence{after-spinlock} ; }
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -6,8 +6,7 @@
>  Store, e.g., WRITE_ONCE()            Y                                       Y
>  Load, e.g., READ_ONCE()              Y                              Y        Y

READ_ONCE() now includes smp_read_barrier_depends, so this row should
be divided to:

   Simple Load                          Y                              Y        Y

>  Unsuccessful RMW operation           Y                              Y        Y
> -smp_read_barrier_depends()              Y                       Y   Y
   READ_ONCE()                          Y                          Y   Y        Y
> -*_dereference()                      Y                          Y   Y        Y
> +rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
>  smp_rmb()                               Y       R        Y      Y        R
> 
> 

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> kernel, it has not been necessary to use smp_read_barrier_depends().
> Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> lockless_dereference()") removed lockless_dereference() from the
> kernel.
> 
> Since these primitives are no longer part of the kernel, they do not
> belong in the Linux Kernel Memory Consistency Model.  This patch
> removes them, along with the internal rb-dep relation, and updates the
> revelant documentation.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

I queued this, but would welcome an update that addressed Akira's
feedback as appropriate.

							Thanx, Paul

> ---
> 
> Index: usb-4.x/tools/memory-model/linux-kernel.cat
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.cat
> +++ usb-4.x/tools/memory-model/linux-kernel.cat
> @@ -25,7 +25,6 @@ include "lock.cat"
>  (*******************)
> 
>  (* Fences *)
> -let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
>  let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
>  let wmb = [W] ; fencerel(Wmb) ; [W]
>  let mb = ([M] ; fencerel(Mb) ; [M]) |
> @@ -61,11 +60,9 @@ let dep = addr | data
>  let rwdep = (dep | ctrl) ; [W]
>  let overwrite = co | fr
>  let to-w = rwdep | (overwrite & int)
> -let rrdep = addr | (dep ; rfi)
> -let strong-rrdep = rrdep+ & rb-dep
> -let to-r = strong-rrdep | rfi-rel-acq
> +let to-r = addr | (dep ; rfi) | rfi-rel-acq
>  let fence = strong-fence | wmb | po-rel | rmb | acq-po
> -let ppo = rrdep* ; (to-r | to-w | fence)
> +let ppo = to-r | to-w | fence
> 
>  (* Propagation: Ordering from release operations and strong fences. *)
>  let A-cumul(r) = rfe? ; r
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -1,5 +1,5 @@
> -Explanation of the Linux-Kernel Memory Model
> -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> +Explanation of the Linux-Kernel Memory Consistency Model
> +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> 
>  :Author: Alan Stern <stern@rowland.harvard.edu>
>  :Created: October 2017
> @@ -35,25 +35,24 @@ Explanation of the Linux-Kernel Memory M
>  INTRODUCTION
>  ------------
> 
> -The Linux-kernel memory model (LKMM) is rather complex and obscure.
> -This is particularly evident if you read through the linux-kernel.bell
> -and linux-kernel.cat files that make up the formal version of the
> -memory model; they are extremely terse and their meanings are far from
> -clear.
> +The Linux-kernel memory consistency model (LKMM) is rather complex and
> +obscure.  This is particularly evident if you read through the
> +linux-kernel.bell and linux-kernel.cat files that make up the formal
> +version of the model; they are extremely terse and their meanings are
> +far from clear.
> 
>  This document describes the ideas underlying the LKMM.  It is meant
> -for people who want to understand how the memory model was designed.
> -It does not go into the details of the code in the .bell and .cat
> -files; rather, it explains in English what the code expresses
> -symbolically.
> +for people who want to understand how the model was designed.  It does
> +not go into the details of the code in the .bell and .cat files;
> +rather, it explains in English what the code expresses symbolically.
> 
>  Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed
> -toward beginners; they explain what memory models are and the basic
> -notions shared by all such models.  People already familiar with these
> -concepts can skim or skip over them.  Sections 6 (EVENTS) through 12
> -(THE FROM_READS RELATION) describe the fundamental relations used in
> -many memory models.  Starting in Section 13 (AN OPERATIONAL MODEL),
> -the workings of the LKMM itself are covered.
> +toward beginners; they explain what memory consistency models are and
> +the basic notions shared by all such models.  People already familiar
> +with these concepts can skim or skip over them.  Sections 6 (EVENTS)
> +through 12 (THE FROM_READS RELATION) describe the fundamental
> +relations used in many models.  Starting in Section 13 (AN OPERATIONAL
> +MODEL), the workings of the LKMM itself are covered.
> 
>  Warning: The code examples in this document are not written in the
>  proper format for litmus tests.  They don't include a header line, the
> @@ -827,8 +826,8 @@ A-cumulative; they only affect the propa
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
> 
> -smp_read_barrier_depends(), rcu_read_lock(), rcu_read_unlock(), and
> -synchronize_rcu() fences have other properties which we discuss later.
> +read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> +other properties which we discuss later.
> 
> 
>  PROPAGATION ORDER RELATION: cumul-fence
> @@ -988,8 +987,8 @@ Another possibility, not mentioned earli
>  section, is:
> 
>  	X and Y are both loads, X ->addr Y (i.e., there is an address
> -	dependency from X to Y), and an smp_read_barrier_depends()
> -	fence occurs between them.
> +	dependency from X to Y), and X is a READ_ONCE() or an atomic
> +	access.
> 
>  Dependencies can also cause instructions to be executed in program
>  order.  This is uncontroversial when the second instruction is a
> @@ -1015,9 +1014,9 @@ After all, a CPU cannot ask the memory s
>  a particular location before it knows what that location is.  However,
>  the split-cache design used by Alpha can cause it to behave in a way
>  that looks as if the loads were executed out of order (see the next
> -section for more details).  For this reason, the LKMM does not include
> -address dependencies between read events in the ppo relation unless an
> -smp_read_barrier_depends() fence is present.
> +section for more details).  The kernel includes a workaround for this
> +problem when the loads come from READ_ONCE(), and therefore the LKMM
> +includes address dependencies to loads in the ppo relation.
> 
>  On the other hand, dependencies can indirectly affect the ordering of
>  two loads.  This happens when there is a dependency from a load to a
> @@ -1114,11 +1113,12 @@ code such as the following:
>  		int *r1;
>  		int r2;
> 
> -		r1 = READ_ONCE(ptr);
> +		r1 = ptr;
>  		r2 = READ_ONCE(*r1);
>  	}
> 
> -can malfunction on Alpha systems.  It is quite possible that r1 = &x
> +can malfunction on Alpha systems (notice that P1 uses an ordinary load
> +to read ptr instead of READ_ONCE()).  It is quite possible that r1 = &x
>  and r2 = 0 at the end, in spite of the address dependency.
> 
>  At first glance this doesn't seem to make sense.  We know that the
> @@ -1141,11 +1141,15 @@ This could not have happened if the loca
>  incoming stores in FIFO order.  In constrast, other architectures
>  maintain at least the appearance of FIFO order.
> 
> -In practice, this difficulty is solved by inserting an
> -smp_read_barrier_depends() fence between P1's two loads.  The effect
> -of this fence is to cause the CPU not to execute any po-later
> -instructions until after the local cache has finished processing all
> -the stores it has already received.  Thus, if the code was changed to:
> +In practice, this difficulty is solved by inserting a special fence
> +between P1's two loads when the kernel is compiled for the Alpha
> +architecture.  In fact, as of version 4.15, the kernel automatically
> +adds this fence (called smp_read_barrier_depends() and defined as
> +nothing at all on non-Alpha builds) after every READ_ONCE() and atomic
> +load.  The effect of the fence is to cause the CPU not to execute any
> +po-later instructions until after the local cache has finished
> +processing all the stores it has already received.  Thus, if the code
> +was changed to:
> 
>  	P1()
>  	{
> @@ -1153,13 +1157,15 @@ the stores it has already received.  Thu
>  		int r2;
> 
>  		r1 = READ_ONCE(ptr);
> -		smp_read_barrier_depends();
>  		r2 = READ_ONCE(*r1);
>  	}
> 
>  then we would never get r1 = &x and r2 = 0.  By the time P1 executed
>  its second load, the x = 1 store would already be fully processed by
> -the local cache and available for satisfying the read request.
> +the local cache and available for satisfying the read request.  Thus
> +we have yet another reason why shared data should always be read with
> +READ_ONCE() or another synchronization primitive rather than accessed
> +directly.
> 
>  The LKMM requires that smp_rmb(), acquire fences, and strong fences
>  share this property with smp_read_barrier_depends(): They do not allow
> @@ -1751,11 +1757,10 @@ no further involvement from the CPU.  Si
>  the value of x, there is nothing for the smp_rmb() fence to act on.
> 
>  The LKMM defines a few extra synchronization operations in terms of
> -things we have already covered.  In particular, rcu_dereference() and
> -lockless_dereference() are both treated as a READ_ONCE() followed by
> -smp_read_barrier_depends() -- which also happens to be how they are
> -defined in include/linux/rcupdate.h and include/linux/compiler.h,
> -respectively.
> +things we have already covered.  In particular, rcu_dereference() is
> +treated as READ_ONCE() and rcu_assign_pointer() is treated as
> +smp_store_release() -- which is basically how the Linux kernel treats
> +them.
> 
>  There are a few oddball fences which need special treatment:
>  smp_mb__before_atomic(), smp_mb__after_atomic(), and
> Index: usb-4.x/tools/memory-model/linux-kernel.bell
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.bell
> +++ usb-4.x/tools/memory-model/linux-kernel.bell
> @@ -24,7 +24,6 @@ instructions RMW[{'once,'acquire,'releas
>  enum Barriers = 'wmb (*smp_wmb*) ||
>  		'rmb (*smp_rmb*) ||
>  		'mb (*smp_mb*) ||
> -		'rb_dep (*smp_read_barrier_depends*) ||
>  		'rcu-lock (*rcu_read_lock*)  ||
>  		'rcu-unlock (*rcu_read_unlock*) ||
>  		'sync-rcu (*synchronize_rcu*) ||
> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,14 +13,12 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -lockless_dereference(X) __load{lderef}(X)
>  rcu_dereference(X) __load{deref}(X)
> 
>  // Fences
>  smp_mb() { __fence{mb} ; }
>  smp_rmb() { __fence{rmb} ; }
>  smp_wmb() { __fence{wmb} ; }
> -smp_read_barrier_depends() { __fence{rb_dep}; }
>  smp_mb__before_atomic() { __fence{before-atomic} ; }
>  smp_mb__after_atomic() { __fence{after-atomic} ; }
>  smp_mb__after_spinlock() { __fence{after-spinlock} ; }
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -6,8 +6,7 @@
>  Store, e.g., WRITE_ONCE()            Y                                       Y
>  Load, e.g., READ_ONCE()              Y                              Y        Y
>  Unsuccessful RMW operation           Y                              Y        Y
> -smp_read_barrier_depends()              Y                       Y   Y
> -*_dereference()                      Y                          Y   Y        Y
> +rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
>  smp_rmb()                               Y       R        Y      Y        R
> 
> 

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Andrea Parri]

On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> kernel, it has not been necessary to use smp_read_barrier_depends().
> Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> lockless_dereference()") removed lockless_dereference() from the
> kernel.
> 
> Since these primitives are no longer part of the kernel, they do not
> belong in the Linux Kernel Memory Consistency Model.  This patch
> removes them, along with the internal rb-dep relation, and updates the
> revelant documentation.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 
> ---

[...]


> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,14 +13,12 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -lockless_dereference(X) __load{lderef}(X)
>  rcu_dereference(X) __load{deref}(X)

^^^ __load{once}


>  
>  // Fences
>  smp_mb() { __fence{mb} ; }
>  smp_rmb() { __fence{rmb} ; }
>  smp_wmb() { __fence{wmb} ; }
> -smp_read_barrier_depends() { __fence{rb_dep}; }
>  smp_mb__before_atomic() { __fence{before-atomic} ; }
>  smp_mb__after_atomic() { __fence{after-atomic} ; }
>  smp_mb__after_spinlock() { __fence{after-spinlock} ; }
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x/tools/memory-model.orig/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -6,8 +6,7 @@
>  Store, e.g., WRITE_ONCE()            Y                                       Y
>  Load, e.g., READ_ONCE()              Y                              Y        Y
>  Unsuccessful RMW operation           Y                              Y        Y
> -smp_read_barrier_depends()              Y                       Y   Y
> -*_dereference()                      Y                          Y   Y        Y
> +rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
>  smp_rmb()                               Y       R        Y      Y        R

Akira's observation about READ_ONCE extends to all (annotated) loads.  In
fact, it also applies to loads corresponding to unsuccessful RMW operations;
consider, for example, the following variation of MP+onceassign+derefonce:

C T

{
y=z;
z=0;
}

P0(int *x, int **y)
{
	WRITE_ONCE(*x, 1);
	smp_store_release(y, x);
}

P1(int **y, int *z)
{
	int *r0;
	int r1;

	r0 = cmpxchg_relaxed(y, z, z);
	r1 = READ_ONCE(*r0);
}

exists (1:r0=x /\ 1:r1=0)

The final state is allowed w/o the patch, and forbidden w/ the patch.

This also reminds me of

   5a8897cc7631fa544d079c443800f4420d1b173f
   ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics")

(that we probably want to mention in the commit message).

  Andrea


> 
> 

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Andrea Parri]

On Sat, Feb 17, 2018 at 04:25:35AM +0100, Andrea Parri wrote:
> On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> > Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> > smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> > kernel, it has not been necessary to use smp_read_barrier_depends().
> > Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> > lockless_dereference()") removed lockless_dereference() from the
> > kernel.
> > 
> > Since these primitives are no longer part of the kernel, they do not
> > belong in the Linux Kernel Memory Consistency Model.  This patch
> > removes them, along with the internal rb-dep relation, and updates the
> > revelant documentation.
> > 
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > 
> > ---
> 
> [...]
> 
> 
> > Index: usb-4.x/tools/memory-model/linux-kernel.def
> > ===================================================================
> > --- usb-4.x/tools/memory-model.orig/linux-kernel.def
> > +++ usb-4.x/tools/memory-model/linux-kernel.def
> > @@ -13,14 +13,12 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
> >  smp_store_release(X,V) { __store{release}(*X,V); }
> >  smp_load_acquire(X) __load{acquire}(*X)
> >  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> > -lockless_dereference(X) __load{lderef}(X)
> >  rcu_dereference(X) __load{deref}(X)
> 
> ^^^ __load{once}
> 
> 
> >  
> >  // Fences
> >  smp_mb() { __fence{mb} ; }
> >  smp_rmb() { __fence{rmb} ; }
> >  smp_wmb() { __fence{wmb} ; }
> > -smp_read_barrier_depends() { __fence{rb_dep}; }
> >  smp_mb__before_atomic() { __fence{before-atomic} ; }
> >  smp_mb__after_atomic() { __fence{after-atomic} ; }
> >  smp_mb__after_spinlock() { __fence{after-spinlock} ; }
> > Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> > ===================================================================
> > --- usb-4.x/tools/memory-model.orig/Documentation/cheatsheet.txt
> > +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> > @@ -6,8 +6,7 @@
> >  Store, e.g., WRITE_ONCE()            Y                                       Y
> >  Load, e.g., READ_ONCE()              Y                              Y        Y
> >  Unsuccessful RMW operation           Y                              Y        Y
> > -smp_read_barrier_depends()              Y                       Y   Y
> > -*_dereference()                      Y                          Y   Y        Y
> > +rcu_dereference()                    Y                          Y   Y        Y
> >  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
> >  Successful *_release()         C        Y  Y    Y     W                      Y
> >  smp_rmb()                               Y       R        Y      Y        R
> 
> Akira's observation about READ_ONCE extends to all (annotated) loads.  In
> fact, it also applies to loads corresponding to unsuccessful RMW operations;
> consider, for example, the following variation of MP+onceassign+derefonce:
> 
> C T
> 
> {
> y=z;
> z=0;
> }
> 
> P0(int *x, int **y)
> {
> 	WRITE_ONCE(*x, 1);
> 	smp_store_release(y, x);
> }
> 
> P1(int **y, int *z)
> {
> 	int *r0;
> 	int r1;
> 
> 	r0 = cmpxchg_relaxed(y, z, z);
> 	r1 = READ_ONCE(*r0);
> }
> 
> exists (1:r0=x /\ 1:r1=0)
> 
> The final state is allowed w/o the patch, and forbidden w/ the patch.
> 
> This also reminds me of
> 
>    5a8897cc7631fa544d079c443800f4420d1b173f
>    ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics")
> 
> (that we probably want to mention in the commit message).

Please also notice that 5a8897cc7631f only touched alpha's atomic.h:
I see no corresponding commit/change on {,cmp}xchg.h (where the "mb"
is currently conditionally executed).

  Andrea


> 
>   Andrea
> 
> 
> > 
> > 

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Akira Yokosawa]

On 2018/02/14 14:52:38 -0800, Paul E. McKenney wrote:
> On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote:
>> On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote:
>>> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
>>>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
>>>> From: Akira Yokosawa <akiyks@gmail.com>
>>>> Date: Fri, 9 Feb 2018 04:51:05 -0800
>>>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
>>>>
>>>> As of herd7 7.47, these '-'s are not permitted and end up in
>>>> errors such as:
>>>>
>>>>     File "./linux-kernel.def", line 44, characters 29-30:
>>>>     unexpected '-' (in macros)
>>>>
>>>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
>>>> identifiers match ASPLOS paper") in the repository at
>>>> https://github.com/aparri/memory-model can restore the compatibility
>>>> with herd7 7.47.
>>>>
>>>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
>>>> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
>>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>>>> ---
>>>> Paul,
>>>>
>>>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
>>>
>>> Thank you, Akira!
>>>
>>> I am going to hold off on this for a bit to see if we can instead get
>>> a new release of herd7, but if we can't. this might well be a very good
>>> way to go.
>>
>> So, herdtools7.7.48 is now available by "opam update; opam upgrade".
>> Maybe mentioning the required version of herdtools7 in README would help.
> 
> Or have some way for the memory model's .cat files to state what version
> they need, but in the meantime please see the patch below.  But even with
> such version specification, we probably want to have the version in the
> README...
> 
>> One glitch I'm aware of is one of the output of klitmus7 fails to
>> compile on kernels prior to 4.14, because of smp_mb__after_spinlock()
>> used in Z6.0+pooncelock+poonceLock+pombonce.litmus.
> 
> This is one advantage of having the memory model in the kernel source
> itself -- the versions match.  And people can always fire up a different
> kernel version (for example, within a VM) to run the output of klitmus7.
> 

There is another unfortunate mismatch in kernel and herdtools7 updates.

klitmus7 in herdtools7 7.48 requires definition of ACCESS_ONCE() in kernel
headers, but it has been removed in Linux 4.15. This means klitmus7 of
herdtools7 7.48 works only on Linux 4.14.

In the repository of herdtools7, with the suggestion of Andrea, commit
e87d7f9287d1 ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated
ACCESS_ONCE in "user" synchronization barrier") has addressed the issue. 

This series is intended to be merged in Linux 4.17 merge window,
and hopefully we can have another update of herdtools7 by the time the merge
window opens...

Dependency to out-of-tree tools looks quite tricky. We need some neat way to
manage things.

Umm...

        Thanks, Akira
[...]

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

On Sat, 17 Feb 2018, Andrea Parri wrote:

> > Akira's observation about READ_ONCE extends to all (annotated) loads.  In
> > fact, it also applies to loads corresponding to unsuccessful RMW operations;
> > consider, for example, the following variation of MP+onceassign+derefonce:
> > 
> > C T
> > 
> > {
> > y=z;
> > z=0;
> > }
> > 
> > P0(int *x, int **y)
> > {
> > 	WRITE_ONCE(*x, 1);
> > 	smp_store_release(y, x);
> > }
> > 
> > P1(int **y, int *z)
> > {
> > 	int *r0;
> > 	int r1;
> > 
> > 	r0 = cmpxchg_relaxed(y, z, z);
> > 	r1 = READ_ONCE(*r0);
> > }
> > 
> > exists (1:r0=x /\ 1:r1=0)
> > 
> > The final state is allowed w/o the patch, and forbidden w/ the patch.
> > 
> > This also reminds me of
> > 
> >    5a8897cc7631fa544d079c443800f4420d1b173f
> >    ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics")
> > 
> > (that we probably want to mention in the commit message).
> 
> Please also notice that 5a8897cc7631f only touched alpha's atomic.h:
> I see no corresponding commit/change on {,cmp}xchg.h (where the "mb"
> is currently conditionally executed).

This leaves us with a question: Do we want to change the kernel by
adding memory barriers after unsuccessful RMW operations on Alpha, or
do we want to change the model by excluding such operations from
address dependencies?

Note that operations like atomic_add_unless() already include memory 
barriers.

Alan

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Peter Zijlstra]

On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> This leaves us with a question: Do we want to change the kernel by
> adding memory barriers after unsuccessful RMW operations on Alpha, or
> do we want to change the model by excluding such operations from
> address dependencies?

I think we want to put all the 'pain and weirdness' in Alpha.

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Peter Zijlstra]

On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> Note that operations like atomic_add_unless() already include memory 
> barriers.

It is valid for atomic_add_unless() to not imply any barriers when the
addition doesn't happen.

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> On Sat, 17 Feb 2018, Andrea Parri wrote:
> 
> > > Akira's observation about READ_ONCE extends to all (annotated) loads.  In
> > > fact, it also applies to loads corresponding to unsuccessful RMW operations;
> > > consider, for example, the following variation of MP+onceassign+derefonce:
> > > 
> > > C T
> > > 
> > > {
> > > y=z;
> > > z=0;
> > > }
> > > 
> > > P0(int *x, int **y)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	smp_store_release(y, x);
> > > }
> > > 
> > > P1(int **y, int *z)
> > > {
> > > 	int *r0;
> > > 	int r1;
> > > 
> > > 	r0 = cmpxchg_relaxed(y, z, z);
> > > 	r1 = READ_ONCE(*r0);
> > > }
> > > 
> > > exists (1:r0=x /\ 1:r1=0)
> > > 
> > > The final state is allowed w/o the patch, and forbidden w/ the patch.
> > > 
> > > This also reminds me of
> > > 
> > >    5a8897cc7631fa544d079c443800f4420d1b173f
> > >    ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics")
> > > 
> > > (that we probably want to mention in the commit message).
> > 
> > Please also notice that 5a8897cc7631f only touched alpha's atomic.h:
> > I see no corresponding commit/change on {,cmp}xchg.h (where the "mb"
> > is currently conditionally executed).
> 
> This leaves us with a question: Do we want to change the kernel by
> adding memory barriers after unsuccessful RMW operations on Alpha, or
> do we want to change the model by excluding such operations from
> address dependencies?

I vote for adding the barrier on Alpha.  However, I don't know of any
code in the Linux kernel that relies on read-to-read address dependency
ordering headed by a failing RMW operation, so I don't feel all that
strongly about this.

> Note that operations like atomic_add_unless() already include memory 
> barriers.

And I don't see an atomic_add_unless_relaxed(), so we are good on this
one.  So far, anyway!  ;-)

							Thanx, Paul

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Peter Zijlstra]

On Mon, Feb 19, 2018 at 11:41:23AM -0800, Paul E. McKenney wrote:
> On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > This leaves us with a question: Do we want to change the kernel by
> > adding memory barriers after unsuccessful RMW operations on Alpha, or
> > do we want to change the model by excluding such operations from
> > address dependencies?
> 
> I vote for adding the barrier on Alpha.  However, I don't know of any
> code in the Linux kernel that relies on read-to-read address dependency
> ordering headed by a failing RMW operation, so I don't feel all that
> strongly about this.

Right, but not knowing doesn't mean doesn't exist, and most certainly
doesn't mean will never exist.

> > Note that operations like atomic_add_unless() already include memory 
> > barriers.
> 
> And I don't see an atomic_add_unless_relaxed(), so we are good on this
> one.  So far, anyway!  ;-)

Not the point, add_unless() is a conditional operation, and therefore
doesn't need to imply anything when failing.

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Andrea Parri]

On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> On Sat, 17 Feb 2018, Andrea Parri wrote:
> 
> > > Akira's observation about READ_ONCE extends to all (annotated) loads.  In
> > > fact, it also applies to loads corresponding to unsuccessful RMW operations;
> > > consider, for example, the following variation of MP+onceassign+derefonce:
> > > 
> > > C T
> > > 
> > > {
> > > y=z;
> > > z=0;
> > > }
> > > 
> > > P0(int *x, int **y)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	smp_store_release(y, x);
> > > }
> > > 
> > > P1(int **y, int *z)
> > > {
> > > 	int *r0;
> > > 	int r1;
> > > 
> > > 	r0 = cmpxchg_relaxed(y, z, z);
> > > 	r1 = READ_ONCE(*r0);
> > > }
> > > 
> > > exists (1:r0=x /\ 1:r1=0)
> > > 
> > > The final state is allowed w/o the patch, and forbidden w/ the patch.
> > > 
> > > This also reminds me of
> > > 
> > >    5a8897cc7631fa544d079c443800f4420d1b173f
> > >    ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics")
> > > 
> > > (that we probably want to mention in the commit message).
> > 
> > Please also notice that 5a8897cc7631f only touched alpha's atomic.h:
> > I see no corresponding commit/change on {,cmp}xchg.h (where the "mb"
> > is currently conditionally executed).
> 
> This leaves us with a question: Do we want to change the kernel by
> adding memory barriers after unsuccessful RMW operations on Alpha, or
> do we want to change the model by excluding such operations from
> address dependencies?

I'd like to continue to treat R[once] and R*[once] equally if possible.
Given the (unconditional) smp_read_barrier_depends in READ_ONCE and in
atomics, it seems reasonable to have it unconditionally in cmpxchg.

As with the following patch?

  Andrea

---
diff --git a/arch/alpha/include/asm/xchg.h b/arch/alpha/include/asm/xchg.h
index 68dfb3cb71454..e2660866ce972 100644
--- a/arch/alpha/include/asm/xchg.h
+++ b/arch/alpha/include/asm/xchg.h
@@ -128,10 +128,9 @@ ____xchg(, volatile void *ptr, unsigned long x, int size)
  * store NEW in MEM.  Return the initial value in MEM.  Success is
  * indicated by comparing RETURN with OLD.
  *
- * The memory barrier should be placed in SMP only when we actually
- * make the change. If we don't change anything (so if the returned
- * prev is equal to old) then we aren't acquiring anything new and
- * we don't need any memory barrier as far I can tell.
+ * The memory barrier is placed in SMP unconditionally, in order to
+ * guarantee that dependency ordering is preserved when a dependency
+ * is headed by an unsuccessful operation.
  */
 
 static inline unsigned long
@@ -150,8 +149,8 @@ ____cmpxchg(_u8, volatile char *m, unsigned char old, unsigned char new)
 	"	or	%1,%2,%2\n"
 	"	stq_c	%2,0(%4)\n"
 	"	beq	%2,3f\n"
-		__ASM__MB
 	"2:\n"
+		__ASM__MB
 	".subsection 2\n"
 	"3:	br	1b\n"
 	".previous"
@@ -177,8 +176,8 @@ ____cmpxchg(_u16, volatile short *m, unsigned short old, unsigned short new)
 	"	or	%1,%2,%2\n"
 	"	stq_c	%2,0(%4)\n"
 	"	beq	%2,3f\n"
-		__ASM__MB
 	"2:\n"
+		__ASM__MB
 	".subsection 2\n"
 	"3:	br	1b\n"
 	".previous"
@@ -200,8 +199,8 @@ ____cmpxchg(_u32, volatile int *m, int old, int new)
 	"	mov %4,%1\n"
 	"	stl_c %1,%2\n"
 	"	beq %1,3f\n"
-		__ASM__MB
 	"2:\n"
+		__ASM__MB
 	".subsection 2\n"
 	"3:	br 1b\n"
 	".previous"
@@ -223,8 +222,8 @@ ____cmpxchg(_u64, volatile long *m, unsigned long old, unsigned long new)
 	"	mov %4,%1\n"
 	"	stq_c %1,%2\n"
 	"	beq %1,3f\n"
-		__ASM__MB
 	"2:\n"
+		__ASM__MB
 	".subsection 2\n"
 	"3:	br 1b\n"
 	".previous"


> 
> Note that operations like atomic_add_unless() already include memory 
> barriers.
> 
> Alan
> 

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Peter Zijlstra]

On Tue, Feb 20, 2018 at 10:33:47AM +0100, Andrea Parri wrote:
> I'd like to continue to treat R[once] and R*[once] equally if possible.
> Given the (unconditional) smp_read_barrier_depends in READ_ONCE and in
> atomics, it seems reasonable to have it unconditionally in cmpxchg.
> 
> As with the following patch?
> 
>   Andrea
> 
> ---
> diff --git a/arch/alpha/include/asm/xchg.h b/arch/alpha/include/asm/xchg.h
> index 68dfb3cb71454..e2660866ce972 100644
> --- a/arch/alpha/include/asm/xchg.h
> +++ b/arch/alpha/include/asm/xchg.h
> @@ -128,10 +128,9 @@ ____xchg(, volatile void *ptr, unsigned long x, int size)
>   * store NEW in MEM.  Return the initial value in MEM.  Success is
>   * indicated by comparing RETURN with OLD.
>   *
> - * The memory barrier should be placed in SMP only when we actually
> - * make the change. If we don't change anything (so if the returned
> - * prev is equal to old) then we aren't acquiring anything new and
> - * we don't need any memory barrier as far I can tell.
> + * The memory barrier is placed in SMP unconditionally, in order to
> + * guarantee that dependency ordering is preserved when a dependency
> + * is headed by an unsuccessful operation.
>   */
>  
>  static inline unsigned long
> @@ -150,8 +149,8 @@ ____cmpxchg(_u8, volatile char *m, unsigned char old, unsigned char new)
>  	"	or	%1,%2,%2\n"
>  	"	stq_c	%2,0(%4)\n"
>  	"	beq	%2,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br	1b\n"
>  	".previous"
> @@ -177,8 +176,8 @@ ____cmpxchg(_u16, volatile short *m, unsigned short old, unsigned short new)
>  	"	or	%1,%2,%2\n"
>  	"	stq_c	%2,0(%4)\n"
>  	"	beq	%2,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br	1b\n"
>  	".previous"
> @@ -200,8 +199,8 @@ ____cmpxchg(_u32, volatile int *m, int old, int new)
>  	"	mov %4,%1\n"
>  	"	stl_c %1,%2\n"
>  	"	beq %1,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br 1b\n"
>  	".previous"
> @@ -223,8 +222,8 @@ ____cmpxchg(_u64, volatile long *m, unsigned long old, unsigned long new)
>  	"	mov %4,%1\n"
>  	"	stq_c %1,%2\n"
>  	"	beq %1,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br 1b\n"
>  	".previous"

ACK

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Mon, Feb 19, 2018 at 06:44:13PM +0100, Peter Zijlstra wrote:
> On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > Note that operations like atomic_add_unless() already include memory 
> > barriers.
> 
> It is valid for atomic_add_unless() to not imply any barriers when the
> addition doesn't happen.

Agreed, given that atomic_add_unless() just returns 0 or 1, not the
pointer being added.  Of course, the __atomic_add_unless() function
that it calls is another story, as it does return the old value.  Sigh.
And __atomic_add_unless() is called directly from some code.  All of
which looks to be counters rather than pointers, thankfully.

So, do we want to rely on atomic_add_unless() always being
invoked on counters rather than pointers, or does it need an
smp_read_barrier_depends()?

							Thanx, Paul

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Mon, Feb 19, 2018 at 09:28:44PM +0100, Peter Zijlstra wrote:
> On Mon, Feb 19, 2018 at 11:41:23AM -0800, Paul E. McKenney wrote:
> > On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > > This leaves us with a question: Do we want to change the kernel by
> > > adding memory barriers after unsuccessful RMW operations on Alpha, or
> > > do we want to change the model by excluding such operations from
> > > address dependencies?
> > 
> > I vote for adding the barrier on Alpha.  However, I don't know of any
> > code in the Linux kernel that relies on read-to-read address dependency
> > ordering headed by a failing RMW operation, so I don't feel all that
> > strongly about this.
> 
> Right, but not knowing doesn't mean doesn't exist, and most certainly
> doesn't mean will never exist.

Fair enough, safety first!

> > > Note that operations like atomic_add_unless() already include memory 
> > > barriers.
> > 
> > And I don't see an atomic_add_unless_relaxed(), so we are good on this
> > one.  So far, anyway!  ;-)
> 
> Not the point, add_unless() is a conditional operation, and therefore
> doesn't need to imply anything when failing.

Plus it doesn't return a pointer, so there is no problem with dereferences.
Unless someone wants to use its return value as an array index and rely
on dependency ordering to the array, but I would NAK that use case.

							Thanx, Paul

Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Paul E. McKenney]

On Mon, Feb 19, 2018 at 12:46:51AM +0900, Akira Yokosawa wrote:
> On 2018/02/14 14:52:38 -0800, Paul E. McKenney wrote:
> > On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote:
> >> On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote:
> >>> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
> >>>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
> >>>> From: Akira Yokosawa <akiyks@gmail.com>
> >>>> Date: Fri, 9 Feb 2018 04:51:05 -0800
> >>>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
> >>>>
> >>>> As of herd7 7.47, these '-'s are not permitted and end up in
> >>>> errors such as:
> >>>>
> >>>>     File "./linux-kernel.def", line 44, characters 29-30:
> >>>>     unexpected '-' (in macros)
> >>>>
> >>>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
> >>>> identifiers match ASPLOS paper") in the repository at
> >>>> https://github.com/aparri/memory-model can restore the compatibility
> >>>> with herd7 7.47.
> >>>>
> >>>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
> >>>> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> >>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >>>> ---
> >>>> Paul,
> >>>>
> >>>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> >>>
> >>> Thank you, Akira!
> >>>
> >>> I am going to hold off on this for a bit to see if we can instead get
> >>> a new release of herd7, but if we can't. this might well be a very good
> >>> way to go.
> >>
> >> So, herdtools7.7.48 is now available by "opam update; opam upgrade".
> >> Maybe mentioning the required version of herdtools7 in README would help.
> > 
> > Or have some way for the memory model's .cat files to state what version
> > they need, but in the meantime please see the patch below.  But even with
> > such version specification, we probably want to have the version in the
> > README...
> > 
> >> One glitch I'm aware of is one of the output of klitmus7 fails to
> >> compile on kernels prior to 4.14, because of smp_mb__after_spinlock()
> >> used in Z6.0+pooncelock+poonceLock+pombonce.litmus.
> > 
> > This is one advantage of having the memory model in the kernel source
> > itself -- the versions match.  And people can always fire up a different
> > kernel version (for example, within a VM) to run the output of klitmus7.
> > 
> 
> There is another unfortunate mismatch in kernel and herdtools7 updates.
> 
> klitmus7 in herdtools7 7.48 requires definition of ACCESS_ONCE() in kernel
> headers, but it has been removed in Linux 4.15. This means klitmus7 of
> herdtools7 7.48 works only on Linux 4.14.
> 
> In the repository of herdtools7, with the suggestion of Andrea, commit
> e87d7f9287d1 ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated
> ACCESS_ONCE in "user" synchronization barrier") has addressed the issue. 
> 
> This series is intended to be merged in Linux 4.17 merge window,
> and hopefully we can have another update of herdtools7 by the time the merge
> window opens...
> 
> Dependency to out-of-tree tools looks quite tricky. We need some neat way to
> manage things.
> 
> Umm...

Yes, dependencies on out-of-tree tools is quite tricky, witness the
"fun and excitement" provided even by GCC from time to time.

I agree that another herdtools7 release is required, and I do very much
thank you for testing this and finding this issue!

							Thanx, Paul

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

On Tue, 20 Feb 2018, Paul E. McKenney wrote:

> On Mon, Feb 19, 2018 at 09:28:44PM +0100, Peter Zijlstra wrote:
> > On Mon, Feb 19, 2018 at 11:41:23AM -0800, Paul E. McKenney wrote:
> > > On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > > > This leaves us with a question: Do we want to change the kernel by
> > > > adding memory barriers after unsuccessful RMW operations on Alpha, or
> > > > do we want to change the model by excluding such operations from
> > > > address dependencies?
> > > 
> > > I vote for adding the barrier on Alpha.  However, I don't know of any
> > > code in the Linux kernel that relies on read-to-read address dependency
> > > ordering headed by a failing RMW operation, so I don't feel all that
> > > strongly about this.
> > 
> > Right, but not knowing doesn't mean doesn't exist, and most certainly
> > doesn't mean will never exist.
> 
> Fair enough, safety first!
> 
> > > > Note that operations like atomic_add_unless() already include memory 
> > > > barriers.
> > > 
> > > And I don't see an atomic_add_unless_relaxed(), so we are good on this
> > > one.  So far, anyway!  ;-)
> > 
> > Not the point, add_unless() is a conditional operation, and therefore
> > doesn't need to imply anything when failing.
> 
> Plus it doesn't return a pointer, so there is no problem with dereferences.
> Unless someone wants to use its return value as an array index and rely
> on dependency ordering to the array, but I would NAK that use case.

You may not get the chance to NAK it.

We need to be consistent.  Array indexing is indeed a form of address
dependency, so either we assert that the dependency is enforced when
the array index is derived from a failed atomic operation, or else we
assert that failed atomic operations do not create address
dependencies.

Alan

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Andrea Parri]

On Tue, Feb 20, 2018 at 06:48:13AM -0800, Paul E. McKenney wrote:
> On Mon, Feb 19, 2018 at 06:44:13PM +0100, Peter Zijlstra wrote:
> > On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > > Note that operations like atomic_add_unless() already include memory 
> > > barriers.
> > 
> > It is valid for atomic_add_unless() to not imply any barriers when the
> > addition doesn't happen.
> 
> Agreed, given that atomic_add_unless() just returns 0 or 1, not the
> pointer being added.  Of course, the __atomic_add_unless() function
> that it calls is another story, as it does return the old value.  Sigh.
> And __atomic_add_unless() is called directly from some code.  All of
> which looks to be counters rather than pointers, thankfully.
> 
> So, do we want to rely on atomic_add_unless() always being
> invoked on counters rather than pointers, or does it need an
> smp_read_barrier_depends()?

alpha's implementation of __atomic_add_unless() has an unconditional smp_mb()
before returning so, as far as dependencies are concerned, these seem fine.

  Andrea


> 
> 							Thanx, Paul
> 

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

On Tue, 20 Feb 2018, Andrea Parri wrote:

> > This leaves us with a question: Do we want to change the kernel by
> > adding memory barriers after unsuccessful RMW operations on Alpha, or
> > do we want to change the model by excluding such operations from
> > address dependencies?
> 
> I'd like to continue to treat R[once] and R*[once] equally if possible.
> Given the (unconditional) smp_read_barrier_depends in READ_ONCE and in
> atomics, it seems reasonable to have it unconditionally in cmpxchg.
> 
> As with the following patch?

Yes, this seems reasonable to me.  If Will gives it his "Acked-by"  
to go with Peter's, you should submit it to Ingo Molnar.

And once this is made, there shouldn't be any trouble with the proposed 
patch for the memory model.

Alan

>   Andrea
> 
> ---
> diff --git a/arch/alpha/include/asm/xchg.h b/arch/alpha/include/asm/xchg.h
> index 68dfb3cb71454..e2660866ce972 100644
> --- a/arch/alpha/include/asm/xchg.h
> +++ b/arch/alpha/include/asm/xchg.h
> @@ -128,10 +128,9 @@ ____xchg(, volatile void *ptr, unsigned long x, int size)
>   * store NEW in MEM.  Return the initial value in MEM.  Success is
>   * indicated by comparing RETURN with OLD.
>   *
> - * The memory barrier should be placed in SMP only when we actually
> - * make the change. If we don't change anything (so if the returned
> - * prev is equal to old) then we aren't acquiring anything new and
> - * we don't need any memory barrier as far I can tell.
> + * The memory barrier is placed in SMP unconditionally, in order to
> + * guarantee that dependency ordering is preserved when a dependency
> + * is headed by an unsuccessful operation.
>   */
>  
>  static inline unsigned long
> @@ -150,8 +149,8 @@ ____cmpxchg(_u8, volatile char *m, unsigned char old, unsigned char new)
>  	"	or	%1,%2,%2\n"
>  	"	stq_c	%2,0(%4)\n"
>  	"	beq	%2,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br	1b\n"
>  	".previous"
> @@ -177,8 +176,8 @@ ____cmpxchg(_u16, volatile short *m, unsigned short old, unsigned short new)
>  	"	or	%1,%2,%2\n"
>  	"	stq_c	%2,0(%4)\n"
>  	"	beq	%2,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br	1b\n"
>  	".previous"
> @@ -200,8 +199,8 @@ ____cmpxchg(_u32, volatile int *m, int old, int new)
>  	"	mov %4,%1\n"
>  	"	stl_c %1,%2\n"
>  	"	beq %1,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br 1b\n"
>  	".previous"
> @@ -223,8 +222,8 @@ ____cmpxchg(_u64, volatile long *m, unsigned long old, unsigned long new)
>  	"	mov %4,%1\n"
>  	"	stq_c %1,%2\n"
>  	"	beq %1,3f\n"
> -		__ASM__MB
>  	"2:\n"
> +		__ASM__MB
>  	".subsection 2\n"
>  	"3:	br 1b\n"
>  	".previous"
> 
> 
> > 
> > Note that operations like atomic_add_unless() already include memory 
> > barriers.
> > 
> > Alan

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Tue, Feb 20, 2018 at 10:11:06AM -0500, Alan Stern wrote:
> On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> 
> > On Mon, Feb 19, 2018 at 09:28:44PM +0100, Peter Zijlstra wrote:
> > > On Mon, Feb 19, 2018 at 11:41:23AM -0800, Paul E. McKenney wrote:
> > > > On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > > > > This leaves us with a question: Do we want to change the kernel by
> > > > > adding memory barriers after unsuccessful RMW operations on Alpha, or
> > > > > do we want to change the model by excluding such operations from
> > > > > address dependencies?
> > > > 
> > > > I vote for adding the barrier on Alpha.  However, I don't know of any
> > > > code in the Linux kernel that relies on read-to-read address dependency
> > > > ordering headed by a failing RMW operation, so I don't feel all that
> > > > strongly about this.
> > > 
> > > Right, but not knowing doesn't mean doesn't exist, and most certainly
> > > doesn't mean will never exist.
> > 
> > Fair enough, safety first!
> > 
> > > > > Note that operations like atomic_add_unless() already include memory 
> > > > > barriers.
> > > > 
> > > > And I don't see an atomic_add_unless_relaxed(), so we are good on this
> > > > one.  So far, anyway!  ;-)
> > > 
> > > Not the point, add_unless() is a conditional operation, and therefore
> > > doesn't need to imply anything when failing.
> > 
> > Plus it doesn't return a pointer, so there is no problem with dereferences.
> > Unless someone wants to use its return value as an array index and rely
> > on dependency ordering to the array, but I would NAK that use case.
> 
> You may not get the chance to NAK it.
> 
> We need to be consistent.  Array indexing is indeed a form of address
> dependency, so either we assert that the dependency is enforced when
> the array index is derived from a failed atomic operation, or else we
> assert that failed atomic operations do not create address
> dependencies.

The problem is that the compiler can get up to a great deal more mischief
with integers than it can with pointers.  I agree that it would be quite
challenging to represent this distinction between integers and pointers in
the model, but then again herd does not yet support array indexing anyway.

So for the time being, anyway, I must stand by my NAK.

							Thanx, Paul

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Tue, Feb 20, 2018 at 04:17:52PM +0100, Andrea Parri wrote:
> On Tue, Feb 20, 2018 at 06:48:13AM -0800, Paul E. McKenney wrote:
> > On Mon, Feb 19, 2018 at 06:44:13PM +0100, Peter Zijlstra wrote:
> > > On Mon, Feb 19, 2018 at 12:14:45PM -0500, Alan Stern wrote:
> > > > Note that operations like atomic_add_unless() already include memory 
> > > > barriers.
> > > 
> > > It is valid for atomic_add_unless() to not imply any barriers when the
> > > addition doesn't happen.
> > 
> > Agreed, given that atomic_add_unless() just returns 0 or 1, not the
> > pointer being added.  Of course, the __atomic_add_unless() function
> > that it calls is another story, as it does return the old value.  Sigh.
> > And __atomic_add_unless() is called directly from some code.  All of
> > which looks to be counters rather than pointers, thankfully.
> > 
> > So, do we want to rely on atomic_add_unless() always being
> > invoked on counters rather than pointers, or does it need an
> > smp_read_barrier_depends()?
> 
> alpha's implementation of __atomic_add_unless() has an unconditional smp_mb()
> before returning so, as far as dependencies are concerned, these seem fine.

Very good!

							Thanx, Paul

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

On Fri, 16 Feb 2018, Paul E. McKenney wrote:

> On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> > Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> > smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> > kernel, it has not been necessary to use smp_read_barrier_depends().
> > Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> > lockless_dereference()") removed lockless_dereference() from the
> > kernel.
> > 
> > Since these primitives are no longer part of the kernel, they do not
> > belong in the Linux Kernel Memory Consistency Model.  This patch
> > removes them, along with the internal rb-dep relation, and updates the
> > revelant documentation.
> > 
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 
> I queued this, but would welcome an update that addressed Akira's
> feedback as appropriate.

Is it too late to send a v2 of this patch?  I didn't want to do it 
before now because the issue raised by Andrea wasn't settled.  (Some 
could claim that it still isn't fully settled...)

Alan

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 10:00:20AM -0500, Alan Stern wrote:
> On Fri, 16 Feb 2018, Paul E. McKenney wrote:
> 
> > On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> > > Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> > > smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> > > kernel, it has not been necessary to use smp_read_barrier_depends().
> > > Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> > > lockless_dereference()") removed lockless_dereference() from the
> > > kernel.
> > > 
> > > Since these primitives are no longer part of the kernel, they do not
> > > belong in the Linux Kernel Memory Consistency Model.  This patch
> > > removes them, along with the internal rb-dep relation, and updates the
> > > revelant documentation.
> > > 
> > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > 
> > I queued this, but would welcome an update that addressed Akira's
> > feedback as appropriate.
> 
> Is it too late to send a v2 of this patch?  I didn't want to do it 
> before now because the issue raised by Andrea wasn't settled.  (Some 
> could claim that it still isn't fully settled...)

Would you be willing to send a delta patch?  I can then place it directly
on top of your original patch, and once it settles out, I can ask Ingo
if he is willing to update the patch in -tip.

							Thanx, Paul

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Ingo Molnar]

* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:

> On Wed, Feb 21, 2018 at 10:00:20AM -0500, Alan Stern wrote:
> > On Fri, 16 Feb 2018, Paul E. McKenney wrote:
> > 
> > > On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> > > > Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> > > > smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> > > > kernel, it has not been necessary to use smp_read_barrier_depends().
> > > > Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> > > > lockless_dereference()") removed lockless_dereference() from the
> > > > kernel.
> > > > 
> > > > Since these primitives are no longer part of the kernel, they do not
> > > > belong in the Linux Kernel Memory Consistency Model.  This patch
> > > > removes them, along with the internal rb-dep relation, and updates the
> > > > revelant documentation.
> > > > 
> > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > 
> > > I queued this, but would welcome an update that addressed Akira's
> > > feedback as appropriate.
> > 
> > Is it too late to send a v2 of this patch?  I didn't want to do it 
> > before now because the issue raised by Andrea wasn't settled.  (Some 
> > could claim that it still isn't fully settled...)
> 
> Would you be willing to send a delta patch?  I can then place it directly
> on top of your original patch, and once it settles out, I can ask Ingo
> if he is willing to update the patch in -tip.

It would be better to have followup fixes as separate patches. I applied the 
current set of fixes/improvements today to help move things along - it's all 
advancing very nicely!

Thanks,

	Ingo

[PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
smp_read_barrier_depends, and lockless_dereference") was accidentally
merged too early, while it was still in RFC form.  This patch adds in
the missing pieces.

Akira pointed out some typos in the original patch, and he noted that
cheatsheet.txt should be updated to indicate how unsuccessful RMW
operations relate to address dependencies.

Andrea pointed out that the macro for rcu_dereference() in linux.def
should now use the "once" annotation instead of "deref".  He also
suggested that the comments should mention commit 5a8897cc7631
("locking/atomics/alpha: Add smp_read_barrier_depends() to
_release()/_relaxed() atomics") as an important precursor, and he
contributed commit cb13b424e986 ("locking/xchg/alpha: Add
unconditional memory barrier to cmpxchg()"), another prerequisite.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Suggested-by: Akira Yokosawa <akiyks@gmail.com>
Suggested-by: Andrea Parri <parri.andrea@gmail.com>
Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")

---

 tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
 tools/memory-model/Documentation/explanation.txt |    4 ++--
 tools/memory-model/linux-kernel.def              |    2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
===================================================================
--- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
+++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
@@ -1,11 +1,11 @@
                                   Prior Operation     Subsequent Operation
                                   ---------------  ---------------------------
                                C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
-                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
+                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
 
 Store, e.g., WRITE_ONCE()            Y                                       Y
-Load, e.g., READ_ONCE()              Y                              Y        Y
-Unsuccessful RMW operation           Y                              Y        Y
+Load, e.g., READ_ONCE()              Y                          Y   Y        Y
+Unsuccessful RMW operation           Y                          Y   Y        Y
 rcu_dereference()                    Y                          Y   Y        Y
 Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
 Successful *_release()         C        Y  Y    Y     W                      Y
Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
===================================================================
--- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
+++ usb-4.x/tools/memory-model/Documentation/explanation.txt
@@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
 executed on C before the fence (i.e., those which precede the fence in
 program order).
 
-read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
+read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
 other properties which we discuss later.
 
 
@@ -1138,7 +1138,7 @@ final effect is that even though the two
 program order, it appears that they aren't.
 
 This could not have happened if the local cache had processed the
-incoming stores in FIFO order.  In constrast, other architectures
+incoming stores in FIFO order.  By contrast, other architectures
 maintain at least the appearance of FIFO order.
 
 In practice, this difficulty is solved by inserting a special fence
Index: usb-4.x/tools/memory-model/linux-kernel.def
===================================================================
--- usb-4.x.orig/tools/memory-model/linux-kernel.def
+++ usb-4.x/tools/memory-model/linux-kernel.def
@@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
 smp_store_release(X,V) { __store{release}(*X,V); }
 smp_load_acquire(X) __load{acquire}(*X)
 rcu_assign_pointer(X,V) { __store{release}(X,V); }
-rcu_dereference(X) __load{deref}(X)
+rcu_dereference(X) __load{once}(X)
 
 // Fences
 smp_mb() { __fence{mb} ; }

Re: [PATCH] tools/memory-model: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 05:51:43PM +0100, Ingo Molnar wrote:
> 
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> 
> > On Wed, Feb 21, 2018 at 10:00:20AM -0500, Alan Stern wrote:
> > > On Fri, 16 Feb 2018, Paul E. McKenney wrote:
> > > 
> > > > On Fri, Feb 16, 2018 at 05:22:55PM -0500, Alan Stern wrote:
> > > > > Since commit 76ebbe78f739 ("locking/barriers: Add implicit
> > > > > smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15
> > > > > kernel, it has not been necessary to use smp_read_barrier_depends().
> > > > > Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill
> > > > > lockless_dereference()") removed lockless_dereference() from the
> > > > > kernel.
> > > > > 
> > > > > Since these primitives are no longer part of the kernel, they do not
> > > > > belong in the Linux Kernel Memory Consistency Model.  This patch
> > > > > removes them, along with the internal rb-dep relation, and updates the
> > > > > revelant documentation.
> > > > > 
> > > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > > 
> > > > I queued this, but would welcome an update that addressed Akira's
> > > > feedback as appropriate.
> > > 
> > > Is it too late to send a v2 of this patch?  I didn't want to do it 
> > > before now because the issue raised by Andrea wasn't settled.  (Some 
> > > could claim that it still isn't fully settled...)
> > 
> > Would you be willing to send a delta patch?  I can then place it directly
> > on top of your original patch, and once it settles out, I can ask Ingo
> > if he is willing to update the patch in -tip.
> 
> It would be better to have followup fixes as separate patches. I applied the 
> current set of fixes/improvements today to help move things along - it's all 
> advancing very nicely!

Will do, and glad you like it!

								Thanx, Paul

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Andrea Parri]

On Wed, Feb 21, 2018 at 12:15:56PM -0500, Alan Stern wrote:
> Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> smp_read_barrier_depends, and lockless_dereference") was accidentally
> merged too early, while it was still in RFC form.  This patch adds in
> the missing pieces.
> 
> Akira pointed out some typos in the original patch, and he noted that
> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> operations relate to address dependencies.
> 
> Andrea pointed out that the macro for rcu_dereference() in linux.def
> should now use the "once" annotation instead of "deref".  He also
> suggested that the comments should mention commit 5a8897cc7631
> ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> _release()/_relaxed() atomics") as an important precursor, and he
> contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> unconditional memory barrier to cmpxchg()"), another prerequisite.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")

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

Thanks,
  Andrea


> 
> ---
> 
>  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
>  tools/memory-model/Documentation/explanation.txt |    4 ++--
>  tools/memory-model/linux-kernel.def              |    2 +-
>  3 files changed, 6 insertions(+), 6 deletions(-)
> 
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -1,11 +1,11 @@
>                                    Prior Operation     Subsequent Operation
>                                    ---------------  ---------------------------
>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
>  
>  Store, e.g., WRITE_ONCE()            Y                                       Y
> -Load, e.g., READ_ONCE()              Y                              Y        Y
> -Unsuccessful RMW operation           Y                              Y        Y
> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> +Unsuccessful RMW operation           Y                          Y   Y        Y
>  rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
>  
> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
>  other properties which we discuss later.
>  
>  
> @@ -1138,7 +1138,7 @@ final effect is that even though the two
>  program order, it appears that they aren't.
>  
>  This could not have happened if the local cache had processed the
> -incoming stores in FIFO order.  In constrast, other architectures
> +incoming stores in FIFO order.  By contrast, other architectures
>  maintain at least the appearance of FIFO order.
>  
>  In practice, this difficulty is solved by inserting a special fence
> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -rcu_dereference(X) __load{deref}(X)
> +rcu_dereference(X) __load{once}(X)
>  
>  // Fences
>  smp_mb() { __fence{mb} ; }
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 12:15:56PM -0500, Alan Stern wrote:
> Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> smp_read_barrier_depends, and lockless_dereference") was accidentally
> merged too early, while it was still in RFC form.  This patch adds in
> the missing pieces.
> 
> Akira pointed out some typos in the original patch, and he noted that
> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> operations relate to address dependencies.
> 
> Andrea pointed out that the macro for rcu_dereference() in linux.def
> should now use the "once" annotation instead of "deref".  He also
> suggested that the comments should mention commit 5a8897cc7631
> ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> _release()/_relaxed() atomics") as an important precursor, and he
> contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> unconditional memory barrier to cmpxchg()"), another prerequisite.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")

Queued, thank you!

							Thanx, Paul

> ---
> 
>  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
>  tools/memory-model/Documentation/explanation.txt |    4 ++--
>  tools/memory-model/linux-kernel.def              |    2 +-
>  3 files changed, 6 insertions(+), 6 deletions(-)
> 
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -1,11 +1,11 @@
>                                    Prior Operation     Subsequent Operation
>                                    ---------------  ---------------------------
>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
> 
>  Store, e.g., WRITE_ONCE()            Y                                       Y
> -Load, e.g., READ_ONCE()              Y                              Y        Y
> -Unsuccessful RMW operation           Y                              Y        Y
> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> +Unsuccessful RMW operation           Y                          Y   Y        Y
>  rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
> 
> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
>  other properties which we discuss later.
> 
> 
> @@ -1138,7 +1138,7 @@ final effect is that even though the two
>  program order, it appears that they aren't.
> 
>  This could not have happened if the local cache had processed the
> -incoming stores in FIFO order.  In constrast, other architectures
> +incoming stores in FIFO order.  By contrast, other architectures
>  maintain at least the appearance of FIFO order.
> 
>  In practice, this difficulty is solved by inserting a special fence
> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -rcu_dereference(X) __load{deref}(X)
> +rcu_dereference(X) __load{once}(X)
> 
>  // Fences
>  smp_mb() { __fence{mb} ; }
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Wed, Feb 21, 2018 at 06:58:57PM +0100, Andrea Parri wrote:
> On Wed, Feb 21, 2018 at 12:15:56PM -0500, Alan Stern wrote:
> > Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> > smp_read_barrier_depends, and lockless_dereference") was accidentally
> > merged too early, while it was still in RFC form.  This patch adds in
> > the missing pieces.
> > 
> > Akira pointed out some typos in the original patch, and he noted that
> > cheatsheet.txt should be updated to indicate how unsuccessful RMW
> > operations relate to address dependencies.
> > 
> > Andrea pointed out that the macro for rcu_dereference() in linux.def
> > should now use the "once" annotation instead of "deref".  He also
> > suggested that the comments should mention commit 5a8897cc7631
> > ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> > _release()/_relaxed() atomics") as an important precursor, and he
> > contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> > unconditional memory barrier to cmpxchg()"), another prerequisite.
> > 
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> > Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> > Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
> 
> Acked-by: Andrea Parri <parri.andrea@gmail.com>

Applied, thank you!

							Thanx, Paul

> Thanks,
>   Andrea
> 
> 
> > 
> > ---
> > 
> >  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
> >  tools/memory-model/Documentation/explanation.txt |    4 ++--
> >  tools/memory-model/linux-kernel.def              |    2 +-
> >  3 files changed, 6 insertions(+), 6 deletions(-)
> > 
> > Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> > ===================================================================
> > --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
> > +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> > @@ -1,11 +1,11 @@
> >                                    Prior Operation     Subsequent Operation
> >                                    ---------------  ---------------------------
> >                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> > -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> > +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
> >  
> >  Store, e.g., WRITE_ONCE()            Y                                       Y
> > -Load, e.g., READ_ONCE()              Y                              Y        Y
> > -Unsuccessful RMW operation           Y                              Y        Y
> > +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> > +Unsuccessful RMW operation           Y                          Y   Y        Y
> >  rcu_dereference()                    Y                          Y   Y        Y
> >  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
> >  Successful *_release()         C        Y  Y    Y     W                      Y
> > Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> > ===================================================================
> > --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> > +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> > @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
> >  executed on C before the fence (i.e., those which precede the fence in
> >  program order).
> >  
> > -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> > +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> >  other properties which we discuss later.
> >  
> >  
> > @@ -1138,7 +1138,7 @@ final effect is that even though the two
> >  program order, it appears that they aren't.
> >  
> >  This could not have happened if the local cache had processed the
> > -incoming stores in FIFO order.  In constrast, other architectures
> > +incoming stores in FIFO order.  By contrast, other architectures
> >  maintain at least the appearance of FIFO order.
> >  
> >  In practice, this difficulty is solved by inserting a special fence
> > Index: usb-4.x/tools/memory-model/linux-kernel.def
> > ===================================================================
> > --- usb-4.x.orig/tools/memory-model/linux-kernel.def
> > +++ usb-4.x/tools/memory-model/linux-kernel.def
> > @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
> >  smp_store_release(X,V) { __store{release}(*X,V); }
> >  smp_load_acquire(X) __load{acquire}(*X)
> >  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> > -rcu_dereference(X) __load{deref}(X)
> > +rcu_dereference(X) __load{once}(X)
> >  
> >  // Fences
> >  smp_mb() { __fence{mb} ; }
> > 
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Akira Yokosawa]

On 2018/02/22 2:15, Alan Stern wrote:
> Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> smp_read_barrier_depends, and lockless_dereference") was accidentally
> merged too early, while it was still in RFC form.  This patch adds in
> the missing pieces.
> 
> Akira pointed out some typos in the original patch, and he noted that
> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> operations relate to address dependencies.

My point was to separate unannotated loads from READ_ONCE(), if the
cheatsheet should concern such accesses as well.
Unsuccessful RMW operations were brought up by Andrea.

> 
> Andrea pointed out that the macro for rcu_dereference() in linux.def
> should now use the "once" annotation instead of "deref".  He also
> suggested that the comments should mention commit 5a8897cc7631
> ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> _release()/_relaxed() atomics") as an important precursor, and he
> contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> unconditional memory barrier to cmpxchg()"), another prerequisite.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
> 

The change itself looks good to me.

Acked-by: Akira Yokosawa <akiyks@gmail.com>

       Thanks, Akira

> ---
> 
>  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
>  tools/memory-model/Documentation/explanation.txt |    4 ++--
>  tools/memory-model/linux-kernel.def              |    2 +-
>  3 files changed, 6 insertions(+), 6 deletions(-)
> 
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -1,11 +1,11 @@
>                                    Prior Operation     Subsequent Operation
>                                    ---------------  ---------------------------
>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
>  
>  Store, e.g., WRITE_ONCE()            Y                                       Y
> -Load, e.g., READ_ONCE()              Y                              Y        Y
> -Unsuccessful RMW operation           Y                              Y        Y
> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> +Unsuccessful RMW operation           Y                          Y   Y        Y
>  rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
>  
> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
>  other properties which we discuss later.
>  
>  
> @@ -1138,7 +1138,7 @@ final effect is that even though the two
>  program order, it appears that they aren't.
>  
>  This could not have happened if the local cache had processed the
> -incoming stores in FIFO order.  In constrast, other architectures
> +incoming stores in FIFO order.  By contrast, other architectures
>  maintain at least the appearance of FIFO order.
>  
>  In practice, this difficulty is solved by inserting a special fence
> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -rcu_dereference(X) __load{deref}(X)
> +rcu_dereference(X) __load{once}(X)
>  
>  // Fences
>  smp_mb() { __fence{mb} ; }
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Akira Yokosawa]

On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
> On 2018/02/22 2:15, Alan Stern wrote:
>> Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
>> smp_read_barrier_depends, and lockless_dereference") was accidentally
>> merged too early, while it was still in RFC form.  This patch adds in
>> the missing pieces.
>>
>> Akira pointed out some typos in the original patch, and he noted that
>> cheatsheet.txt should be updated to indicate how unsuccessful RMW
>> operations relate to address dependencies.
> 
> My point was to separate unannotated loads from READ_ONCE(), if the
> cheatsheet should concern such accesses as well.
> Unsuccessful RMW operations were brought up by Andrea.
>

Paul, can you amend above paragraph in the change log to something like:

    Akira pointed out some typos in the original patch, and he noted that
    cheatsheet.txt should be updated to indicate READ_ONCE() implies
    address dependency, which invited Andrea's observation that it should
    also be updated to indicate how unsuccessful RMW operations relate to
    address dependencies.

, if Alan and Andrea are OK with the amendment.

Also, please append my Acked-by.

Acked-by: Akira Yokosawa <akiyks@gmail.com>

        Thanks, Akira
 
>>
>> Andrea pointed out that the macro for rcu_dereference() in linux.def
>> should now use the "once" annotation instead of "deref".  He also
>> suggested that the comments should mention commit 5a8897cc7631
>> ("locking/atomics/alpha: Add smp_read_barrier_depends() to
>> _release()/_relaxed() atomics") as an important precursor, and he
>> contributed commit cb13b424e986 ("locking/xchg/alpha: Add
>> unconditional memory barrier to cmpxchg()"), another prerequisite.
>>
>> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
>> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
>> Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
>>
> 
> The change itself looks good to me.
> 
> Acked-by: Akira Yokosawa <akiyks@gmail.com>
> 
>        Thanks, Akira
> 
>> ---
>>
>>  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
>>  tools/memory-model/Documentation/explanation.txt |    4 ++--
>>  tools/memory-model/linux-kernel.def              |    2 +-
>>  3 files changed, 6 insertions(+), 6 deletions(-)
>>
>> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
>> ===================================================================
>> --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
>> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
>> @@ -1,11 +1,11 @@
>>                                    Prior Operation     Subsequent Operation
>>                                    ---------------  ---------------------------
>>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
>> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
>> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
>>  
>>  Store, e.g., WRITE_ONCE()            Y                                       Y
>> -Load, e.g., READ_ONCE()              Y                              Y        Y
>> -Unsuccessful RMW operation           Y                              Y        Y
>> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
>> +Unsuccessful RMW operation           Y                          Y   Y        Y
>>  rcu_dereference()                    Y                          Y   Y        Y
>>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>>  Successful *_release()         C        Y  Y    Y     W                      Y
>> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
>> ===================================================================
>> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
>> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
>> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
>>  executed on C before the fence (i.e., those which precede the fence in
>>  program order).
>>  
>> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
>> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
>>  other properties which we discuss later.
>>  
>>  
>> @@ -1138,7 +1138,7 @@ final effect is that even though the two
>>  program order, it appears that they aren't.
>>  
>>  This could not have happened if the local cache had processed the
>> -incoming stores in FIFO order.  In constrast, other architectures
>> +incoming stores in FIFO order.  By contrast, other architectures
>>  maintain at least the appearance of FIFO order.
>>  
>>  In practice, this difficulty is solved by inserting a special fence
>> Index: usb-4.x/tools/memory-model/linux-kernel.def
>> ===================================================================
>> --- usb-4.x.orig/tools/memory-model/linux-kernel.def
>> +++ usb-4.x/tools/memory-model/linux-kernel.def
>> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>>  smp_store_release(X,V) { __store{release}(*X,V); }
>>  smp_load_acquire(X) __load{acquire}(*X)
>>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
>> -rcu_dereference(X) __load{deref}(X)
>> +rcu_dereference(X) __load{once}(X)
>>  
>>  // Fences
>>  smp_mb() { __fence{mb} ; }
>>
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Sat, Feb 24, 2018 at 12:22:24PM +0900, Akira Yokosawa wrote:
> On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
> > On 2018/02/22 2:15, Alan Stern wrote:
> >> Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> >> smp_read_barrier_depends, and lockless_dereference") was accidentally
> >> merged too early, while it was still in RFC form.  This patch adds in
> >> the missing pieces.
> >>
> >> Akira pointed out some typos in the original patch, and he noted that
> >> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> >> operations relate to address dependencies.
> > 
> > My point was to separate unannotated loads from READ_ONCE(), if the
> > cheatsheet should concern such accesses as well.
> > Unsuccessful RMW operations were brought up by Andrea.
> >
> 
> Paul, can you amend above paragraph in the change log to something like:
> 
>     Akira pointed out some typos in the original patch, and he noted that
>     cheatsheet.txt should be updated to indicate READ_ONCE() implies
>     address dependency, which invited Andrea's observation that it should
>     also be updated to indicate how unsuccessful RMW operations relate to
>     address dependencies.
> 
> , if Alan and Andrea are OK with the amendment.
> 
> Also, please append my Acked-by.
> 
> Acked-by: Akira Yokosawa <akiyks@gmail.com>

I can still amend this, and have added your Acked-by.  If Alan and Andrea
OK with your change, I will apply that also.

							Thanx, Paul

> >> Andrea pointed out that the macro for rcu_dereference() in linux.def
> >> should now use the "once" annotation instead of "deref".  He also
> >> suggested that the comments should mention commit 5a8897cc7631
> >> ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> >> _release()/_relaxed() atomics") as an important precursor, and he
> >> contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> >> unconditional memory barrier to cmpxchg()"), another prerequisite.
> >>
> >> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> >> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> >> Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
> >>
> > 
> > The change itself looks good to me.
> > 
> > Acked-by: Akira Yokosawa <akiyks@gmail.com>
> > 
> >        Thanks, Akira
> > 
> >> ---
> >>
> >>  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
> >>  tools/memory-model/Documentation/explanation.txt |    4 ++--
> >>  tools/memory-model/linux-kernel.def              |    2 +-
> >>  3 files changed, 6 insertions(+), 6 deletions(-)
> >>
> >> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> >> ===================================================================
> >> --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
> >> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> >> @@ -1,11 +1,11 @@
> >>                                    Prior Operation     Subsequent Operation
> >>                                    ---------------  ---------------------------
> >>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> >> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> >> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
> >>  
> >>  Store, e.g., WRITE_ONCE()            Y                                       Y
> >> -Load, e.g., READ_ONCE()              Y                              Y        Y
> >> -Unsuccessful RMW operation           Y                              Y        Y
> >> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> >> +Unsuccessful RMW operation           Y                          Y   Y        Y
> >>  rcu_dereference()                    Y                          Y   Y        Y
> >>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
> >>  Successful *_release()         C        Y  Y    Y     W                      Y
> >> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> >> ===================================================================
> >> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> >> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> >> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
> >>  executed on C before the fence (i.e., those which precede the fence in
> >>  program order).
> >>  
> >> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> >> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> >>  other properties which we discuss later.
> >>  
> >>  
> >> @@ -1138,7 +1138,7 @@ final effect is that even though the two
> >>  program order, it appears that they aren't.
> >>  
> >>  This could not have happened if the local cache had processed the
> >> -incoming stores in FIFO order.  In constrast, other architectures
> >> +incoming stores in FIFO order.  By contrast, other architectures
> >>  maintain at least the appearance of FIFO order.
> >>  
> >>  In practice, this difficulty is solved by inserting a special fence
> >> Index: usb-4.x/tools/memory-model/linux-kernel.def
> >> ===================================================================
> >> --- usb-4.x.orig/tools/memory-model/linux-kernel.def
> >> +++ usb-4.x/tools/memory-model/linux-kernel.def
> >> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
> >>  smp_store_release(X,V) { __store{release}(*X,V); }
> >>  smp_load_acquire(X) __load{acquire}(*X)
> >>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> >> -rcu_dereference(X) __load{deref}(X)
> >> +rcu_dereference(X) __load{once}(X)
> >>  
> >>  // Fences
> >>  smp_mb() { __fence{mb} ; }
> >>
> > 
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Andrea Parri]

On Fri, Feb 23, 2018 at 07:30:13PM -0800, Paul E. McKenney wrote:
> On Sat, Feb 24, 2018 at 12:22:24PM +0900, Akira Yokosawa wrote:
> > On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
> > > On 2018/02/22 2:15, Alan Stern wrote:

[...]

> > >>
> > >> Akira pointed out some typos in the original patch, and he noted that
> > >> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> > >> operations relate to address dependencies.
> > > 
> > > My point was to separate unannotated loads from READ_ONCE(), if the
> > > cheatsheet should concern such accesses as well.
> > > Unsuccessful RMW operations were brought up by Andrea.
> > >
> > 
> > Paul, can you amend above paragraph in the change log to something like:
> > 
> >     Akira pointed out some typos in the original patch, and he noted that
> >     cheatsheet.txt should be updated to indicate READ_ONCE() implies
> >     address dependency, which invited Andrea's observation that it should
> >     also be updated to indicate how unsuccessful RMW operations relate to
> >     address dependencies.
> > 
> > , if Alan and Andrea are OK with the amendment.
> > 
> > Also, please append my Acked-by.
> > 
> > Acked-by: Akira Yokosawa <akiyks@gmail.com>
> 
> I can still amend this, and have added your Acked-by.  If Alan and Andrea
> OK with your change, I will apply that also.

LGTM. Thanks,

  Andrea


> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Alan Stern]

On Sat, 24 Feb 2018, Andrea Parri wrote:

> On Fri, Feb 23, 2018 at 07:30:13PM -0800, Paul E. McKenney wrote:
> > On Sat, Feb 24, 2018 at 12:22:24PM +0900, Akira Yokosawa wrote:
> > > On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
> > > > On 2018/02/22 2:15, Alan Stern wrote:
> 
> [...]
> 
> > > >>
> > > >> Akira pointed out some typos in the original patch, and he noted that
> > > >> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> > > >> operations relate to address dependencies.
> > > > 
> > > > My point was to separate unannotated loads from READ_ONCE(), if the
> > > > cheatsheet should concern such accesses as well.
> > > > Unsuccessful RMW operations were brought up by Andrea.
> > > >
> > > 
> > > Paul, can you amend above paragraph in the change log to something like:
> > > 
> > >     Akira pointed out some typos in the original patch, and he noted that
> > >     cheatsheet.txt should be updated to indicate READ_ONCE() implies
> > >     address dependency, which invited Andrea's observation that it should
> > >     also be updated to indicate how unsuccessful RMW operations relate to
> > >     address dependencies.
> > > 
> > > , if Alan and Andrea are OK with the amendment.
> > > 
> > > Also, please append my Acked-by.
> > > 
> > > Acked-by: Akira Yokosawa <akiyks@gmail.com>
> > 
> > I can still amend this, and have added your Acked-by.  If Alan and Andrea
> > OK with your change, I will apply that also.
> 
> LGTM. Thanks,

Me too.

Alan

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Sat, Feb 24, 2018 at 11:49:20AM -0500, Alan Stern wrote:
> On Sat, 24 Feb 2018, Andrea Parri wrote:
> 
> > On Fri, Feb 23, 2018 at 07:30:13PM -0800, Paul E. McKenney wrote:
> > > On Sat, Feb 24, 2018 at 12:22:24PM +0900, Akira Yokosawa wrote:
> > > > On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
> > > > > On 2018/02/22 2:15, Alan Stern wrote:
> > 
> > [...]
> > 
> > > > >>
> > > > >> Akira pointed out some typos in the original patch, and he noted that
> > > > >> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> > > > >> operations relate to address dependencies.
> > > > > 
> > > > > My point was to separate unannotated loads from READ_ONCE(), if the
> > > > > cheatsheet should concern such accesses as well.
> > > > > Unsuccessful RMW operations were brought up by Andrea.
> > > > >
> > > > 
> > > > Paul, can you amend above paragraph in the change log to something like:
> > > > 
> > > >     Akira pointed out some typos in the original patch, and he noted that
> > > >     cheatsheet.txt should be updated to indicate READ_ONCE() implies
> > > >     address dependency, which invited Andrea's observation that it should
> > > >     also be updated to indicate how unsuccessful RMW operations relate to
> > > >     address dependencies.
> > > > 
> > > > , if Alan and Andrea are OK with the amendment.
> > > > 
> > > > Also, please append my Acked-by.
> > > > 
> > > > Acked-by: Akira Yokosawa <akiyks@gmail.com>
> > > 
> > > I can still amend this, and have added your Acked-by.  If Alan and Andrea
> > > OK with your change, I will apply that also.
> > 
> > LGTM. Thanks,
> 
> Me too.

Very good, how about this for the new version?

							Thanx, Paul

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

commit 21ede43970e50b7397420f17ed08bb02c187e2eb
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Wed Feb 21 12:15:56 2018 -0500

    tools/memory-model: Update: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference
    
    Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
    smp_read_barrier_depends, and lockless_dereference") was accidentally
    merged too early, while it was still in RFC form.  This patch adds in
    the missing pieces.
    
    Akira pointed out some typos in the original patch, and he noted that
    cheatsheet.txt should indicate that READ_ONCE() now implies an address
    dependency.  Andrea suggested documenting the relationship betwwen
    unsuccessful RMW operations and address dependencies.
    
    Andrea pointed out that the macro for rcu_dereference() in linux.def
    should now use the "once" annotation instead of "deref".  He also
    suggested that the comments should mention commit 5a8897cc7631
    ("locking/atomics/alpha: Add smp_read_barrier_depends() to
    _release()/_relaxed() atomics") as an important precursor, and he
    contributed commit cb13b424e986 ("locking/xchg/alpha: Add
    unconditional memory barrier to cmpxchg()"), another prerequisite.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Suggested-by: Akira Yokosawa <akiyks@gmail.com>
    Suggested-by: Andrea Parri <parri.andrea@gmail.com>
    Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
    Acked-by: Andrea Parri <parri.andrea@gmail.com>
    Acked-by: Akira Yokosawa <akiyks@gmail.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
index 04e458acd6d4..956b1ae4aafb 100644
--- a/tools/memory-model/Documentation/cheatsheet.txt
+++ b/tools/memory-model/Documentation/cheatsheet.txt
@@ -1,11 +1,11 @@
                                   Prior Operation     Subsequent Operation
                                   ---------------  ---------------------------
                                C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
-                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
+                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
 
 Store, e.g., WRITE_ONCE()            Y                                       Y
-Load, e.g., READ_ONCE()              Y                              Y        Y
-Unsuccessful RMW operation           Y                              Y        Y
+Load, e.g., READ_ONCE()              Y                          Y   Y        Y
+Unsuccessful RMW operation           Y                          Y   Y        Y
 rcu_dereference()                    Y                          Y   Y        Y
 Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
 Successful *_release()         C        Y  Y    Y     W                      Y
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index dae8b8cb2ad3..889fabef7d83 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -826,7 +826,7 @@ A-cumulative; they only affect the propagation of stores that are
 executed on C before the fence (i.e., those which precede the fence in
 program order).
 
-read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
+read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
 other properties which we discuss later.
 
 
@@ -1138,7 +1138,7 @@ final effect is that even though the two loads really are executed in
 program order, it appears that they aren't.
 
 This could not have happened if the local cache had processed the
-incoming stores in FIFO order.  In constrast, other architectures
+incoming stores in FIFO order.  By contrast, other architectures
 maintain at least the appearance of FIFO order.
 
 In practice, this difficulty is solved by inserting a special fence
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 5dfb9c7f3462..397e4e67e8c8 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
 smp_store_release(X,V) { __store{release}(*X,V); }
 smp_load_acquire(X) __load{acquire}(*X)
 rcu_assign_pointer(X,V) { __store{release}(X,V); }
-rcu_dereference(X) __load{deref}(X)
+rcu_dereference(X) __load{once}(X)
 
 // Fences
 smp_mb() { __fence{mb} ; }

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Akira Yokosawa]

On 2018/02/24 10:08:14 -0800, Paul E. McKenney wrote:
> On Sat, Feb 24, 2018 at 11:49:20AM -0500, Alan Stern wrote:
>> On Sat, 24 Feb 2018, Andrea Parri wrote:
>>
>>> On Fri, Feb 23, 2018 at 07:30:13PM -0800, Paul E. McKenney wrote:
>>>> On Sat, Feb 24, 2018 at 12:22:24PM +0900, Akira Yokosawa wrote:
>>>>> On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
>>>>>> On 2018/02/22 2:15, Alan Stern wrote:
>>>
>>> [...]
>>>
>>>>>>>
>>>>>>> Akira pointed out some typos in the original patch, and he noted that
>>>>>>> cheatsheet.txt should be updated to indicate how unsuccessful RMW
>>>>>>> operations relate to address dependencies.
>>>>>>
>>>>>> My point was to separate unannotated loads from READ_ONCE(), if the
>>>>>> cheatsheet should concern such accesses as well.
>>>>>> Unsuccessful RMW operations were brought up by Andrea.
>>>>>>
>>>>>
>>>>> Paul, can you amend above paragraph in the change log to something like:
>>>>>
>>>>>     Akira pointed out some typos in the original patch, and he noted that
>>>>>     cheatsheet.txt should be updated to indicate READ_ONCE() implies
>>>>>     address dependency, which invited Andrea's observation that it should
>>>>>     also be updated to indicate how unsuccessful RMW operations relate to
>>>>>     address dependencies.
>>>>>
>>>>> , if Alan and Andrea are OK with the amendment.
>>>>>
>>>>> Also, please append my Acked-by.
>>>>>
>>>>> Acked-by: Akira Yokosawa <akiyks@gmail.com>
>>>>
>>>> I can still amend this, and have added your Acked-by.  If Alan and Andrea
>>>> OK with your change, I will apply that also.
>>>
>>> LGTM. Thanks,
>>
>> Me too.
> 
> Very good, how about this for the new version?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit 21ede43970e50b7397420f17ed08bb02c187e2eb
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Wed Feb 21 12:15:56 2018 -0500
> 
>     tools/memory-model: Update: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference
>     
>     Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
>     smp_read_barrier_depends, and lockless_dereference") was accidentally
>     merged too early, while it was still in RFC form.  This patch adds in
>     the missing pieces.
>     
>     Akira pointed out some typos in the original patch, and he noted that
>     cheatsheet.txt should indicate that READ_ONCE() now implies an address
>     dependency.  Andrea suggested documenting the relationship betwwen
>     unsuccessful RMW operations and address dependencies.

Looks good. But I've found a remaining typo in the patch. See below.

>     >     Andrea pointed out that the macro for rcu_dereference() in linux.def
>     should now use the "once" annotation instead of "deref".  He also
>     suggested that the comments should mention commit 5a8897cc7631
>     ("locking/atomics/alpha: Add smp_read_barrier_depends() to
>     _release()/_relaxed() atomics") as an important precursor, and he
>     contributed commit cb13b424e986 ("locking/xchg/alpha: Add
>     unconditional memory barrier to cmpxchg()"), another prerequisite.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Suggested-by: Akira Yokosawa <akiyks@gmail.com>
>     Suggested-by: Andrea Parri <parri.andrea@gmail.com>
>     Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
>     Acked-by: Andrea Parri <parri.andrea@gmail.com>
>     Acked-by: Akira Yokosawa <akiyks@gmail.com>
>     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
> index 04e458acd6d4..956b1ae4aafb 100644
> --- a/tools/memory-model/Documentation/cheatsheet.txt
> +++ b/tools/memory-model/Documentation/cheatsheet.txt
> @@ -1,11 +1,11 @@
>                                    Prior Operation     Subsequent Operation
>                                    ---------------  ---------------------------
>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
>  
>  Store, e.g., WRITE_ONCE()            Y                                       Y
> -Load, e.g., READ_ONCE()              Y                              Y        Y
> -Unsuccessful RMW operation           Y                              Y        Y
> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> +Unsuccessful RMW operation           Y                          Y   Y        Y
>  rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index dae8b8cb2ad3..889fabef7d83 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propagation of stores that are
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
>  
> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have

   rcu_read_lock()

Don't ask why I missed this in the first place...

Paul, can you fix this directly?

        Thanks, Akira
        
>  other properties which we discuss later.
>  
>  
> @@ -1138,7 +1138,7 @@ final effect is that even though the two loads really are executed in
>  program order, it appears that they aren't.
>  
>  This could not have happened if the local cache had processed the
> -incoming stores in FIFO order.  In constrast, other architectures
> +incoming stores in FIFO order.  By contrast, other architectures
>  maintain at least the appearance of FIFO order.
>  
>  In practice, this difficulty is solved by inserting a special fence
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 5dfb9c7f3462..397e4e67e8c8 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -rcu_dereference(X) __load{deref}(X)
> +rcu_dereference(X) __load{once}(X)
>  
>  // Fences
>  smp_mb() { __fence{mb} ; }
> 

Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Paul E. McKenney]

On Sun, Feb 25, 2018 at 07:47:23AM +0900, Akira Yokosawa wrote:
> On 2018/02/24 10:08:14 -0800, Paul E. McKenney wrote:
> > On Sat, Feb 24, 2018 at 11:49:20AM -0500, Alan Stern wrote:
> >> On Sat, 24 Feb 2018, Andrea Parri wrote:
> >>
> >>> On Fri, Feb 23, 2018 at 07:30:13PM -0800, Paul E. McKenney wrote:
> >>>> On Sat, Feb 24, 2018 at 12:22:24PM +0900, Akira Yokosawa wrote:
> >>>>> On 2018/02/22 07:29:02 +0900, Akira Yokosawa wrote:
> >>>>>> On 2018/02/22 2:15, Alan Stern wrote:
> >>>
> >>> [...]
> >>>
> >>>>>>>
> >>>>>>> Akira pointed out some typos in the original patch, and he noted that
> >>>>>>> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> >>>>>>> operations relate to address dependencies.
> >>>>>>
> >>>>>> My point was to separate unannotated loads from READ_ONCE(), if the
> >>>>>> cheatsheet should concern such accesses as well.
> >>>>>> Unsuccessful RMW operations were brought up by Andrea.
> >>>>>>
> >>>>>
> >>>>> Paul, can you amend above paragraph in the change log to something like:
> >>>>>
> >>>>>     Akira pointed out some typos in the original patch, and he noted that
> >>>>>     cheatsheet.txt should be updated to indicate READ_ONCE() implies
> >>>>>     address dependency, which invited Andrea's observation that it should
> >>>>>     also be updated to indicate how unsuccessful RMW operations relate to
> >>>>>     address dependencies.
> >>>>>
> >>>>> , if Alan and Andrea are OK with the amendment.
> >>>>>
> >>>>> Also, please append my Acked-by.
> >>>>>
> >>>>> Acked-by: Akira Yokosawa <akiyks@gmail.com>
> >>>>
> >>>> I can still amend this, and have added your Acked-by.  If Alan and Andrea
> >>>> OK with your change, I will apply that also.
> >>>
> >>> LGTM. Thanks,
> >>
> >> Me too.
> > 
> > Very good, how about this for the new version?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit 21ede43970e50b7397420f17ed08bb02c187e2eb
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Wed Feb 21 12:15:56 2018 -0500
> > 
> >     tools/memory-model: Update: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference
> >     
> >     Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> >     smp_read_barrier_depends, and lockless_dereference") was accidentally
> >     merged too early, while it was still in RFC form.  This patch adds in
> >     the missing pieces.
> >     
> >     Akira pointed out some typos in the original patch, and he noted that
> >     cheatsheet.txt should indicate that READ_ONCE() now implies an address
> >     dependency.  Andrea suggested documenting the relationship betwwen
> >     unsuccessful RMW operations and address dependencies.
> 
> Looks good. But I've found a remaining typo in the patch. See below.
> 
> >     >     Andrea pointed out that the macro for rcu_dereference() in linux.def
> >     should now use the "once" annotation instead of "deref".  He also
> >     suggested that the comments should mention commit 5a8897cc7631
> >     ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> >     _release()/_relaxed() atomics") as an important precursor, and he
> >     contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> >     unconditional memory barrier to cmpxchg()"), another prerequisite.
> >     
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> >     Suggested-by: Andrea Parri <parri.andrea@gmail.com>
> >     Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
> >     Acked-by: Andrea Parri <parri.andrea@gmail.com>
> >     Acked-by: Akira Yokosawa <akiyks@gmail.com>
> >     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
> > index 04e458acd6d4..956b1ae4aafb 100644
> > --- a/tools/memory-model/Documentation/cheatsheet.txt
> > +++ b/tools/memory-model/Documentation/cheatsheet.txt
> > @@ -1,11 +1,11 @@
> >                                    Prior Operation     Subsequent Operation
> >                                    ---------------  ---------------------------
> >                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> > -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> > +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
> >  
> >  Store, e.g., WRITE_ONCE()            Y                                       Y
> > -Load, e.g., READ_ONCE()              Y                              Y        Y
> > -Unsuccessful RMW operation           Y                              Y        Y
> > +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> > +Unsuccessful RMW operation           Y                          Y   Y        Y
> >  rcu_dereference()                    Y                          Y   Y        Y
> >  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
> >  Successful *_release()         C        Y  Y    Y     W                      Y
> > diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> > index dae8b8cb2ad3..889fabef7d83 100644
> > --- a/tools/memory-model/Documentation/explanation.txt
> > +++ b/tools/memory-model/Documentation/explanation.txt
> > @@ -826,7 +826,7 @@ A-cumulative; they only affect the propagation of stores that are
> >  executed on C before the fence (i.e., those which precede the fence in
> >  program order).
> >  
> > -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> > +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> 
>    rcu_read_lock()
> 
> Don't ask why I missed this in the first place...
> 
> Paul, can you fix this directly?

Done!

								Thanx, Paul

>         Thanks, Akira
>         
> >  other properties which we discuss later.
> >  
> >  
> > @@ -1138,7 +1138,7 @@ final effect is that even though the two loads really are executed in
> >  program order, it appears that they aren't.
> >  
> >  This could not have happened if the local cache had processed the
> > -incoming stores in FIFO order.  In constrast, other architectures
> > +incoming stores in FIFO order.  By contrast, other architectures
> >  maintain at least the appearance of FIFO order.
> >  
> >  In practice, this difficulty is solved by inserting a special fence
> > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > index 5dfb9c7f3462..397e4e67e8c8 100644
> > --- a/tools/memory-model/linux-kernel.def
> > +++ b/tools/memory-model/linux-kernel.def
> > @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
> >  smp_store_release(X,V) { __store{release}(*X,V); }
> >  smp_load_acquire(X) __load{acquire}(*X)
> >  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> > -rcu_dereference(X) __load{deref}(X)
> > +rcu_dereference(X) __load{once}(X)
> >  
> >  // Fences
> >  smp_mb() { __fence{mb} ; }
> > 
>