linux-kernel.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [PATCH tip/core/rcu 01/21] tools/memory-model: Make scripts be executable
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 02/21] tools/memory-model: Fix comment in MP+poonceonces.litmus Paul E. McKenney
                   ` (19 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit simplifies life a bit by making all of the scripts in
tools/memory-model/scripts be executable.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/checkghlitmus.sh   | 0
 tools/memory-model/scripts/checklitmushist.sh | 0
 tools/memory-model/scripts/cmplitmushist.sh   | 0
 tools/memory-model/scripts/initlitmushist.sh  | 0
 tools/memory-model/scripts/judgelitmus.sh     | 0
 tools/memory-model/scripts/newlitmushist.sh   | 0
 tools/memory-model/scripts/parseargs.sh       | 0
 tools/memory-model/scripts/runlitmushist.sh   | 0
 8 files changed, 0 insertions(+), 0 deletions(-)
 mode change 100644 => 100755 tools/memory-model/scripts/checkghlitmus.sh
 mode change 100644 => 100755 tools/memory-model/scripts/checklitmushist.sh
 mode change 100644 => 100755 tools/memory-model/scripts/cmplitmushist.sh
 mode change 100644 => 100755 tools/memory-model/scripts/initlitmushist.sh
 mode change 100644 => 100755 tools/memory-model/scripts/judgelitmus.sh
 mode change 100644 => 100755 tools/memory-model/scripts/newlitmushist.sh
 mode change 100644 => 100755 tools/memory-model/scripts/parseargs.sh
 mode change 100644 => 100755 tools/memory-model/scripts/runlitmushist.sh

diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
old mode 100644
new mode 100755
-- 
2.17.1


^ permalink raw reply	[flat|nested] 28+ messages in thread

* [PATCH RFC memory-model 0/21] LKMM updates for review
@ 2019-03-26 23:41 Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 01/21] tools/memory-model: Make scripts be executable Paul E. McKenney
                   ` (20 more replies)
  0 siblings, 21 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks

Hello!

This series contains LKMM updates:

1.	Make scripts be executable.

2.	Fix comment in MP+poonceonces.litmus, courtesy of Andrea Parri.

3.	Do not use "herd" to refer to "herd7", courtesy of Andrea Parri.

4.	Rewrite "KERNEL I/O BARRIER EFFECTS" section of memory-barriers.txt,
	courtesy of Will Deacon.

5-6.	Make LKMM scripts note timeouts instead of just saying that
	the validation was bad.

7.	Make LKMM scripts identify litmus-test typos and use of
	unsupported primitives instead of just saying that the validation
	was bad.

8.	Add support for synchronize_srcu_expedited().

9.	Make LKMM scripts detect unconditional deadlocks.

10-21.	Leverage Boqun Feng's C-to-assembly litmus-test-translation
	capability to allow verifying LKMM against hardware models
	for checkalllitmus.sh.  This is a work in progress.

							Thanx, Paul

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

 Documentation/memory-barriers.txt                     |  115 +++++++++------
 tools/memory-model/linux-kernel.def                   |    1 
 tools/memory-model/litmus-tests/.gitignore            |    4 
 tools/memory-model/litmus-tests/MP+poonceonces.litmus |    2 
 tools/memory-model/litmus-tests/README                |    2 
 tools/memory-model/lock.cat                           |    2 
 tools/memory-model/scripts/README                     |   12 -
 tools/memory-model/scripts/checkalllitmus.sh          |   29 +--
 tools/memory-model/scripts/checklitmus.sh             |  101 +++++--------
 tools/memory-model/scripts/cmplitmushist.sh           |   53 ++++++
 tools/memory-model/scripts/judgelitmus.sh             |  114 +++++++++++---
 tools/memory-model/scripts/parseargs.sh               |   11 +
 tools/memory-model/scripts/runlitmus.sh               |  137 ++++++++++++++----
 tools/memory-model/scripts/runlitmushist.sh           |    3 
 tools/memory-model/scripts/simpletest.sh              |   35 ++++
 15 files changed, 425 insertions(+), 196 deletions(-)


