* [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes
@ 2018-02-20 23:24 Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 01/12] tools/memory-model: Clarify the origin/scope of the tool name Paul E. McKenney
` (11 more replies)
0 siblings, 12 replies; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:24 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov
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 punctuation errors in litmus-tests/README.
6. Add Akira Yokosawa as an LKMM reviewer.
7. Cross-reference tools/memory-model from memory-barriers.txt,
courtesy of Andrea Parri and Akira Yokosawa.
8. Fix description of data dependency barriers, courtesy of
Nikolay Borisov.
9. Add required herd7 version to README file.
10. Add a S lock-based external-view litmus test, courtesy of Alan
Stern.
11. Convert underscores to hyphens in .bell and .cat files for
consistency with typical cat-language code.
12. Remove rb-dep, smp_read_barrier_depends, and lockless_dereference,
which reflect recent Linux-kernel changes, courtesy of
Alan Stern.
Changes since v1:
o Applied feedback from v1 posting.
o Squashing patches together, as promised in v1.
o Added patches 7-10 and 12.
Thanx, Paul
------------------------------------------------------------------------
/tools/memory-model/MAINTAINERS | 15 -
b/Documentation/memory-barriers.txt | 8
b/MAINTAINERS | 18 ++
b/tools/memory-model/Documentation/cheatsheet.txt | 3
b/tools/memory-model/Documentation/explanation.txt | 81 +++++-----
b/tools/memory-model/MAINTAINERS | 2
b/tools/memory-model/README | 17 +-
b/tools/memory-model/linux-kernel.bell | 9 -
b/tools/memory-model/linux-kernel.cat | 15 -
b/tools/memory-model/linux-kernel.def | 8
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+pooncelock+pooncelock+pombonce.litmus | 41 +++++
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 +
40 files changed, 380 insertions(+), 88 deletions(-)
^ permalink raw reply [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 01/12] tools/memory-model: Clarify the origin/scope of the tool name
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:39 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 02/12] MAINTAINERS: Add the Memory Consistency Model subsystem Paul E. McKenney
` (10 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 02/12] MAINTAINERS: Add the Memory Consistency Model subsystem
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 01/12] tools/memory-model: Clarify the origin/scope of the tool name Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:39 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 03/12] MAINTAINERS: List file memory-barriers.txt within the LKMM entry Paul E. McKenney
` (9 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
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..50bcedbdca86 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 (LKMM)
+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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 03/12] MAINTAINERS: List file memory-barriers.txt within the LKMM entry
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 01/12] tools/memory-model: Clarify the origin/scope of the tool name Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 02/12] MAINTAINERS: Add the Memory Consistency Model subsystem Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:40 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 04/12] EXP litmus_tests: Add comments explaining tests' purposes Paul E. McKenney
` (8 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
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 50bcedbdca86..674b35c3f28e 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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 04/12] EXP litmus_tests: Add comments explaining tests' purposes
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (2 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 03/12] MAINTAINERS: List file memory-barriers.txt within the LKMM entry Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:40 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 05/12] README: Fix a couple of punctuation errors Paul E. McKenney
` (7 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
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..4b54dd6a6cd9 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: Sometimes
+ *
+ * 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..10a2aa04cd07 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: Sometimes
+ *
+ * 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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 05/12] README: Fix a couple of punctuation errors
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (3 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 04/12] EXP litmus_tests: Add comments explaining tests' purposes Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:41 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 06/12] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer Paul E. McKenney
` (6 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 06/12] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (4 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 05/12] README: Fix a couple of punctuation errors Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:41 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 07/12] Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/" Paul E. McKenney
` (5 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 07/12] Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/"
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (5 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 06/12] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:42 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 08/12] memory-barriers: Fix description of data dependency barriers Paul E. McKenney
` (4 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
Paul E. McKenney
From: Andrea Parri <parri.andrea@gmail.com>
A memory consistency model is now available for the Linux kernel [1],
which "can (roughly speaking) be thought of as an automated version of
memory-barriers.txt" and which is (in turn) "accompanied by extensive
documentation on its use and its design".
Inform the (occasional) reader of memory-barriers.txt of these
developments.
[1] https://marc.info/?l=linux-kernel&m=151687290114799&w=2
Co-developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-developed-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
Documentation/memory-barriers.txt | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 479ecec80593..74ad222d11ed 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -14,7 +14,11 @@ DISCLAIMER
This document is not a specification; it is intentionally (for the sake of
brevity) and unintentionally (due to being human) incomplete. This document is
meant as a guide to using the various memory barriers provided by Linux, but
-in case of any doubt (and there are many) please ask.
+in case of any doubt (and there are many) please ask. Some doubts may be
+resolved by referring to the formal memory consistency model and related
+documentation at tools/memory-model/. Nevertheless, even this memory
+model should be viewed as the collective opinion of its maintainers rather
+than as an infallible oracle.
To repeat, this document is not a specification of what Linux expects from
hardware.
--
2.5.2
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 08/12] memory-barriers: Fix description of data dependency barriers
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (6 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 07/12] Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/" Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:42 ` [tip:locking/core] " tip-bot for Nikolay Borisov
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file Paul E. McKenney
` (3 subsequent siblings)
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
Paul E. McKenney
From: Nikolay Borisov <nborisov@suse.com>
In the description of data dependency barriers the words 'before' is
used erroneously. Since such barrier order dependent loads one after
the other. So substitute 'before' with 'after'.
Signed-off-by: Nikolay Borisov <nborisov@suse.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
Documentation/memory-barriers.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 74ad222d11ed..0d83333b84a9 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -400,7 +400,7 @@ Memory barriers come in four basic varieties:
where two loads are performed such that the second depends on the result
of the first (eg: the first load retrieves the address to which the second
load will be directed), a data dependency barrier would be required to
- make sure that the target of the second load is updated before the address
+ make sure that the target of the second load is updated after the address
obtained by the first load is accessed.
A data dependency barrier is a partial ordering on interdependent loads
--
2.5.2
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (7 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 08/12] memory-barriers: Fix description of data dependency barriers Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-21 15:10 ` [PATCH RFC tools/lkmm 09/12] " Alan Stern
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test Paul E. McKenney
` (2 subsequent siblings)
11 siblings, 2 replies; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
Paul E. McKenney
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>
---
tools/memory-model/README | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
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
--
2.5.2
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (8 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Alan Stern
` (2 more replies)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 11/12] tools/memory-model: Convert underscores to hyphens Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 12/12] tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference Paul E. McKenney
11 siblings, 3 replies; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
Paul E. McKenney
From: Alan Stern <stern@rowland.harvard.edu>
This commit adds a litmus test in which P0() and P1() form a lock-based S
litmus test, with the addition of P2(), which observes P0()'s and P1()'s
accesses with a full memory barrier but without the lock. This litmus
test asks whether writes carried out by two different processes under the
same lock will be seen in order by a third process not holding that lock.
The answer to this question is "yes" for all architectures supporting
the Linux kernel, but is "no" according to the current version of LKMM.
A patch to LKMM is under development.
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
.../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
1 file changed, 41 insertions(+)
create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
new file mode 100644
index 000000000000..7a39a0aaa976
--- /dev/null
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -0,0 +1,41 @@
+C ISA2+pooncelock+pooncelock+pombonce.litmus
+
+(*
+ * Result: Sometimes
+ *
+ * This test shows that the ordering provided by a lock-protected S
+ * litmus test (P0() and P1()) are not visible to external process P2().
+ * This is likely to change soon.
+ *)
+
+{}
+
+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)
--
2.5.2
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 11/12] tools/memory-model: Convert underscores to hyphens
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (9 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:44 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 12/12] tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference Paul E. McKenney
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
Paul E. McKenney
Typical cat-language code uses hyphens for word separators in
identifiers, but several LKMM identifiers use underscores instead.
This commit therefore converts underscores to hyphens in the .bell-
and .cat-file identifiers corresponding to smp_mb__before_atomic(),
smp_mb__after_atomic(), and smp_mb__after_spinlock().
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
tools/memory-model/linux-kernel.bell | 6 +++---
tools/memory-model/linux-kernel.cat | 6 +++---
tools/memory-model/linux-kernel.def | 6 +++---
3 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index b984bbda01a5..18885ad15de9 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -28,9 +28,9 @@ 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*) ||
- 'after_atomic (*smp_mb__after_atomic*) ||
- 'after_spinlock (*smp_mb__after_spinlock*)
+ '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 *)
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index babe2b3b0bb3..f0d27f813ec2 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -29,9 +29,9 @@ 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])
+ ([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 a397387f77cc..f5a1eb04cb64 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)
--
2.5.2
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [PATCH RFC tools/lkmm 12/12] tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
` (10 preceding siblings ...)
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 11/12] tools/memory-model: Convert underscores to hyphens Paul E. McKenney
@ 2018-02-20 23:25 ` Paul E. McKenney
2018-02-21 10:45 ` [tip:locking/core] " tip-bot for Alan Stern
11 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-20 23:25 UTC (permalink / raw)
To: linux-kernel, linux-arch
Cc: mingo, stern, parri.andrea, will.deacon, peterz, boqun.feng,
npiggin, dhowells, j.alglave, luc.maranget, akiyks, nborisov,
Paul E. McKenney
From: Alan Stern <stern@rowland.harvard.edu>
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>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
tools/memory-model/Documentation/cheatsheet.txt | 3 +-
tools/memory-model/Documentation/explanation.txt | 81 +++++++++++++-----------
tools/memory-model/linux-kernel.bell | 1 -
tools/memory-model/linux-kernel.cat | 7 +-
tools/memory-model/linux-kernel.def | 2 -
5 files changed, 46 insertions(+), 48 deletions(-)
diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
index 1917712bce99..04e458acd6d4 100644
--- a/tools/memory-model/Documentation/cheatsheet.txt
+++ b/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
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 867e0ea69b6d..dae8b8cb2ad3 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/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 Model
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 propagation of stores that are
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 earlier but discussed in the next
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 subsystem to load a value from
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 local cache had processed the
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. Thus, if the code was changed to:
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. Since the CPU doesn't ever read
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
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 18885ad15de9..432c7cf71b23 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -24,7 +24,6 @@ instructions RMW[{'once,'acquire,'release}]
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*) ||
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index f0d27f813ec2..df97db03b6c2 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/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
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index f5a1eb04cb64..5dfb9c7f3462 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/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} ; }
--
2.5.2
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] tools/memory-model: Clarify the origin/scope of the tool name
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 01/12] tools/memory-model: Clarify the origin/scope of the tool name Paul E. McKenney
@ 2018-02-21 10:39 ` tip-bot for Andrea Parri
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Andrea Parri @ 2018-02-21 10:39 UTC (permalink / raw)
To: linux-tip-commits
Cc: mingo, paulmck, peterz, torvalds, stern, tglx, hpa, linux-kernel,
will.deacon, parri.andrea
Commit-ID: 48d44d4e8a583c66d9f376e18c1a1fcc445f4b64
Gitweb: https://git.kernel.org/tip/48d44d4e8a583c66d9f376e18c1a1fcc445f4b64
Author: Andrea Parri <parri.andrea@gmail.com>
AuthorDate: Tue, 20 Feb 2018 15:25:01 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:12 +0100
tools/memory-model: Clarify the origin/scope of the tool name
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>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Link: http://lkml.kernel.org/r/1519169112-20593-1-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
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 711cbe7..db3bd3f 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 43ba494..91414a4 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 5711250..b984bbd 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 15b7a5d..babe2b3 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.
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] MAINTAINERS: Add the Memory Consistency Model subsystem
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 02/12] MAINTAINERS: Add the Memory Consistency Model subsystem Paul E. McKenney
@ 2018-02-21 10:39 ` tip-bot for Andrea Parri
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Andrea Parri @ 2018-02-21 10:39 UTC (permalink / raw)
To: linux-tip-commits
Cc: paulmck, hpa, linux-kernel, torvalds, mingo, peterz, stern,
parri.andrea, will.deacon, tglx
Commit-ID: e7d74c9f900a12ea0bd5cabb3be142441530e24e
Gitweb: https://git.kernel.org/tip/e7d74c9f900a12ea0bd5cabb3be142441530e24e
Author: Andrea Parri <parri.andrea@gmail.com>
AuthorDate: Tue, 20 Feb 2018 15:25:02 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:12 +0100
MAINTAINERS: Add the Memory Consistency Model subsystem
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>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Link: http://lkml.kernel.org/r/1519169112-20593-2-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
MAINTAINERS | 16 ++++++++++++++++
tools/memory-model/MAINTAINERS | 15 ---------------
2 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/MAINTAINERS b/MAINTAINERS
index 9a7f76e..654c6c6 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8148,6 +8148,22 @@ M: Kees Cook <keescook@chromium.org>
S: Maintained
F: drivers/misc/lkdtm*
+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>
+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 db3bd3f..0000000
--- 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/
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] MAINTAINERS: List file memory-barriers.txt within the LKMM entry
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 03/12] MAINTAINERS: List file memory-barriers.txt within the LKMM entry Paul E. McKenney
@ 2018-02-21 10:40 ` tip-bot for Andrea Parri
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Andrea Parri @ 2018-02-21 10:40 UTC (permalink / raw)
To: linux-tip-commits
Cc: paulmck, peterz, linux-kernel, hpa, mingo, will.deacon, tglx,
torvalds, parri.andrea
Commit-ID: ea52d698c1ed0c4555656de0dd1f7ac5866f89e1
Gitweb: https://git.kernel.org/tip/ea52d698c1ed0c4555656de0dd1f7ac5866f89e1
Author: Andrea Parri <parri.andrea@gmail.com>
AuthorDate: Tue, 20 Feb 2018 15:25:03 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:13 +0100
MAINTAINERS: List file memory-barriers.txt within the LKMM entry
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>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: stern@rowland.harvard.edu
Link: http://lkml.kernel.org/r/1519169112-20593-3-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
MAINTAINERS | 1 +
1 file changed, 1 insertion(+)
diff --git a/MAINTAINERS b/MAINTAINERS
index 654c6c6..42da350 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8163,6 +8163,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>
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] EXP litmus_tests: Add comments explaining tests' purposes
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 04/12] EXP litmus_tests: Add comments explaining tests' purposes Paul E. McKenney
@ 2018-02-21 10:40 ` tip-bot for Paul E. McKenney
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Paul E. McKenney @ 2018-02-21 10:40 UTC (permalink / raw)
To: linux-tip-commits
Cc: hpa, torvalds, linux-kernel, paulmck, tglx, mingo, peterz
Commit-ID: 8f32543b61d7daeddb5b64c80b5ad5f05cc97722
Gitweb: https://git.kernel.org/tip/8f32543b61d7daeddb5b64c80b5ad5f05cc97722
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
AuthorDate: Tue, 20 Feb 2018 15:25:04 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:13 +0100
EXP litmus_tests: Add comments explaining tests' purposes
This commit adds comments to the litmus tests summarizing what these
tests are intended to demonstrate.
[ paulmck: Apply Andrea's and Alan's feedback. ]
Suggested-by: Ingo Molnar <mingo@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-4-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
.../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 5b83d57..967f9f2 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 fab91c1..4635739 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 6a35ec2..bb068c9 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 32a96b8..0d9f0a9 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 7eba2c6..50d5db9 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 b0556c6..4b54dd6 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: Sometimes
+ *
+ * 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 9a1a233..b321aa6 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 235195e..025b046 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 dd5ac3a..de67082 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 47bd613..07b9904 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 a5cdf02..74c49cb 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 1a2fe58..97731b4 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 5fe6f1e..712a4fcd 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 46e1ac7b..b2b60b8 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 0b00cc7..d52c684 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 90d011c..72c9276 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 604ad41..c078f38 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 e69b9e3..a0e884a 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 f7a12e0..5386f12 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 d0d541c..8c9c2f8 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 1d292d0..c533502 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 b76caa5..74b874f 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 c1797e03..10d5507 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 f5e7c92..6a2bc12 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 e3d0018..97fcbff 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 9c2cb53..415248f 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 c9a1f1a..10a2aa0 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: Sometimes
+ *
+ * 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 25409a0..a20fc3f 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)
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] README: Fix a couple of punctuation errors
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 05/12] README: Fix a couple of punctuation errors Paul E. McKenney
@ 2018-02-21 10:41 ` tip-bot for Paul E. McKenney
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Paul E. McKenney @ 2018-02-21 10:41 UTC (permalink / raw)
To: linux-tip-commits
Cc: torvalds, linux-kernel, hpa, tglx, paulmck, mingo, peterz
Commit-ID: 62155147048f6c811b82cbb53bee246aee083774
Gitweb: https://git.kernel.org/tip/62155147048f6c811b82cbb53bee246aee083774
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
AuthorDate: Tue, 20 Feb 2018 15:25:05 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:14 +0100
README: Fix a couple of punctuation errors
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-5-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
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 9a3bb59..dca7d823 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()
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 06/12] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer Paul E. McKenney
@ 2018-02-21 10:41 ` tip-bot for Paul E. McKenney
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Paul E. McKenney @ 2018-02-21 10:41 UTC (permalink / raw)
To: linux-tip-commits
Cc: tglx, linux-kernel, hpa, peterz, mingo, torvalds, paulmck
Commit-ID: 65b65f8e8b941785b0a08cf24ffd7084c8df327c
Gitweb: https://git.kernel.org/tip/65b65f8e8b941785b0a08cf24ffd7084c8df327c
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
AuthorDate: Tue, 20 Feb 2018 15:25:06 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:14 +0100
MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-6-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
MAINTAINERS | 1 +
1 file changed, 1 insertion(+)
diff --git a/MAINTAINERS b/MAINTAINERS
index 42da350..1dd9cc2 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -8159,6 +8159,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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/"
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 07/12] Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/" Paul E. McKenney
@ 2018-02-21 10:42 ` tip-bot for Andrea Parri
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Andrea Parri @ 2018-02-21 10:42 UTC (permalink / raw)
To: linux-tip-commits
Cc: mingo, akiyks, hpa, parri.andrea, peterz, linux-kernel, paulmck,
torvalds, tglx
Commit-ID: 621df431b0ac931e318679f54047c47eb23cfdd2
Gitweb: https://git.kernel.org/tip/621df431b0ac931e318679f54047c47eb23cfdd2
Author: Andrea Parri <parri.andrea@gmail.com>
AuthorDate: Tue, 20 Feb 2018 15:25:07 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:14 +0100
Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/"
A memory consistency model is now available for the Linux kernel [1],
which "can (roughly speaking) be thought of as an automated version of
memory-barriers.txt" and which is (in turn) "accompanied by extensive
documentation on its use and its design".
Inform the (occasional) reader of memory-barriers.txt of these
developments.
[1] https://marc.info/?l=linux-kernel&m=151687290114799&w=2
Co-developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-developed-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-7-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
Documentation/memory-barriers.txt | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index a863009..a37d3af 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -14,7 +14,11 @@ DISCLAIMER
This document is not a specification; it is intentionally (for the sake of
brevity) and unintentionally (due to being human) incomplete. This document is
meant as a guide to using the various memory barriers provided by Linux, but
-in case of any doubt (and there are many) please ask.
+in case of any doubt (and there are many) please ask. Some doubts may be
+resolved by referring to the formal memory consistency model and related
+documentation at tools/memory-model/. Nevertheless, even this memory
+model should be viewed as the collective opinion of its maintainers rather
+than as an infallible oracle.
To repeat, this document is not a specification of what Linux expects from
hardware.
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] memory-barriers: Fix description of data dependency barriers
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 08/12] memory-barriers: Fix description of data dependency barriers Paul E. McKenney
@ 2018-02-21 10:42 ` tip-bot for Nikolay Borisov
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Nikolay Borisov @ 2018-02-21 10:42 UTC (permalink / raw)
To: linux-tip-commits
Cc: mingo, torvalds, linux-kernel, paulmck, peterz, hpa, nborisov, tglx
Commit-ID: 51de78892b1294d1521c41226a5ef215a910c25f
Gitweb: https://git.kernel.org/tip/51de78892b1294d1521c41226a5ef215a910c25f
Author: Nikolay Borisov <nborisov@suse.com>
AuthorDate: Tue, 20 Feb 2018 15:25:08 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:14 +0100
memory-barriers: Fix description of data dependency barriers
In the description of data dependency barriers the words 'before' is
used erroneously. Since such barrier order dependent loads one after
the other. So substitute 'before' with 'after'.
Signed-off-by: Nikolay Borisov <nborisov@suse.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-8-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
Documentation/memory-barriers.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index a37d3af..da6525b 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -403,7 +403,7 @@ Memory barriers come in four basic varieties:
where two loads are performed such that the second depends on the result
of the first (eg: the first load retrieves the address to which the second
load will be directed), a data dependency barrier would be required to
- make sure that the target of the second load is updated before the address
+ make sure that the target of the second load is updated after the address
obtained by the first load is accessed.
A data dependency barrier is a partial ordering on interdependent loads
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] tools/memory-model: Add required herd7 version to README file
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file Paul E. McKenney
@ 2018-02-21 10:43 ` tip-bot for Paul E. McKenney
2018-02-21 15:10 ` [PATCH RFC tools/lkmm 09/12] " Alan Stern
1 sibling, 0 replies; 46+ messages in thread
From: tip-bot for Paul E. McKenney @ 2018-02-21 10:43 UTC (permalink / raw)
To: linux-tip-commits
Cc: akiyks, mingo, hpa, tglx, paulmck, torvalds, linux-kernel, peterz
Commit-ID: 8f7f2fbd00898deaf01e05a00095411811befd64
Gitweb: https://git.kernel.org/tip/8f7f2fbd00898deaf01e05a00095411811befd64
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
AuthorDate: Tue, 20 Feb 2018 15:25:09 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:15 +0100
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>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-9-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
tools/memory-model/README | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/tools/memory-model/README b/tools/memory-model/README
index 91414a4..ea950c5 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
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test Paul E. McKenney
@ 2018-02-21 10:43 ` tip-bot for Alan Stern
2018-02-21 15:09 ` [PATCH RFC tools/lkmm 10/12] " Alan Stern
2018-02-22 3:23 ` Boqun Feng
2 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Alan Stern @ 2018-02-21 10:43 UTC (permalink / raw)
To: linux-tip-commits
Cc: paulmck, hpa, torvalds, tglx, peterz, stern, mingo, linux-kernel
Commit-ID: 556bb7d252ae42d4653557325670e665087c38ad
Gitweb: https://git.kernel.org/tip/556bb7d252ae42d4653557325670e665087c38ad
Author: Alan Stern <stern@rowland.harvard.edu>
AuthorDate: Tue, 20 Feb 2018 15:25:10 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:15 +0100
tools/memory-model: Add a S lock-based external-view litmus test
This commit adds a litmus test in which P0() and P1() form a lock-based S
litmus test, with the addition of P2(), which observes P0()'s and P1()'s
accesses with a full memory barrier but without the lock. This litmus
test asks whether writes carried out by two different processes under the
same lock will be seen in order by a third process not holding that lock.
The answer to this question is "yes" for all architectures supporting
the Linux kernel, but is "no" according to the current version of LKMM.
A patch to LKMM is under development.
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-10-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
...ce.litmus => ISA2+pooncelock+pooncelock+pombonce.litmus} | 13 +++++++------
1 file changed, 7 insertions(+), 6 deletions(-)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
similarity index 55%
copy from tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
copy to tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
index 10a2aa0..7a39a0a 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -1,11 +1,11 @@
-C Z6.0+pooncelock+pooncelock+pombonce
+C ISA2+pooncelock+pooncelock+pombonce.litmus
(*
* Result: Sometimes
*
- * 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.
+ * This test shows that the ordering provided by a lock-protected S
+ * litmus test (P0() and P1()) are not visible to external process P2().
+ * This is likely to change soon.
*)
{}
@@ -31,10 +31,11 @@ P1(int *y, int *z, spinlock_t *mylock)
P2(int *x, int *z)
{
int r1;
+ int r2;
- WRITE_ONCE(*z, 2);
+ r2 = READ_ONCE(*z);
smp_mb();
r1 = READ_ONCE(*x);
}
-exists (1:r0=1 /\ z=2 /\ 2:r1=0)
+exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] tools/memory-model: Convert underscores to hyphens
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 11/12] tools/memory-model: Convert underscores to hyphens Paul E. McKenney
@ 2018-02-21 10:44 ` tip-bot for Paul E. McKenney
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Paul E. McKenney @ 2018-02-21 10:44 UTC (permalink / raw)
To: linux-tip-commits
Cc: hpa, paulmck, tglx, mingo, linux-kernel, torvalds, peterz
Commit-ID: cac79a39f200ef73ae7fc8a429ce2859ebb118d9
Gitweb: https://git.kernel.org/tip/cac79a39f200ef73ae7fc8a429ce2859ebb118d9
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
AuthorDate: Tue, 20 Feb 2018 15:25:11 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:15 +0100
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 underscores to hyphens in the .bell-
and .cat-file identifiers corresponding to smp_mb__before_atomic(),
smp_mb__after_atomic(), and smp_mb__after_spinlock().
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-11-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
tools/memory-model/linux-kernel.bell | 6 +++---
tools/memory-model/linux-kernel.cat | 6 +++---
tools/memory-model/linux-kernel.def | 6 +++---
3 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index b984bbd..18885ad 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -28,9 +28,9 @@ 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*) ||
- 'after_atomic (*smp_mb__after_atomic*) ||
- 'after_spinlock (*smp_mb__after_spinlock*)
+ '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 *)
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index babe2b3..f0d27f8 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -29,9 +29,9 @@ 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])
+ ([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 a397387..f5a1eb0 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)
^ permalink raw reply related [flat|nested] 46+ messages in thread
* [tip:locking/core] tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 12/12] tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference Paul E. McKenney
@ 2018-02-21 10:45 ` tip-bot for Alan Stern
0 siblings, 0 replies; 46+ messages in thread
From: tip-bot for Alan Stern @ 2018-02-21 10:45 UTC (permalink / raw)
To: linux-tip-commits
Cc: torvalds, hpa, tglx, peterz, mingo, linux-kernel, stern, paulmck
Commit-ID: bf28ae5627442355dbb8d99238da4fb95c2dd4ec
Gitweb: https://git.kernel.org/tip/bf28ae5627442355dbb8d99238da4fb95c2dd4ec
Author: Alan Stern <stern@rowland.harvard.edu>
AuthorDate: Tue, 20 Feb 2018 15:25:12 -0800
Committer: Ingo Molnar <mingo@kernel.org>
CommitDate: Wed, 21 Feb 2018 09:58:16 +0100
tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference
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>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: nborisov@suse.com
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/1519169112-20593-12-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
---
tools/memory-model/Documentation/cheatsheet.txt | 3 +-
tools/memory-model/Documentation/explanation.txt | 81 +++++++++++++-----------
tools/memory-model/linux-kernel.bell | 1 -
tools/memory-model/linux-kernel.cat | 7 +-
tools/memory-model/linux-kernel.def | 2 -
5 files changed, 46 insertions(+), 48 deletions(-)
diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
index 1917712..04e458a 100644
--- a/tools/memory-model/Documentation/cheatsheet.txt
+++ b/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
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 867e0ea..dae8b8c 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/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 Model
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 propagation of stores that are
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 earlier but discussed in the next
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 subsystem to load a value from
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 local cache had processed the
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. Thus, if the code was changed to:
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. Since the CPU doesn't ever read
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
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 18885ad..432c7cf 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -24,7 +24,6 @@ instructions RMW[{'once,'acquire,'release}]
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*) ||
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index f0d27f8..df97db0 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/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
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index f5a1eb0..5dfb9c7 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/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} ; }
^ permalink raw reply related [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Alan Stern
@ 2018-02-21 15:09 ` Alan Stern
2018-02-21 16:12 ` Paul E. McKenney
2018-02-22 3:23 ` Boqun Feng
2 siblings, 1 reply; 46+ messages in thread
From: Alan Stern @ 2018-02-21 15:09 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> From: Alan Stern <stern@rowland.harvard.edu>
>
> This commit adds a litmus test in which P0() and P1() form a lock-based S
> litmus test, with the addition of P2(), which observes P0()'s and P1()'s
Why do you call this an "S" litmus test? Isn't ISA2 a better
description?
> accesses with a full memory barrier but without the lock. This litmus
> test asks whether writes carried out by two different processes under the
> same lock will be seen in order by a third process not holding that lock.
> The answer to this question is "yes" for all architectures supporting
> the Linux kernel, but is "no" according to the current version of LKMM.
>
> A patch to LKMM is under development.
>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> ---
> .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> 1 file changed, 41 insertions(+)
> create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
Aren't these tests supposed to be described in litmus-tests/README?
> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> new file mode 100644
> index 000000000000..7a39a0aaa976
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -0,0 +1,41 @@
> +C ISA2+pooncelock+pooncelock+pombonce.litmus
> +
> +(*
> + * Result: Sometimes
> + *
> + * This test shows that the ordering provided by a lock-protected S
> + * litmus test (P0() and P1()) are not visible to external process P2().
> + * This is likely to change soon.
That last line may be premature. We haven't reached any consensus on
how RISC-V will handle this. If RISC-V allows the test then the memory
model can't forbid it.
Alan
> + *)
> +
> +{}
> +
> +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)
>
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Paul E. McKenney
@ 2018-02-21 15:10 ` Alan Stern
2018-02-21 16:15 ` Paul E. McKenney
1 sibling, 1 reply; 46+ messages in thread
From: Alan Stern @ 2018-02-21 15:10 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> 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>
> ---
> tools/memory-model/README | 3 ++-
> 1 file changed, 2 insertions(+), 1 deletion(-)
>
> 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
The text immediately below this mentions the Docker image and gentoo
package. Aren't they both seriously out of date at this point? In
which case, shouldn't we remove them from the README?
Alan
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 15:09 ` [PATCH RFC tools/lkmm 10/12] " Alan Stern
@ 2018-02-21 16:12 ` Paul E. McKenney
2018-02-21 16:50 ` Alan Stern
0 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-21 16:12 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> On Tue, 20 Feb 2018, Paul E. McKenney wrote:
>
> > From: Alan Stern <stern@rowland.harvard.edu>
> >
> > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
>
> Why do you call this an "S" litmus test? Isn't ISA2 a better
> description?
Indeed, the name of the test is in fact ISA2.
> > accesses with a full memory barrier but without the lock. This litmus
> > test asks whether writes carried out by two different processes under the
> > same lock will be seen in order by a third process not holding that lock.
> > The answer to this question is "yes" for all architectures supporting
> > the Linux kernel, but is "no" according to the current version of LKMM.
> >
> > A patch to LKMM is under development.
> >
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > ---
> > .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> > 1 file changed, 41 insertions(+)
> > create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
>
> Aren't these tests supposed to be described in litmus-tests/README?
>
> > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > new file mode 100644
> > index 000000000000..7a39a0aaa976
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -0,0 +1,41 @@
> > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This test shows that the ordering provided by a lock-protected S
> > + * litmus test (P0() and P1()) are not visible to external process P2().
> > + * This is likely to change soon.
>
> That last line may be premature. We haven't reached any consensus on
> how RISC-V will handle this. If RISC-V allows the test then the memory
> model can't forbid it.
Agreed. How about this? If the RISC-V question is answered by the
end of next week, I update accordingly. If not, I update the comment
to give the details.
Hey, at least having the memory model go in at about the same time as
a new architecture is giving us good practice! ;-)
Thanx, Paul
> Alan
>
> > + *)
> > +
> > +{}
> > +
> > +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)
> >
>
>
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file
2018-02-21 15:10 ` [PATCH RFC tools/lkmm 09/12] " Alan Stern
@ 2018-02-21 16:15 ` Paul E. McKenney
2018-02-21 16:51 ` Alan Stern
0 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-21 16:15 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, Feb 21, 2018 at 10:10:52AM -0500, Alan Stern wrote:
> On Tue, 20 Feb 2018, Paul E. McKenney wrote:
>
> > 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>
> > ---
> > tools/memory-model/README | 3 ++-
> > 1 file changed, 2 insertions(+), 1 deletion(-)
> >
> > 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
>
> The text immediately below this mentions the Docker image and gentoo
> package. Aren't they both seriously out of date at this point? In
> which case, shouldn't we remove them from the README?
Agreed, we should. How about the following?
Thanx, Paul
------------------------------------------------------------------------
commit b59fd89b465f0bfbfe06bf47e22c0cf160aef66b
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date: Wed Feb 21 08:13:48 2018 -0800
tools/memory-model: Remove mention of docker/gentoo image
Because the docker and gentoo images haven't been updated in quite some
time, they are likely to provide more confusion than help. This commit
therefore removes mention of them from the README file.
Reported-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/tools/memory-model/README b/tools/memory-model/README
index ea950c566ffd..0b3a5f3c9ccd 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -27,21 +27,6 @@ separately:
See "herdtools7/INSTALL.md" for installation instructions.
-Alternatively, Abhishek Bhardwaj has kindly provided a Docker image
-of these tools at "abhishek40/memory-model". Abhishek suggests the
-following commands to install and use this image:
-
- - Users should install Docker for their distribution.
- - docker run -itd abhishek40/memory-model
- - docker attach <id-emitted-from-the-previous-command>
-
-Gentoo users might wish to make use of Patrick McLean's package:
-
- https://gitweb.gentoo.org/repo/gentoo.git/tree/dev-util/herdtools7
-
-These packages may not be up-to-date with respect to the GitHub
-repository.
-
==================
BASIC USAGE: HERD7
^ permalink raw reply related [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 16:12 ` Paul E. McKenney
@ 2018-02-21 16:50 ` Alan Stern
2018-02-21 17:53 ` Paul E. McKenney
0 siblings, 1 reply; 46+ messages in thread
From: Alan Stern @ 2018-02-21 16:50 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> >
> > > From: Alan Stern <stern@rowland.harvard.edu>
> > >
> > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> >
> > Why do you call this an "S" litmus test? Isn't ISA2 a better
> > description?
>
> Indeed, the name of the test is in fact ISA2.
Sure; and the Changelog entry should reflect this.
> > > accesses with a full memory barrier but without the lock. This litmus
> > > test asks whether writes carried out by two different processes under the
> > > same lock will be seen in order by a third process not holding that lock.
> > > The answer to this question is "yes" for all architectures supporting
> > > the Linux kernel, but is "no" according to the current version of LKMM.
> > >
> > > A patch to LKMM is under development.
> > >
> > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > ---
> > > .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> > > 1 file changed, 41 insertions(+)
> > > create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >
> > Aren't these tests supposed to be described in litmus-tests/README?
You apparently missed this recommendation.
> > > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > new file mode 100644
> > > index 000000000000..7a39a0aaa976
> > > --- /dev/null
> > > +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > @@ -0,0 +1,41 @@
> > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > +
> > > +(*
> > > + * Result: Sometimes
> > > + *
> > > + * This test shows that the ordering provided by a lock-protected S
> > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > + * This is likely to change soon.
> >
> > That last line may be premature. We haven't reached any consensus on
> > how RISC-V will handle this. If RISC-V allows the test then the memory
> > model can't forbid it.
>
> Agreed. How about this? If the RISC-V question is answered by the
> end of next week, I update accordingly. If not, I update the comment
> to give the details.
The README also should be updated.
> Hey, at least having the memory model go in at about the same time as
> a new architecture is giving us good practice! ;-)
Hopefully things will settle down in a week or two.
Alan
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file
2018-02-21 16:15 ` Paul E. McKenney
@ 2018-02-21 16:51 ` Alan Stern
0 siblings, 0 replies; 46+ messages in thread
From: Alan Stern @ 2018-02-21 16:51 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> On Wed, Feb 21, 2018 at 10:10:52AM -0500, Alan Stern wrote:
> > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> >
> > > 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>
> > > ---
> > > tools/memory-model/README | 3 ++-
> > > 1 file changed, 2 insertions(+), 1 deletion(-)
> > >
> > > 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
> >
> > The text immediately below this mentions the Docker image and gentoo
> > package. Aren't they both seriously out of date at this point? In
> > which case, shouldn't we remove them from the README?
>
> Agreed, we should. How about the following?
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit b59fd89b465f0bfbfe06bf47e22c0cf160aef66b
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date: Wed Feb 21 08:13:48 2018 -0800
>
> tools/memory-model: Remove mention of docker/gentoo image
>
> Because the docker and gentoo images haven't been updated in quite some
> time, they are likely to provide more confusion than help. This commit
> therefore removes mention of them from the README file.
>
> Reported-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index ea950c566ffd..0b3a5f3c9ccd 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -27,21 +27,6 @@ separately:
>
> See "herdtools7/INSTALL.md" for installation instructions.
>
> -Alternatively, Abhishek Bhardwaj has kindly provided a Docker image
> -of these tools at "abhishek40/memory-model". Abhishek suggests the
> -following commands to install and use this image:
> -
> - - Users should install Docker for their distribution.
> - - docker run -itd abhishek40/memory-model
> - - docker attach <id-emitted-from-the-previous-command>
> -
> -Gentoo users might wish to make use of Patrick McLean's package:
> -
> - https://gitweb.gentoo.org/repo/gentoo.git/tree/dev-util/herdtools7
> -
> -These packages may not be up-to-date with respect to the GitHub
> -repository.
> -
>
> ==================
> BASIC USAGE: HERD7
Yeah, that's good.
Alan
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 16:50 ` Alan Stern
@ 2018-02-21 17:53 ` Paul E. McKenney
2018-02-21 18:38 ` Alan Stern
0 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-21 17:53 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
>
> > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > >
> > > > From: Alan Stern <stern@rowland.harvard.edu>
> > > >
> > > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > >
> > > Why do you call this an "S" litmus test? Isn't ISA2 a better
> > > description?
> >
> > Indeed, the name of the test is in fact ISA2.
>
> Sure; and the Changelog entry should reflect this.
No argument.
> > > > accesses with a full memory barrier but without the lock. This litmus
> > > > test asks whether writes carried out by two different processes under the
> > > > same lock will be seen in order by a third process not holding that lock.
> > > > The answer to this question is "yes" for all architectures supporting
> > > > the Linux kernel, but is "no" according to the current version of LKMM.
> > > >
> > > > A patch to LKMM is under development.
> > > >
> > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > > ---
> > > > .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> > > > 1 file changed, 41 insertions(+)
> > > > create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > >
> > > Aren't these tests supposed to be described in litmus-tests/README?
>
> You apparently missed this recommendation.
I did, please accept my apologies and please see below.
> > > > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > new file mode 100644
> > > > index 000000000000..7a39a0aaa976
> > > > --- /dev/null
> > > > +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > @@ -0,0 +1,41 @@
> > > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > +
> > > > +(*
> > > > + * Result: Sometimes
> > > > + *
> > > > + * This test shows that the ordering provided by a lock-protected S
> > > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > > + * This is likely to change soon.
> > >
> > > That last line may be premature. We haven't reached any consensus on
> > > how RISC-V will handle this. If RISC-V allows the test then the memory
> > > model can't forbid it.
> >
> > Agreed. How about this? If the RISC-V question is answered by the
> > end of next week, I update accordingly. If not, I update the comment
> > to give the details.
>
> The README also should be updated.
Agreed.
> > Hey, at least having the memory model go in at about the same time as
> > a new architecture is giving us good practice! ;-)
>
> Hopefully things will settle down in a week or two.
Here is hoping!
Thanx, Paul
------------------------------------------------------------------------
commit e6658d1d7fcc6391f3d00beaadc484243123a893
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date: Wed Feb 21 09:49:01 2018 -0800
tools/memory-order: Add documentation of new litmus test
The litmus-tests/README file lacked any mention of then litmus test
named ISA2+pooncelock+pooncelock+pombonce.litmus. This commit therefore
adds this test.
Reported-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index dca7d823ad57..aff3eb90e067 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
order of a pair of writes, where each write is to a different
variable by a different process?
+ISA2+pooncelock+pooncelock+pombonce.litmus
+ Tests whether the ordering provided by a lock-protected S litmus
+ test is visible to an external process whose accesses are
+ separated by smp_mb().
+
ISA2+poonceonces.litmus
As below, but with store-release replaced with WRITE_ONCE()
and load-acquire replaced with READ_ONCE().
^ permalink raw reply related [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 17:53 ` Paul E. McKenney
@ 2018-02-21 18:38 ` Alan Stern
2018-02-21 19:05 ` Paul E. McKenney
0 siblings, 1 reply; 46+ messages in thread
From: Alan Stern @ 2018-02-21 18:38 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> > On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> >
> > > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > >
> > > > > From: Alan Stern <stern@rowland.harvard.edu>
> > > > >
> > > > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > >
> > > > Why do you call this an "S" litmus test? Isn't ISA2 a better
> > > > description?
> > >
> > > Indeed, the name of the test is in fact ISA2.
> >
> > Sure; and the Changelog entry should reflect this.
>
> No argument.
> ------------------------------------------------------------------------
>
> commit e6658d1d7fcc6391f3d00beaadc484243123a893
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date: Wed Feb 21 09:49:01 2018 -0800
>
> tools/memory-order: Add documentation of new litmus test
>
> The litmus-tests/README file lacked any mention of then litmus test
s/lacked/lacks/
s/then/the new/
> named ISA2+pooncelock+pooncelock+pombonce.litmus. This commit therefore
s/named //
> adds this test.
It adds a description of the test, not the test itself.
>
> Reported-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>
> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index dca7d823ad57..aff3eb90e067 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
> order of a pair of writes, where each write is to a different
> variable by a different process?
>
> +ISA2+pooncelock+pooncelock+pombonce.litmus
> + Tests whether the ordering provided by a lock-protected S litmus
Call it an ISA2 litmus test, not an S litmus test!
> + test is visible to an external process whose accesses are
> + separated by smp_mb().
> +
> ISA2+poonceonces.litmus
> As below, but with store-release replaced with WRITE_ONCE()
> and load-acquire replaced with READ_ONCE().
Alan
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 18:38 ` Alan Stern
@ 2018-02-21 19:05 ` Paul E. McKenney
2018-02-21 19:27 ` Alan Stern
0 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-21 19:05 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, Feb 21, 2018 at 01:38:35PM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
>
> > On Wed, Feb 21, 2018 at 11:50:31AM -0500, Alan Stern wrote:
> > > On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> > >
> > > > On Wed, Feb 21, 2018 at 10:09:00AM -0500, Alan Stern wrote:
> > > > > On Tue, 20 Feb 2018, Paul E. McKenney wrote:
> > > > >
> > > > > > From: Alan Stern <stern@rowland.harvard.edu>
> > > > > >
> > > > > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > > > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > > >
> > > > > Why do you call this an "S" litmus test? Isn't ISA2 a better
> > > > > description?
> > > >
> > > > Indeed, the name of the test is in fact ISA2.
> > >
> > > Sure; and the Changelog entry should reflect this.
> >
> > No argument.
>
> > ------------------------------------------------------------------------
> >
> > commit e6658d1d7fcc6391f3d00beaadc484243123a893
> > Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > Date: Wed Feb 21 09:49:01 2018 -0800
> >
> > tools/memory-order: Add documentation of new litmus test
> >
> > The litmus-tests/README file lacked any mention of then litmus test
>
> s/lacked/lacks/
> s/then/the new/
>
> > named ISA2+pooncelock+pooncelock+pombonce.litmus. This commit therefore
>
> s/named //
>
> > adds this test.
>
> It adds a description of the test, not the test itself.
Good catches, fixed.
> > Reported-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> >
> > diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> > index dca7d823ad57..aff3eb90e067 100644
> > --- a/tools/memory-model/litmus-tests/README
> > +++ b/tools/memory-model/litmus-tests/README
> > @@ -32,6 +32,11 @@ IRIW+poonceonces+OnceOnce.litmus
> > order of a pair of writes, where each write is to a different
> > variable by a different process?
> >
> > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > + Tests whether the ordering provided by a lock-protected S litmus
>
> Call it an ISA2 litmus test, not an S litmus test!
Given the structure of the test, the relationship to S is important
because it helps motivate why anyone might care. But yes, having ISA2
only in the filename is a bit obtuse. How about the following?
ISA2+pooncelock+pooncelock+pombonce.litmus
Tests whether the ordering provided by a lock-protected S
litmus test is visible to an external process whose accesses are
separated by smp_mb(). This addition of an external process to
S is otherwise known as ISA2.
Thanx, Paul
> > + test is visible to an external process whose accesses are
> > + separated by smp_mb().
> > +
> > ISA2+poonceonces.litmus
> > As below, but with store-release replaced with WRITE_ONCE()
> > and load-acquire replaced with READ_ONCE().
>
> Alan
>
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 19:05 ` Paul E. McKenney
@ 2018-02-21 19:27 ` Alan Stern
2018-02-21 22:25 ` Paul E. McKenney
0 siblings, 1 reply; 46+ messages in thread
From: Alan Stern @ 2018-02-21 19:27 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, 21 Feb 2018, Paul E. McKenney wrote:
> > > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > > + Tests whether the ordering provided by a lock-protected S litmus
> >
> > Call it an ISA2 litmus test, not an S litmus test!
>
> Given the structure of the test, the relationship to S is important
> because it helps motivate why anyone might care. But yes, having ISA2
> only in the filename is a bit obtuse. How about the following?
>
> ISA2+pooncelock+pooncelock+pombonce.litmus
> Tests whether the ordering provided by a lock-protected S
> litmus test is visible to an external process whose accesses are
> separated by smp_mb(). This addition of an external process to
> S is otherwise known as ISA2.
Okay, that's somewhat better.
However, I still don't understand why you think of this as a form of S.
In S, the first variable written by P0 is the same as the variable
written by P1. In this test, no variable other than the spinlock gets
written twice. To me that seems like a pretty fundamental difference.
Alan
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-21 19:27 ` Alan Stern
@ 2018-02-21 22:25 ` Paul E. McKenney
0 siblings, 0 replies; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-21 22:25 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, mingo, parri.andrea, will.deacon,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov
On Wed, Feb 21, 2018 at 02:27:04PM -0500, Alan Stern wrote:
> On Wed, 21 Feb 2018, Paul E. McKenney wrote:
>
> > > > +ISA2+pooncelock+pooncelock+pombonce.litmus
> > > > + Tests whether the ordering provided by a lock-protected S litmus
> > >
> > > Call it an ISA2 litmus test, not an S litmus test!
> >
> > Given the structure of the test, the relationship to S is important
> > because it helps motivate why anyone might care. But yes, having ISA2
> > only in the filename is a bit obtuse. How about the following?
> >
> > ISA2+pooncelock+pooncelock+pombonce.litmus
> > Tests whether the ordering provided by a lock-protected S
> > litmus test is visible to an external process whose accesses are
> > separated by smp_mb(). This addition of an external process to
> > S is otherwise known as ISA2.
>
> Okay, that's somewhat better.
>
> However, I still don't understand why you think of this as a form of S.
> In S, the first variable written by P0 is the same as the variable
> written by P1. In this test, no variable other than the spinlock gets
> written twice. To me that seems like a pretty fundamental difference.
There is a chain of processes connected by variables, similar to
a snap-together toy. If you "disconnect" S at the end and snap in
a process having a pair of reads separated by a full memory barrier,
you get ISA2. And yes, this does rename one of S's variables, but that
is OK because in this view, each variable is defined by the connection
between a given pair of pair of processes.
Unconventional perhaps, but then again remember who you are emailing
with. ;-)
Another (perhaps more conventional) way to think of this is in terms of
Andrea's python script that identified equivalent litmus tests. For that
script, both the variable names and process numbers are irrelevant.
Thanx, Paul
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Alan Stern
2018-02-21 15:09 ` [PATCH RFC tools/lkmm 10/12] " Alan Stern
@ 2018-02-22 3:23 ` Boqun Feng
2018-02-22 4:13 ` Paul E. McKenney
2 siblings, 1 reply; 46+ messages in thread
From: Boqun Feng @ 2018-02-22 3:23 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, stern, parri.andrea,
will.deacon, peterz, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov, Benjamin Herrenschmidt, Paul Mackerras,
Michael Ellerman
[-- Attachment #1: Type: text/plain, Size: 2567 bytes --]
On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> From: Alan Stern <stern@rowland.harvard.edu>
>
> This commit adds a litmus test in which P0() and P1() form a lock-based S
> litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> accesses with a full memory barrier but without the lock. This litmus
> test asks whether writes carried out by two different processes under the
> same lock will be seen in order by a third process not holding that lock.
> The answer to this question is "yes" for all architectures supporting
Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
Or there is an upcomming commit to switch PowerPC's lock implementation?
[Cc ppc maintainers]
Regards,
Boqun
> the Linux kernel, but is "no" according to the current version of LKMM.
>
> A patch to LKMM is under development.
>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> ---
> .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> 1 file changed, 41 insertions(+)
> create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
>
> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> new file mode 100644
> index 000000000000..7a39a0aaa976
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -0,0 +1,41 @@
> +C ISA2+pooncelock+pooncelock+pombonce.litmus
> +
> +(*
> + * Result: Sometimes
> + *
> + * This test shows that the ordering provided by a lock-protected S
> + * litmus test (P0() and P1()) are not visible to external process P2().
> + * This is likely to change soon.
> + *)
> +
> +{}
> +
> +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)
> --
> 2.5.2
>
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 3:23 ` Boqun Feng
@ 2018-02-22 4:13 ` Paul E. McKenney
2018-02-22 5:27 ` Boqun Feng
0 siblings, 1 reply; 46+ messages in thread
From: Paul E. McKenney @ 2018-02-22 4:13 UTC (permalink / raw)
To: Boqun Feng
Cc: linux-kernel, linux-arch, mingo, stern, parri.andrea,
will.deacon, peterz, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov, Benjamin Herrenschmidt, Paul Mackerras,
Michael Ellerman
On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> > From: Alan Stern <stern@rowland.harvard.edu>
> >
> > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > accesses with a full memory barrier but without the lock. This litmus
> > test asks whether writes carried out by two different processes under the
> > same lock will be seen in order by a third process not holding that lock.
> > The answer to this question is "yes" for all architectures supporting
>
> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> Or there is an upcomming commit to switch PowerPC's lock implementation?
The PowerPC lock implementation's unlock-lock pair does not order writes
from the previous critical section against reads from the later critical
section, but it does order other combinations of reads and writes.
Some have apparently said that RISC-V 's unlock-lock pair also does not
order writes from the previous critical section against writes from the
later critical section. And no, I don't claim to have yet gotten my
head around RISC-V memory ordering. ;-)
Thanx, Paul
> [Cc ppc maintainers]
>
> Regards,
> Boqun
>
> > the Linux kernel, but is "no" according to the current version of LKMM.
> >
> > A patch to LKMM is under development.
> >
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > ---
> > .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> > 1 file changed, 41 insertions(+)
> > create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >
> > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > new file mode 100644
> > index 000000000000..7a39a0aaa976
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -0,0 +1,41 @@
> > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This test shows that the ordering provided by a lock-protected S
> > + * litmus test (P0() and P1()) are not visible to external process P2().
> > + * This is likely to change soon.
> > + *)
> > +
> > +{}
> > +
> > +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)
> > --
> > 2.5.2
> >
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 4:13 ` Paul E. McKenney
@ 2018-02-22 5:27 ` Boqun Feng
2018-02-22 5:42 ` Daniel Lustig
0 siblings, 1 reply; 46+ messages in thread
From: Boqun Feng @ 2018-02-22 5:27 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, stern, parri.andrea,
will.deacon, peterz, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov, Benjamin Herrenschmidt, Paul Mackerras,
Michael Ellerman
[-- Attachment #1: Type: text/plain, Size: 3985 bytes --]
On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> > On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> > > From: Alan Stern <stern@rowland.harvard.edu>
> > >
> > > This commit adds a litmus test in which P0() and P1() form a lock-based S
> > > litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> > > accesses with a full memory barrier but without the lock. This litmus
> > > test asks whether writes carried out by two different processes under the
> > > same lock will be seen in order by a third process not holding that lock.
> > > The answer to this question is "yes" for all architectures supporting
> >
> > Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> > spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> > why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> > Or there is an upcomming commit to switch PowerPC's lock implementation?
>
> The PowerPC lock implementation's unlock-lock pair does not order writes
> from the previous critical section against reads from the later critical
> section, but it does order other combinations of reads and writes.
Ah.. right! Thanks for the explanation ;-)
> Some have apparently said that RISC-V 's unlock-lock pair also does not
> order writes from the previous critical section against writes from the
> later critical section. And no, I don't claim to have yet gotten my
> head around RISC-V memory ordering. ;-)
>
Me neither. Now I remember this: we have a off-list(accidentally)
discussion about this, and IIRC at that moment riscv people confirmed
that riscv's unlock-lock pair doesn't order write->write, but that was
before their memory model draft posted for discussions, so things may
change now...
Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
Regards,
Boqun
> Thanx, Paul
>
> > [Cc ppc maintainers]
> >
> > Regards,
> > Boqun
> >
> > > the Linux kernel, but is "no" according to the current version of LKMM.
> > >
> > > A patch to LKMM is under development.
> > >
> > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > > ---
> > > .../ISA2+pooncelock+pooncelock+pombonce.litmus | 41 ++++++++++++++++++++++
> > > 1 file changed, 41 insertions(+)
> > > create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > >
> > > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > new file mode 100644
> > > index 000000000000..7a39a0aaa976
> > > --- /dev/null
> > > +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > > @@ -0,0 +1,41 @@
> > > +C ISA2+pooncelock+pooncelock+pombonce.litmus
> > > +
> > > +(*
> > > + * Result: Sometimes
> > > + *
> > > + * This test shows that the ordering provided by a lock-protected S
> > > + * litmus test (P0() and P1()) are not visible to external process P2().
> > > + * This is likely to change soon.
> > > + *)
> > > +
> > > +{}
> > > +
> > > +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)
> > > --
> > > 2.5.2
> > >
>
>
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 5:27 ` Boqun Feng
@ 2018-02-22 5:42 ` Daniel Lustig
2018-02-22 6:58 ` Boqun Feng
2018-02-22 10:06 ` Peter Zijlstra
0 siblings, 2 replies; 46+ messages in thread
From: Daniel Lustig @ 2018-02-22 5:42 UTC (permalink / raw)
To: Boqun Feng, Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, stern, parri.andrea,
will.deacon, peterz, npiggin, dhowells, j.alglave, luc.maranget,
akiyks, nborisov, Benjamin Herrenschmidt, Paul Mackerras,
Michael Ellerman
On 2/21/2018 9:27 PM, Boqun Feng wrote:
> On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
>> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
>>> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
>>>> From: Alan Stern <stern@rowland.harvard.edu>
>>>>
>>>> This commit adds a litmus test in which P0() and P1() form a lock-based S
>>>> litmus test, with the addition of P2(), which observes P0()'s and P1()'s
>>>> accesses with a full memory barrier but without the lock. This litmus
>>>> test asks whether writes carried out by two different processes under the
>>>> same lock will be seen in order by a third process not holding that lock.
>>>> The answer to this question is "yes" for all architectures supporting
>>>
>>> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
>>> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
>>> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
>>> Or there is an upcomming commit to switch PowerPC's lock implementation?
>>
>> The PowerPC lock implementation's unlock-lock pair does not order writes
>> from the previous critical section against reads from the later critical
>> section, but it does order other combinations of reads and writes.
>
> Ah.. right! Thanks for the explanation ;-)
>
>> Some have apparently said that RISC-V 's unlock-lock pair also does not
>> order writes from the previous critical section against writes from the
>> later critical section. And no, I don't claim to have yet gotten my
>> head around RISC-V memory ordering. ;-)
>>
>
> Me neither. Now I remember this: we have a off-list(accidentally)
> discussion about this, and IIRC at that moment riscv people confirmed
> that riscv's unlock-lock pair doesn't order write->write, but that was
> before their memory model draft posted for discussions, so things may
> change now...
>
> Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
>
> Regards,
> Boqun
>
>> Thanx, Paul
>>
As a matter of fact, the RISC-V memory model committee is debating this
exact question at the moment. Now that I see this thread I'll have to
go back and catch up on what I've missed, but at least I can be on cc
from this point on to answer any RISC-V questions that come up from
here on.
(Is there some place I should add my name as a RISC-V memory model
contact, so I don't miss threads like this in the future?)
And yes, if we go with a purely RCpc interpretation of acquire and
release, then I don't believe the writes in the previous critical
section would be ordered with the writes in the subsequent critical
section. That's really all the argument boils down to. We'd like
to support RCpc if we can since that's all some software needs, but
we also obviously want to make sure we can support RCsc and these
kinds of LKMM subtleties efficiently too when needed. So we have a
few encoding details that we're still finalizing, because questions
like this one are still popping up :)
Let me know if you had other RISC-V-specific questions I can help
answer.
Dan
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 5:42 ` Daniel Lustig
@ 2018-02-22 6:58 ` Boqun Feng
2018-02-22 10:15 ` Peter Zijlstra
2018-02-22 10:06 ` Peter Zijlstra
1 sibling, 1 reply; 46+ messages in thread
From: Boqun Feng @ 2018-02-22 6:58 UTC (permalink / raw)
To: Daniel Lustig
Cc: Paul E. McKenney, linux-kernel, linux-arch, mingo, stern,
parri.andrea, will.deacon, peterz, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, nborisov, Benjamin Herrenschmidt,
Paul Mackerras, Michael Ellerman
[-- Attachment #1: Type: text/plain, Size: 4144 bytes --]
On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> On 2/21/2018 9:27 PM, Boqun Feng wrote:
> > On Wed, Feb 21, 2018 at 08:13:57PM -0800, Paul E. McKenney wrote:
> >> On Thu, Feb 22, 2018 at 11:23:49AM +0800, Boqun Feng wrote:
> >>> On Tue, Feb 20, 2018 at 03:25:10PM -0800, Paul E. McKenney wrote:
> >>>> From: Alan Stern <stern@rowland.harvard.edu>
> >>>>
> >>>> This commit adds a litmus test in which P0() and P1() form a lock-based S
> >>>> litmus test, with the addition of P2(), which observes P0()'s and P1()'s
> >>>> accesses with a full memory barrier but without the lock. This litmus
> >>>> test asks whether writes carried out by two different processes under the
> >>>> same lock will be seen in order by a third process not holding that lock.
> >>>> The answer to this question is "yes" for all architectures supporting
> >>>
> >>> Hmm.. it this true? Our spin_lock() is RCpc because of PowerPC, so
> >>> spin_lock()+spin_unlock() pairs don't provide transitivity, and that's
> >>> why we have smp_mb__after_unlock_lock(). Is there something I'm missing?
> >>> Or there is an upcomming commit to switch PowerPC's lock implementation?
> >>
> >> The PowerPC lock implementation's unlock-lock pair does not order writes
> >> from the previous critical section against reads from the later critical
> >> section, but it does order other combinations of reads and writes.
> >
> > Ah.. right! Thanks for the explanation ;-)
> >
> >> Some have apparently said that RISC-V 's unlock-lock pair also does not
> >> order writes from the previous critical section against writes from the
> >> later critical section. And no, I don't claim to have yet gotten my
> >> head around RISC-V memory ordering. ;-)
> >>
> >
> > Me neither. Now I remember this: we have a off-list(accidentally)
> > discussion about this, and IIRC at that moment riscv people confirmed
> > that riscv's unlock-lock pair doesn't order write->write, but that was
> > before their memory model draft posted for discussions, so things may
> > change now...
> >
> > Besides, I think the smp_mb() on P2 can be relaxed to smp_rmb(), no?
> >
> > Regards,
> > Boqun
> >
> >> Thanx, Paul
> >>
>
> As a matter of fact, the RISC-V memory model committee is debating this
> exact question at the moment. Now that I see this thread I'll have to
> go back and catch up on what I've missed, but at least I can be on cc
> from this point on to answer any RISC-V questions that come up from
> here on.
>
Hi Daniel ;-)
> (Is there some place I should add my name as a RISC-V memory model
> contact, so I don't miss threads like this in the future?)
>
You can submit a patch to add yourself as a Maintainer or Reviewer for
LKMM, Patch #6 in this series is a good example:
https://marc.info/?l=linux-kernel&m=151916916630299&w=2
, and "get_maintainer.pl" will help people find you for memory model
stuffs.
> And yes, if we go with a purely RCpc interpretation of acquire and
> release, then I don't believe the writes in the previous critical
> section would be ordered with the writes in the subsequent critical
> section. That's really all the argument boils down to. We'd like
I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
Alan and Andrea?
And we are not going to change it, are we?
If atomics in Linux kernel are purely RCpc, then it cerntainly makes
sense for riscv to provide purely RCpc atomics.
> to support RCpc if we can since that's all some software needs, but
> we also obviously want to make sure we can support RCsc and these
> kinds of LKMM subtleties efficiently too when needed. So we have a
I think the problem here is that locks in Linux kernel are more strict
than RCpc but weaker than RCsc, and there is not a well-known concept
for the semantics of locks in Linux kernel AFAIK.
Regards,
Boqun
> few encoding details that we're still finalizing, because questions
> like this one are still popping up :)
>
> Let me know if you had other RISC-V-specific questions I can help
> answer.
>
> Dan
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 5:42 ` Daniel Lustig
2018-02-22 6:58 ` Boqun Feng
@ 2018-02-22 10:06 ` Peter Zijlstra
2018-02-22 10:20 ` Peter Zijlstra
1 sibling, 1 reply; 46+ messages in thread
From: Peter Zijlstra @ 2018-02-22 10:06 UTC (permalink / raw)
To: Daniel Lustig
Cc: Boqun Feng, Paul E. McKenney, linux-kernel, linux-arch, mingo,
stern, parri.andrea, will.deacon, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, nborisov, Benjamin Herrenschmidt,
Paul Mackerras, Michael Ellerman
On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> And yes, if we go with a purely RCpc interpretation of acquire and
> release, then I don't believe the writes in the previous critical
> section would be ordered with the writes in the subsequent critical
> section.
Excuse my ignorance (also jumping in the middle of things), but how can
this be?
spin_unlock() is a store-release, this means the write to the lock word
must happen after any stores inside the critical section.
spin_lock() is a load-acquire + test-and-set-ctrl-dep, we'll only
proceed with the critical section if we observe the lock 'unlocked',
which also means we must observe the stores prior to the unlock.
And both the ctrl-dep and the ACQUIRE ensure future stores cannot happen
before.
So while the lock store and subsequent critical section stores are
unordered, I don't see how it would be possible to not be ordered
against stores from a previous critical section.
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 6:58 ` Boqun Feng
@ 2018-02-22 10:15 ` Peter Zijlstra
2018-02-22 10:45 ` Boqun Feng
0 siblings, 1 reply; 46+ messages in thread
From: Peter Zijlstra @ 2018-02-22 10:15 UTC (permalink / raw)
To: Boqun Feng
Cc: Daniel Lustig, Paul E. McKenney, linux-kernel, linux-arch, mingo,
stern, parri.andrea, will.deacon, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, nborisov, Benjamin Herrenschmidt,
Paul Mackerras, Michael Ellerman
On Thu, Feb 22, 2018 at 02:58:47PM +0800, Boqun Feng wrote:
> > And yes, if we go with a purely RCpc interpretation of acquire and
> > release, then I don't believe the writes in the previous critical
> > section would be ordered with the writes in the subsequent critical
> > section. That's really all the argument boils down to. We'd like
>
> I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
> Alan and Andrea?
>
> And we are not going to change it, are we?
>
> If atomics in Linux kernel are purely RCpc, then it cerntainly makes
> sense for riscv to provide purely RCpc atomics.
So there's 3 things:
smp_load_acquire(), smp_store_release()
atomic*_{acquire,release}()
*_{lock,unlock}();
Which are all quite distinct.
smp_load_acquire() and smp_store_release() are RCpc, and there is no
discussion of ever wanting to change that.
The atomics also follow this and are RCpc, in fact the RELEASE only
applies to the STORE and the ACQUIRE only applies to the LOAD of the
atomics.
The locking primitives OTOH we would really rather like to be RCsc, and
everybody except PPC has them as such, PPC being the only one having
RCpc locks.
I read the part you quoted from Daniel as being purely about spinlocks,
the 'critical section' wording being a dead give away, so I'm then
somewhat confused why you talk about atomics.
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 10:06 ` Peter Zijlstra
@ 2018-02-22 10:20 ` Peter Zijlstra
0 siblings, 0 replies; 46+ messages in thread
From: Peter Zijlstra @ 2018-02-22 10:20 UTC (permalink / raw)
To: Daniel Lustig
Cc: Boqun Feng, Paul E. McKenney, linux-kernel, linux-arch, mingo,
stern, parri.andrea, will.deacon, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, nborisov, Benjamin Herrenschmidt,
Paul Mackerras, Michael Ellerman
On Thu, Feb 22, 2018 at 11:06:36AM +0100, Peter Zijlstra wrote:
> On Wed, Feb 21, 2018 at 09:42:08PM -0800, Daniel Lustig wrote:
> > And yes, if we go with a purely RCpc interpretation of acquire and
> > release, then I don't believe the writes in the previous critical
> > section would be ordered with the writes in the subsequent critical
> > section.
>
> Excuse my ignorance (also jumping in the middle of things), but how can
> this be?
>
> spin_unlock() is a store-release, this means the write to the lock word
> must happen after any stores inside the critical section.
>
> spin_lock() is a load-acquire + test-and-set-ctrl-dep, we'll only
> proceed with the critical section if we observe the lock 'unlocked',
> which also means we must observe the stores prior to the unlock.
>
> And both the ctrl-dep and the ACQUIRE ensure future stores cannot happen
> before.
>
> So while the lock store and subsequent critical section stores are
> unordered, I don't see how it would be possible to not be ordered
> against stores from a previous critical section.
>
Or are we talking about a third party observing while not partaking in
the lock-chain? Then I agree, the stores can be observed out of order by
this 3rd actor.
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 10:15 ` Peter Zijlstra
@ 2018-02-22 10:45 ` Boqun Feng
2018-02-22 11:59 ` Peter Zijlstra
0 siblings, 1 reply; 46+ messages in thread
From: Boqun Feng @ 2018-02-22 10:45 UTC (permalink / raw)
To: Peter Zijlstra
Cc: Daniel Lustig, Paul E. McKenney, linux-kernel, linux-arch, mingo,
stern, parri.andrea, will.deacon, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, nborisov, Benjamin Herrenschmidt,
Paul Mackerras, Michael Ellerman
[-- Attachment #1: Type: text/plain, Size: 2400 bytes --]
On Thu, Feb 22, 2018 at 11:15:04AM +0100, Peter Zijlstra wrote:
> On Thu, Feb 22, 2018 at 02:58:47PM +0800, Boqun Feng wrote:
> > > And yes, if we go with a purely RCpc interpretation of acquire and
> > > release, then I don't believe the writes in the previous critical
> > > section would be ordered with the writes in the subsequent critical
> > > section. That's really all the argument boils down to. We'd like
> >
> > I think atomics in Linux kernel(and in LKMM) are purely RCpc, right?
> > Alan and Andrea?
> >
> > And we are not going to change it, are we?
> >
> > If atomics in Linux kernel are purely RCpc, then it cerntainly makes
> > sense for riscv to provide purely RCpc atomics.
>
> So there's 3 things:
>
> smp_load_acquire(), smp_store_release()
>
> atomic*_{acquire,release}()
>
> *_{lock,unlock}();
>
> Which are all quite distinct.
>
> smp_load_acquire() and smp_store_release() are RCpc, and there is no
> discussion of ever wanting to change that.
>
> The atomics also follow this and are RCpc, in fact the RELEASE only
> applies to the STORE and the ACQUIRE only applies to the LOAD of the
> atomics.
>
> The locking primitives OTOH we would really rather like to be RCsc, and
> everybody except PPC has them as such, PPC being the only one having
> RCpc locks.
>
> I read the part you quoted from Daniel as being purely about spinlocks,
> the 'critical section' wording being a dead give away, so I'm then
> somewhat confused why you talk about atomics.
Maybe it's me who misunderstand Daniel's words. But my understanding is
that riscv people are on a debate about whether their "RCpc" atomic
instructions need to be more strict: release+acquire pair orders two
writes. And I thought that atomics(including RmW atomics) in kernel only
have purely RCpc semantics, which I needed to check with you guy. And if
I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
purely RCpc.
Note that even on PPC, the release+acquire pair of atomics orders writes
before and after, and on x86, writes are ordered since it's TSO. So
strictly speaking, I think our current implementation of atomics are a
little more strict than purely RCpc. If we think this is an requirement
for implementation of atomic primitives, than the current version of
riscv's "RCpc" atomics don't suffice.
Regards,
Boqun
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]
^ permalink raw reply [flat|nested] 46+ messages in thread
* Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test
2018-02-22 10:45 ` Boqun Feng
@ 2018-02-22 11:59 ` Peter Zijlstra
0 siblings, 0 replies; 46+ messages in thread
From: Peter Zijlstra @ 2018-02-22 11:59 UTC (permalink / raw)
To: Boqun Feng
Cc: Daniel Lustig, Paul E. McKenney, linux-kernel, linux-arch, mingo,
stern, parri.andrea, will.deacon, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, nborisov, Benjamin Herrenschmidt,
Paul Mackerras, Michael Ellerman
On Thu, Feb 22, 2018 at 06:45:32PM +0800, Boqun Feng wrote:
> Maybe it's me who misunderstand Daniel's words. But my understanding is
> that riscv people are on a debate about whether their "RCpc" atomic
> instructions need to be more strict: release+acquire pair orders two
> writes. And I thought that atomics(including RmW atomics) in kernel only
> have purely RCpc semantics, which I needed to check with you guy. And if
> I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
> purely RCpc.
>
> Note that even on PPC, the release+acquire pair of atomics orders writes
> before and after, and on x86, writes are ordered since it's TSO. So
> strictly speaking, I think our current implementation of atomics are a
> little more strict than purely RCpc. If we think this is an requirement
> for implementation of atomic primitives, than the current version of
> riscv's "RCpc" atomics don't suffice.
So the question is:
P0()
{
WRITE_ONCE(x, 1);
smp_store_release(&y, 1);
r0 = smp_load_acquire(&y);
WRITE_ONCE(z, 1);
}
P1()
{
r1 = READ_ONCE(z);
smp_rmb();
r2 = READ_ONCE(x);
}
exists: r0 == 1 /\ r1==1 /\ r2==0
Which per the current LKMM would be forbidden? How would strict RCpc
allow that? Due to a fwd from the release to the acquire and then
defeating the ordering or something like that?
My vote would go to disallowing this. Allowing this would be rather
subtle and unexpected IMO.
^ permalink raw reply [flat|nested] 46+ messages in thread
end of thread, other threads:[~2018-02-22 11:59 UTC | newest]
Thread overview: 46+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-02-20 23:24 [PATCH RFC tools/lkmm 0/12] Miscellaneous fixes Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 01/12] tools/memory-model: Clarify the origin/scope of the tool name Paul E. McKenney
2018-02-21 10:39 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 02/12] MAINTAINERS: Add the Memory Consistency Model subsystem Paul E. McKenney
2018-02-21 10:39 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 03/12] MAINTAINERS: List file memory-barriers.txt within the LKMM entry Paul E. McKenney
2018-02-21 10:40 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 04/12] EXP litmus_tests: Add comments explaining tests' purposes Paul E. McKenney
2018-02-21 10:40 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 05/12] README: Fix a couple of punctuation errors Paul E. McKenney
2018-02-21 10:41 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 06/12] MAINTAINERS: Add Akira Yokosawa as an LKMM reviewer Paul E. McKenney
2018-02-21 10:41 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 07/12] Documentation/memory-barriers.txt: Cross-reference "tools/memory-model/" Paul E. McKenney
2018-02-21 10:42 ` [tip:locking/core] " tip-bot for Andrea Parri
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 08/12] memory-barriers: Fix description of data dependency barriers Paul E. McKenney
2018-02-21 10:42 ` [tip:locking/core] " tip-bot for Nikolay Borisov
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 09/12] tools/memory-model: Add required herd7 version to README file Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-21 15:10 ` [PATCH RFC tools/lkmm 09/12] " Alan Stern
2018-02-21 16:15 ` Paul E. McKenney
2018-02-21 16:51 ` Alan Stern
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test Paul E. McKenney
2018-02-21 10:43 ` [tip:locking/core] " tip-bot for Alan Stern
2018-02-21 15:09 ` [PATCH RFC tools/lkmm 10/12] " Alan Stern
2018-02-21 16:12 ` Paul E. McKenney
2018-02-21 16:50 ` Alan Stern
2018-02-21 17:53 ` Paul E. McKenney
2018-02-21 18:38 ` Alan Stern
2018-02-21 19:05 ` Paul E. McKenney
2018-02-21 19:27 ` Alan Stern
2018-02-21 22:25 ` Paul E. McKenney
2018-02-22 3:23 ` Boqun Feng
2018-02-22 4:13 ` Paul E. McKenney
2018-02-22 5:27 ` Boqun Feng
2018-02-22 5:42 ` Daniel Lustig
2018-02-22 6:58 ` Boqun Feng
2018-02-22 10:15 ` Peter Zijlstra
2018-02-22 10:45 ` Boqun Feng
2018-02-22 11:59 ` Peter Zijlstra
2018-02-22 10:06 ` Peter Zijlstra
2018-02-22 10:20 ` Peter Zijlstra
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 11/12] tools/memory-model: Convert underscores to hyphens Paul E. McKenney
2018-02-21 10:44 ` [tip:locking/core] " tip-bot for Paul E. McKenney
2018-02-20 23:25 ` [PATCH RFC tools/lkmm 12/12] tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference Paul E. McKenney
2018-02-21 10:45 ` [tip:locking/core] " tip-bot for Alan Stern
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).