[PATCH RFC memory-model 0/6] LKMM updates

[PATCH RFC memory-model 0/6] LKMM updates

[Paul E. McKenney]

Hello!

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

1-3.	Add SRCU support, courtesy of Alan Stern.

4.	Update README for adding of SRCU support.

5.	Update memory-barriers.txt on enforcing heavy ordering for
	port-I/O accesses, courtesy of Will Deacon.  This one needs
	an ack, preferably by someone from Intel.  Matthew Wilcox
	posted some feedback from an Intel manual here, which might
	be considered to be a close substitute, but...  ;-)

	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org

6.	Update Documentation/explanation.txt to include SRCU support,
	courtesy of Alan Stern.

7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
	Luc Maranget.  This needs an ack.

							Thanx, Paul

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

 Documentation/memory-barriers.txt                |    6 
 tools/memory-model/Documentation/explanation.txt |  289 ++++++++++++-----------
 tools/memory-model/README                        |   25 +
 tools/memory-model/linux-kernel.bell             |   37 ++
 tools/memory-model/linux-kernel.cat              |   55 ++--
 tools/memory-model/linux-kernel.def              |    7 
 6 files changed, 250 insertions(+), 169 deletions(-)

[PATCH RFC LKMM 1/7] tools/memory-model: Rename some RCU relations

[Paul E. McKenney]

From: Alan Stern <stern@rowland.harvard.edu>

In preparation for adding support for SRCU, rename "crit" to
"rcu-rscs", rename "rscs" to "rcu-rscsi", and remove the restriction
to only the outermost level of nesting.

The name change is needed for disambiguating RCU read-side critical
sections from SRCU read-side critical sections.  Adding the "i" at the
end of "rcu-rscsi" emphasizes that the relation is inverted; it links
rcu_read_unlock() events to their corresponding preceding
rcu_read_lock() events.

The restriction to outermost nesting levels was never essential; it
was included mostly to show that it could be done.  Rather than add
equivalent unnecessary code for SRCU lock nesting, it seemed better to
remove the existing code.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 tools/memory-model/linux-kernel.bell |  9 +++------
 tools/memory-model/linux-kernel.cat  | 10 +++++-----
 2 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 796513362c05..353c8d68e030 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -34,7 +34,7 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 instructions F[Barriers]
 
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
-let matched = let rec
+let rcu-rscs = let rec
 	    unmatched-locks = Rcu-lock \ domain(matched)
 	and unmatched-unlocks = Rcu-unlock \ range(matched)
 	and unmatched = unmatched-locks | unmatched-unlocks
@@ -46,8 +46,5 @@ let matched = let rec
 	in matched
 
 (* Validate nesting *)
-flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
-flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
-
-(* Outermost level of nesting only *)
-let crit = matched \ (po^-1 ; matched ; po^-1)
+flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
+flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 8f23c74a96fd..ab9de9c1234b 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -95,7 +95,7 @@ acyclic pb as propagation
  * onward on the one hand and from the rcu_read_unlock() backwards on the
  * other hand.
  *)
-let rscs = po ; crit^-1 ; po?
+let rcu-rscsi = po ; rcu-rscs^-1 ; po?
 
 (*
  * The synchronize_rcu() strong fence is special in that it can order not
@@ -109,10 +109,10 @@ let rcu-link = hb* ; pb* ; prop
  * critical sections (joined by rcu-link) acts as a generalized strong fence.
  *)
 let rec rcu-fence = gp |
-	(gp ; rcu-link ; rscs) |
-	(rscs ; rcu-link ; gp) |
-	(gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) |
-	(rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) |
+	(gp ; rcu-link ; rcu-rscsi) |
+	(rcu-rscsi ; rcu-link ; gp) |
+	(gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
+	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; gp) |
 	(rcu-fence ; rcu-link ; rcu-fence)
 
 (* rb orders instructions just as pb does *)
-- 
2.17.1

[PATCH RFC LKMM 2/7] tools/memory-model: Refactor some RCU relations

[Paul E. McKenney]

From: Alan Stern <stern@rowland.harvard.edu>

In preparation for adding support for SRCU, refactor the definitions
of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po?
terms from the first two to the second two.  An rcu-gp relation is
added; it is equivalent to gp with the po and po? terms removed.

This is necessary because for SRCU, we will have to use the loc
relation to check that the terms at the start and end of each disjunct
in the definition of rcu-fence refer to the same srcu_struct
location.  If these terms are hidden behind po and po?, there's no way
to carry out this check.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 tools/memory-model/linux-kernel.cat | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index ab9de9c1234b..b8e6197f05af 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -91,32 +91,37 @@ acyclic pb as propagation
 (*******)
 
 (*
- * Effect of read-side critical section proceeds from the rcu_read_lock()
- * onward on the one hand and from the rcu_read_unlock() backwards on the
+ * Effects of read-side critical sections proceed from the rcu_read_unlock()
+ * backwards on the one hand, and from the rcu_read_lock() forwards on the
  * other hand.
+ *
+ * In the definition of rcu-fence below, the po term at the left-hand side
+ * of each disjunct and the po? term at the right-hand end have been factored
+ * out.  They have been moved into the definitions of rcu-link and rb.
  *)
-let rcu-rscsi = po ; rcu-rscs^-1 ; po?
+let rcu-gp = [Sync-rcu]		(* Compare with gp *)
+let rcu-rscsi = rcu-rscs^-1
 
 (*
  * The synchronize_rcu() strong fence is special in that it can order not
  * one but two non-rf relations, but only in conjunction with an RCU
  * read-side critical section.
  *)
-let rcu-link = hb* ; pb* ; prop
+let rcu-link = po? ; hb* ; pb* ; prop ; po
 
 (*
  * Any sequence containing at least as many grace periods as RCU read-side
  * critical sections (joined by rcu-link) acts as a generalized strong fence.
  *)
-let rec rcu-fence = gp |
-	(gp ; rcu-link ; rcu-rscsi) |
-	(rcu-rscsi ; rcu-link ; gp) |
-	(gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
-	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; gp) |
+let rec rcu-fence = rcu-gp |
+	(rcu-gp ; rcu-link ; rcu-rscsi) |
+	(rcu-rscsi ; rcu-link ; rcu-gp) |
+	(rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
+	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) |
 	(rcu-fence ; rcu-link ; rcu-fence)
 
 (* rb orders instructions just as pb does *)
-let rb = prop ; rcu-fence ; hb* ; pb*
+let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
 
 irreflexive rb as rcu
 
-- 
2.17.1

[PATCH RFC LKMM 3/7] tools/memory-model: Add SRCU support

[Paul E. McKenney]

From: Alan Stern <stern@rowland.harvard.edu>

Add support for SRCU.  Herd creates srcu events and linux-kernel.def
associates them with three possible annotations (srcu-lock,
srcu-unlock, and sync-srcu) corresponding to the API routines
srcu_read_lock(), srcu_read_unlock(), and synchronize_srcu().

