=====================================		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.49 of the "herd7" and "klitmus7" tools must be downloadedseparately:   https://github.com/herd/herdtools7 See "herdtools7/INSTALL.md" for installation instructions.  ==================BASIC USAGE: HERD7================== The memory model is used, in conjunction with "herd7", to exhaustivelyexplore 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 thatthis 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" 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.  ====================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 fromthe 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 aremore likely to be addressed by incorporating the Linux-kernel memory modelinto other tools.