Automate memory-barriers.txt; provide Linux-kernel memory model

There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test".  This tool's functionality is roughly similar to
a full state-space search.  Please note that this is a design-time tool,
not useful for regression testing.  However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.

The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch.  The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model.  A brief description of each of these other files is provided
in the README file.  Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).

A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing.  As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).

Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail.  In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.

This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.

This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget.  For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference.  However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015.  This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers.  This prompted a copyright review.

From Alan Stern:

	To say that the model was mine is not entirely accurate.
	Pieces of it (especially the Scpv and Atomic axioms) were taken
	directly from Jade's models.  And of course the Happens-before
	and Propagation relations and axioms were heavily based on
	Jade and Luc's work, even though they weren't identical to the
	earlier versions.  Only the RCU portion was completely original.

	. . .

	One can make a much better case that I wrote the bulk of lock.cat.
	However, it was inspired by Luc's earlier version (and still
	shares some elements in common), and of course it benefited from
	feedback and testing from all members of our group.

The model prior to Alan's was Luc Maranget's.  From Luc:

	 I totally agree on Alan Stern's account of the linux kernel model
	 genesis.  I thank him for his acknowledgments of my participation
	 to previous model drafts.  I'd like to complete Alan Stern's
	 statement: any bell cat code I have written has its roots in
	 discussions with Jade Alglave and Paul McKenney. Moreover I
	 have borrowed cat and bell code written by Jade Alglave freely.

This copyright review therefore resulted in late adds to the copyright
statements of several files.

Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:

o	Under what conditions should ordering provided by pure locking
	be seen by CPUs not holding the relevant lock(s)?  In particular,
	should the message-passing pattern be forbidden?

o	Should examples involving C11 release sequences be forbidden?
	Note that this C11 is still a moving target for this issue:
	http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html

o	Some details of the handling of internal dependencies for atomic
	read-modify-write atomic operations are still subject to debate.

o	Changes recently accepted into mainline greatly reduce the need
	to handle DEC Alpha as a special case.  These changes add an
	smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
	to respect ordering of dependent reads.  If these changes stick,
	the memory model can be simplified accordingly.

o	Will changes be required to accommodate RISC-V?

Differences from v1:
	(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)

o	Add SPDX notations to .bell and .cat files, replacing
	textual license statements.

o	Add reference to upcoming ASPLOS paper to .bell and .cat files.

o	Updated identifier names in .bell and .cat files to match those
	used in the ASPLOS paper.

o	Updates to READMEs and other documentation based on review
	feedback.

o	Added a memory-ordering cheatsheet.

o	Update sigs to new Co-Developed-by and add acks and
	reviewed-bys.

o	Simplify rules detecting nested RCU read-side critical sections.

o	Update copyright statements as noted above.

Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>

1 files changed, 220 insertions, 0 deletions