The linux-kernel.bell file now declares the annotations
and determines matching lock/unlock pairs delimiting SRCU read-side
critical sections, and it also checks for synchronize_srcu() calls
inside an RCU critical section (which would generate a "sleeping in
atomic context" error in real kernel code).  The linux-kernel.cat file
now adds SRCU-induced ordering, analogous to the existing RCU-induced
ordering, to the gp and rcu-fence relations.

Curiously enough, these small changes to the model's .cat code are all
that is needed to describe SRCU.

Portions of this patch (linux-kernel.def and the first hunk in
linux-kernel.bell) were written by Luc Maranget.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
CC: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 tools/memory-model/linux-kernel.bell | 25 +++++++++++++++++++++++++
 tools/memory-model/linux-kernel.cat  | 18 ++++++++++++++----
 tools/memory-model/linux-kernel.def  |  5 +++++
 3 files changed, 44 insertions(+), 4 deletions(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 353c8d68e030..9c42cd9ddcb4 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -33,6 +33,12 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'after-unlock-lock (*smp_mb__after_unlock_lock*)
 instructions F[Barriers]
 
+(* SRCU *)
+enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
+instructions SRCU[SRCU]
+(* All srcu events *)
+let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu
+
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
 let rcu-rscs = let rec
 	    unmatched-locks = Rcu-lock \ domain(matched)
@@ -48,3 +54,22 @@ let rcu-rscs = let rec
 (* Validate nesting *)
 flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
 flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
+
+(* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
+let srcu-rscs = let rec
+	    unmatched-locks = Srcu-lock \ domain(matched)
+	and unmatched-unlocks = Srcu-unlock \ range(matched)
+	and unmatched = unmatched-locks | unmatched-unlocks
+	and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
+	and unmatched-locks-to-unlocks =
+		([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
+	and matched = matched | (unmatched-locks-to-unlocks \
+		(unmatched-po ; unmatched-po))
+	in matched
+
+(* Validate nesting *)
+flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
+flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
+
+(* Check for use of synchronize_srcu() inside an RCU critical section *)
+flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index b8e6197f05af..8dcb37835b61 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -33,7 +33,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) |
 	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
 	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
 		fencerel(After-unlock-lock) ; [M])
-let gp = po ; [Sync-rcu] ; po?
+let gp = po ; [Sync-rcu | Sync-srcu] ; po?
 
 let strong-fence = mb | gp
 
@@ -92,15 +92,18 @@ acyclic pb as propagation
 
 (*
  * Effects of read-side critical sections proceed from the rcu_read_unlock()
- * backwards on the one hand, and from the rcu_read_lock() forwards on the
- * other hand.
+ * or srcu_read_unlock() backwards on the one hand, and from the
+ * rcu_read_lock() or srcu_read_lock() forwards on the other hand.
  *
  * In the definition of rcu-fence below, the po term at the left-hand side
  * of each disjunct and the po? term at the right-hand end have been factored
  * out.  They have been moved into the definitions of rcu-link and rb.
+ * This was necessary in order to apply the "& loc" tests correctly.
  *)
 let rcu-gp = [Sync-rcu]		(* Compare with gp *)
+let srcu-gp = [Sync-srcu]
 let rcu-rscsi = rcu-rscs^-1
+let srcu-rscsi = srcu-rscs^-1
 
 (*
  * The synchronize_rcu() strong fence is special in that it can order not
@@ -112,12 +115,19 @@ let rcu-link = po? ; hb* ; pb* ; prop ; po
 (*
  * Any sequence containing at least as many grace periods as RCU read-side
  * critical sections (joined by rcu-link) acts as a generalized strong fence.
+ * Likewise for SRCU grace periods and read-side critical sections, provided
+ * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same
+ * struct srcu_struct location.
  *)
-let rec rcu-fence = rcu-gp |
+let rec rcu-fence = rcu-gp | srcu-gp |
 	(rcu-gp ; rcu-link ; rcu-rscsi) |
+	((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |
 	(rcu-rscsi ; rcu-link ; rcu-gp) |
+	((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |
 	(rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
+	((srcu-gp ; rcu-link ; rcu-fence ; rcu-link ; srcu-rscsi) & loc) |
 	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) |
+	((srcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; srcu-gp) & loc) |
 	(rcu-fence ; rcu-link ; rcu-fence)
 
 (* rb orders instructions just as pb does *)
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index b27911cc087d..1d6a120cde14 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -47,6 +47,11 @@ rcu_read_unlock() { __fence{rcu-unlock}; }
 synchronize_rcu() { __fence{sync-rcu}; }
 synchronize_rcu_expedited() { __fence{sync-rcu}; }
 
+// SRCU
+srcu_read_lock(X)  __srcu{srcu-lock}(X)
+srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
+synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
+
 // Atomic
 atomic_read(X) READ_ONCE(*X)
 atomic_set(X,V) { WRITE_ONCE(*X,V); }
-- 
2.17.1

[PATCH RFC LKMM 4/7] tools/memory-model: Update README for addition of SRCU

[Paul E. McKenney]

This commit updates the section on LKMM limitations to no longer say
that SRCU is not modeled, but instead describe how LKMM's modeling of
SRCU departs from the Linux-kernel implementation.

TL;DR:  There is no known valid use case that cares about the Linux
kernel's ability to have partially overlapping SRCU read-side critical
sections.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 tools/memory-model/README | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/tools/memory-model/README b/tools/memory-model/README
index 0f2c366518c6..9d7d4f23503f 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -221,8 +221,29 @@ The Linux-kernel memory model has the following limitations:
 		additional call_rcu() process to the site of the
 		emulated rcu-barrier().
 
-	e.	Sleepable RCU (SRCU) is not modeled.  It can be
-		emulated, but perhaps not simply.
+	e.	Although sleepable RCU (SRCU) is now modeled, there
+		are some subtle differences between its semantics and
+		those in the Linux kernel.  For example, the kernel
+		might interpret the following sequence as two partially
+		overlapping SRCU read-side critical sections:
+
+			 1  r1 = srcu_read_lock(&my_srcu);
+			 2  do_something_1();
+			 3  r2 = srcu_read_lock(&my_srcu);
+			 4  do_something_2();
+			 5  srcu_read_unlock(&my_srcu, r1);
+			 6  do_something_3();
+			 7  srcu_read_unlock(&my_srcu, r2);
+
+		In contrast, LKMM will interpret this as a nested pair of
+		SRCU read-side critical sections, with the outer critical
+		section spanning lines 1-7 and the inner critical section
+		spanning lines 3-5.
+
+		This difference would be more of a concern had anyone
+		identified a reasonable use case for partially overlapping
+		SRCU read-side critical sections.  For more information,
+		please see: https://paulmck.livejournal.com/40593.html
 
 	f.	Reader-writer locking is not modeled.  It can be
 		emulated in litmus tests using atomic read-modify-write
-- 
2.17.1

[PATCH RFC LKMM 5/7] docs/memory-barriers.txt: Enforce heavy ordering for port I/O accesses

[Paul E. McKenney]

From: Will Deacon <will.deacon@arm.com>

David Laight explains:

  | A long time ago there was a document from Intel that said that
  | inb/outb weren't necessarily synchronised wrt memory accesses.
  | (Might be P-pro era). However no processors actually behaved that
  | way and more recent docs say that inb/outb are fully ordered.

This also reflects the situation on other architectures, the the port
accessor macros tend to be implemented in terms of readX/writeX.

Update Documentation/memory-barriers.txt to reflect reality.

Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
Cc: Arnd Bergmann <arnd@arndb.de>
Cc: David Laight <David.Laight@ACULAB.COM>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: <linux-arch@vger.kernel.org>
Cc: <linux-doc@vger.kernel.org>
Cc: <linux-kernel@vger.kernel.org>
Signed-off-by: Will Deacon <will.deacon@arm.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 Documentation/memory-barriers.txt | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 1c22b21ae922..a70104e2a087 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -2619,10 +2619,8 @@ functions:
      intermediary bridges (such as the PCI host bridge) may not fully honour
      that.
 
-     They are guaranteed to be fully ordered with respect to each other.
-
-     They are not guaranteed to be fully ordered with respect to other types of
-     memory and I/O operation.
+     They are guaranteed to be fully ordered with respect to each other and
+     also with respect to other types of memory and I/O operation.
 
  (*) readX(), writeX():
 
-- 
2.17.1

[PATCH RFC LKMM 6/7] tools/memory-model: Update Documentation/explanation.txt to include SRCU support

[Paul E. McKenney]

From: Alan Stern <stern@rowland.harvard.edu>

The recent commit adding support for SRCU to the Linux Kernel Memory
Model ended up changing the names and meanings of several relations.
This patch updates the explanation.txt documentation file to reflect
those changes.

It also revises the statement of the RCU Guarantee to a more accurate
form, and it adds a short paragraph mentioning the new support for SRCU.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Andrea Parri <andrea.parri@amarulasolutions.com>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Will Deacon <will.deacon@arm.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 .../Documentation/explanation.txt             | 289 +++++++++---------
 1 file changed, 152 insertions(+), 137 deletions(-)

diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 35bff92cc773..68caa9a976d0 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -27,7 +27,7 @@ Explanation of the Linux-Kernel Memory Consistency Model
   19. AND THEN THERE WAS ALPHA
   20. THE HAPPENS-BEFORE RELATION: hb
   21. THE PROPAGATES-BEFORE RELATION: pb
-  22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
+  22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-fence, and rb
   23. LOCKING
   24. ODDS AND ENDS
 
@@ -1430,8 +1430,8 @@ they execute means that it cannot have cycles.  This requirement is
 the content of the LKMM's "propagation" axiom.
 
 
-RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
-----------------------------------------------------
+RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-fence, and rb
+-------------------------------------------------------------
 
 RCU (Read-Copy-Update) is a powerful synchronization mechanism.  It
 rests on two concepts: grace periods and read-side critical sections.
@@ -1446,17 +1446,19 @@ As far as memory models are concerned, RCU's main feature is its
 Grace-Period Guarantee, which states that a critical section can never
 span a full grace period.  In more detail, the Guarantee says:
 
-	If a critical section starts before a grace period then it
-	must end before the grace period does.  In addition, every
-	store that propagates to the critical section's CPU before the
-	end of the critical section must propagate to every CPU before
-	the end of the grace period.
+	For any critical section C and any grace period G, at least
+	one of the following statements must hold:
 
-	If a critical section ends after a grace period ends then it
-	must start after the grace period does.  In addition, every
-	store that propagates to the grace period's CPU before the
-	start of the grace period must propagate to every CPU before
-	the start of the critical section.
+(1)	C ends before G does, and in addition, every store that
+	propagates to C's CPU before the end of C must propagate to
+	every CPU before G ends.
+
+(2)	G starts before C does, and in addition, every store that
+	propagates to G's CPU before the start of G must propagate
+	to every CPU before C starts.
+
+In particular, it is not possible for a critical section to both start
+before and end after a grace period.
 
 Here is a simple example of RCU in action:
 
@@ -1483,10 +1485,11 @@ The Grace Period Guarantee tells us that when this code runs, it will
 never end with r1 = 1 and r2 = 0.  The reasoning is as follows.  r1 = 1
 means that P0's store to x propagated to P1 before P1 called
 synchronize_rcu(), so P0's critical section must have started before
-P1's grace period.  On the other hand, r2 = 0 means that P0's store to
-y, which occurs before the end of the critical section, did not
-propagate to P1 before the end of the grace period, violating the
-Guarantee.
+P1's grace period, contrary to part (2) of the Guarantee.  On the
+other hand, r2 = 0 means that P0's store to y, which occurs before the
+end of the critical section, did not propagate to P1 before the end of
+the grace period, contrary to part (1).  Together the results violate
+the Guarantee.
 
 In the kernel's implementations of RCU, the requirements for stores
 to propagate to every CPU are fulfilled by placing strong fences at
@@ -1504,11 +1507,11 @@ before" or "ends after" a grace period?  Some aspects of the meaning
 are pretty obvious, as in the example above, but the details aren't
 entirely clear.  The LKMM formalizes this notion by means of the
 rcu-link relation.  rcu-link encompasses a very general notion of
-"before": Among other things, X ->rcu-link Z includes cases where X
-happens-before or is equal to some event Y which is equal to or comes
-before Z in the coherence order.  When Y = Z this says that X ->rfe Z
-implies X ->rcu-link Z.  In addition, when Y = X it says that X ->fr Z
-and X ->co Z each imply X ->rcu-link Z.
+"before": If E and F are RCU fence events (i.e., rcu_read_lock(),
+rcu_read_unlock(), or synchronize_rcu()) then among other things,
+E ->rcu-link F includes cases where E is po-before some memory-access
+event X, F is po-after some memory-access event Y, and we have any of
+X ->rfe Y, X ->co Y, or X ->fr Y.
 
 The formal definition of the rcu-link relation is more than a little
 obscure, and we won't give it here.  It is closely related to the pb
@@ -1516,171 +1519,173 @@ relation, and the details don't matter unless you want to comb through
 a somewhat lengthy formal proof.  Pretty much all you need to know
 about rcu-link is the information in the preceding paragraph.
 
-The LKMM also defines the gp and rscs relations.  They bring grace
-periods and read-side critical sections into the picture, in the
+The LKMM also defines the rcu-gp and rcu-rscsi relations.  They bring
+grace periods and read-side critical sections into the picture, in the
 following way:
 
-	E ->gp F means there is a synchronize_rcu() fence event S such
-	that E ->po S and either S ->po F or S = F.  In simple terms,
-	there is a grace period po-between E and F.
+	E ->rcu-gp F means that E and F are in fact the same event,
+	and that event is a synchronize_rcu() fence (i.e., a grace
+	period).
 
-	E ->rscs F means there is a critical section delimited by an
-	rcu_read_lock() fence L and an rcu_read_unlock() fence U, such
-	that E ->po U and either L ->po F or L = F.  You can think of
-	this as saying that E and F are in the same critical section
-	(in fact, it also allows E to be po-before the start of the
-	critical section and F to be po-after the end).
+	E ->rcu-rscsi F means that E and F are the rcu_read_unlock()
+	and rcu_read_lock() fence events delimiting some read-side
+	critical section.  (The 'i' at the end of the name emphasizes
+	that this relation is "inverted": It links the end of the
+	critical section to the start.)
 
 If we think of the rcu-link relation as standing for an extended
-"before", then X ->gp Y ->rcu-link Z says that X executes before a
-grace period which ends before Z executes.  (In fact it covers more
-than this, because it also includes cases where X executes before a
-grace period and some store propagates to Z's CPU before Z executes
-but doesn't propagate to some other CPU until after the grace period
-ends.)  Similarly, X ->rscs Y ->rcu-link Z says that X is part of (or
-before the start of) a critical section which starts before Z
-executes.
-
-The LKMM goes on to define the rcu-fence relation as a sequence of gp
-and rscs links separated by rcu-link links, in which the number of gp
-links is >= the number of rscs links.  For example:
+"before", then X ->rcu-gp Y ->rcu-link Z roughly says that X is a
+grace period which ends before Z begins.  (In fact it covers more than
+this, because it also includes cases where some store propagates to
+Z's CPU before Z begins but doesn't propagate to some other CPU until
+after X ends.)  Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is
+the end of a critical section which starts before Z begins.
+
+The LKMM goes on to define the rcu-fence relation as a sequence of
+rcu-gp and rcu-rscsi links separated by rcu-link links, in which the
+number of rcu-gp links is >= the number of rcu-rscsi links.  For
+example:
 
-	X ->gp Y ->rcu-link Z ->rscs T ->rcu-link U ->gp V
+	X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
 
 would imply that X ->rcu-fence V, because this sequence contains two
-gp links and only one rscs link.  (It also implies that X ->rcu-fence T
-and Z ->rcu-fence V.)  On the other hand:
+rcu-gp links and one rcu-rscsi link.  (It also implies that
+X ->rcu-fence T and Z ->rcu-fence V.)  On the other hand:
 
-	X ->rscs Y ->rcu-link Z ->rscs T ->rcu-link U ->gp V
+	X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
 
 does not imply X ->rcu-fence V, because the sequence contains only
-one gp link but two rscs links.
+one rcu-gp link but two rcu-rscsi links.
 
 The rcu-fence relation is important because the Grace Period Guarantee
 means that rcu-fence acts kind of like a strong fence.  In particular,
-if W is a write and we have W ->rcu-fence Z, the Guarantee says that W
-will propagate to every CPU before Z executes.
+E ->rcu-fence F implies not only that E begins before F ends, but also
+that any write po-before E will propagate to every CPU before any
+instruction po-after F can execute.  (However, it does not imply that
+E must execute before F; in fact, each synchronize_rcu() fence event
+is linked to itself by rcu-fence as a degenerate case.)
 
 To prove this in full generality requires some intellectual effort.
 We'll consider just a very simple case:
 
-	W ->gp X ->rcu-link Y ->rscs Z.
+	G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F.
 
-This formula means that there is a grace period G and a critical
-section C such that:
+This formula means that G and W are the same event (a grace period),
+and there are events X, Y and a read-side critical section C such that:
 
-	1. W is po-before G;
+	1. G = W is po-before or equal to X;
 
-	2. X is equal to or po-after G;
+	2. X comes "before" Y in some sense (including rfe, co and fr);
 
-	3. X comes "before" Y in some sense;
+	2. Y is po-before Z;
 
-	4. Y is po-before the end of C;
+	4. Z is the rcu_read_unlock() event marking the end of C;
 
-	5. Z is equal to or po-after the start of C.
+	5. F is the rcu_read_lock() event marking the start of C.
 
-From 2 - 4 we deduce that the grace period G ends before the critical
-section C.  Then the second part of the Grace Period Guarantee says
-not only that G starts before C does, but also that W (which executes
-on G's CPU before G starts) must propagate to every CPU before C
-starts.  In particular, W propagates to every CPU before Z executes
-(or finishes executing, in the case where Z is equal to the
-rcu_read_lock() fence event which starts C.)  This sort of reasoning
-can be expanded to handle all the situations covered by rcu-fence.
+From 1 - 4 we deduce that the grace period G ends before the critical
+section C.  Then part (2) of the Grace Period Guarantee says not only
+that G starts before C does, but also that any write which executes on
+G's CPU before G starts must propagate to every CPU before C starts.
+In particular, the write propagates to every CPU before F finishes
+executing and hence before any instruction po-after F can execute.
+This sort of reasoning can be extended to handle all the situations
+covered by rcu-fence.
 
 Finally, the LKMM defines the RCU-before (rb) relation in terms of
 rcu-fence.  This is done in essentially the same way as the pb
 relation was defined in terms of strong-fence.  We will omit the
-details; the end result is that E ->rb F implies E must execute before
-F, just as E ->pb F does (and for much the same reasons).
+details; the end result is that E ->rb F implies E must execute
+before F, just as E ->pb F does (and for much the same reasons).
 
 Putting this all together, the LKMM expresses the Grace Period
 Guarantee by requiring that the rb relation does not contain a cycle.
-Equivalently, this "rcu" axiom requires that there are no events E and
-F with E ->rcu-link F ->rcu-fence E.  Or to put it a third way, the
-axiom requires that there are no cycles consisting of gp and rscs
-alternating with rcu-link, where the number of gp links is >= the
-number of rscs links.
+Equivalently, this "rcu" axiom requires that there are no events E
+and F with E ->rcu-link F ->rcu-fence E.  Or to put it a third way,
+the axiom requires that there are no cycles consisting of rcu-gp and
+rcu-rscsi alternating with rcu-link, where the number of rcu-gp links
+is >= the number of rcu-rscsi links.
 
 Justifying the axiom isn't easy, but it is in fact a valid
 formalization of the Grace Period Guarantee.  We won't attempt to go
 through the detailed argument, but the following analysis gives a
-taste of what is involved.  Suppose we have a violation of the first
-part of the Guarantee: A critical section starts before a grace
-period, and some store propagates to the critical section's CPU before
-the end of the critical section but doesn't propagate to some other
-CPU until after the end of the grace period.
+taste of what is involved.  Suppose both parts of the Guarantee are
+violated: A critical section starts before a grace period, and some
+store propagates to the critical section's CPU before the end of the
+critical section but doesn't propagate to some other CPU until after
+the end of the grace period.
 
 Putting symbols to these ideas, let L and U be the rcu_read_lock() and
 rcu_read_unlock() fence events delimiting the critical section in
 question, and let S be the synchronize_rcu() fence event for the grace
 period.  Saying that the critical section starts before S means there
-are events E and F where E is po-after L (which marks the start of the
-critical section), E is "before" F in the sense of the rcu-link
-relation, and F is po-before the grace period S:
+are events Q and R where Q is po-after L (which marks the start of the
+critical section), Q is "before" R in the sense used by the rcu-link
+relation, and R is po-before the grace period S.  Thus we have:
 
-	L ->po E ->rcu-link F ->po S.
+	L ->rcu-link S.
 
-Let W be the store mentioned above, let Z come before the end of the
+Let W be the store mentioned above, let Y come before the end of the
 critical section and witness that W propagates to the critical
-section's CPU by reading from W, and let Y on some arbitrary CPU be a
-witness that W has not propagated to that CPU, where Y happens after
+section's CPU by reading from W, and let Z on some arbitrary CPU be a
+witness that W has not propagated to that CPU, where Z happens after
 some event X which is po-after S.  Symbolically, this amounts to:
 
-	S ->po X ->hb* Y ->fr W ->rf Z ->po U.
+	S ->po X ->hb* Z ->fr W ->rf Y ->po U.
 
-The fr link from Y to W indicates that W has not propagated to Y's CPU
-at the time that Y executes.  From this, it can be shown (see the
-discussion of the rcu-link relation earlier) that X and Z are related
-by rcu-link, yielding:
+The fr link from Z to W indicates that W has not propagated to Z's CPU
+at the time that Z executes.  From this, it can be shown (see the
+discussion of the rcu-link relation earlier) that S and U are related
+by rcu-link:
 
-	S ->po X ->rcu-link Z ->po U.
+	S ->rcu-link U.
 
-The formulas say that S is po-between F and X, hence F ->gp X.  They
-also say that Z comes before the end of the critical section and E
-comes after its start, hence Z ->rscs E.  From all this we obtain:
+Since S is a grace period we have S ->rcu-gp S, and since L and U are
+the start and end of the critical section C we have U ->rcu-rscsi L.
+From this we obtain:
 
-	F ->gp X ->rcu-link Z ->rscs E ->rcu-link F,
+	S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S,
 
 a forbidden cycle.  Thus the "rcu" axiom rules out this violation of
 the Grace Period Guarantee.
 
 For something a little more down-to-earth, let's see how the axiom
 works out in practice.  Consider the RCU code example from above, this
-time with statement labels added to the memory access instructions:
+time with statement labels added:
 
 	int x, y;
 
 	P0()
 	{
-		rcu_read_lock();
-		W: WRITE_ONCE(x, 1);
-		X: WRITE_ONCE(y, 1);
-		rcu_read_unlock();
+		L: rcu_read_lock();
+		X: WRITE_ONCE(x, 1);
+		Y: WRITE_ONCE(y, 1);
+		U: rcu_read_unlock();
 	}
 
 	P1()
 	{
 		int r1, r2;
 
-		Y: r1 = READ_ONCE(x);
-		synchronize_rcu();
-		Z: r2 = READ_ONCE(y);
+		Z: r1 = READ_ONCE(x);
+		S: synchronize_rcu();
+		W: r2 = READ_ONCE(y);
 	}
 
 
-If r2 = 0 at the end then P0's store at X overwrites the value that
-P1's load at Z reads from, so we have Z ->fre X and thus Z ->rcu-link X.
-In addition, there is a synchronize_rcu() between Y and Z, so therefore
-we have Y ->gp Z.
+If r2 = 0 at the end then P0's store at Y overwrites the value that
+P1's load at W reads from, so we have W ->fre Y.  Since S ->po W and
+also Y ->po U, we get S ->rcu-link U.  In addition, S ->rcu-gp S
+because S is a grace period.
 
-If r1 = 1 at the end then P1's load at Y reads from P0's store at W,
-so we have W ->rcu-link Y.  In addition, W and X are in the same critical
-section, so therefore we have X ->rscs W.
+If r1 = 1 at the end then P1's load at Z reads from P0's store at X,
+so we have X ->rfe Z.  Together with L ->po X and Z ->po S, this
+yields L ->rcu-link S.  And since L and U are the start and end of a
+critical section, we have U ->rcu-rscsi L.
 
-Then X ->rscs W ->rcu-link Y ->gp Z ->rcu-link X is a forbidden cycle,
-violating the "rcu" axiom.  Hence the outcome is not allowed by the
-LKMM, as we would expect.
+Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a
+forbidden cycle, violating the "rcu" axiom.  Hence the outcome is not
+allowed by the LKMM, as we would expect.
 
 For contrast, let's see what can happen in a more complicated example:
 
@@ -1690,51 +1695,52 @@ For contrast, let's see what can happen in a more complicated example:
 	{
 		int r0;
 
-		rcu_read_lock();
-		W: r0 = READ_ONCE(x);
-		X: WRITE_ONCE(y, 1);
-		rcu_read_unlock();
+		L0: rcu_read_lock();
+		    r0 = READ_ONCE(x);
+		    WRITE_ONCE(y, 1);
+		U0: rcu_read_unlock();
 	}
 
 	P1()
 	{
 		int r1;
 
-		Y: r1 = READ_ONCE(y);
-		synchronize_rcu();
-		Z: WRITE_ONCE(z, 1);
+		    r1 = READ_ONCE(y);
+		S1: synchronize_rcu();
+		    WRITE_ONCE(z, 1);
 	}
 
 	P2()
 	{
 		int r2;
 
-		rcu_read_lock();
-		U: r2 = READ_ONCE(z);
-		V: WRITE_ONCE(x, 1);
-		rcu_read_unlock();
+		L2: rcu_read_lock();
+		    r2 = READ_ONCE(z);
+		    WRITE_ONCE(x, 1);
+		U2: rcu_read_unlock();
 	}
 
 If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows
-that W ->rscs X ->rcu-link Y ->gp Z ->rcu-link U ->rscs V ->rcu-link W.
-However this cycle is not forbidden, because the sequence of relations
-contains fewer instances of gp (one) than of rscs (two).  Consequently
-the outcome is allowed by the LKMM.  The following instruction timing
-diagram shows how it might actually occur:
+that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi
+L2 ->rcu-link U0.  However this cycle is not forbidden, because the
+sequence of relations contains fewer instances of rcu-gp (one) than of
+rcu-rscsi (two).  Consequently the outcome is allowed by the LKMM.
+The following instruction timing diagram shows how it might actually
+occur:
 
 P0			P1			P2
 --------------------	--------------------	--------------------
 rcu_read_lock()
-X: WRITE_ONCE(y, 1)
-			Y: r1 = READ_ONCE(y)
+WRITE_ONCE(y, 1)
+			r1 = READ_ONCE(y)
 			synchronize_rcu() starts
 			.			rcu_read_lock()
-			.			V: WRITE_ONCE(x, 1)
-W: r0 = READ_ONCE(x)	.
+			.			WRITE_ONCE(x, 1)
+r0 = READ_ONCE(x)	.
 rcu_read_unlock()	.
 			synchronize_rcu() ends
-			Z: WRITE_ONCE(z, 1)
-						U: r2 = READ_ONCE(z)
+			WRITE_ONCE(z, 1)
+						r2 = READ_ONCE(z)
 						rcu_read_unlock()
 
 This requires P0 and P2 to execute their loads and stores out of
@@ -1744,6 +1750,15 @@ section in P0 both starts before P1's grace period does and ends
 before it does, and the critical section in P2 both starts after P1's
 grace period does and ends after it does.
 
+Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in
+addition to normal RCU.  The ideas involved are much the same as
+above, with new relations srcu-gp and srcu-rscsi added to represent
+SRCU grace periods and read-side critical sections.  There is a
+restriction on the srcu-gp and srcu-rscsi links that can appear in an
+rcu-fence sequence (the srcu-rscsi links must be paired with srcu-gp
+links having the same SRCU domain with proper nesting); the details
+are relatively unimportant.
+
 
 LOCKING
 -------
-- 
2.17.1

[PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Paul E. McKenney]

From: Luc Maranget <Luc.Maranget@inria.fr>

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting.  This check operates as follows:

   1. srcu_read_lock() creates an integer token, which is stored into
      the generated events.
   2. srcu_read_unlock() records its second (token) argument into the
      generated event.
   3. A new herd primitive 'different-values' filters out pairs of events
      with identical values from the relation passed as its argument.
   4. The bell file applies the above primitive to the (srcu)
      read-side-critical-section relation 'srcu-rscs' and flags non-empty
      results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
---
 tools/memory-model/linux-kernel.bell | 3 +++
 tools/memory-model/linux-kernel.cat  | 2 ++
 tools/memory-model/linux-kernel.def  | 2 +-
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 9c42cd9ddcb4..def9131d3d8e 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -73,3 +73,6 @@ flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
 
 (* Check for use of synchronize_srcu() inside an RCU critical section *)
 flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
+
+(* Validate SRCU dynamic match *)
+flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 8dcb37835b61..95bf45f1215f 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0+
 (*
+ * Requires herd version 7.51+6 or higher.
+ *
  * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
  * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
  * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 1d6a120cde14..0c3f0ef486f4 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
 
 // SRCU
 srcu_read_lock(X)  __srcu{srcu-lock}(X)
-srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
+srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
 synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
 
 // Atomic
-- 
2.17.1

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Andrea Parri]

On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> Hello!
> 
> This series contains updates for the Linux-kernel memory model:
> 
> 1-3.	Add SRCU support, courtesy of Alan Stern.
> 
> 4.	Update README for adding of SRCU support.
> 
> 5.	Update memory-barriers.txt on enforcing heavy ordering for
> 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> 	an ack, preferably by someone from Intel.  Matthew Wilcox
> 	posted some feedback from an Intel manual here, which might
> 	be considered to be a close substitute, but...  ;-)
> 
> 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> 
> 6.	Update Documentation/explanation.txt to include SRCU support,
> 	courtesy of Alan Stern.
> 
> 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> 	Luc Maranget.  This needs an ack.

It seems that

  1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
  
from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
considered that, IIRC, you introduced the primitive and RCU is currently
its only user.)

  Andrea


> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
>  Documentation/memory-barriers.txt                |    6 
>  tools/memory-model/Documentation/explanation.txt |  289 ++++++++++++-----------
>  tools/memory-model/README                        |   25 +
>  tools/memory-model/linux-kernel.bell             |   37 ++
>  tools/memory-model/linux-kernel.cat              |   55 ++--
>  tools/memory-model/linux-kernel.def              |    7 
>  6 files changed, 250 insertions(+), 169 deletions(-)
> 

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Paul E. McKenney]

On Thu, Jan 10, 2019 at 12:18:53AM +0100, Andrea Parri wrote:
> On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> > Hello!
> > 
> > This series contains updates for the Linux-kernel memory model:
> > 
> > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > 
> > 4.	Update README for adding of SRCU support.
> > 
> > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > 	posted some feedback from an Intel manual here, which might
> > 	be considered to be a close substitute, but...  ;-)
> > 
> > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > 
> > 6.	Update Documentation/explanation.txt to include SRCU support,
> > 	courtesy of Alan Stern.
> > 
> > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > 	Luc Maranget.  This needs an ack.
> 
> It seems that
> 
>   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
>   
> from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> considered that, IIRC, you introduced the primitive and RCU is currently
> its only user.)

That commit is in -tip:

4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")

So it has already left my -rcu tree.  ;-)

							Thanx, Paul

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Andrea Parri]

On Wed, Jan 09, 2019 at 03:40:43PM -0800, Paul E. McKenney wrote:
> On Thu, Jan 10, 2019 at 12:18:53AM +0100, Andrea Parri wrote:
> > On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> > > Hello!
> > > 
> > > This series contains updates for the Linux-kernel memory model:
> > > 
> > > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > > 
> > > 4.	Update README for adding of SRCU support.
> > > 
> > > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > > 	posted some feedback from an Intel manual here, which might
> > > 	be considered to be a close substitute, but...  ;-)
> > > 
> > > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > > 
> > > 6.	Update Documentation/explanation.txt to include SRCU support,
> > > 	courtesy of Alan Stern.
> > > 
> > > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > > 	Luc Maranget.  This needs an ack.
> > 
> > It seems that
> > 
> >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> >   
> > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > considered that, IIRC, you introduced the primitive and RCU is currently
> > its only user.)
> 
> That commit is in -tip:
> 
> 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> 
> So it has already left my -rcu tree.  ;-)

