diff options
Diffstat (limited to 'tools/memory-model/README')
| -rw-r--r-- | tools/memory-model/README | 220 |
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. |