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
 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         Note that this limitation in turn limits LKMM's ability to
 175         accurately model address, control, and data dependencies.
 176         For example, if the compiler can deduce the value of some variable
 177         carrying a dependency, then the compiler can break that dependency
 178         by substituting a constant of that value.
 179
 180 2.      Multiple access sizes for a single variable are not supported,
 181         and neither are misaligned or partially overlapping accesses.
 182
 183 3.      Exceptions and interrupts are not modeled.  In some cases,
 184         this limitation can be overcome by modeling the interrupt or
 185         exception with an additional process.
 186
 187 4.      I/O such as MMIO or DMA is not supported.
 188
 189 5.      Self-modifying code (such as that found in the kernel's
 190         alternatives mechanism, function tracer, Berkeley Packet Filter
 191         JIT compiler, and module loader) is not supported.
 192
 193 6.      Complete modeling of all variants of atomic read-modify-write
 194         operations, locking primitives, and RCU is not provided.
 195         For example, call_rcu() and rcu_barrier() are not supported.
 196         However, a substantial amount of support is provided for these
 197         operations, as shown in the linux-kernel.def file.
 198
 199         a.      When rcu_assign_pointer() is passed NULL, the Linux
 200                 kernel provides no ordering, but LKMM models this
 201                 case as a store release.
 202
 203         b.      The "unless" RMW operations are not currently modeled:
 204                 atomic_long_add_unless(), atomic_add_unless(),
 205                 atomic_inc_unless_negative(), and
 206                 atomic_dec_unless_positive().  These can be emulated
 207                 in litmus tests, for example, by using atomic_cmpxchg().
 208
 209         c.      The call_rcu() function is not modeled.  It can be
 210                 emulated in litmus tests by adding another process that
 211                 invokes synchronize_rcu() and the body of the callback
 212                 function, with (for example) a release-acquire from
 213                 the site of the emulated call_rcu() to the beginning
 214                 of the additional process.
 215
 216         d.      The rcu_barrier() function is not modeled.  It can be
 217                 emulated in litmus tests emulating call_rcu() via
 218                 (for example) a release-acquire from the end of each
 219                 additional call_rcu() process to the site of the
 220                 emulated rcu-barrier().
 221
 222         e.      Sleepable RCU (SRCU) is not modeled.  It can be
 223                 emulated, but perhaps not simply.
 224
 225         f.      Reader-writer locking is not modeled.  It can be
 226                 emulated in litmus tests using atomic read-modify-write
 227                 operations.
 228
 229 The "herd7" tool has some additional limitations of its own, apart from
 230 the memory model:
 231
 232 1.      Non-trivial data structures such as arrays or structures are
 233         not supported.  However, pointers are supported, allowing trivial
 234         linked lists to be constructed.
 235
 236 2.      Dynamic memory allocation is not supported, although this can
 237         be worked around in some cases by supplying multiple statically
 238         allocated variables.
 239
 240 Some of these limitations may be overcome in the future, but others are
 241 more likely to be addressed by incorporating the Linux-kernel memory model
 242 into other tools.
 243
 244 Finally, please note that LKMM is subject to change as hardware, use cases,
 245 and compilers evolve.