Oh, you're right: now I see the commit (e.g., with "git show"), but I
don't see the corresponding changes applied to the tree.

  https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
  https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core

Is this expected?

  Andrea


> 
> 							Thanx, Paul
> 

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Paul E. McKenney]

On Thu, Jan 10, 2019 at 01:39:52AM +0100, Andrea Parri wrote:
> On Wed, Jan 09, 2019 at 03:40:43PM -0800, Paul E. McKenney wrote:
> > On Thu, Jan 10, 2019 at 12:18:53AM +0100, Andrea Parri wrote:
> > > On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> > > > Hello!
> > > > 
> > > > This series contains updates for the Linux-kernel memory model:
> > > > 
> > > > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > > > 
> > > > 4.	Update README for adding of SRCU support.
> > > > 
> > > > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > > > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > > > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > > > 	posted some feedback from an Intel manual here, which might
> > > > 	be considered to be a close substitute, but...  ;-)
> > > > 
> > > > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > > > 
> > > > 6.	Update Documentation/explanation.txt to include SRCU support,
> > > > 	courtesy of Alan Stern.
> > > > 
> > > > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > > > 	Luc Maranget.  This needs an ack.
> > > 
> > > It seems that
> > > 
> > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > >   
> > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > its only user.)
> > 
> > That commit is in -tip:
> > 
> > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > 
> > So it has already left my -rcu tree.  ;-)
> 
> Oh, you're right: now I see the commit (e.g., with "git show"), but I
> don't see the corresponding changes applied to the tree.
> 
>   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
>   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> 
> Is this expected?

