tools/memory-model/README

   1                 =====================================
   2                 LINUX KERNEL MEMORY CONSISTENCY MODEL
   3                 =====================================
   4
   5 ============
   6 INTRODUCTION
   7 ============
   8
   9 This directory contains the memory consistency model (memory model, for
  10 short) of the Linux kernel, written in the "cat" language and executable
  11 by the externally provided "herd7" simulator, which exhaustively explores
  12 the state space of small litmus tests.
  13
  14 In addition, the "klitmus7" tool (also externally provided) may be used
  15 to convert a litmus test to a Linux kernel module, which in turn allows
  16 that litmus test to be exercised within the Linux kernel.
  17
  18
  19 ============
  20 REQUIREMENTS
  21 ============
  22
  23 Version 7.48 of the "herd7" and "klitmus7" tools must be downloaded
  24 separately:
  25
  26   https://github.com/herd/herdtools7
  27
  28 See "herdtools7/INSTALL.md" for installation instructions.
  29
  30
  31 ==================
  32 BASIC USAGE: HERD7
  33 ==================
  34
  35 The memory model is used, in conjunction with "herd7", to exhaustively
  36 explore the state space of small litmus tests.
  37
  38 For example, to run SB+mbonceonces.litmus against the memory model:
  39
  40   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus
  41
  42 Here is the corresponding output:
  43
  44   Test SB+mbonceonces Allowed
  45   States 3
  46   0:r0=0; 1:r0=1;
  47   0:r0=1; 1:r0=0;
  48   0:r0=1; 1:r0=1;
  49   No
  50   Witnesses
  51   Positive: 0 Negative: 3
  52   Condition exists (0:r0=0 /\ 1:r0=0)
  53   Observation SB+mbonceonces Never 0 3
  54   Time SB+mbonceonces 0.01
  55   Hash=d66d99523e2cac6b06e66f4c995ebb48
  56
  57 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
  58 this litmus test's "exists" clause can not be satisfied.
  59
  60 See "herd7 -help" or "herdtools7/doc/" for more information.
  61
  62
  63 =====================
  64 BASIC USAGE: KLITMUS7
  65 =====================
  66
  67 The "klitmus7" tool converts a litmus test into a Linux kernel module,
  68 which may then be loaded and run.
  69
  70 For example, to run SB+mbonceonces.litmus against hardware:
  71
  72   $ mkdir mymodules
  73   $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus
  74   $ cd mymodules ; make
  75   $ sudo sh run.sh
  76
  77 The corresponding output includes:
  78
  79   Test SB+mbonceonces Allowed
  80   Histogram (3 states)
  81   644580  :>0:r0=1; 1:r0=0;
  82   644328  :>0:r0=0; 1:r0=1;
  83   711092  :>0:r0=1; 1:r0=1;
  84   No
  85   Witnesses
  86   Positive: 0, Negative: 2000000
  87   Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
  88   Hash=d66d99523e2cac6b06e66f4c995ebb48
  89   Observation SB+mbonceonces Never 0 2000000
  90   Time SB+mbonceonces 0.16
  91
  92 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
  93 that during two million trials, the state specified in this litmus
  94 test's "exists" clause was not reached.
  95
  96 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
  97 for more information.
  98
  99
 100 ====================
 101 DESCRIPTION OF FILES
 102 ====================
 103
 104 Documentation/cheatsheet.txt
 105         Quick-reference guide to the Linux-kernel memory model.
 106
 107 Documentation/explanation.txt
 108         Describes the memory model in detail.
 109
 110 Documentation/recipes.txt
 111         Lists common memory-ordering patterns.
 112
 113 Documentation/references.txt
 114         Provides background reading.
 115
 116 linux-kernel.bell
 117         Categorizes the relevant instructions, including memory
 118         references, memory barriers, atomic read-modify-write operations,
 119         lock acquisition/release, and RCU operations.
 120
 121         More formally, this file (1) lists the subtypes of the various
 122         event types used by the memory model and (2) performs RCU
 123         read-side critical section nesting analysis.
 124
 125 linux-kernel.cat
 126         Specifies what reorderings are forbidden by memory references,
 127         memory barriers, atomic read-modify-write operations, and RCU.
 128
 129         More formally, this file specifies what executions are forbidden
 130         by the memory model.  Allowed executions are those which
 131         satisfy the model's "coherence", "atomic", "happens-before",
 132         "propagation", and "rcu" axioms, which are defined in the file.
 133
 134 linux-kernel.cfg
 135         Convenience file that gathers the common-case herd7 command-line
 136         arguments.
 137
 138 linux-kernel.def
 139         Maps from C-like syntax to herd7's internal litmus-test
 140         instruction-set architecture.
 141
 142 litmus-tests
 143         Directory containing a few representative litmus tests, which
 144         are listed in litmus-tests/README.  A great deal more litmus
 145         tests are available at https://github.com/paulmckrcu/litmus.
 146
 147 lock.cat
 148         Provides a front-end analysis of lock acquisition and release,
 149         for example, associating a lock acquisition with the preceding
 150         and following releases and checking for self-deadlock.
 151
 152         More formally, this file defines a performance-enhanced scheme
 153         for generation of the possible reads-from and coherence order
 154         relations on the locking primitives.
 155
 156 README
 157         This file.
 158
 159
 160 ===========
 161 LIMITATIONS
 162 ===========
 163
 164 The Linux-kernel memory model has the following limitations:
 165
 166 1.      Compiler optimizations are not modeled.  Of course, the use
 167         of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
 168         to optimize, but there is Linux-kernel code that uses bare C
 169         memory accesses.  Handling this code is on the to-do list.
 170         For more information, see Documentation/explanation.txt (in
 171         particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
 172         and "A WARNING" sections).
 173
 174 2.      Multiple access sizes for a single variable are not supported,
 175         and neither are misaligned or partially overlapping accesses.
 176
 177 3.      Exceptions and interrupts are not modeled.  In some cases,
 178         this limitation can be overcome by modeling the interrupt or
 179         exception with an additional process.
 180
 181 4.      I/O such as MMIO or DMA is not supported.
 182
 183 5.      Self-modifying code (such as that found in the kernel's
 184         alternatives mechanism, function tracer, Berkeley Packet Filter
 185         JIT compiler, and module loader) is not supported.
 186
 187 6.      Complete modeling of all variants of atomic read-modify-write
 188         operations, locking primitives, and RCU is not provided.
 189         For example, call_rcu() and rcu_barrier() are not supported.
 190         However, a substantial amount of support is provided for these
 191         operations, as shown in the linux-kernel.def file.
 192
 193 The "herd7" tool has some additional limitations of its own, apart from
 194 the memory model:
 195
 196 1.      Non-trivial data structures such as arrays or structures are
 197         not supported.  However, pointers are supported, allowing trivial
 198         linked lists to be constructed.
 199
 200 2.      Dynamic memory allocation is not supported, although this can
 201         be worked around in some cases by supplying multiple statically
 202         allocated variables.
 203
 204 Some of these limitations may be overcome in the future, but others are
 205 more likely to be addressed by incorporating the Linux-kernel memory model
 206 into other tools.