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.49 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+fencembonceonces.litmus against the memory model:
  39
  40   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
  41
  42 Here is the corresponding output:
  43
  44   Test SB+fencembonceonces 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+fencembonceonces Never 0 3
  54   Time SB+fencembonceonces 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+fencembonceonces.litmus against hardware:
  71
  72   $ mkdir mymodules
  73   $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
  74   $ cd mymodules ; make
  75   $ sudo sh run.sh
  76
  77 The corresponding output includes:
  78
  79   Test SB+fencembonceonces 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+fencembonceonces Never 0 2000000
  90   Time SB+fencembonceonces 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 scripts Various scripts, see scripts/README.
 160
 161
 162 ===========
 163 LIMITATIONS
 164 ===========
 165
 166 The Linux-kernel memory model has the following limitations:
 167
 168 1.      Compiler optimizations are not modeled.  Of course, the use
 169         of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
 170         to optimize, but there is Linux-kernel code that uses bare C
 171         memory accesses.  Handling this code is on the to-do list.
 172         For more information, see Documentation/explanation.txt (in
 173         particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
 174         and "A WARNING" sections).
 175
 176         Note that this limitation in turn limits LKMM's ability to
 177         accurately model address, control, and data dependencies.
 178         For example, if the compiler can deduce the value of some variable
 179         carrying a dependency, then the compiler can break that dependency
 180         by substituting a constant of that value.
 181
 182 2.      Multiple access sizes for a single variable are not supported,
 183         and neither are misaligned or partially overlapping accesses.
 184
 185 3.      Exceptions and interrupts are not modeled.  In some cases,
 186         this limitation can be overcome by modeling the interrupt or
 187         exception with an additional process.
 188
 189 4.      I/O such as MMIO or DMA is not supported.
 190
 191 5.      Self-modifying code (such as that found in the kernel's
 192         alternatives mechanism, function tracer, Berkeley Packet Filter
 193         JIT compiler, and module loader) is not supported.
 194
 195 6.      Complete modeling of all variants of atomic read-modify-write
 196         operations, locking primitives, and RCU is not provided.
 197         For example, call_rcu() and rcu_barrier() are not supported.
 198         However, a substantial amount of support is provided for these
 199         operations, as shown in the linux-kernel.def file.
 200
 201         a.      When rcu_assign_pointer() is passed NULL, the Linux
 202                 kernel provides no ordering, but LKMM models this
 203                 case as a store release.
 204
 205         b.      The "unless" RMW operations are not currently modeled:
 206                 atomic_long_add_unless(), atomic_add_unless(),
 207                 atomic_inc_unless_negative(), and
 208                 atomic_dec_unless_positive().  These can be emulated
 209                 in litmus tests, for example, by using atomic_cmpxchg().
 210
 211         c.      The call_rcu() function is not modeled.  It can be
 212                 emulated in litmus tests by adding another process that
 213                 invokes synchronize_rcu() and the body of the callback
 214                 function, with (for example) a release-acquire from
 215                 the site of the emulated call_rcu() to the beginning
 216                 of the additional process.
 217
 218         d.      The rcu_barrier() function is not modeled.  It can be
 219                 emulated in litmus tests emulating call_rcu() via
 220                 (for example) a release-acquire from the end of each
 221                 additional call_rcu() process to the site of the
 222                 emulated rcu-barrier().
 223
 224         e.      Sleepable RCU (SRCU) is not modeled.  It can be
 225                 emulated, but perhaps not simply.
 226
 227         f.      Reader-writer locking is not modeled.  It can be
 228                 emulated in litmus tests using atomic read-modify-write
 229                 operations.
 230
 231 The "herd7" tool has some additional limitations of its own, apart from
 232 the memory model:
 233
 234 1.      Non-trivial data structures such as arrays or structures are
 235         not supported.  However, pointers are supported, allowing trivial
 236         linked lists to be constructed.
 237
 238 2.      Dynamic memory allocation is not supported, although this can
 239         be worked around in some cases by supplying multiple statically
 240         allocated variables.
 241
 242 Some of these limitations may be overcome in the future, but others are
 243 more likely to be addressed by incorporating the Linux-kernel memory model
 244 into other tools.
 245
 246 Finally, please note that LKMM is subject to change as hardware, use cases,
 247 and compilers evolve.