Are you asking why it is in -tip but not in mainline?  I am not sure,
but given that the merge window was over the holiday season and that
the length of the merge window proved to be shorter than many people
expected it to be, I am not too surprised.  ;-)

							Thanx, Paul

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Andrea Parri]

> > > > It seems that
> > > > 
> > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > >   
> > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > its only user.)
> > > 
> > > That commit is in -tip:
> > > 
> > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > 
> > > So it has already left my -rcu tree.  ;-)
> > 
> > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > don't see the corresponding changes applied to the tree.
> > 
> >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > 
> > Is this expected?
> 
> Are you asking why it is in -tip but not in mainline?  I am not sure,
> but given that the merge window was over the holiday season and that
> the length of the merge window proved to be shorter than many people
> expected it to be, I am not too surprised.  ;-)

Mmh, let me try again:

  $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
  $ cd tip
  $ git checkout -b locking/core origin/locking/core

  $ git show 4607abbcf464
  commit 4607abbcf464ea2be14da444215d05c73025cf6e
  Author: Andrea Parri <andrea.parri@amarulasolutions.com>
  Date:   Mon Dec 3 15:04:49 2018 -0800

      tools/memory-model: Model smp_mb__after_unlock_lock()

  $ cd tools/memory-model
  $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
  File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)

  [aka, linux-kernel.def in tip:locking/core does not have the
   smp_mb__after_unlock_lock() added by 4607abbcf464]

  Andrea