diff --git a/tools/memory-model/README b/tools/memory-model/README
new file mode 100644
index 000000000000..43ba49492111
--- /dev/null
+++ b/tools/memory-model/README
@@ -0,0 +1,220 @@
+			=========================
+			LINUX KERNEL MEMORY MODEL
+			=========================
+
+============
+INTRODUCTION
+============
+
+This directory contains the memory model of the Linux kernel, written
+in the "cat" language and executable by the (externally provided)
+"herd7" simulator, which exhaustively explores the state space of
+small litmus tests.
+
+In addition, the "klitmus7" tool (also externally provided) may be used
+to convert a litmus test to a Linux kernel module, which in turn allows
+that litmus test to be exercised within the Linux kernel.
+
+
+============
+REQUIREMENTS
+============
+
+The "herd7" and "klitmus7" tools must be downloaded separately:
+
+  https://github.com/herd/herdtools7
+
+See "herdtools7/INSTALL.md" for installation instructions.
+
+Alternatively, Abhishek Bhardwaj has kindly provided a Docker image
+of these tools at "abhishek40/memory-model".  Abhishek suggests the
+following commands to install and use this image:
+
+  - Users should install Docker for their distribution.
+  - docker run -itd abhishek40/memory-model
+  - docker attach <id-emitted-from-the-previous-command>
+
+Gentoo users might wish to make use of Patrick McLean's package:
+
+  https://gitweb.gentoo.org/repo/gentoo.git/tree/dev-util/herdtools7
+
+These packages may not be up-to-date with respect to the GitHub
+repository.
+
+
+==================
+BASIC USAGE: HERD7
+==================
+
+The memory model is used, in conjunction with "herd7", to exhaustively
+explore the state space of small litmus tests.
+
+For example, to run SB+mbonceonces.litmus against the memory model:
+
+  $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus
+
+Here is the corresponding output:
+
+  Test SB+mbonceonces Allowed
+  States 3
+  0:r0=0; 1:r0=1;
+  0:r0=1; 1:r0=0;
+  0:r0=1; 1:r0=1;
+  No
+  Witnesses
+  Positive: 0 Negative: 3
+  Condition exists (0:r0=0 /\ 1:r0=0)
+  Observation SB+mbonceonces Never 0 3
+  Time SB+mbonceonces 0.01
+  Hash=d66d99523e2cac6b06e66f4c995ebb48
+
+The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
+this litmus test's "exists" clause can not be satisfied.
+
+See "herd7 -help" or "herdtools7/doc/" for more information.
+
+
+=====================
+BASIC USAGE: KLITMUS7
+=====================
+
+The "klitmus7" tool converts a litmus test into a Linux kernel module,
+which may then be loaded and run.
+
+For example, to run SB+mbonceonces.litmus against hardware:
+
+  $ mkdir mymodules
+  $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus
+  $ cd mymodules ; make
+  $ sudo sh run.sh
+
+The corresponding output includes:
+
+  Test SB+mbonceonces Allowed
+  Histogram (3 states)
+  644580  :>0:r0=1; 1:r0=0;
+  644328  :>0:r0=0; 1:r0=1;
+  711092  :>0:r0=1; 1:r0=1;
+  No
+  Witnesses
+  Positive: 0, Negative: 2000000
+  Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
+  Hash=d66d99523e2cac6b06e66f4c995ebb48
+  Observation SB+mbonceonces Never 0 2000000
+  Time SB+mbonceonces 0.16
+
+The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
+that during two million trials, the state specified in this litmus
+test's "exists" clause was not reached.
+
+And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
+for more information.
+
+
+====================
+DESCRIPTION OF FILES
+====================
+
+Documentation/cheatsheet.txt
+	Quick-reference guide to the Linux-kernel memory model.
+
+Documentation/explanation.txt
+	Describes the memory model in detail.
+
+Documentation/recipes.txt
+	Lists common memory-ordering patterns.
+
+Documentation/references.txt
+	Provides background reading.
+
+linux-kernel.bell
+	Categorizes the relevant instructions, including memory
+	references, memory barriers, atomic read-modify-write operations,
+	lock acquisition/release, and RCU operations.
+
+	More formally, this file (1) lists the subtypes of the various
+	event types used by the memory model and (2) performs RCU
+	read-side critical section nesting analysis.
+
+linux-kernel.cat
+	Specifies what reorderings are forbidden by memory references,
+	memory barriers, atomic read-modify-write operations, and RCU.
+
+	More formally, this file specifies what executions are forbidden
+	by the memory model.  Allowed executions are those which
+	satisfy the model's "coherence", "atomic", "happens-before",
+	"propagation", and "rcu" axioms, which are defined in the file.
+
+linux-kernel.cfg
+	Convenience file that gathers the common-case herd7 command-line
+	arguments.
+
+linux-kernel.def
+	Maps from C-like syntax to herd7's internal litmus-test
+	instruction-set architecture.
+
+litmus-tests
+	Directory containing a few representative litmus tests, which
+	are listed in litmus-tests/README.  A great deal more litmus
+	tests are available at https://github.com/paulmckrcu/litmus.
+
+lock.cat
+	Provides a front-end analysis of lock acquisition and release,
+	for example, associating a lock acquisition with the preceding
+	and following releases and checking for self-deadlock.
+
+	More formally, this file defines a performance-enhanced scheme
+	for generation of the possible reads-from and coherence order
+	relations on the locking primitives.
+
+README
+	This file.
+
+
+===========
+LIMITATIONS
+===========
+
+The Linux-kernel memory model has the following limitations:
+
+1.	Compiler optimizations are not modeled.  Of course, the use
+	of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
+	to optimize, but there is Linux-kernel code that uses bare C
+	memory accesses.  Handling this code is on the to-do list.
+	For more information, see Documentation/explanation.txt (in
+	particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
+	and "A WARNING" sections).
+
+2.	Multiple access sizes for a single variable are not supported,
+	and neither are misaligned or partially overlapping accesses.
+
+3.	Exceptions and interrupts are not modeled.  In some cases,
+	this limitation can be overcome by modeling the interrupt or
+	exception with an additional process.
+
+4.	I/O such as MMIO or DMA is not supported.
+
+5.	Self-modifying code (such as that found in the kernel's
+	alternatives mechanism, function tracer, Berkeley Packet Filter
+	JIT compiler, and module loader) is not supported.
+
+6.	Complete modeling of all variants of atomic read-modify-write
+	operations, locking primitives, and RCU is not provided.
+	For example, call_rcu() and rcu_barrier() are not supported.
+	However, a substantial amount of support is provided for these
+	operations, as shown in the linux-kernel.def file.
+
+The "herd7" tool has some additional limitations of its own, apart from
+the memory model:
+
+1.	Non-trivial data structures such as arrays or structures are
+	not supported.	However, pointers are supported, allowing trivial
+	linked lists to be constructed.
+
+2.	Dynamic memory allocation is not supported, although this can
+	be worked around in some cases by supplying multiple statically
+	allocated variables.
+
+Some of these limitations may be overcome in the future, but others are
+more likely to be addressed by incorporating the Linux-kernel memory model
+into other tools.