^ permalink raw reply	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 02/21] tools/memory-model: Fix comment in MP+poonceonces.litmus
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 01/21] tools/memory-model: Make scripts be executable Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 03/21] tools/memory-model: Do not use "herd" to refer to "herd7" Paul E. McKenney
                   ` (18 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney,
	Daniel Lustig

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

The comment should say "Sometimes" for the result.

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

diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index b2b60b84fb9d..172f0145301c 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -1,7 +1,7 @@
 C MP+poonceonces
 
 (*
- * Result: Maybe
+ * Result: Sometimes
  *
  * Can the counter-intuitive message-passing outcome be prevented with
  * no ordering at all?
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 03/21] tools/memory-model: Do not use "herd" to refer to "herd7"
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 01/21] tools/memory-model: Make scripts be executable Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 02/21] tools/memory-model: Fix comment in MP+poonceonces.litmus Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section Paul E. McKenney
                   ` (17 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney,
	Daniel Lustig

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

Use "herd7" in each such reference.

Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will.deacon@arm.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/litmus-tests/README       | 2 +-
 tools/memory-model/lock.cat                  | 2 +-
 tools/memory-model/scripts/README            | 4 ++--
 tools/memory-model/scripts/checkalllitmus.sh | 2 +-
 tools/memory-model/scripts/checklitmus.sh    | 2 +-
 tools/memory-model/scripts/parseargs.sh      | 2 +-
 tools/memory-model/scripts/runlitmushist.sh  | 2 +-
 7 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 5ee08f129094..681f9067fa9e 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -244,7 +244,7 @@ produce the name:
 Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus
 
 The descriptors that describe connections between consecutive accesses
-within the cycle through a given litmus test can be provided by the herd
+within the cycle through a given litmus test can be provided by the herd7
 tool (Rfi, Po, Fre, and so on) or by the linux-kernel.bell file (Once,
 Release, Acquire, and so on).
 
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index a059d1a6d8a2..6b52f365d73a 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -11,7 +11,7 @@
 include "cross.cat"
 
 (*
- * The lock-related events generated by herd are as follows:
+ * The lock-related events generated by herd7 are as follows:
  *
  * LKR		Lock-Read: the read part of a spin_lock() or successful
  *			spin_trylock() read-modify-write event pair
diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
index 29375a1fbbfa..095c7eb36f9f 100644
--- a/tools/memory-model/scripts/README
+++ b/tools/memory-model/scripts/README
@@ -22,7 +22,7 @@ checklitmushist.sh
 
 	Run all litmus tests having .litmus.out files from previous
 	initlitmushist.sh or newlitmushist.sh runs, comparing the
-	herd output to that of the original runs.
+	herd7 output to that of the original runs.
 
 checklitmus.sh
 
@@ -43,7 +43,7 @@ initlitmushist.sh
 
 judgelitmus.sh
 
-	Given a .litmus file and its .litmus.out herd output, check the
+	Given a .litmus file and its .litmus.out herd7 output, check the
 	.litmus.out file against the .litmus file's "Result:" comment to
 	judge whether the test ran correctly.  Not normally run manually,
 	provided instead for use by other scripts.
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index b35fcd61ecf6..3c0c7fbbd223 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -1,7 +1,7 @@
 #!/bin/sh
 # SPDX-License-Identifier: GPL-2.0+
 #
-# Run herd tests on all .litmus files in the litmus-tests directory
+# Run herd7 tests on all .litmus files in the litmus-tests directory
 # and check each file's result against a "Result:" comment within that
 # litmus test.  If the verification result does not match that specified
 # in the litmus test, this script prints an error message prefixed with
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index dd08801a30b0..11461ed40b5e 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -1,7 +1,7 @@
 #!/bin/sh
 # SPDX-License-Identifier: GPL-2.0+
 #
-# Run a herd test and invokes judgelitmus.sh to check the result against
+# Run a herd7 test and invokes judgelitmus.sh to check the result against
 # a "Result:" comment within the litmus test.  It also outputs verification
 # results to a file whose name is that of the specified litmus test, but
 # with ".out" appended.
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 859e1d581e05..40f52080fdbd 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -91,7 +91,7 @@ do
 		shift
 		;;
 	--herdopts|--herdopt)
-		checkarg --destdir "(herd options)" "$#" "$2" '.*' '^--'
+		checkarg --destdir "(herd7 options)" "$#" "$2" '.*' '^--'
 		LKMM_HERD_OPTIONS="$2"
 		shift
 		;;
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
index e507f5f933d5..6ed376f495bb 100755
--- a/tools/memory-model/scripts/runlitmushist.sh
+++ b/tools/memory-model/scripts/runlitmushist.sh
@@ -79,7 +79,7 @@ then
 	echo ' ---' Summary: 1>&2
 	grep '!!!' $T/*.sh.out 1>&2
 	nfail="`grep '!!!' $T/*.sh.out | wc -l`"
-	echo 'Number of failed herd runs (e.g., timeout): ' $nfail 1>&2
+	echo 'Number of failed herd7 runs (e.g., timeout): ' $nfail 1>&2
 	exit 1
 else
 	echo All runs completed successfully. 1>&2
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (2 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 03/21] tools/memory-model: Do not use "herd" to refer to "herd7" Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-04-02 13:03   ` Will Deacon
  2019-03-26 23:41 ` [PATCH tip/core/rcu 05/21] tools/memory-model: Make judgelitmus.sh note timeouts Paul E. McKenney
                   ` (16 subsequent siblings)
  20 siblings, 1 reply; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney,
	Benjamin Herrenschmidt, Michael Ellerman, Arnd Bergmann,
	Palmer Dabbelt, Daniel Lustig, Linus Torvalds, Maciej W. Rozycki,
	Mikulas Patocka

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

The "KERNEL I/O BARRIER EFFECTS" section of memory-barriers.txt is vague,
x86-centric, out-of-date, incomplete and demonstrably incorrect in places.
This is largely because I/O ordering is a horrible can of worms, but also
because the document has stagnated as our understanding has evolved.

Attempt to address some of that, by rewriting the section based on
recent(-ish) discussions with Arnd, BenH and others. Maybe one day we'll
find a way to formalise this stuff, but for now let's at least try to
make the English easier to understand.

Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
Cc: Michael Ellerman <mpe@ellerman.id.au>
Cc: Arnd Bergmann <arnd@arndb.de>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Andrea Parri <andrea.parri@amarulasolutions.com>
Cc: Palmer Dabbelt <palmer@sifive.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: "Maciej W. Rozycki" <macro@linux-mips.org>
Cc: Mikulas Patocka <mpatocka@redhat.com>
Signed-off-by: Will Deacon <will.deacon@arm.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 Documentation/memory-barriers.txt | 115 ++++++++++++++++++------------
 1 file changed, 70 insertions(+), 45 deletions(-)

diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 1c22b21ae922..158947ae78c2 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -2599,72 +2599,97 @@ likely, then interrupt-disabling locks should be used to guarantee ordering.
 KERNEL I/O BARRIER EFFECTS
 ==========================
 
-When accessing I/O memory, drivers should use the appropriate accessor
-functions:
+Interfacing with peripherals via I/O accesses is deeply architecture and device
+specific. Therefore, drivers which are inherently non-portable may rely on
+specific behaviours of their target systems in order to achieve synchronization
+in the most lightweight manner possible. For drivers intending to be portable
+between multiple architectures and bus implementations, the kernel offers a
+series of accessor functions that provide various degrees of ordering
+guarantees:
 
- (*) inX(), outX():
+ (*) readX(), writeX():
 
-     These are intended to talk to I/O space rather than memory space, but
-     that's primarily a CPU-specific concept.  The i386 and x86_64 processors
-     do indeed have special I/O space access cycles and instructions, but many
-     CPUs don't have such a concept.
+     The readX() and writeX() MMIO accessors take a pointer to the peripheral
+     being accessed as an __iomem * parameter. For pointers mapped with the
+     default I/O attributes (e.g. those returned by ioremap()), then the
+     ordering guarantees are as follows:
 
-     The PCI bus, amongst others, defines an I/O space concept which - on such
-     CPUs as i386 and x86_64 - readily maps to the CPU's concept of I/O
-     space.  However, it may also be mapped as a virtual I/O space in the CPU's
-     memory map, particularly on those CPUs that don't support alternate I/O
-     spaces.
+     1. All readX() and writeX() accesses to the same peripheral are ordered
+        with respect to each other. For example, this ensures that MMIO register
+	writes by the CPU to a particular device will arrive in program order.
 
-     Accesses to this space may be fully synchronous (as on i386), but
-     intermediary bridges (such as the PCI host bridge) may not fully honour
-     that.
+     2. A writeX() by the CPU to the peripheral will first wait for the
+        completion of all prior CPU writes to memory. For example, this ensures
+        that writes by the CPU to an outbound DMA buffer allocated by
+        dma_alloc_coherent() will be visible to a DMA engine when the CPU writes
+        to its MMIO control register to trigger the transfer.
 
-     They are guaranteed to be fully ordered with respect to each other.
+     3. A readX() by the CPU from the peripheral will complete before any
+	subsequent CPU reads from memory can begin. For example, this ensures
+	that reads by the CPU from an incoming DMA buffer allocated by
+	dma_alloc_coherent() will not see stale data after reading from the DMA
+	engine's MMIO status register to establish that the DMA transfer has
+	completed.
 
-     They are not guaranteed to be fully ordered with respect to other types of
-     memory and I/O operation.
+     4. A readX() by the CPU from the peripheral will complete before any
+	subsequent delay() loop can begin execution. For example, this ensures
+	that two MMIO register writes by the CPU to a peripheral will arrive at
+	least 1us apart if the first write is immediately read back with readX()
+	and udelay(1) is called prior to the second writeX().
 
- (*) readX(), writeX():
+     __iomem pointers obtained with non-default attributes (e.g. those returned
+     by ioremap_wc()) are unlikely to provide many of these guarantees.
 
-     Whether these are guaranteed to be fully ordered and uncombined with
-     respect to each other on the issuing CPU depends on the characteristics
-     defined for the memory window through which they're accessing.  On later
-     i386 architecture machines, for example, this is controlled by way of the
-     MTRR registers.
+ (*) readX_relaxed(), writeX_relaxed():
 
-     Ordinarily, these will be guaranteed to be fully ordered and uncombined,
-     provided they're not accessing a prefetchable device.
+     These are similar to readX() and writeX(), but provide weaker memory
+     ordering guarantees. Specifically, they do not guarantee ordering with
+     respect to normal memory accesses or delay() loops (i.e bullets 2-4 above)
+     but they are still guaranteed to be ordered with respect to other accesses
+     to the same peripheral when operating on __iomem pointers mapped with the
+     default I/O attributes.
 
-     However, intermediary hardware (such as a PCI bridge) may indulge in
-     deferral if it so wishes; to flush a store, a load from the same location
-     is preferred[*], but a load from the same device or from configuration
-     space should suffice for PCI.
+ (*) readsX(), writesX():
 
-     [*] NOTE! attempting to load from the same location as was written to may
-	 cause a malfunction - consider the 16550 Rx/Tx serial registers for
-	 example.
+     The readsX() and writesX() MMIO accessors are designed for accessing
+     register-based, memory-mapped FIFOs residing on peripherals that are not
+     capable of performing DMA. Consequently, they provide only the ordering
+     guarantees of readX_relaxed() and writeX_relaxed(), as documented above.
 
-     Used with prefetchable I/O memory, an mmiowb() barrier may be required to
-     force stores to be ordered.
+ (*) inX(), outX():
 
-     Please refer to the PCI specification for more information on interactions
-     between PCI transactions.
+     The inX() and outX() accessors are intended to access legacy port-mapped
+     I/O peripherals, which may require special instructions on some
+     architectures (notably x86). The port number of the peripheral being
+     accessed is passed as an argument.
 
- (*) readX_relaxed(), writeX_relaxed()
+     Since many CPU architectures ultimately access these peripherals via an
+     internal virtual memory mapping, the portable ordering guarantees provided
+     by inX() and outX() are the same as those provided by readX() and writeX()
+     respectively when accessing a mapping with the default I/O attributes.
 
-     These are similar to readX() and writeX(), but provide weaker memory
-     ordering guarantees.  Specifically, they do not guarantee ordering with
-     respect to normal memory accesses (e.g. DMA buffers) nor do they guarantee
-     ordering with respect to LOCK or UNLOCK operations.  If the latter is
-     required, an mmiowb() barrier can be used.  Note that relaxed accesses to
-     the same peripheral are guaranteed to be ordered with respect to each
-     other.
+     Device drivers may expect outX() to emit a non-posted write transaction
+     that waits for a completion response from the I/O peripheral before
+     returning. This is not guaranteed by all architectures and is therefore
+     not part of the portable ordering semantics.
+
+ (*) insX(), outsX():
+
+     As above, the insX() and outX() accessors provide the same ordering
+     guarantees as readsX() and writesX() respectively when accessing a mapping
+     with the default I/O attributes.
 
  (*) ioreadX(), iowriteX()
 
      These will perform appropriately for the type of access they're actually
      doing, be it inX()/outX() or readX()/writeX().
 
+All of these accessors assume that the underlying peripheral is little-endian,
+and will therefore perform byte-swapping operations on big-endian architectures.
+
+Composing I/O ordering barriers with SMP ordering barriers and LOCK/UNLOCK
+operations is a dangerous sport which may require the use of mmiowb(). See the
+subsection "Acquires vs I/O accesses" for more information.
 
 ========================================
 ASSUMED MINIMUM EXECUTION ORDERING MODEL
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 05/21] tools/memory-model: Make judgelitmus.sh note timeouts
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (3 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 06/21] tools/memory-model: Make cmplitmushist.sh " Paul E. McKenney
                   ` (15 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

Currently, judgelitmus.sh treats timeouts (as in the "--timeout" argument)
as "!!! Verification error".  This can be misleading because it is quite
possible that running the test longer would have produced a verification.
This commit therefore changes judgelitmus.sh to check for timeouts and
to report them with "!!! Timeout".

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/judgelitmus.sh | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 0cc63875e395..d3c313b9a458 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -42,6 +42,14 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out
 if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
 then
 	:
+elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out
+then
+	echo ' !!! Timeout' $litmus
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	then
+		echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1
+	fi
+	exit 124
 else
 	echo ' !!! Verification error' $litmus
 	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 06/21] tools/memory-model: Make cmplitmushist.sh note timeouts
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (4 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 05/21] tools/memory-model: Make judgelitmus.sh note timeouts Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 07/21] tools/memory-model: Make judgelitmus.sh identify bad macros Paul E. McKenney
                   ` (14 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

Currently, cmplitmushist.sh treats timeouts (as in the "--timeout"
argument) as "Missing Observation line".  This can be misleading because
it is quite possible that running the test longer would have produced
a verification.  This commit therefore changes cmplitmushist.sh to check
for timeouts and to report them with "Timed out".

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/cmplitmushist.sh | 22 +++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
index 0f498aeeccf5..b9c174dd8004 100755
--- a/tools/memory-model/scripts/cmplitmushist.sh
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -12,12 +12,30 @@ trap 'rm -rf $T' 0
 mkdir $T
 
 # comparetest oldpath newpath
+timedout=0
 perfect=0
 obsline=0
 noobsline=0
 obsresult=0
 badcompare=0
 comparetest () {
+	if grep -q '^Command exited with non-zero status 124' $1 ||
+	   grep -q '^Command exited with non-zero status 124' $2
+	then
+		if grep -q '^Command exited with non-zero status 124' $1 &&
+		   grep -q '^Command exited with non-zero status 124' $2
+		then
+			echo Both runs timed out: $2
+		elif grep -q '^Command exited with non-zero status 124' $1
+		then
+			echo Old run timed out: $2
+		elif grep -q '^Command exited with non-zero status 124' $2
+		then
+			echo New run timed out: $2
+		fi
+		timedout=`expr "$timedout" + 1`
+		return 0
+	fi
 	grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout
 	grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout
 	if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1
@@ -78,6 +96,10 @@ if test "$obsresult" -ne 0
 then
 	echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2
 fi
+if test "$timedout" -ne 0
+then
+	echo "!!!" Timed out: $timedout 1>&2
+fi
 if test "$badcompare" -ne 0
 then
 	echo "!!!" Result changed: $badcompare 1>&2
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 07/21] tools/memory-model: Make judgelitmus.sh identify bad macros
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (5 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 06/21] tools/memory-model: Make cmplitmushist.sh " Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited() Paul E. McKenney
                   ` (13 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

Currently, judgelitmus.sh treats use of unknown primitives (such as
srcu_read_lock() prior to SRCU support) as "!!! Verification error".
This can be misleading because it fails to call out typos and running
a version LKMM on a litmus test requiring a feature not provided by
that version.  This commit therefore changes judgelitmus.sh to check
for unknown primitives and to report them, for example, with:

	'!!! Current LKMM version does not know "rcu_write_lock"'.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/cmplitmushist.sh | 31 ++++++++++++++++++---
 tools/memory-model/scripts/judgelitmus.sh   | 12 ++++++++
 2 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
index b9c174dd8004..ca1ac8b64614 100755
--- a/tools/memory-model/scripts/cmplitmushist.sh
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -12,6 +12,7 @@ trap 'rm -rf $T' 0
 mkdir $T
 
 # comparetest oldpath newpath
+badmacnam=0
 timedout=0
 perfect=0
 obsline=0
@@ -19,8 +20,26 @@ noobsline=0
 obsresult=0
 badcompare=0
 comparetest () {
-	if grep -q '^Command exited with non-zero status 124' $1 ||
-	   grep -q '^Command exited with non-zero status 124' $2
+	if grep -q ': Unknown macro ' $1 || grep -q ': Unknown macro ' $2
+	then
+		if grep -q ': Unknown macro ' $1
+		then
+			badname=`grep ': Unknown macro ' $1 |
+				sed -e 's/^.*: Unknown macro //' |
+				sed -e 's/ (User error).*$//'`
+			echo 'Current LKMM version does not know "'$badname'"' $1
+		fi
+		if grep -q ': Unknown macro ' $2
+		then
+			badname=`grep ': Unknown macro ' $2 |
+				sed -e 's/^.*: Unknown macro //' |
+				sed -e 's/ (User error).*$//'`
+			echo 'Current LKMM version does not know "'$badname'"' $2
+		fi
+		badmacnam=`expr "$badmacnam" + 1`
+		return 0
+	elif grep -q '^Command exited with non-zero status 124' $1 ||
+	     grep -q '^Command exited with non-zero status 124' $2
 	then
 		if grep -q '^Command exited with non-zero status 124' $1 &&
 		   grep -q '^Command exited with non-zero status 124' $2
@@ -56,7 +75,7 @@ comparetest () {
 			return 0
 		fi
 	else
-		echo Missing Observation line "(e.g., herd7 timeout)": $2
+		echo Missing Observation line "(e.g., syntax error)": $2
 		noobsline=`expr "$noobsline" + 1`
 		return 0
 	fi
@@ -90,7 +109,7 @@ then
 fi
 if test "$noobsline" -ne 0
 then
-	echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2
+	echo Missing Observation line "(e.g., syntax error)": $noobsline 1>&2
 fi
 if test "$obsresult" -ne 0
 then
@@ -100,6 +119,10 @@ if test "$timedout" -ne 0
 then
 	echo "!!!" Timed out: $timedout 1>&2
 fi
+if test "$badmacnam" -ne 0
+then
+	echo "!!!" Unknown primitive: $badmacnam 1>&2
+fi
 if test "$badcompare" -ne 0
 then
 	echo "!!!" Result changed: $badcompare 1>&2
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index d3c313b9a458..d40439c7b71e 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -42,6 +42,18 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out
 if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
 then
 	:
+elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out
+then
+	badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out |
+		sed -e 's/^.*: Unknown macro //' |
+		sed -e 's/ (User error).*$//'`
+	badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"
+	echo $badmsg
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	then
+		echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1
+	fi
+	exit 254
 elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out
 then
 	echo ' !!! Timeout' $litmus
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited()
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (6 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 07/21] tools/memory-model: Make judgelitmus.sh identify bad macros Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-04-02 14:49   ` Andrea Parri
  2019-03-26 23:41 ` [PATCH tip/core/rcu 09/21] tools/memory-model: Make judgelitmus.sh detect hard deadlocks Paul E. McKenney
                   ` (12 subsequent siblings)
  20 siblings, 1 reply; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

Given that synchronize_rcu_expedited() is supported, this commit adds
support for synchronize_srcu_expedited().

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/linux-kernel.def | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 0c3f0ef486f4..551eeaa389d4 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -51,6 +51,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
 srcu_read_lock(X)  __srcu{srcu-lock}(X)
 srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
 synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
+synchronize_srcu_expedited(X)  { __srcu{sync-srcu}(X); }
 
 // Atomic
 atomic_read(X) READ_ONCE(*X)
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 09/21] tools/memory-model: Make judgelitmus.sh detect hard deadlocks
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (7 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited() Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 10/21] tools/memory-model: Update parseargs.sh for hardware verification Paul E. McKenney
                   ` (11 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

If a litmus test specifies "Result: Never" and if it contains an
unconditional ("hard") deadlock, then running checklitmus.sh on it will
not flag any errors, despite the fact that there are no executions.
This commit therefore updates judgelitmus.sh to complain about tests
with no executions that are marked, but not as "Result: DEADLOCK".

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/judgelitmus.sh | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index d40439c7b71e..84c62eee321b 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -83,6 +83,14 @@ then
 		fi
 		ret=1
 	fi
+elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+then
+	echo " !!! Unexpected non-$outcome deadlock" $litmus
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	then
+		echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+	fi
+	ret=1
 elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
 then
 	ret=0
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 10/21] tools/memory-model: Update parseargs.sh for hardware verification
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (8 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 09/21] tools/memory-model: Make judgelitmus.sh detect hard deadlocks Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 11/21] tools/memory-model: Make judgelitmus.sh handle hardware verifications Paul E. McKenney
                   ` (10 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit adds a --hw argument to parseargs.sh to specify the CPU
family for a hardware verification.  For example, "--hw AArch64" will
specify that a C-language litmus test is to be translated to ARMv8 and
the result verified.  This will set the LKMM_HW_MAP_FILE environment
variable accordingly.  If there is no --hw argument, this environment
variable will be set to the empty string.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/parseargs.sh | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 40f52080fdbd..0dd087a8410e 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -27,6 +27,7 @@ initparam () {
 
 initparam LKMM_DESTDIR "."
 initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg"
+initparam LKMM_HW_MAP_FILE ""
 initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN`
 initparam LKMM_PROCS "3"
 initparam LKMM_TIMEOUT "1m"
@@ -37,10 +38,11 @@ usagehelp () {
 	echo "Usage $scriptname [ arguments ]"
 	echo "      --destdir path (place for .litmus.out, default by .litmus)"
 	echo "      --herdopts -conf linux-kernel.cfg ..."
+	echo "      --hw AArch64"
 	echo "      --jobs N (number of jobs, default one per CPU)"
 	echo "      --procs N (litmus tests with at most this many processes)"
 	echo "      --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')"
-	echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
+	echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --hw '$LKMM_HW_MAP_FILE' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
 	exit 1
 }
 
@@ -95,6 +97,11 @@ do
 		LKMM_HERD_OPTIONS="$2"
 		shift
 		;;
+	--hw)
+		checkarg --hw "(.map file architecture name)" "$#" "$2" '^[A-Za-z0-9_-]\+' '^--'
+		LKMM_HW_MAP_FILE="$2"
+		shift
+		;;
 	-j[1-9]*)
 		njobs="`echo $1 | sed -e 's/^-j//'`"
 		trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`"
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 11/21] tools/memory-model: Make judgelitmus.sh handle hardware verifications
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (9 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 10/21] tools/memory-model: Update parseargs.sh for hardware verification Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 12/21] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU Paul E. McKenney
                   ` (9 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit makes the judgelitmus.sh script check the --hw argument
(AKA the LKMM_HW_MAP_FILE environment variable) and to adjust its
judgment for a run where a C-language litmus test has been translated to
assembly and the assembly version verified.  In this case, the assembly
verification output is checked against the C-language script's "Result:"
comment.  However, because hardware can be stronger than LKMM requires,
the judgelitmus.sh script forgives verification mismatches featuring
a "Sometimes" in the C-language script and an "Always" or "Never"
assembly-language verification.

Note that deadlock is not forgiven, however, this should not normally be
an issue given that C-language tests containing locking, RCU, or SRCU
cannot be translated to assembly.  However, this issue can crop up in
litmus tests that mimic deadlock by using the "filter" clause to ignore
all executions.  It can also crop up when certain herd arguments are
used to autofilter everything that does not match the "exists" clause
in cases where the "exists" clause cannot be satisfied.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/README         |  8 +--
 tools/memory-model/scripts/judgelitmus.sh | 75 ++++++++++++++---------
 2 files changed, 51 insertions(+), 32 deletions(-)

diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
index 095c7eb36f9f..0e29a52044c1 100644
--- a/tools/memory-model/scripts/README
+++ b/tools/memory-model/scripts/README
@@ -43,10 +43,10 @@ initlitmushist.sh
 
 judgelitmus.sh
 
-	Given a .litmus file and its .litmus.out herd7 output, check the
-	.litmus.out file against the .litmus file's "Result:" comment to
-	judge whether the test ran correctly.  Not normally run manually,
-	provided instead for use by other scripts.
+	Given a .litmus file and its herd7 output, check the output file
+	against the .litmus file's "Result:" comment to judge whether
+	the test ran correctly.  Not normally run manually, provided
+	instead for use by other scripts.
 
 newlitmushist.sh
 
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 84c62eee321b..a5a865620f14 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -1,9 +1,14 @@
 #!/bin/sh
 # SPDX-License-Identifier: GPL-2.0+
 #
-# Given a .litmus test and the corresponding .litmus.out file, check
-# the .litmus.out file against the "Result:" comment to judge whether
-# the test ran correctly.
+# Given a .litmus test and the corresponding litmus output file, check
+# the .litmus.out file against the "Result:" comment to judge whether the
+# test ran correctly.  If the --hw argument is omitted, check against the
+# LKMM output, which is assumed to be in file.litmus.out.  If this argument
+# is provided, this is assumed to be a hardware test, and the output is
+# assumed to be in file.HW.litmus.out, where "HW" is the --hw argument.
+# In addition, non-Sometimes verification results will be noted, but
+# forgiven.
 #
 # Usage:
 #	judgelitmus.sh file.litmus
@@ -24,11 +29,18 @@ else
 	echo ' --- ' error: \"$litmus\" is not a readable file
 	exit 255
 fi
-if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
+if test -z "$LKMM_HW_MAP_FILE"
+then
+	litmusout=$litmus.out
+else
+	litmusout="`echo $litmus |
+		sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"
+fi
+if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
 then
 	:
 else
-	echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
+	echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
 	exit 255
 fi
 if grep -q '^ \* Result: ' $litmus
@@ -38,69 +50,76 @@ else
 	outcome=specified
 fi
 
-grep '^Observation' $LKMM_DESTDIR/$litmus.out
-if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
+grep '^Observation' $LKMM_DESTDIR/$litmusout
+if grep -q '^Observation' $LKMM_DESTDIR/$litmusout
 then
 	:
-elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out
+elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout
 then
-	badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out |
+	badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |
 		sed -e 's/^.*: Unknown macro //' |
 		sed -e 's/ (User error).*$//'`
 	badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"
 	echo $badmsg
-	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
 	then
-		echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1
+		echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1
 	fi
 	exit 254
-elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out
+elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout
 then
 	echo ' !!! Timeout' $litmus
-	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
 	then
-		echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1
+		echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1
 	fi
 	exit 124
 else
 	echo ' !!! Verification error' $litmus
-	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
 	then
-		echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
+		echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1
 	fi
 	exit 255
 fi
 if test "$outcome" = DEADLOCK
 then
-	if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+	if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
 	then
 		ret=0
 	else
 		echo " !!! Unexpected non-$outcome verification" $litmus
-		if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+		if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
 		then
-			echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
+			echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
 		fi
 		ret=1
 	fi
-elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
 then
 	echo " !!! Unexpected non-$outcome deadlock" $litmus
-	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
 	then
-		echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+		echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1
 	fi
 	ret=1
-elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
+elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe
 then
 	ret=0
 else
-	echo " !!! Unexpected non-$outcome verification" $litmus
-	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+	if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes
 	then
-		echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
+		flag="--- Forgiven"
+		ret=0
+	else
+		flag="!!! Unexpected"
+		ret=1
+	fi
+	echo " $flag non-$outcome verification" $litmus
+	if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout
+	then
+		echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
 	fi
-	ret=1
 fi
-tail -2 $LKMM_DESTDIR/$litmus.out | head -1
+tail -2 $LKMM_DESTDIR/$litmusout | head -1
 exit $ret
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 12/21] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (10 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 11/21] tools/memory-model: Make judgelitmus.sh handle hardware verifications Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 13/21] tools/memory-model: Fix checkalllitmus.sh comment Paul E. McKenney
                   ` (8 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit abstracts out common function to check a given litmus test
for locking, RCU, and SRCU in order to avoid duplicating code.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/simpletest.sh | 35 ++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100755 tools/memory-model/scripts/simpletest.sh

diff --git a/tools/memory-model/scripts/simpletest.sh b/tools/memory-model/scripts/simpletest.sh
new file mode 100755
index 000000000000..b03420e0dbb6
--- /dev/null
+++ b/tools/memory-model/scripts/simpletest.sh
@@ -0,0 +1,35 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Give zero status if this is a simple test and non-zero otherwise.
+# Simple tests do not contain locking, RCU, or SRCU.
+#
+# Usage:
+#	simpletest.sh file.litmus
+#
+# Copyright IBM Corporation, 2019
+#
+# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
+
+
+litmus=$1
+
+if test -f "$litmus" -a -r "$litmus"
+then
+	:
+else
+	echo ' --- ' error: \"$litmus\" is not a readable file
+	exit 255
+fi
+exclude="^[[:space:]]*\("
+exclude="${exclude}spin_lock(\|spin_unlock(\|spin_trylock(\|spin_is_locked("
+exclude="${exclude}\|rcu_read_lock(\|rcu_read_unlock("
+exclude="${exclude}\|synchronize_rcu(\|synchronize_rcu_expedited("
+exclude="${exclude}\|srcu_read_lock(\|srcu_read_unlock("
+exclude="${exclude}\|synchronize_srcu(\|synchronize_srcu_expedited("
+exclude="${exclude}\)"
+if grep -q $exclude $litmus
+then
+	exit 255
+fi
+exit 0
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 13/21] tools/memory-model: Fix checkalllitmus.sh comment
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (11 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 12/21] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 14/21] tools/memory-model: Hardware checking for check{,all}litmus.sh Paul E. McKenney
                   ` (7 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

The checkalllitmus.sh runs litmus tests in the litmus-tests directory,
not those in the github archive, so this commit updates the comment to
reflect this reality.

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

diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index 3c0c7fbbd223..d43c6b91db30 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -30,8 +30,8 @@ else
 	exit 255
 fi
 
-# Create any new directories that have appeared in the github litmus
-# repo since the last run.
+# Create any new directories that have appeared in the litmus-tests
+# directory since the last run.
 if test "$LKMM_DESTDIR" != "."
 then
 	find $litmusdir -type d -print |
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 14/21] tools/memory-model: Hardware checking for check{,all}litmus.sh
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (12 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 13/21] tools/memory-model: Fix checkalllitmus.sh comment Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 15/21] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files Paul E. McKenney
                   ` (6 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit makes checklitmus.sh and checkalllitmus.sh check to see
if a hardware verification was specified (via the --hw command-line
argument, which sets the LKMM_HW_MAP_FILE environment variable).
If so, the C-language litmus test is converted to the specified type
of assembly-language litmus test and herd is run on it.  Hardware is
permitted to be stronger than LKMM requires, so "Always" and "Never"
verifications of "Sometimes" C-language litmus tests are forgiven.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/checkalllitmus.sh | 23 +++++------
 tools/memory-model/scripts/checklitmus.sh    | 42 ++++++++++++++++++--
 2 files changed, 49 insertions(+), 16 deletions(-)

diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index d43c6b91db30..1e7afd3a51e4 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 # SPDX-License-Identifier: GPL-2.0+
 #
 # Run herd7 tests on all .litmus files in the litmus-tests directory
@@ -8,6 +8,11 @@
 # "^^^".  It also outputs verification results to a file whose name is
 # that of the specified litmus test, but with ".out" appended.
 #
+# If the --hw argument is specified, this script translates the .litmus
+# C-language file to the specified type of assembly and verifies that.
+# But in this case, litmus tests using complex synchronization (such as
+# locking, RCU, and SRCU) are cheerfully ignored.
+#
 # Usage:
 #	checkalllitmus.sh
 #
@@ -38,21 +43,15 @@ then
 	( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
 fi
 
-# Find the checklitmus script.  If it is not where we expect it, then
-# assume that the caller has the PATH environment variable set
-# appropriately.
-if test -x scripts/checklitmus.sh
-then
-	clscript=scripts/checklitmus.sh
-else
-	clscript=checklitmus.sh
-fi
-
 # Run the script on all the litmus tests in the specified directory
 ret=0
 for i in $litmusdir/*.litmus
 do
-	if ! $clscript $i
+	if test -n "$LKMM_HW_MAP_FILE" && ! scripts/simpletest.sh $i
+	then
+		continue
+	fi
+	if ! scripts/checklitmus.sh $i
 	then
 		ret=1
 	fi
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index 11461ed40b5e..1922a5af2c17 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -6,6 +6,11 @@
 # results to a file whose name is that of the specified litmus test, but
 # with ".out" appended.
 #
+# If the --hw argument is specified, this script translates the .litmus
+# C-language file to the specified type of assembly and verifies that.
+# But in this case, litmus tests using complex synchronization (such as
+# locking, RCU, and SRCU) are cheerfully ignored.
+#
 # Usage:
 #	checklitmus.sh file.litmus
 #
@@ -18,8 +23,6 @@
 # Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
 
 litmus=$1
-herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
-
 if test -f "$litmus" -a -r "$litmus"
 then
 	:
@@ -28,7 +31,38 @@ else
 	exit 255
 fi
 
-echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
-/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+if test -z "$LKMM_HW_MAP_FILE"
+then
+	# LKMM run
+	herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
+	echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
+	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+else
+	# Hardware run
+
+	T=/tmp/checklitmushw.sh.$$
+	trap 'rm -rf $T' 0 2
+	mkdir $T
+
+	# Generate filenames
+	catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
+	mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
+	themefile="$T/${LKMM_HW_MAP_FILE}.theme"
+	herdoptions="-model $LKMM_HW_CAT_FILE"
+	hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+	hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
+
+	# Don't run on litmus tests with complex synchronization
+	if ! scripts/simpletest.sh $litmus
+	then
+		echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
+		exit 254
+	fi
+
+	# Generate the assembly code and run herd on it.
+	gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
+	jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
+	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+fi
 
 scripts/judgelitmus.sh $litmus
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 15/21] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (13 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 14/21] tools/memory-model: Hardware checking for check{,all}litmus.sh Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 16/21] tools/memory-model: Split runlitmus.sh out of checklitmus.sh Paul E. McKenney
                   ` (5 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

The judgelitmus.sh script currently relies solely on the "Result:"
comment in the .litmus file.  This is problematic when using the --hw
argument, because it is necessary to check the hardware model against
LKMM even in the absence of "Result:" comments.

This commit therefore modifies judgelitmus.sh to check the observation
in a .litmus.out file, in case one was generated by a previous LKMM run.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/judgelitmus.sh | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index a5a865620f14..a1313f9960c3 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -8,7 +8,9 @@
 # is provided, this is assumed to be a hardware test, and the output is
 # assumed to be in file.HW.litmus.out, where "HW" is the --hw argument.
 # In addition, non-Sometimes verification results will be noted, but
-# forgiven.
+# forgiven.  Furthermore, if there is no "Result:" comment but there is
+# an LKMM .litmus.out file, the observation in that file will be used
+# to judge the assembly-language verification.
 #
 # Usage:
 #	judgelitmus.sh file.litmus
@@ -32,9 +34,11 @@ fi
 if test -z "$LKMM_HW_MAP_FILE"
 then
 	litmusout=$litmus.out
+	lkmmout=
 else
 	litmusout="`echo $litmus |
 		sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"
+	lkmmout=$litmus.out
 fi
 if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
 then
@@ -46,6 +50,9 @@ fi
 if grep -q '^ \* Result: ' $litmus
 then
 	outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
+elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
+then
+	outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
 else
 	outcome=specified
 fi
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 16/21] tools/memory-model: Split runlitmus.sh out of checklitmus.sh
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (14 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 15/21] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 17/21] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw Paul E. McKenney
                   ` (4 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit prepares for adding --hw capability to github litmus-test
scripts by splitting runlitmus.sh (which simply runs the verification)
out of checklitmus.sh (which also judges the results).

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/checklitmus.sh | 57 ++-----------------
 tools/memory-model/scripts/runlitmus.sh   | 69 +++++++++++++++++++++++
 2 files changed, 73 insertions(+), 53 deletions(-)
 create mode 100755 tools/memory-model/scripts/runlitmus.sh

diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index 1922a5af2c17..31a120d68a79 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -1,15 +1,8 @@
 #!/bin/sh
 # SPDX-License-Identifier: GPL-2.0+
 #
-# Run a herd7 test and invokes judgelitmus.sh to check the result against
-# a "Result:" comment within the litmus test.  It also outputs verification
-# results to a file whose name is that of the specified litmus test, but
-# with ".out" appended.
-#
-# If the --hw argument is specified, this script translates the .litmus
-# C-language file to the specified type of assembly and verifies that.
-# But in this case, litmus tests using complex synchronization (such as
-# locking, RCU, and SRCU) are cheerfully ignored.
+# Invokes runlitmus.sh and judgelitmus.sh on its arguments to run the
+# specified litmus test and pass judgment on the results.
 #
 # Usage:
 #	checklitmus.sh file.litmus
@@ -22,47 +15,5 @@
 #
 # Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
 
-litmus=$1
-if test -f "$litmus" -a -r "$litmus"
-then
-	:
-else
-	echo ' --- ' error: \"$litmus\" is not a readable file
-	exit 255
-fi
-
-if test -z "$LKMM_HW_MAP_FILE"
-then
-	# LKMM run
-	herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
-	echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
-	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
-else
-	# Hardware run
-
-	T=/tmp/checklitmushw.sh.$$
-	trap 'rm -rf $T' 0 2
-	mkdir $T
-
-	# Generate filenames
-	catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
-	mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
-	themefile="$T/${LKMM_HW_MAP_FILE}.theme"
-	herdoptions="-model $LKMM_HW_CAT_FILE"
-	hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
-	hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
-
-	# Don't run on litmus tests with complex synchronization
-	if ! scripts/simpletest.sh $litmus
-	then
-		echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
-		exit 254
-	fi
-
-	# Generate the assembly code and run herd on it.
-	gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
-	jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
-	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
-fi
-
-scripts/judgelitmus.sh $litmus
+scripts/runlitmus.sh $1
+scripts/judgelitmus.sh $1
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
new file mode 100755
index 000000000000..0ae46ab08cbd
--- /dev/null
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -0,0 +1,69 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Without the -hw argument, runs a herd7 test and outputs verification
+# results to a file whose name is that of the specified litmus test,
+# but with ".out" appended.
+#
+# If the --hw argument is specified, this script translates the .litmus
+# C-language file to the specified type of assembly and verifies that.
+# But in this case, litmus tests using complex synchronization (such as
+# locking, RCU, and SRCU) are cheerfully ignored.
+#
+# Either way, return the status of the herd command.
+#
+# Usage:
+#	runlitmus.sh file.litmus
+#
+# Run this in the directory containing the memory model, specifying the
+# pathname of the litmus test to check.  The caller is expected to have
+# properly set up the LKMM environment variables.
+#
+# Copyright IBM Corporation, 2019
+#
+# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
+
+litmus=$1
+if test -f "$litmus" -a -r "$litmus"
+then
+	:
+else
+	echo ' --- ' error: \"$litmus\" is not a readable file
+	exit 255
+fi
+
+if test -z "$LKMM_HW_MAP_FILE"
+then
+	# LKMM run
+	herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
+	echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
+	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+else
+	# Hardware run
+
+	T=/tmp/checklitmushw.sh.$$
+	trap 'rm -rf $T' 0 2
+	mkdir $T
+
+	# Generate filenames
+	catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
+	mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
+	themefile="$T/${LKMM_HW_MAP_FILE}.theme"
+	herdoptions="-model $LKMM_HW_CAT_FILE"
+	hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+	hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
+
+	# Don't run on litmus tests with complex synchronization
+	if ! scripts/simpletest.sh $litmus
+	then
+		echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
+		exit 254
+	fi
+
+	# Generate the assembly code and run herd on it.
+	gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
+	jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
+	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+fi
+
+exit $?
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 17/21] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (15 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 16/21] tools/memory-model: Split runlitmus.sh out of checklitmus.sh Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 18/21] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out Paul E. McKenney
                   ` (3 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

In the absence of "Result:" comments, the runlitmus.sh script relies on
litmus.out files from prior LKMM runs.  This can be a bit user-hostile,
so this commit makes runlitmus.sh generate any needed .litmus.out files
that don't already exist.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/runlitmus.sh | 54 ++++++++++++++-----------
 1 file changed, 30 insertions(+), 24 deletions(-)

diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 0ae46ab08cbd..186944a7a528 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -28,42 +28,48 @@ if test -f "$litmus" -a -r "$litmus"
 then
 	:
 else
-	echo ' --- ' error: \"$litmus\" is not a readable file
+	echo ' !!! ' error: \"$litmus\" is not a readable file
 	exit 255
 fi
 
-if test -z "$LKMM_HW_MAP_FILE"
+if test -z "$LKMM_HW_MAP_FILE" -o ! -e $LKMM_DESTDIR/$litmus.out
 then
 	# LKMM run
 	herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
 	echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
 	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
-else
-	# Hardware run
+	ret=$?
+	if test -z "$LKMM_HW_MAP_FILE"
+	then
+		exit $ret
+	fi
+	echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run
+fi
 
-	T=/tmp/checklitmushw.sh.$$
-	trap 'rm -rf $T' 0 2
-	mkdir $T
+# Hardware run
 
-	# Generate filenames
-	catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
-	mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
-	themefile="$T/${LKMM_HW_MAP_FILE}.theme"
-	herdoptions="-model $LKMM_HW_CAT_FILE"
-	hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
-	hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
+T=/tmp/checklitmushw.sh.$$
+trap 'rm -rf $T' 0 2
+mkdir $T
 
-	# Don't run on litmus tests with complex synchronization
-	if ! scripts/simpletest.sh $litmus
-	then
-		echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
-		exit 254
-	fi
+# Generate filenames
+catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
+mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
+themefile="$T/${LKMM_HW_MAP_FILE}.theme"
+herdoptions="-model $LKMM_HW_CAT_FILE"
+hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
 
-	# Generate the assembly code and run herd on it.
-	gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
-	jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
-	/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+# Don't run on litmus tests with complex synchronization
+if ! scripts/simpletest.sh $litmus
+then
+	echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
+	exit 254
 fi
 
+# Generate the assembly code and run herd on it.
+gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
+jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+
 exit $?
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 18/21] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (16 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 17/21] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 19/21] tools/memory-model: Keep assembly-language litmus tests Paul E. McKenney
                   ` (2 subsequent siblings)
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

When the github scripts see ".litmus.out", they assume that there must be
a corresponding C-language ".litmus" file.  Won't they be disappointed
when they instead see nothing, or, worse yet, the corresponding
assembly-language litmus test?  This commit therefore swaps the hardware
tag with the "litmus" to avoid this sort of disappointment.

This commit also adjusts the .gitignore file so as to avoid adding these
new ".out" files to git.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/litmus-tests/.gitignore | 2 +-
 tools/memory-model/scripts/judgelitmus.sh  | 2 +-
 tools/memory-model/scripts/runlitmus.sh    | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore
index 6e2ddc54152f..f47cb2045f13 100644
--- a/tools/memory-model/litmus-tests/.gitignore
+++ b/tools/memory-model/litmus-tests/.gitignore
@@ -1 +1 @@
-*.litmus.out
+*.out
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index a1313f9960c3..6ecd223c0f4c 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -37,7 +37,7 @@ then
 	lkmmout=
 else
 	litmusout="`echo $litmus |
-		sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"
+		sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out"
 	lkmmout=$litmus.out
 fi
 if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 186944a7a528..154c95ce79da 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -57,7 +57,7 @@ catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
 mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
 themefile="$T/${LKMM_HW_MAP_FILE}.theme"
 herdoptions="-model $LKMM_HW_CAT_FILE"
-hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`
 hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
 
 # Don't run on litmus tests with complex synchronization
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 19/21] tools/memory-model: Keep assembly-language litmus tests
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (17 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 18/21] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 20/21] tools/memory-model: Allow herd to deduce CPU type Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 21/21] tools/memory-model: Make runlitmus.sh check for jingle errors Paul E. McKenney
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

This commit retains the assembly-language litmus tests generated from
the C-language litmus tests, appending the hardware tag to the original
C-language litmus test's filename.  Thus, S+poonceonces.litmus.AArch64
contains the Armv8 assembly language corresponding to the C-language
S+poonceonces.litmus test.

This commit also updates the .gitignore to avoid commiting these
automatically generated assembly-language litmus tests.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/litmus-tests/.gitignore | 2 +-
 tools/memory-model/scripts/runlitmus.sh    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore
index f47cb2045f13..848e62d2a9b3 100644
--- a/tools/memory-model/litmus-tests/.gitignore
+++ b/tools/memory-model/litmus-tests/.gitignore
@@ -1 +1 @@
-*.out
+*.litmus.*
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 154c95ce79da..71d13bb0c764 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -69,7 +69,7 @@ fi
 
 # Generate the assembly code and run herd on it.
 gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
-jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
-/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
 
 exit $?
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 20/21] tools/memory-model: Allow herd to deduce CPU type
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (18 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 19/21] tools/memory-model: Keep assembly-language litmus tests Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  2019-03-26 23:41 ` [PATCH tip/core/rcu 21/21] tools/memory-model: Make runlitmus.sh check for jingle errors Paul E. McKenney
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

Currently, the scripts specify the CPU's .cat file to herd.  But this is
pointless because herd will select a good and sufficient .cat file from
the assembly-language litmus test itself.  This commit therefore removes
the -model argument to herd, allowing herd to figure the CPU family out
itself.

Note that the user can override herd's choice using the "--herdopts"
argument to the scripts.

Suggested-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/runlitmus.sh | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 71d13bb0c764..482ed7a08951 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -53,7 +53,6 @@ trap 'rm -rf $T' 0 2
 mkdir $T
 
 # Generate filenames
-catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
 mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
 themefile="$T/${LKMM_HW_MAP_FILE}.theme"
 herdoptions="-model $LKMM_HW_CAT_FILE"
@@ -70,6 +69,6 @@ fi
 # Generate the assembly code and run herd on it.
 gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
 jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
-/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
 
 exit $?
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* [PATCH tip/core/rcu 21/21] tools/memory-model: Make runlitmus.sh check for jingle errors
  2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
                   ` (19 preceding siblings ...)
  2019-03-26 23:41 ` [PATCH tip/core/rcu 20/21] tools/memory-model: Allow herd to deduce CPU type Paul E. McKenney
@ 2019-03-26 23:41 ` Paul E. McKenney
  20 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-03-26 23:41 UTC (permalink / raw)
  To: linux-kernel, linux-arch, mingo
  Cc: stern, andrea.parri, will.deacon, peterz, boqun.feng, npiggin,
	dhowells, j.alglave, luc.maranget, akiyks, Paul E. McKenney

It turns out that the jingle7 tool is currently a bit picky about
the litmus tests it is willing to process.  This commit therefore
ensures that jingle7 failures are reported.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
---
 tools/memory-model/scripts/runlitmus.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 482ed7a08951..6a997a6df3ce 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -69,6 +69,11 @@ fi
 # Generate the assembly code and run herd on it.
 gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
 jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
+if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out
+then
+	echo ' !!! ' jingle7 failed, no $hwlitmus generated
+	exit 253
+fi
 /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
 
 exit $?
-- 
2.17.1


^ permalink raw reply related	[flat|nested] 28+ messages in thread

* Re: [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section
  2019-03-26 23:41 ` [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section Paul E. McKenney
@ 2019-04-02 13:03   ` Will Deacon
  2019-04-04 15:58     ` Akira Yokosawa
  0 siblings, 1 reply; 28+ messages in thread
From: Will Deacon @ 2019-04-02 13:03 UTC (permalink / raw)
  To: Paul E. McKenney
  Cc: linux-kernel, linux-arch, mingo, stern, andrea.parri, peterz,
	boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks,
	Benjamin Herrenschmidt, Michael Ellerman, Arnd Bergmann,
	Palmer Dabbelt, Daniel Lustig, Linus Torvalds, Maciej W. Rozycki,
	Mikulas Patocka

On Tue, Mar 26, 2019 at 04:41:16PM -0700, Paul E. McKenney wrote:
> From: Will Deacon <will.deacon@arm.com>
> 
> The "KERNEL I/O BARRIER EFFECTS" section of memory-barriers.txt is vague,
> x86-centric, out-of-date, incomplete and demonstrably incorrect in places.
> This is largely because I/O ordering is a horrible can of worms, but also
> because the document has stagnated as our understanding has evolved.
> 
> Attempt to address some of that, by rewriting the section based on
> recent(-ish) discussions with Arnd, BenH and others. Maybe one day we'll
> find a way to formalise this stuff, but for now let's at least try to
> make the English easier to understand.
> 
> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
> Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
> Cc: Michael Ellerman <mpe@ellerman.id.au>
> Cc: Arnd Bergmann <arnd@arndb.de>
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: Andrea Parri <andrea.parri@amarulasolutions.com>
> Cc: Palmer Dabbelt <palmer@sifive.com>
> Cc: Daniel Lustig <dlustig@nvidia.com>
> Cc: David Howells <dhowells@redhat.com>
> Cc: Alan Stern <stern@rowland.harvard.edu>
> Cc: Linus Torvalds <torvalds@linux-foundation.org>
> Cc: "Maciej W. Rozycki" <macro@linux-mips.org>
> Cc: Mikulas Patocka <mpatocka@redhat.com>
> Signed-off-by: Will Deacon <will.deacon@arm.com>
> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> ---
>  Documentation/memory-barriers.txt | 115 ++++++++++++++++++------------
>  1 file changed, 70 insertions(+), 45 deletions(-)

If somebody could provide an Ack on this patch, I'd really appreciate it,
please. Whilst the portable ordering guarantees that I've documented are
fairly conservative, I do think that this change is a big improvement and
gives you what you need if you're writing a portable device driver for a new
piece of hardware. I'm tackling the removal of MMIOWB as a separate series.

I think Paul now requires an Ack before he'll send a patch to mainline,
hence the grovelling.

Cheers,

Will

> diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
> index 1c22b21ae922..158947ae78c2 100644
> --- a/Documentation/memory-barriers.txt
> +++ b/Documentation/memory-barriers.txt
> @@ -2599,72 +2599,97 @@ likely, then interrupt-disabling locks should be used to guarantee ordering.
>  KERNEL I/O BARRIER EFFECTS
>  ==========================
>  
> -When accessing I/O memory, drivers should use the appropriate accessor
> -functions:
> +Interfacing with peripherals via I/O accesses is deeply architecture and device
> +specific. Therefore, drivers which are inherently non-portable may rely on
> +specific behaviours of their target systems in order to achieve synchronization
> +in the most lightweight manner possible. For drivers intending to be portable
> +between multiple architectures and bus implementations, the kernel offers a
> +series of accessor functions that provide various degrees of ordering
> +guarantees:
>  
> - (*) inX(), outX():
> + (*) readX(), writeX():
>  
> -     These are intended to talk to I/O space rather than memory space, but
> -     that's primarily a CPU-specific concept.  The i386 and x86_64 processors
> -     do indeed have special I/O space access cycles and instructions, but many
> -     CPUs don't have such a concept.
> +     The readX() and writeX() MMIO accessors take a pointer to the peripheral
> +     being accessed as an __iomem * parameter. For pointers mapped with the
> +     default I/O attributes (e.g. those returned by ioremap()), then the
> +     ordering guarantees are as follows:
>  
> -     The PCI bus, amongst others, defines an I/O space concept which - on such
> -     CPUs as i386 and x86_64 - readily maps to the CPU's concept of I/O
> -     space.  However, it may also be mapped as a virtual I/O space in the CPU's
> -     memory map, particularly on those CPUs that don't support alternate I/O
> -     spaces.
> +     1. All readX() and writeX() accesses to the same peripheral are ordered
> +        with respect to each other. For example, this ensures that MMIO register
> +	writes by the CPU to a particular device will arrive in program order.
>  
> -     Accesses to this space may be fully synchronous (as on i386), but
> -     intermediary bridges (such as the PCI host bridge) may not fully honour
> -     that.
> +     2. A writeX() by the CPU to the peripheral will first wait for the
> +        completion of all prior CPU writes to memory. For example, this ensures
> +        that writes by the CPU to an outbound DMA buffer allocated by
> +        dma_alloc_coherent() will be visible to a DMA engine when the CPU writes
> +        to its MMIO control register to trigger the transfer.
>  
> -     They are guaranteed to be fully ordered with respect to each other.
> +     3. A readX() by the CPU from the peripheral will complete before any
> +	subsequent CPU reads from memory can begin. For example, this ensures
> +	that reads by the CPU from an incoming DMA buffer allocated by
> +	dma_alloc_coherent() will not see stale data after reading from the DMA
> +	engine's MMIO status register to establish that the DMA transfer has
> +	completed.
>  
> -     They are not guaranteed to be fully ordered with respect to other types of
> -     memory and I/O operation.
> +     4. A readX() by the CPU from the peripheral will complete before any
> +	subsequent delay() loop can begin execution. For example, this ensures
> +	that two MMIO register writes by the CPU to a peripheral will arrive at
> +	least 1us apart if the first write is immediately read back with readX()
> +	and udelay(1) is called prior to the second writeX().
>  
> - (*) readX(), writeX():
> +     __iomem pointers obtained with non-default attributes (e.g. those returned
> +     by ioremap_wc()) are unlikely to provide many of these guarantees.
>  
> -     Whether these are guaranteed to be fully ordered and uncombined with
> -     respect to each other on the issuing CPU depends on the characteristics
> -     defined for the memory window through which they're accessing.  On later
> -     i386 architecture machines, for example, this is controlled by way of the
> -     MTRR registers.
> + (*) readX_relaxed(), writeX_relaxed():
>  
> -     Ordinarily, these will be guaranteed to be fully ordered and uncombined,
> -     provided they're not accessing a prefetchable device.
> +     These are similar to readX() and writeX(), but provide weaker memory
> +     ordering guarantees. Specifically, they do not guarantee ordering with
> +     respect to normal memory accesses or delay() loops (i.e bullets 2-4 above)
> +     but they are still guaranteed to be ordered with respect to other accesses
> +     to the same peripheral when operating on __iomem pointers mapped with the
> +     default I/O attributes.
>  
> -     However, intermediary hardware (such as a PCI bridge) may indulge in
> -     deferral if it so wishes; to flush a store, a load from the same location
> -     is preferred[*], but a load from the same device or from configuration
> -     space should suffice for PCI.
> + (*) readsX(), writesX():
>  
> -     [*] NOTE! attempting to load from the same location as was written to may
> -	 cause a malfunction - consider the 16550 Rx/Tx serial registers for
> -	 example.
> +     The readsX() and writesX() MMIO accessors are designed for accessing
> +     register-based, memory-mapped FIFOs residing on peripherals that are not
> +     capable of performing DMA. Consequently, they provide only the ordering
> +     guarantees of readX_relaxed() and writeX_relaxed(), as documented above.
>  
> -     Used with prefetchable I/O memory, an mmiowb() barrier may be required to
> -     force stores to be ordered.
> + (*) inX(), outX():
>  
> -     Please refer to the PCI specification for more information on interactions
> -     between PCI transactions.
> +     The inX() and outX() accessors are intended to access legacy port-mapped
> +     I/O peripherals, which may require special instructions on some
> +     architectures (notably x86). The port number of the peripheral being
> +     accessed is passed as an argument.
>  
> - (*) readX_relaxed(), writeX_relaxed()
> +     Since many CPU architectures ultimately access these peripherals via an
> +     internal virtual memory mapping, the portable ordering guarantees provided
> +     by inX() and outX() are the same as those provided by readX() and writeX()
> +     respectively when accessing a mapping with the default I/O attributes.
>  
> -     These are similar to readX() and writeX(), but provide weaker memory
> -     ordering guarantees.  Specifically, they do not guarantee ordering with
> -     respect to normal memory accesses (e.g. DMA buffers) nor do they guarantee
> -     ordering with respect to LOCK or UNLOCK operations.  If the latter is
> -     required, an mmiowb() barrier can be used.  Note that relaxed accesses to
> -     the same peripheral are guaranteed to be ordered with respect to each
> -     other.
> +     Device drivers may expect outX() to emit a non-posted write transaction
> +     that waits for a completion response from the I/O peripheral before
> +     returning. This is not guaranteed by all architectures and is therefore
> +     not part of the portable ordering semantics.
> +
> + (*) insX(), outsX():
> +
> +     As above, the insX() and outX() accessors provide the same ordering
> +     guarantees as readsX() and writesX() respectively when accessing a mapping
> +     with the default I/O attributes.
>  
>   (*) ioreadX(), iowriteX()
>  
>       These will perform appropriately for the type of access they're actually
>       doing, be it inX()/outX() or readX()/writeX().
>  
> +All of these accessors assume that the underlying peripheral is little-endian,
> +and will therefore perform byte-swapping operations on big-endian architectures.
> +
> +Composing I/O ordering barriers with SMP ordering barriers and LOCK/UNLOCK
> +operations is a dangerous sport which may require the use of mmiowb(). See the
> +subsection "Acquires vs I/O accesses" for more information.
>  
>  ========================================
>  ASSUMED MINIMUM EXECUTION ORDERING MODEL
> -- 
> 2.17.1
> 

^ permalink raw reply	[flat|nested] 28+ messages in thread

* Re: [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited()
  2019-03-26 23:41 ` [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited() Paul E. McKenney
@ 2019-04-02 14:49   ` Andrea Parri
  2019-04-04 20:50     ` Paul E. McKenney
  0 siblings, 1 reply; 28+ messages in thread
From: Andrea Parri @ 2019-04-02 14:49 UTC (permalink / raw)
  To: Paul E. McKenney
  Cc: linux-kernel, linux-arch, mingo, stern, will.deacon, peterz,
	boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks

On Tue, Mar 26, 2019 at 04:41:20PM -0700, Paul E. McKenney wrote:
> Given that synchronize_rcu_expedited() is supported, this commit adds
> support for synchronize_srcu_expedited().
> 
> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> ---
>  tools/memory-model/linux-kernel.def | 1 +
>  1 file changed, 1 insertion(+)
> 
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 0c3f0ef486f4..551eeaa389d4 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -51,6 +51,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
>  srcu_read_lock(X)  __srcu{srcu-lock}(X)
>  srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
>  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
> +synchronize_srcu_expedited(X)  { __srcu{sync-srcu}(X); }

This and the other patches from the series do not apply to "tip/core/rcu"
(from the Subject), but this seems straightforward enough:

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

  Andrea


>  
>  // Atomic
>  atomic_read(X) READ_ONCE(*X)
> -- 
> 2.17.1
> 

^ permalink raw reply	[flat|nested] 28+ messages in thread

* Re: [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section
  2019-04-02 13:03   ` Will Deacon
@ 2019-04-04 15:58     ` Akira Yokosawa
  2019-04-04 16:40       ` Will Deacon
  0 siblings, 1 reply; 28+ messages in thread
From: Akira Yokosawa @ 2019-04-04 15:58 UTC (permalink / raw)
  To: Will Deacon, Paul E. McKenney
  Cc: linux-kernel, linux-arch, mingo, stern, andrea.parri, peterz,
	boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
	Benjamin Herrenschmidt, Michael Ellerman, Arnd Bergmann,
	Palmer Dabbelt, Daniel Lustig, Linus Torvalds, Maciej W. Rozycki,
	Mikulas Patocka

Hi Will,

On Tue, 2 Apr 2019 14:03:46 +0100, Will Deacon wrote:
> On Tue, Mar 26, 2019 at 04:41:16PM -0700, Paul E. McKenney wrote:
>> From: Will Deacon <will.deacon@arm.com>
>>
>> The "KERNEL I/O BARRIER EFFECTS" section of memory-barriers.txt is vague,
>> x86-centric, out-of-date, incomplete and demonstrably incorrect in places.
>> This is largely because I/O ordering is a horrible can of worms, but also
>> because the document has stagnated as our understanding has evolved.
>>
>> Attempt to address some of that, by rewriting the section based on
>> recent(-ish) discussions with Arnd, BenH and others. Maybe one day we'll
>> find a way to formalise this stuff, but for now let's at least try to
>> make the English easier to understand.
>>
>> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
>> Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
>> Cc: Michael Ellerman <mpe@ellerman.id.au>
>> Cc: Arnd Bergmann <arnd@arndb.de>
>> Cc: Peter Zijlstra <peterz@infradead.org>
>> Cc: Andrea Parri <andrea.parri@amarulasolutions.com>
>> Cc: Palmer Dabbelt <palmer@sifive.com>
>> Cc: Daniel Lustig <dlustig@nvidia.com>
>> Cc: David Howells <dhowells@redhat.com>
>> Cc: Alan Stern <stern@rowland.harvard.edu>
>> Cc: Linus Torvalds <torvalds@linux-foundation.org>
>> Cc: "Maciej W. Rozycki" <macro@linux-mips.org>
>> Cc: Mikulas Patocka <mpatocka@redhat.com>
>> Signed-off-by: Will Deacon <will.deacon@arm.com>
>> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
>> ---
>>  Documentation/memory-barriers.txt | 115 ++++++++++++++++++------------
>>  1 file changed, 70 insertions(+), 45 deletions(-)
> 
> If somebody could provide an Ack on this patch, I'd really appreciate it,
> please. Whilst the portable ordering guarantees that I've documented are
> fairly conservative, I do think that this change is a big improvement and
> gives you what you need if you're writing a portable device driver for a new
> piece of hardware. I'm tackling the removal of MMIOWB as a separate series.
> 
> I think Paul now requires an Ack before he'll send a patch to mainline,
> hence the grovelling.

I'm afraid I'm not that qualified to provide an Ack to this patch,
but please find a nit fix below.

> 
> Cheers,
> 
> Will
> 
>> diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
>> index 1c22b21ae922..158947ae78c2 100644
>> --- a/Documentation/memory-barriers.txt
>> +++ b/Documentation/memory-barriers.txt
>> @@ -2599,72 +2599,97 @@ likely, then interrupt-disabling locks should be used to guarantee ordering.
>>  KERNEL I/O BARRIER EFFECTS
>>  ==========================
>>  
>> -When accessing I/O memory, drivers should use the appropriate accessor
>> -functions:
>> +Interfacing with peripherals via I/O accesses is deeply architecture and device
>> +specific. Therefore, drivers which are inherently non-portable may rely on
>> +specific behaviours of their target systems in order to achieve synchronization
>> +in the most lightweight manner possible. For drivers intending to be portable
>> +between multiple architectures and bus implementations, the kernel offers a
>> +series of accessor functions that provide various degrees of ordering
>> +guarantees:
>>  
>> - (*) inX(), outX():
>> + (*) readX(), writeX():
>>  
>> -     These are intended to talk to I/O space rather than memory space, but
>> -     that's primarily a CPU-specific concept.  The i386 and x86_64 processors
>> -     do indeed have special I/O space access cycles and instructions, but many
>> -     CPUs don't have such a concept.
>> +     The readX() and writeX() MMIO accessors take a pointer to the peripheral
>> +     being accessed as an __iomem * parameter. For pointers mapped with the
>> +     default I/O attributes (e.g. those returned by ioremap()), then the
>> +     ordering guarantees are as follows:
>>  
>> -     The PCI bus, amongst others, defines an I/O space concept which - on such
>> -     CPUs as i386 and x86_64 - readily maps to the CPU's concept of I/O
>> -     space.  However, it may also be mapped as a virtual I/O space in the CPU's
>> -     memory map, particularly on those CPUs that don't support alternate I/O
>> -     spaces.
>> +     1. All readX() and writeX() accesses to the same peripheral are ordered
>> +        with respect to each other. For example, this ensures that MMIO register
>> +	writes by the CPU to a particular device will arrive in program order.
>>  
>> -     Accesses to this space may be fully synchronous (as on i386), but
>> -     intermediary bridges (such as the PCI host bridge) may not fully honour
>> -     that.
>> +     2. A writeX() by the CPU to the peripheral will first wait for the
>> +        completion of all prior CPU writes to memory. For example, this ensures
>> +        that writes by the CPU to an outbound DMA buffer allocated by
>> +        dma_alloc_coherent() will be visible to a DMA engine when the CPU writes
>> +        to its MMIO control register to trigger the transfer.
>>  
>> -     They are guaranteed to be fully ordered with respect to each other.
>> +     3. A readX() by the CPU from the peripheral will complete before any
>> +	subsequent CPU reads from memory can begin. For example, this ensures
>> +	that reads by the CPU from an incoming DMA buffer allocated by
>> +	dma_alloc_coherent() will not see stale data after reading from the DMA
>> +	engine's MMIO status register to establish that the DMA transfer has
>> +	completed.
>>  
>> -     They are not guaranteed to be fully ordered with respect to other types of
>> -     memory and I/O operation.
>> +     4. A readX() by the CPU from the peripheral will complete before any
>> +	subsequent delay() loop can begin execution. For example, this ensures
>> +	that two MMIO register writes by the CPU to a peripheral will arrive at
>> +	least 1us apart if the first write is immediately read back with readX()
>> +	and udelay(1) is called prior to the second writeX().
>>  
>> - (*) readX(), writeX():
>> +     __iomem pointers obtained with non-default attributes (e.g. those returned
>> +     by ioremap_wc()) are unlikely to provide many of these guarantees.
>>  
>> -     Whether these are guaranteed to be fully ordered and uncombined with
>> -     respect to each other on the issuing CPU depends on the characteristics
>> -     defined for the memory window through which they're accessing.  On later
>> -     i386 architecture machines, for example, this is controlled by way of the
>> -     MTRR registers.
>> + (*) readX_relaxed(), writeX_relaxed():
>>  
>> -     Ordinarily, these will be guaranteed to be fully ordered and uncombined,
>> -     provided they're not accessing a prefetchable device.
>> +     These are similar to readX() and writeX(), but provide weaker memory
>> +     ordering guarantees. Specifically, they do not guarantee ordering with
>> +     respect to normal memory accesses or delay() loops (i.e bullets 2-4 above)
>> +     but they are still guaranteed to be ordered with respect to other accesses
>> +     to the same peripheral when operating on __iomem pointers mapped with the
>> +     default I/O attributes.
>>  
>> -     However, intermediary hardware (such as a PCI bridge) may indulge in
>> -     deferral if it so wishes; to flush a store, a load from the same location
>> -     is preferred[*], but a load from the same device or from configuration
>> -     space should suffice for PCI.
>> + (*) readsX(), writesX():
>>  
>> -     [*] NOTE! attempting to load from the same location as was written to may
>> -	 cause a malfunction - consider the 16550 Rx/Tx serial registers for
>> -	 example.
>> +     The readsX() and writesX() MMIO accessors are designed for accessing
>> +     register-based, memory-mapped FIFOs residing on peripherals that are not
>> +     capable of performing DMA. Consequently, they provide only the ordering
>> +     guarantees of readX_relaxed() and writeX_relaxed(), as documented above.
>>  
>> -     Used with prefetchable I/O memory, an mmiowb() barrier may be required to
>> -     force stores to be ordered.
>> + (*) inX(), outX():
>>  
>> -     Please refer to the PCI specification for more information on interactions
>> -     between PCI transactions.
>> +     The inX() and outX() accessors are intended to access legacy port-mapped
>> +     I/O peripherals, which may require special instructions on some
>> +     architectures (notably x86). The port number of the peripheral being
>> +     accessed is passed as an argument.
>>  
>> - (*) readX_relaxed(), writeX_relaxed()
>> +     Since many CPU architectures ultimately access these peripherals via an
>> +     internal virtual memory mapping, the portable ordering guarantees provided
>> +     by inX() and outX() are the same as those provided by readX() and writeX()
>> +     respectively when accessing a mapping with the default I/O attributes.
>>  
>> -     These are similar to readX() and writeX(), but provide weaker memory
>> -     ordering guarantees.  Specifically, they do not guarantee ordering with
>> -     respect to normal memory accesses (e.g. DMA buffers) nor do they guarantee
>> -     ordering with respect to LOCK or UNLOCK operations.  If the latter is
>> -     required, an mmiowb() barrier can be used.  Note that relaxed accesses to
>> -     the same peripheral are guaranteed to be ordered with respect to each
>> -     other.
>> +     Device drivers may expect outX() to emit a non-posted write transaction
>> +     that waits for a completion response from the I/O peripheral before
>> +     returning. This is not guaranteed by all architectures and is therefore
>> +     not part of the portable ordering semantics.
>> +
>> + (*) insX(), outsX():
>> +
>> +     As above, the insX() and outX() accessors provide the same ordering
                                  outsX()

>> +     guarantees as readsX() and writesX() respectively when accessing a mapping
>> +     with the default I/O attributes.
>>  
>>   (*) ioreadX(), iowriteX()
>>  
>>       These will perform appropriately for the type of access they're actually
>>       doing, be it inX()/outX() or readX()/writeX().
>>  
>> +All of these accessors assume that the underlying peripheral is little-endian,
>> +and will therefore perform byte-swapping operations on big-endian architectures.
>> +
>> +Composing I/O ordering barriers with SMP ordering barriers and LOCK/UNLOCK
>> +operations is a dangerous sport which may require the use of mmiowb(). See the
>> +subsection "Acquires vs I/O accesses" for more information.
>>  
>>  ========================================
>>  ASSUMED MINIMUM EXECUTION ORDERING MODEL
>> -- 
>> 2.17.1
>>

JFYI, there is another document Documentation/driver-api/device-io.rst,
which is somewhat related to this update. It looks like this one also needs
some update, as Jon commented in transforming to .rst format in commit
8a8a602fdb83 ("docs: Convert the deviceio template to RST"):
<quote>
    Like the rest of our documentation, this one could use some work.  There's
    no mention of ioremap() and friends, no mention of io_read*() and friends.
    But we have nice documentation for all those folks writing new drivers that
    do port I/O :).
</quote>

This commit was merged in v4.11 cycle. And there has been no update whatsoever
since. mmiowb() is lightly mentioned therein. IMHO, just updating
memory-barriers.txt would widen the gap of information.

Thoughts?

        Thanks, Akira

^ permalink raw reply	[flat|nested] 28+ messages in thread

* Re: [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section
  2019-04-04 15:58     ` Akira Yokosawa
@ 2019-04-04 16:40       ` Will Deacon
  2019-04-04 22:23         ` Akira Yokosawa
  0 siblings, 1 reply; 28+ messages in thread
From: Will Deacon @ 2019-04-04 16:40 UTC (permalink / raw)
  To: Akira Yokosawa
  Cc: Paul E. McKenney, linux-kernel, linux-arch, mingo, stern,
	andrea.parri, peterz, boqun.feng, npiggin, dhowells, j.alglave,
	luc.maranget, Benjamin Herrenschmidt, Michael Ellerman,
	Arnd Bergmann, Palmer Dabbelt, Daniel Lustig, Linus Torvalds,
	Maciej W. Rozycki, Mikulas Patocka

Hi Akira,

On Fri, Apr 05, 2019 at 12:58:36AM +0900, Akira Yokosawa wrote:
> On Tue, 2 Apr 2019 14:03:46 +0100, Will Deacon wrote:
> > On Tue, Mar 26, 2019 at 04:41:16PM -0700, Paul E. McKenney wrote:
> >> From: Will Deacon <will.deacon@arm.com>
> >>
> >> The "KERNEL I/O BARRIER EFFECTS" section of memory-barriers.txt is vague,
> >> x86-centric, out-of-date, incomplete and demonstrably incorrect in places.
> >> This is largely because I/O ordering is a horrible can of worms, but also
> >> because the document has stagnated as our understanding has evolved.
> >>
> >> Attempt to address some of that, by rewriting the section based on
> >> recent(-ish) discussions with Arnd, BenH and others. Maybe one day we'll
> >> find a way to formalise this stuff, but for now let's at least try to
> >> make the English easier to understand.
> >>
> >> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
> >> Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
> >> Cc: Michael Ellerman <mpe@ellerman.id.au>
> >> Cc: Arnd Bergmann <arnd@arndb.de>
> >> Cc: Peter Zijlstra <peterz@infradead.org>
> >> Cc: Andrea Parri <andrea.parri@amarulasolutions.com>
> >> Cc: Palmer Dabbelt <palmer@sifive.com>
> >> Cc: Daniel Lustig <dlustig@nvidia.com>
> >> Cc: David Howells <dhowells@redhat.com>
> >> Cc: Alan Stern <stern@rowland.harvard.edu>
> >> Cc: Linus Torvalds <torvalds@linux-foundation.org>
> >> Cc: "Maciej W. Rozycki" <macro@linux-mips.org>
> >> Cc: Mikulas Patocka <mpatocka@redhat.com>
> >> Signed-off-by: Will Deacon <will.deacon@arm.com>
> >> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> >> ---
> >>  Documentation/memory-barriers.txt | 115 ++++++++++++++++++------------
> >>  1 file changed, 70 insertions(+), 45 deletions(-)
> > 
> > If somebody could provide an Ack on this patch, I'd really appreciate it,
> > please. Whilst the portable ordering guarantees that I've documented are
> > fairly conservative, I do think that this change is a big improvement and
> > gives you what you need if you're writing a portable device driver for a new
> > piece of hardware. I'm tackling the removal of MMIOWB as a separate series.
> > 
> > I think Paul now requires an Ack before he'll send a patch to mainline,
> > hence the grovelling.
> 
> I'm afraid I'm not that qualified to provide an Ack to this patch,
> but please find a nit fix below.

Oh well, thanks for having a look anyway!

> >> + (*) insX(), outsX():
> >> +
> >> +     As above, the insX() and outX() accessors provide the same ordering
>                                   outsX()

Thanks; I'll fix that.

> >> +     guarantees as readsX() and writesX() respectively when accessing a mapping
> >> +     with the default I/O attributes.
> >>  
> >>   (*) ioreadX(), iowriteX()
> >>  
> >>       These will perform appropriately for the type of access they're actually
> >>       doing, be it inX()/outX() or readX()/writeX().
> >>  
> >> +All of these accessors assume that the underlying peripheral is little-endian,
> >> +and will therefore perform byte-swapping operations on big-endian architectures.
> >> +
> >> +Composing I/O ordering barriers with SMP ordering barriers and LOCK/UNLOCK
> >> +operations is a dangerous sport which may require the use of mmiowb(). See the
> >> +subsection "Acquires vs I/O accesses" for more information.
> >>  
> >>  ========================================
> >>  ASSUMED MINIMUM EXECUTION ORDERING MODEL
> >> -- 
> >> 2.17.1
> >>
> 
> JFYI, there is another document Documentation/driver-api/device-io.rst,
> which is somewhat related to this update. It looks like this one also needs
> some update, as Jon commented in transforming to .rst format in commit
> 8a8a602fdb83 ("docs: Convert the deviceio template to RST"):
> <quote>
>     Like the rest of our documentation, this one could use some work.  There's
>     no mention of ioremap() and friends, no mention of io_read*() and friends.
>     But we have nice documentation for all those folks writing new drivers that
>     do port I/O :).
> </quote>
> 
> This commit was merged in v4.11 cycle. And there has been no update whatsoever
> since. mmiowb() is lightly mentioned therein. IMHO, just updating
> memory-barriers.txt would widen the gap of information.
> 
> Thoughts?

I have a subsequent patch which kills mmiowb() entirely:

https://git.kernel.org/pub/scm/linux/kernel/git/arm64/linux.git/commit/?h=for-next/mmiowb&id=3c1a2050c08fb8193777b60b49e60320254a156c

and that one does hit device-io.rst.

Will

^ permalink raw reply	[flat|nested] 28+ messages in thread

* Re: [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited()
  2019-04-02 14:49   ` Andrea Parri
@ 2019-04-04 20:50     ` Paul E. McKenney
  0 siblings, 0 replies; 28+ messages in thread
From: Paul E. McKenney @ 2019-04-04 20:50 UTC (permalink / raw)
  To: Andrea Parri
  Cc: linux-kernel, linux-arch, mingo, stern, will.deacon, peterz,
	boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks

On Tue, Apr 02, 2019 at 04:49:11PM +0200, Andrea Parri wrote:
> On Tue, Mar 26, 2019 at 04:41:20PM -0700, Paul E. McKenney wrote:
> > Given that synchronize_rcu_expedited() is supported, this commit adds
> > support for synchronize_srcu_expedited().
> > 
> > Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> > ---
> >  tools/memory-model/linux-kernel.def | 1 +
> >  1 file changed, 1 insertion(+)
> > 
> > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > index 0c3f0ef486f4..551eeaa389d4 100644
> > --- a/tools/memory-model/linux-kernel.def
> > +++ b/tools/memory-model/linux-kernel.def
> > @@ -51,6 +51,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
> >  srcu_read_lock(X)  __srcu{srcu-lock}(X)
> >  srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
> >  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
> > +synchronize_srcu_expedited(X)  { __srcu{sync-srcu}(X); }
> 
> This and the other patches from the series do not apply to "tip/core/rcu"

Ah, that is instead their hoped-for destination within the -tip tree.
They are included in -rcu branch "dev".

> (from the Subject), but this seems straightforward enough:
> 
> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>

Applied, thank you!

							Thanx, Paul

>   Andrea
> 
> 
> >  
> >  // Atomic
> >  atomic_read(X) READ_ONCE(*X)
> > -- 
> > 2.17.1
> > 
> 


^ permalink raw reply	[flat|nested] 28+ messages in thread

* Re: [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section
  2019-04-04 16:40       ` Will Deacon
@ 2019-04-04 22:23         ` Akira Yokosawa
  0 siblings, 0 replies; 28+ messages in thread
From: Akira Yokosawa @ 2019-04-04 22:23 UTC (permalink / raw)
  To: Will Deacon
  Cc: Paul E. McKenney, linux-kernel, linux-arch, mingo, stern,
	andrea.parri, peterz, boqun.feng, npiggin, dhowells, j.alglave,
	luc.maranget, Benjamin Herrenschmidt, Michael Ellerman,
	Arnd Bergmann, Palmer Dabbelt, Daniel Lustig, Linus Torvalds,
	Maciej W. Rozycki, Mikulas Patocka

On Thu, 4 Apr 2019 17:40:22 +0100, Will Deacon wrote:
> Hi Akira,
> 
> On Fri, Apr 05, 2019 at 12:58:36AM +0900, Akira Yokosawa wrote:
>> On Tue, 2 Apr 2019 14:03:46 +0100, Will Deacon wrote:
>>> On Tue, Mar 26, 2019 at 04:41:16PM -0700, Paul E. McKenney wrote:
>>>> From: Will Deacon <will.deacon@arm.com>
>>>>
>>>> The "KERNEL I/O BARRIER EFFECTS" section of memory-barriers.txt is vague,
>>>> x86-centric, out-of-date, incomplete and demonstrably incorrect in places.
>>>> This is largely because I/O ordering is a horrible can of worms, but also
>>>> because the document has stagnated as our understanding has evolved.
>>>>
>>>> Attempt to address some of that, by rewriting the section based on
>>>> recent(-ish) discussions with Arnd, BenH and others. Maybe one day we'll
>>>> find a way to formalise this stuff, but for now let's at least try to
>>>> make the English easier to understand.
>>>>
>>>> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
>>>> Cc: Benjamin Herrenschmidt <benh@kernel.crashing.org>
>>>> Cc: Michael Ellerman <mpe@ellerman.id.au>
>>>> Cc: Arnd Bergmann <arnd@arndb.de>
>>>> Cc: Peter Zijlstra <peterz@infradead.org>
>>>> Cc: Andrea Parri <andrea.parri@amarulasolutions.com>
>>>> Cc: Palmer Dabbelt <palmer@sifive.com>
>>>> Cc: Daniel Lustig <dlustig@nvidia.com>
>>>> Cc: David Howells <dhowells@redhat.com>
>>>> Cc: Alan Stern <stern@rowland.harvard.edu>
>>>> Cc: Linus Torvalds <torvalds@linux-foundation.org>
>>>> Cc: "Maciej W. Rozycki" <macro@linux-mips.org>
>>>> Cc: Mikulas Patocka <mpatocka@redhat.com>
>>>> Signed-off-by: Will Deacon <will.deacon@arm.com>
>>>> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
>>>> ---
>>>>  Documentation/memory-barriers.txt | 115 ++++++++++++++++++------------
>>>>  1 file changed, 70 insertions(+), 45 deletions(-)
>>>
>>> If somebody could provide an Ack on this patch, I'd really appreciate it,
>>> please. Whilst the portable ordering guarantees that I've documented are
>>> fairly conservative, I do think that this change is a big improvement and
>>> gives you what you need if you're writing a portable device driver for a new
>>> piece of hardware. I'm tackling the removal of MMIOWB as a separate series.
>>>
>>> I think Paul now requires an Ack before he'll send a patch to mainline,
>>> hence the grovelling.
>>
>> I'm afraid I'm not that qualified to provide an Ack to this patch,
>> but please find a nit fix below.
> 
> Oh well, thanks for having a look anyway!
> 
>>>> + (*) insX(), outsX():
>>>> +
>>>> +     As above, the insX() and outX() accessors provide the same ordering
>>                                   outsX()
> 
> Thanks; I'll fix that.
> 
>>>> +     guarantees as readsX() and writesX() respectively when accessing a mapping
>>>> +     with the default I/O attributes.
>>>>  
>>>>   (*) ioreadX(), iowriteX()
>>>>  
>>>>       These will perform appropriately for the type of access they're actually
>>>>       doing, be it inX()/outX() or readX()/writeX().
>>>>  
>>>> +All of these accessors assume that the underlying peripheral is little-endian,
>>>> +and will therefore perform byte-swapping operations on big-endian architectures.
>>>> +
>>>> +Composing I/O ordering barriers with SMP ordering barriers and LOCK/UNLOCK
>>>> +operations is a dangerous sport which may require the use of mmiowb(). See the
>>>> +subsection "Acquires vs I/O accesses" for more information.
>>>>  
>>>>  ========================================
>>>>  ASSUMED MINIMUM EXECUTION ORDERING MODEL
>>>> -- 
>>>> 2.17.1
>>>>
>>
>> JFYI, there is another document Documentation/driver-api/device-io.rst,
>> which is somewhat related to this update. It looks like this one also needs
>> some update, as Jon commented in transforming to .rst format in commit
>> 8a8a602fdb83 ("docs: Convert the deviceio template to RST"):
>> <quote>
>>     Like the rest of our documentation, this one could use some work.  There's
>>     no mention of ioremap() and friends, no mention of io_read*() and friends.
>>     But we have nice documentation for all those folks writing new drivers that
>>     do port I/O :).
>> </quote>
>>
>> This commit was merged in v4.11 cycle. And there has been no update whatsoever
>> since. mmiowb() is lightly mentioned therein. IMHO, just updating
>> memory-barriers.txt would widen the gap of information.
>>
>> Thoughts?
> 
> I have a subsequent patch which kills mmiowb() entirely:
> 
> https://git.kernel.org/pub/scm/linux/kernel/git/arm64/linux.git/commit/?h=for-next/mmiowb&id=3c1a2050c08fb8193777b60b49e60320254a156c
> 
> and that one does hit device-io.rst.

Ah, I see.
So can somebody else have a look at this patch and provide an Ack, please?

        Thanks, Akira

> 
> Will
> 


^ permalink raw reply	[flat|nested] 28+ messages in thread

end of thread, other threads:[~2019-04-04 22:24 UTC | newest]

Thread overview: 28+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-03-26 23:41 [PATCH RFC memory-model 0/21] LKMM updates for review Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 01/21] tools/memory-model: Make scripts be executable Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 02/21] tools/memory-model: Fix comment in MP+poonceonces.litmus Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 03/21] tools/memory-model: Do not use "herd" to refer to "herd7" Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 04/21] docs/memory-barriers.txt: Rewrite "KERNEL I/O BARRIER EFFECTS" section Paul E. McKenney
2019-04-02 13:03   ` Will Deacon
2019-04-04 15:58     ` Akira Yokosawa
2019-04-04 16:40       ` Will Deacon
2019-04-04 22:23         ` Akira Yokosawa
2019-03-26 23:41 ` [PATCH tip/core/rcu 05/21] tools/memory-model: Make judgelitmus.sh note timeouts Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 06/21] tools/memory-model: Make cmplitmushist.sh " Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 07/21] tools/memory-model: Make judgelitmus.sh identify bad macros Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 08/21] tools/memory-model: Add support for synchronize_srcu_expedited() Paul E. McKenney
2019-04-02 14:49   ` Andrea Parri
2019-04-04 20:50     ` Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 09/21] tools/memory-model: Make judgelitmus.sh detect hard deadlocks Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 10/21] tools/memory-model: Update parseargs.sh for hardware verification Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 11/21] tools/memory-model: Make judgelitmus.sh handle hardware verifications Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 12/21] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 13/21] tools/memory-model: Fix checkalllitmus.sh comment Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 14/21] tools/memory-model: Hardware checking for check{,all}litmus.sh Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 15/21] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 16/21] tools/memory-model: Split runlitmus.sh out of checklitmus.sh Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 17/21] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 18/21] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 19/21] tools/memory-model: Keep assembly-language litmus tests Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 20/21] tools/memory-model: Allow herd to deduce CPU type Paul E. McKenney
2019-03-26 23:41 ` [PATCH tip/core/rcu 21/21] tools/memory-model: Make runlitmus.sh check for jingle errors Paul E. McKenney

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).