> 
> 							Thanx, Paul
> 

Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Andrea Parri]

On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote:
> From: Luc Maranget <Luc.Maranget@inria.fr>
> 
> This commit checks that the return value of srcu_read_lock() is passed
> to the matching srcu_read_unlock(), where "matching" is determined by
> nesting.  This check operates as follows:
> 
>    1. srcu_read_lock() creates an integer token, which is stored into
>       the generated events.
>    2. srcu_read_unlock() records its second (token) argument into the
>       generated event.
>    3. A new herd primitive 'different-values' filters out pairs of events
>       with identical values from the relation passed as its argument.
>    4. The bell file applies the above primitive to the (srcu)
>       read-side-critical-section relation 'srcu-rscs' and flags non-empty
>       results.
> 
> BEWARE: Works only with herd version 7.51+6 and onwards.
> 
> Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> [ paulmck: Apply Andrea Parri's off-list feedback. ]
> ---
>  tools/memory-model/linux-kernel.bell | 3 +++
>  tools/memory-model/linux-kernel.cat  | 2 ++
>  tools/memory-model/linux-kernel.def  | 2 +-
>  3 files changed, 6 insertions(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 9c42cd9ddcb4..def9131d3d8e 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -73,3 +73,6 @@ flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
>  
>  (* Check for use of synchronize_srcu() inside an RCU critical section *)
>  flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
> +
> +(* Validate SRCU dynamic match *)
> +flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 8dcb37835b61..95bf45f1215f 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -1,5 +1,7 @@
>  // SPDX-License-Identifier: GPL-2.0+
>  (*
> + * Requires herd version 7.51+6 or higher.

I'm not all that exited about spreading version requirements in the
source: we report this requirement in our README, and apparently we
already struggle to keep this information up-to-date.  So what about
squashing something like the below (assume that 7.52 will be released
by the time this patch hit mainline; if this won't be the case, we
may consider using the development version 7.51+6)? notice that this
also removes an (obsolete, at this point) comment from lock.cat.

  Andrea

diff --git a/tools/memory-model/README b/tools/memory-model/README
index 9d7d4f23503fd..b362a41358fa1 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel.
 REQUIREMENTS
 ============
 
-Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
-separately:
+Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
+downloaded separately:
 
   https://github.com/herd/herdtools7
 
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 95bf45f1215fc..8dcb37835b613 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0+
 (*
- * Requires herd version 7.51+6 or higher.
- *
  * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
  * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
  * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index 305ded17e7411..a059d1a6d8a29 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -6,9 +6,6 @@
 
 (*
  * Generate coherence orders and handle lock operations
- *
- * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48.
- * spin_is_locked() is functional from herd7 version 7.49.
  *)
 
 include "cross.cat"



> + *
>   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
>   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
>   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 1d6a120cde14..0c3f0ef486f4 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
>  
>  // SRCU
>  srcu_read_lock(X)  __srcu{srcu-lock}(X)
> -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
> +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
>  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
>  
>  // Atomic
> -- 
> 2.17.1
> 

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Paul E. McKenney]

On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > It seems that
> > > > > 
> > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > >   
> > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > its only user.)
> > > > 
> > > > That commit is in -tip:
> > > > 
> > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > 
> > > > So it has already left my -rcu tree.  ;-)
> > > 
> > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > don't see the corresponding changes applied to the tree.
> > > 
> > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > 
> > > Is this expected?
> > 
> > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > but given that the merge window was over the holiday season and that
> > the length of the merge window proved to be shorter than many people
> > expected it to be, I am not too surprised.  ;-)
> 
> Mmh, let me try again:
> 
>   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
>   $ cd tip
>   $ git checkout -b locking/core origin/locking/core
> 
>   $ git show 4607abbcf464
>   commit 4607abbcf464ea2be14da444215d05c73025cf6e
>   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
>   Date:   Mon Dec 3 15:04:49 2018 -0800
> 
>       tools/memory-model: Model smp_mb__after_unlock_lock()
> 
>   $ cd tools/memory-model
>   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
>   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> 
>   [aka, linux-kernel.def in tip:locking/core does not have the
>    smp_mb__after_unlock_lock() added by 4607abbcf464]

Color me confused:

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

$ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
$ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }

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

In addition, it handles this litmus test just fine:

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

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)
{
	WRITE_ONCE(*x, 1);
	spin_lock(mylock);
	smp_mb__after_unlock_lock();
	WRITE_ONCE(*y, 1);
	spin_unlock(mylock);
}

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

	spin_lock(mylock);
	r0 = READ_ONCE(*y);
	spin_unlock(mylock);
	r1 = READ_ONCE(*x);
}

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

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

Again, color me confused.

							Thanx, Paul

Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Paul E. McKenney]

