=====================================		LINUX KERNEL MEMORY CONSISTENCY MODEL		===================================== ============INTRODUCTION============ This directory contains the memory consistency model (memory model, forshort) of the Linux kernel, written in the "cat" language and executableby the externally provided "herd7" simulator, which exhaustively exploresthe state space of small litmus tests. In addition, the "klitmus7" tool (also externally provided) may be usedto convert a litmus test to a Linux kernel module, which in turn allowsthat litmus test to be exercised within the Linux kernel.  ============REQUIREMENTS============ Version 7.58 or higher of the "herd7" and "klitmus7" tools must bedownloaded separately:   https://github.com/herd/herdtools7 See "herdtools7/INSTALL.md" for installation instructions. Note that although these tools usually provide backwards compatibility,this is not absolutely guaranteed. For example, a future version of herd7 might not work with the modelin this release.  A compatible model will likely be made available ina later release of Linux kernel. If you absolutely need to run the model in this particular release,please try using the exact version called out above. klitmus7 is independent of the model provided here.  It has its owndependency on a target kernel release where converted code is builtand executed.  Any change in kernel APIs essential to klitmus7 willnecessitate an upgrade of klitmus7. If you find any compatibility issues in klitmus7, please inform thememory model maintainers. klitmus7 Compatibility Table---------------------------- 	============  ==========	target Linux  herdtools7	------------  ----------	     -- 4.14  7.48 --	4.15 -- 4.19  7.49 --	4.20 -- 5.5   7.54 --	5.6  -- 5.16  7.56 --	5.17 --       7.56.1 --	============  ==========  ==================BASIC USAGE: HERD7================== The memory model is used, in conjunction with "herd7", to exhaustivelyexplore the state space of small litmus tests.  Documentation describingthe format, features, capabilities and limitations of these litmustests is available in tools/memory-model/Documentation/litmus-tests.txt. Example litmus tests may be found in the Linux-kernel source tree: 	tools/memory-model/litmus-tests/	Documentation/litmus-tests/ Several thousand more example litmus tests are available here: 	https://github.com/paulmckrcu/litmus	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus Documentation describing litmus tests and how to use them may be foundhere: 	tools/memory-model/Documentation/litmus-tests.txt The remainder of this section uses the SB+fencembonceonces.litmus testlocated in the tools/memory-model directory. To run SB+fencembonceonces.litmus against the memory model:   $ cd $LINUX_SOURCE_TREE/tools/memory-model  $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus Here is the corresponding output:   Test SB+fencembonceonces 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+fencembonceonces Never 0 3  Time SB+fencembonceonces 0.01  Hash=d66d99523e2cac6b06e66f4c995ebb48 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate thatthis litmus test's "exists" clause can not be satisfied. See "herd7 -help" or "herdtools7/doc/" for more information on running thetool itself, but please be aware that this documentation is intended forpeople who work on the memory model itself, that is, people making changesto the tools/memory-model/linux-kernel.* files.  It is not intended forpeople focusing on writing, understanding, and running LKMM litmus tests.  =====================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+fencembonceonces.litmus against hardware:   $ mkdir mymodules  $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus  $ cd mymodules ; make  $ sudo sh run.sh The corresponding output includes:   Test SB+fencembonceonces 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+fencembonceonces Never 0 2000000  Time SB+fencembonceonces 0.16 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicatethat during two million trials, the state specified in this litmustest's "exists" clause was not reached. And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"for more information.  And again, please be aware that this documentationis intended for people who work on the memory model itself, that is,people making changes to the tools/memory-model/linux-kernel.* files.It is not intended for people focusing on writing, understanding, andrunning LKMM litmus tests.  ====================DESCRIPTION OF FILES==================== Documentation/README	Guide to the other documents in the Documentation/ directory. 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. 	By "representative", it means the one in the litmus-tests	directory is: 		1) simple, the number of threads should be relatively		   small and each thread function should be relatively		   simple.		2) orthogonal, there should be no two litmus tests		   describing the same aspect of the memory model.		3) textbook, developers can easily copy-paste-modify		   the litmus tests to use the patterns on their own		   code. 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. scripts	Various scripts, see scripts/README.