On Thu, Jan 10, 2019 at 10:41:31AM +0100, Andrea Parri wrote:
> On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote:
> > From: Luc Maranget <Luc.Maranget@inria.fr>
> > 
> > This commit checks that the return value of srcu_read_lock() is passed
> > to the matching srcu_read_unlock(), where "matching" is determined by
> > nesting.  This check operates as follows:
> > 
> >    1. srcu_read_lock() creates an integer token, which is stored into
> >       the generated events.
> >    2. srcu_read_unlock() records its second (token) argument into the
> >       generated event.
> >    3. A new herd primitive 'different-values' filters out pairs of events
> >       with identical values from the relation passed as its argument.
> >    4. The bell file applies the above primitive to the (srcu)
> >       read-side-critical-section relation 'srcu-rscs' and flags non-empty
> >       results.
> > 
> > BEWARE: Works only with herd version 7.51+6 and onwards.
> > 
> > Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> > [ paulmck: Apply Andrea Parri's off-list feedback. ]
> > ---
> >  tools/memory-model/linux-kernel.bell | 3 +++
> >  tools/memory-model/linux-kernel.cat  | 2 ++
> >  tools/memory-model/linux-kernel.def  | 2 +-
> >  3 files changed, 6 insertions(+), 1 deletion(-)
> > 
> > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> > index 9c42cd9ddcb4..def9131d3d8e 100644
> > --- a/tools/memory-model/linux-kernel.bell
> > +++ b/tools/memory-model/linux-kernel.bell
> > @@ -73,3 +73,6 @@ flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
> >  
> >  (* Check for use of synchronize_srcu() inside an RCU critical section *)
> >  flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
> > +
> > +(* Validate SRCU dynamic match *)
> > +flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index 8dcb37835b61..95bf45f1215f 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -1,5 +1,7 @@
> >  // SPDX-License-Identifier: GPL-2.0+
> >  (*
> > + * Requires herd version 7.51+6 or higher.
> 
> I'm not all that exited about spreading version requirements in the
> source: we report this requirement in our README, and apparently we
> already struggle to keep this information up-to-date.  So what about
> squashing something like the below (assume that 7.52 will be released
> by the time this patch hit mainline; if this won't be the case, we
> may consider using the development version 7.51+6)? notice that this
> also removes an (obsolete, at this point) comment from lock.cat.

Sounds like a very good point to me!

Should have pointers in the various files to the README file?  Or maybe
get people used to using scripting that checks versions?  Or maybe
after answering questions for some time, people will get used to
checking versions?

							Thanx, Paul

>   Andrea
> 
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index 9d7d4f23503fd..b362a41358fa1 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel.
>  REQUIREMENTS
>  ============
>  
> -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
> -separately:
> +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> +downloaded separately:
>  
>    https://github.com/herd/herdtools7
>  
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 95bf45f1215fc..8dcb37835b613 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -1,7 +1,5 @@
>  // SPDX-License-Identifier: GPL-2.0+
>  (*
> - * Requires herd version 7.51+6 or higher.
> - *
>   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
>   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
>   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> index 305ded17e7411..a059d1a6d8a29 100644
> --- a/tools/memory-model/lock.cat
> +++ b/tools/memory-model/lock.cat
> @@ -6,9 +6,6 @@
>  
>  (*
>   * Generate coherence orders and handle lock operations
> - *
> - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48.
> - * spin_is_locked() is functional from herd7 version 7.49.
>   *)
>  
>  include "cross.cat"
> 
> 
> 
> > + *
> >   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > index 1d6a120cde14..0c3f0ef486f4 100644
> > --- a/tools/memory-model/linux-kernel.def
> > +++ b/tools/memory-model/linux-kernel.def
> > @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
> >  
> >  // SRCU
> >  srcu_read_lock(X)  __srcu{srcu-lock}(X)
> > -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
> > +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
> >  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
> >  
> >  // Atomic
> > -- 
> > 2.17.1
> > 
> 

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Alan Stern]

On Thu, 10 Jan 2019, Paul E. McKenney wrote:

> On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > > It seems that
> > > > > > 
> > > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > >   
> > > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > > its only user.)
> > > > > 
> > > > > That commit is in -tip:
> > > > > 
> > > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > 
> > > > > So it has already left my -rcu tree.  ;-)
> > > > 
> > > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > > don't see the corresponding changes applied to the tree.
> > > > 
> > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > > 
> > > > Is this expected?
> > > 
> > > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > > but given that the merge window was over the holiday season and that
> > > the length of the merge window proved to be shorter than many people
> > > expected it to be, I am not too surprised.  ;-)
> > 
> > Mmh, let me try again:
> > 
> >   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
> >   $ cd tip
> >   $ git checkout -b locking/core origin/locking/core
> > 
> >   $ git show 4607abbcf464
> >   commit 4607abbcf464ea2be14da444215d05c73025cf6e
> >   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
> >   Date:   Mon Dec 3 15:04:49 2018 -0800
> > 
> >       tools/memory-model: Model smp_mb__after_unlock_lock()
> > 
> >   $ cd tools/memory-model
> >   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
> >   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> > 
> >   [aka, linux-kernel.def in tip:locking/core does not have the
> >    smp_mb__after_unlock_lock() added by 4607abbcf464]
> 
> Color me confused:
> 
> ------------------------------------------------------------------------
> 
> $ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
> Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
> HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
> $ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
> smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
> 
> ------------------------------------------------------------------------
> 
> In addition, it handles this litmus test just fine:
> 
> ------------------------------------------------------------------------
> 
> 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)
> {
> 	WRITE_ONCE(*x, 1);
> 	spin_lock(mylock);
> 	smp_mb__after_unlock_lock();
> 	WRITE_ONCE(*y, 1);
> 	spin_unlock(mylock);
> }
> 
> P1(int *x, int *y, spinlock_t *mylock)
> {
> 	int r0;
> 	int r1;
> 
> 	spin_lock(mylock);
> 	r0 = READ_ONCE(*y);
> 	spin_unlock(mylock);
> 	r1 = READ_ONCE(*x);
> }
> 
> exists (1:r0=1 /\ 1:r1=0)
> 
> ------------------------------------------------------------------------
> 
> Again, color me confused.

Andrea's point is that while the 1b52d0186177 commit is present in the
tip repository, it isn't in the locking/core branch.

Alan

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Alan Stern]

On Wed, 9 Jan 2019, Paul E. McKenney wrote:

> Hello!
> 
> This series contains updates for the Linux-kernel memory model:
> 
> 1-3.	Add SRCU support, courtesy of Alan Stern.
> 
> 4.	Update README for adding of SRCU support.
> 
> 5.	Update memory-barriers.txt on enforcing heavy ordering for
> 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> 	an ack, preferably by someone from Intel.  Matthew Wilcox
> 	posted some feedback from an Intel manual here, which might
> 	be considered to be a close substitute, but...  ;-)
> 
> 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> 
> 6.	Update Documentation/explanation.txt to include SRCU support,
> 	courtesy of Alan Stern.
> 
> 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> 	Luc Maranget.  This needs an ack.

Does this one still need an ack?  If so, you may apply mine.

Alan

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Paul E. McKenney]

On Thu, Jan 10, 2019 at 10:41:23AM -0500, Alan Stern wrote:
> On Thu, 10 Jan 2019, Paul E. McKenney wrote:
> 
> > On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > > > It seems that
> > > > > > > 
> > > > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > >   
> > > > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > > > its only user.)
> > > > > > 
> > > > > > That commit is in -tip:
> > > > > > 
> > > > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > 
> > > > > > So it has already left my -rcu tree.  ;-)
> > > > > 
> > > > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > > > don't see the corresponding changes applied to the tree.
> > > > > 
> > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > > > 
> > > > > Is this expected?
> > > > 
> > > > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > > > but given that the merge window was over the holiday season and that
> > > > the length of the merge window proved to be shorter than many people
> > > > expected it to be, I am not too surprised.  ;-)
> > > 
> > > Mmh, let me try again:
> > > 
> > >   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
> > >   $ cd tip
> > >   $ git checkout -b locking/core origin/locking/core
> > > 
> > >   $ git show 4607abbcf464
> > >   commit 4607abbcf464ea2be14da444215d05c73025cf6e
> > >   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
> > >   Date:   Mon Dec 3 15:04:49 2018 -0800
> > > 
> > >       tools/memory-model: Model smp_mb__after_unlock_lock()
> > > 
> > >   $ cd tools/memory-model
> > >   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
> > >   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> > > 
> > >   [aka, linux-kernel.def in tip:locking/core does not have the
> > >    smp_mb__after_unlock_lock() added by 4607abbcf464]
> > 
> > Color me confused:
> > 
> > ------------------------------------------------------------------------
> > 
> > $ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
> > Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
> > HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
> > $ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
> > smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
> > 
> > ------------------------------------------------------------------------
> > 
> > In addition, it handles this litmus test just fine:
> > 
> > ------------------------------------------------------------------------
> > 
> > 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)
> > {
> > 	WRITE_ONCE(*x, 1);
> > 	spin_lock(mylock);
> > 	smp_mb__after_unlock_lock();
> > 	WRITE_ONCE(*y, 1);
> > 	spin_unlock(mylock);
> > }
> > 
> > P1(int *x, int *y, spinlock_t *mylock)
> > {
> > 	int r0;
> > 	int r1;
> > 
> > 	spin_lock(mylock);
> > 	r0 = READ_ONCE(*y);
> > 	spin_unlock(mylock);
> > 	r1 = READ_ONCE(*x);
> > }
> > 
> > exists (1:r0=1 /\ 1:r1=0)
> > 
> > ------------------------------------------------------------------------
> > 
> > Again, color me confused.
> 
> Andrea's point is that while the 1b52d0186177 commit is present in the
> tip repository, it isn't in the locking/core branch.

That commit is still in tip/master, so it has not been lost or
forgotten.  ;-)

							Thanx, Paul

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Paul E. McKenney]

On Thu, Jan 10, 2019 at 10:47:26AM -0500, Alan Stern wrote:
> On Wed, 9 Jan 2019, Paul E. McKenney wrote:
> 
> > Hello!
> > 
> > This series contains updates for the Linux-kernel memory model:
> > 
> > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > 
> > 4.	Update README for adding of SRCU support.
> > 
> > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > 	posted some feedback from an Intel manual here, which might
> > 	be considered to be a close substitute, but...  ;-)
> > 
> > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > 
> > 6.	Update Documentation/explanation.txt to include SRCU support,
> > 	courtesy of Alan Stern.
> > 
> > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > 	Luc Maranget.  This needs an ack.
> 
> Does this one still need an ack?  If so, you may apply mine.

Applied, thank you!

							Thanx, Paul

Re: [PATCH RFC memory-model 0/6] LKMM updates

[Andrea Parri]

On Thu, Jan 10, 2019 at 08:31:26AM -0800, Paul E. McKenney wrote:
> On Thu, Jan 10, 2019 at 10:41:23AM -0500, Alan Stern wrote:
> > On Thu, 10 Jan 2019, Paul E. McKenney wrote:
> > 
> > > On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > > > > It seems that
> > > > > > > > 
> > > > > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > > >   
> > > > > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > > > > its only user.)
> > > > > > > 
> > > > > > > That commit is in -tip:
> > > > > > > 
> > > > > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > > 
> > > > > > > So it has already left my -rcu tree.  ;-)
> > > > > > 
> > > > > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > > > > don't see the corresponding changes applied to the tree.
> > > > > > 
> > > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > > > > 
> > > > > > Is this expected?
> > > > > 
> > > > > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > > > > but given that the merge window was over the holiday season and that
> > > > > the length of the merge window proved to be shorter than many people
> > > > > expected it to be, I am not too surprised.  ;-)
> > > > 
> > > > Mmh, let me try again:
> > > > 
> > > >   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
> > > >   $ cd tip
> > > >   $ git checkout -b locking/core origin/locking/core
> > > > 
> > > >   $ git show 4607abbcf464
> > > >   commit 4607abbcf464ea2be14da444215d05c73025cf6e
> > > >   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
> > > >   Date:   Mon Dec 3 15:04:49 2018 -0800
> > > > 
> > > >       tools/memory-model: Model smp_mb__after_unlock_lock()
> > > > 
> > > >   $ cd tools/memory-model
> > > >   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
> > > >   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> > > > 
> > > >   [aka, linux-kernel.def in tip:locking/core does not have the
> > > >    smp_mb__after_unlock_lock() added by 4607abbcf464]
> > > 
> > > Color me confused:
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > $ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
> > > Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
> > > HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
> > > $ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
> > > smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > In addition, it handles this litmus test just fine:
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > 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)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	spin_lock(mylock);
> > > 	smp_mb__after_unlock_lock();
> > > 	WRITE_ONCE(*y, 1);
> > > 	spin_unlock(mylock);
> > > }
> > > 
> > > P1(int *x, int *y, spinlock_t *mylock)
> > > {
> > > 	int r0;
> > > 	int r1;
> > > 
> > > 	spin_lock(mylock);
> > > 	r0 = READ_ONCE(*y);
> > > 	spin_unlock(mylock);
> > > 	r1 = READ_ONCE(*x);
> > > }
> > > 
> > > exists (1:r0=1 /\ 1:r1=0)
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > Again, color me confused.
> > 
> > Andrea's point is that while the 1b52d0186177 commit is present in the
> > tip repository, it isn't in the locking/core branch.
> 
> That commit is still in tip/master, so it has not been lost or
> forgotten.  ;-)

Sounds reassuring!  ;-)

So, up to today, I've been using tip:locking/core as a reference for our
"almost/tentative-upstream" LKMM changes; well, your reply suggests that
I should have known better... thank you for the patience,

  Andrea


> 
> 							Thanx, Paul
> 

Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Andrea Parri]

> > I'm not all that exited about spreading version requirements in the
> > source: we report this requirement in our README, and apparently we
> > already struggle to keep this information up-to-date.  So what about
> > squashing something like the below (assume that 7.52 will be released
> > by the time this patch hit mainline; if this won't be the case, we
> > may consider using the development version 7.51+6)? notice that this
> > also removes an (obsolete, at this point) comment from lock.cat.
> 
> Sounds like a very good point to me!
> 
> Should have pointers in the various files to the README file?  Or maybe
> get people used to using scripting that checks versions?  Or maybe
> after answering questions for some time, people will get used to
> checking versions?

As discussed off-list: I have no strong opinion on this regard, well,
except that I think we ought to fix the README, somehow (consider my
diff below as a first proposal).  Akira actually preceded me on this
and suggested another solution [1].

  Andrea

[1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com


> 
> 							Thanx, Paul
> 
> >   Andrea
> > 
> > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > index 9d7d4f23503fd..b362a41358fa1 100644
> > --- a/tools/memory-model/README
> > +++ b/tools/memory-model/README
> > @@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel.
> >  REQUIREMENTS
> >  ============
> >  
> > -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
> > -separately:
> > +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> > +downloaded separately:
> >  
> >    https://github.com/herd/herdtools7
> >  
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index 95bf45f1215fc..8dcb37835b613 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -1,7 +1,5 @@
> >  // SPDX-License-Identifier: GPL-2.0+
> >  (*
> > - * Requires herd version 7.51+6 or higher.
> > - *
> >   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> > index 305ded17e7411..a059d1a6d8a29 100644
> > --- a/tools/memory-model/lock.cat
> > +++ b/tools/memory-model/lock.cat
> > @@ -6,9 +6,6 @@
> >  
> >  (*
> >   * Generate coherence orders and handle lock operations
> > - *
> > - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48.
> > - * spin_is_locked() is functional from herd7 version 7.49.
> >   *)
> >  
> >  include "cross.cat"
> > 
> > 
> > 
> > > + *
> > >   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> > >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > > index 1d6a120cde14..0c3f0ef486f4 100644
> > > --- a/tools/memory-model/linux-kernel.def
> > > +++ b/tools/memory-model/linux-kernel.def
> > > @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
> > >  
> > >  // SRCU
> > >  srcu_read_lock(X)  __srcu{srcu-lock}(X)
> > > -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
> > > +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
> > >  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
> > >  
> > >  // Atomic
> > > -- 
> > > 2.17.1
> > > 
> > 
> 

Re: [PATCH RFC LKMM 5/7] docs/memory-barriers.txt: Enforce heavy ordering for port I/O accesses

[Peter Zijlstra]

Hi PeterA,

The Cover leter has this:

> 5.	Update memory-barriers.txt on enforcing heavy ordering for
>	port-I/O accesses, courtesy of Will Deacon.  This one needs
>	an ack, preferably by someone from Intel.  Matthew Wilcox
>	posted some feedback from an Intel manual here, which might
>	be considered to be a close substitute, but...  ;-)
>
>	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org

which in turn has:

> Here's a quote from Section 18.6 of volume 1 of the Software Developer
> Manual, November 2018 edition:
> 
> When the I/O address space is used instead of memory-mapped I/O, the
> situation is different in two respects:
> • The processor never buffers I/O writes. Therefore, strict ordering of
> I/O operations is enforced by the processor. (As with memory-mapped I/O,
> it is possible for a chip set to post writes in certain I/O ranges.)
> • The processor synchronizes I/O instruction execution with external
> bus activity (see Table 18-1).
> 
> Table 18-1 says that in* delays execution of the current instruction until
> completion of pending stores, and out* delays execution of the _next_
> instruction until completion of both pending stores and the current store.

Can we give an Intel ACK on the below patch?

On Wed, Jan 09, 2019 at 01:07:46PM -0800, Paul E. McKenney wrote:
> From: Will Deacon <will.deacon@arm.com>
> 
> David Laight explains:
> 
>   | A long time ago there was a document from Intel that said that
>   | inb/outb weren't necessarily synchronised wrt memory accesses.
>   | (Might be P-pro era). However no processors actually behaved that
>   | way and more recent docs say that inb/outb are fully ordered.
> 
> This also reflects the situation on other architectures, the the port
> accessor macros tend to be implemented in terms of readX/writeX.
> 
> Update Documentation/memory-barriers.txt to reflect reality.
> 
> Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
> Cc: Arnd Bergmann <arnd@arndb.de>
> Cc: David Laight <David.Laight@ACULAB.COM>
> Cc: Alan Stern <stern@rowland.harvard.edu>
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: <linux-arch@vger.kernel.org>
> Cc: <linux-doc@vger.kernel.org>
> Cc: <linux-kernel@vger.kernel.org>
> Signed-off-by: Will Deacon <will.deacon@arm.com>
> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> ---
>  Documentation/memory-barriers.txt | 6 ++----
>  1 file changed, 2 insertions(+), 4 deletions(-)
> 
> diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
> index 1c22b21ae922..a70104e2a087 100644
> --- a/Documentation/memory-barriers.txt
> +++ b/Documentation/memory-barriers.txt
> @@ -2619,10 +2619,8 @@ functions:
>       intermediary bridges (such as the PCI host bridge) may not fully honour
>       that.
>  
> -     They are guaranteed to be fully ordered with respect to each other.
> -
> -     They are not guaranteed to be fully ordered with respect to other types of
> -     memory and I/O operation.
> +     They are guaranteed to be fully ordered with respect to each other and
> +     also with respect to other types of memory and I/O operation.
>  
>   (*) readX(), writeX():
>  
> -- 
> 2.17.1
> 

Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Paul E. McKenney]

On Fri, Jan 11, 2019 at 12:20:45AM +0100, Andrea Parri wrote:
> > > I'm not all that exited about spreading version requirements in the
> > > source: we report this requirement in our README, and apparently we
> > > already struggle to keep this information up-to-date.  So what about
> > > squashing something like the below (assume that 7.52 will be released
> > > by the time this patch hit mainline; if this won't be the case, we
> > > may consider using the development version 7.51+6)? notice that this
> > > also removes an (obsolete, at this point) comment from lock.cat.
> > 
> > Sounds like a very good point to me!
> > 
> > Should have pointers in the various files to the README file?  Or maybe
> > get people used to using scripting that checks versions?  Or maybe
> > after answering questions for some time, people will get used to
> > checking versions?
> 
> As discussed off-list: I have no strong opinion on this regard, well,
> except that I think we ought to fix the README, somehow (consider my
> diff below as a first proposal).  Akira actually preceded me on this
> and suggested another solution [1].
> 
>   Andrea
> 
> [1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com

My concern with this approach is that it seems to me to implicitly promise
that herd will provide backwards compatibility, which is a real pain to
test, let alone to provide.  Yes, the latest version of herd probably
supports latest mainline, but will five-years-from-now herd work correctly
on the .bell, .cat, and .def files from current mainline?

							Thanx, Paul

> > >   Andrea
> > > 
> > > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > > index 9d7d4f23503fd..b362a41358fa1 100644
> > > --- a/tools/memory-model/README
> > > +++ b/tools/memory-model/README
> > > @@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel.
> > >  REQUIREMENTS
> > >  ============
> > >  
> > > -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
> > > -separately:
> > > +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> > > +downloaded separately:
> > >  
> > >    https://github.com/herd/herdtools7
> > >  
> > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > > index 95bf45f1215fc..8dcb37835b613 100644
> > > --- a/tools/memory-model/linux-kernel.cat
> > > +++ b/tools/memory-model/linux-kernel.cat
> > > @@ -1,7 +1,5 @@
> > >  // SPDX-License-Identifier: GPL-2.0+
> > >  (*
> > > - * Requires herd version 7.51+6 or higher.
> > > - *
> > >   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> > >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> > > index 305ded17e7411..a059d1a6d8a29 100644
> > > --- a/tools/memory-model/lock.cat
> > > +++ b/tools/memory-model/lock.cat
> > > @@ -6,9 +6,6 @@
> > >  
> > >  (*
> > >   * Generate coherence orders and handle lock operations
> > > - *
> > > - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48.
> > > - * spin_is_locked() is functional from herd7 version 7.49.
> > >   *)
> > >  
> > >  include "cross.cat"
> > > 
> > > 
> > > 
> > > > + *
> > > >   * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> > > >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > > >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > > > index 1d6a120cde14..0c3f0ef486f4 100644
> > > > --- a/tools/memory-model/linux-kernel.def
> > > > +++ b/tools/memory-model/linux-kernel.def
> > > > @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
> > > >  
> > > >  // SRCU
> > > >  srcu_read_lock(X)  __srcu{srcu-lock}(X)
> > > > -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
> > > > +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
> > > >  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
> > > >  
> > > >  // Atomic
> > > > -- 
> > > > 2.17.1
> > > > 
> > > 
> > 
> 

Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Alan Stern]

On Fri, 11 Jan 2019, Paul E. McKenney wrote:

> On Fri, Jan 11, 2019 at 12:20:45AM +0100, Andrea Parri wrote:
> > > > I'm not all that exited about spreading version requirements in the
> > > > source: we report this requirement in our README, and apparently we
> > > > already struggle to keep this information up-to-date.  So what about
> > > > squashing something like the below (assume that 7.52 will be released
> > > > by the time this patch hit mainline; if this won't be the case, we
> > > > may consider using the development version 7.51+6)? notice that this
> > > > also removes an (obsolete, at this point) comment from lock.cat.
> > > 
> > > Sounds like a very good point to me!
> > > 
> > > Should have pointers in the various files to the README file?  Or maybe
> > > get people used to using scripting that checks versions?  Or maybe
> > > after answering questions for some time, people will get used to
> > > checking versions?
> > 
> > As discussed off-list: I have no strong opinion on this regard, well,
> > except that I think we ought to fix the README, somehow (consider my
> > diff below as a first proposal).  Akira actually preceded me on this
> > and suggested another solution [1].
> > 
> >   Andrea
> > 
> > [1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com
> 
> My concern with this approach is that it seems to me to implicitly promise
> that herd will provide backwards compatibility, which is a real pain to
> test, let alone to provide.  Yes, the latest version of herd probably
> supports latest mainline, but will five-years-from-now herd work correctly
> on the .bell, .cat, and .def files from current mainline?

The README file can say something along the lines of:

	Herd version 7.52 (later versions may or may not be 
	compatible).  Herd can be downloaded from...

Alan

Re: [PATCH RFC LKMM 5/7] docs/memory-barriers.txt: Enforce heavy ordering for port I/O accesses

[Will Deacon]

Hi Paul,

On Wed, Jan 09, 2019 at 01:07:46PM -0800, Paul E. McKenney wrote:
> From: Will Deacon <will.deacon@arm.com>
> 
> David Laight explains:
> 
>   | A long time ago there was a document from Intel that said that
>   | inb/outb weren't necessarily synchronised wrt memory accesses.
>   | (Might be P-pro era). However no processors actually behaved that
>   | way and more recent docs say that inb/outb are fully ordered.
> 
> This also reflects the situation on other architectures, the the port
> accessor macros tend to be implemented in terms of readX/writeX.
> 
> Update Documentation/memory-barriers.txt to reflect reality.
> 
> Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
> Cc: Arnd Bergmann <arnd@arndb.de>
> Cc: David Laight <David.Laight@ACULAB.COM>
> Cc: Alan Stern <stern@rowland.harvard.edu>
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: <linux-arch@vger.kernel.org>
> Cc: <linux-doc@vger.kernel.org>
> Cc: <linux-kernel@vger.kernel.org>
> Signed-off-by: Will Deacon <will.deacon@arm.com>
> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> ---
>  Documentation/memory-barriers.txt | 6 ++----
>  1 file changed, 2 insertions(+), 4 deletions(-)
> 
> diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
> index 1c22b21ae922..a70104e2a087 100644
> --- a/Documentation/memory-barriers.txt
> +++ b/Documentation/memory-barriers.txt
> @@ -2619,10 +2619,8 @@ functions:
>       intermediary bridges (such as the PCI host bridge) may not fully honour
>       that.
>  
> -     They are guaranteed to be fully ordered with respect to each other.
> -
> -     They are not guaranteed to be fully ordered with respect to other types of
> -     memory and I/O operation.
> +     They are guaranteed to be fully ordered with respect to each other and
> +     also with respect to other types of memory and I/O operation.

Given the lack of Intel response here, I went away to do some digging.
As evidenced by the commit message, there is certainly an understanding
amongst some developers that inX/outX() are strongly ordered on x86 and
this was re-enforced by Linus in March last year:

https://www.mail-archive.com/linuxppc-dev@lists.ozlabs.org/msg131212.html

It was this information on which I based my patch. The Intel SDM is not
quite as assertive in its claims.

However, it has also occurred to me that this patch is actually missing
the point. memory-barriers.txt should be documenting the *Linux* memory
model, not the x86 one, and so the port accessors should be defined to
have the same ordering semantics as the MMIO accessors. If this wasn't
the case, then macros such as ioreadX() and iowriteX() would be unusable
in portable driver code. The inX/outX implementation in asm-generic would
also be bogus, despite being widely used.

Unfortunately, the whole "KERNEL I/O BARRIER EFFECTS" section in
memory-barriers.txt is vague, x86-centric and out of date. I think the
best way forward is for me to propose a rewrite of that section, based
on the work I did putting together my I/O ordering talk at ELCE last
year. That, at least, will allow us to start off with a portable
semantics rather than trying to infer the details from CPU manuals.

So please drop this for now, and I'll send out a more involved RFC patch
shortly with the usual suspects on cc.

Cheers,

Will

Re: [PATCH RFC LKMM 5/7] docs/memory-barriers.txt: Enforce heavy ordering for port I/O accesses

[Arnd Bergmann]

On Mon, Feb 11, 2019 at 4:30 PM Will Deacon <will.deacon@arm.com> wrote:

> Given the lack of Intel response here, I went away to do some digging.
> As evidenced by the commit message, there is certainly an understanding
> amongst some developers that inX/outX() are strongly ordered on x86 and
> this was re-enforced by Linus in March last year:
>
> https://www.mail-archive.com/linuxppc-dev@lists.ozlabs.org/msg131212.html
>
> It was this information on which I based my patch. The Intel SDM is not
> quite as assertive in its claims.
>
> However, it has also occurred to me that this patch is actually missing
> the point. memory-barriers.txt should be documenting the *Linux* memory
> model, not the x86 one, and so the port accessors should be defined to
> have the same ordering semantics as the MMIO accessors. If this wasn't
> the case, then macros such as ioreadX() and iowriteX() would be unusable
> in portable driver code.

My interpretation of the ioreadX() and iowriteX() semantics is that they
only guarantee readl()/writel() barrier semantics, even though they
may in fact provide stronger barriers for PIO on architectures that use
CONFIG_GENERIC_IOMAP (which falls back to inX()/outX()).

> The inX/outX implementation in asm-generic would
> also be bogus, despite being widely used.

They likely are. The asm-generic files tend to provide a generic
abstraction as much as that is possible, but without having access
to the architecture specific semantics, they raditionally don't know
what should be done here. We now have __io_pbw()/__io_paw()/
__io_pbr()/__io_par() to let architectures get it right, but that is
a fairly recent addition, so nothing other than riscv defines them
today.
To make things worse, a lot of machines are unable to provide
__io_paw(), e.g. when all bus writes are posted.

      Arnd

Re: [PATCH RFC LKMM 5/7] docs/memory-barriers.txt: Enforce heavy ordering for port I/O accesses

[Will Deacon]

Hi Arnd,

On Mon, Feb 11, 2019 at 06:11:48PM +0100, Arnd Bergmann wrote:
> On Mon, Feb 11, 2019 at 4:30 PM Will Deacon <will.deacon@arm.com> wrote:
> 
> > Given the lack of Intel response here, I went away to do some digging.
> > As evidenced by the commit message, there is certainly an understanding
> > amongst some developers that inX/outX() are strongly ordered on x86 and
> > this was re-enforced by Linus in March last year:
> >
> > https://www.mail-archive.com/linuxppc-dev@lists.ozlabs.org/msg131212.html
> >
> > It was this information on which I based my patch. The Intel SDM is not
> > quite as assertive in its claims.
> >
> > However, it has also occurred to me that this patch is actually missing
> > the point. memory-barriers.txt should be documenting the *Linux* memory
> > model, not the x86 one, and so the port accessors should be defined to
> > have the same ordering semantics as the MMIO accessors. If this wasn't
> > the case, then macros such as ioreadX() and iowriteX() would be unusable
> > in portable driver code.
> 
> My interpretation of the ioreadX() and iowriteX() semantics is that they
> only guarantee readl()/writel() barrier semantics, even though they
> may in fact provide stronger barriers for PIO on architectures that use
> CONFIG_GENERIC_IOMAP (which falls back to inX()/outX()).
> 
> > The inX/outX implementation in asm-generic would
> > also be bogus, despite being widely used.
> 
> They likely are. The asm-generic files tend to provide a generic
> abstraction as much as that is possible, but without having access
> to the architecture specific semantics, they raditionally don't know
> what should be done here. We now have __io_pbw()/__io_paw()/
> __io_pbr()/__io_par() to let architectures get it right, but that is
> a fairly recent addition, so nothing other than riscv defines them
> today.
> To make things worse, a lot of machines are unable to provide
> __io_paw(), e.g. when all bus writes are posted.

So I've just sent an RFC (you're on cc) that attempts to rewrite this part
of memory-barriers.txt to reflect reality. Hopefully that can act as a
starting point for discussion if we decide we want to change the documented
behaviour and/or implementation.

Will