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.52 or higher of the "herd7" and "klitmus7" tools must be
  24 downloaded separately:
  25
  26   https://github.com/herd/herdtools7
  27
  28 See "herdtools7/INSTALL.md" for installation instructions.
  29
  30 Note that although these tools usually provide backwards compatibility,
  31 this is not absolutely guaranteed.
  32
  33 For example, a future version of herd7 might not work with the model
  34 in this release.  A compatible model will likely be made available in
  35 a later release of Linux kernel.
  36
  37 If you absolutely need to run the model in this particular release,
  38 please try using the exact version called out above.
  39
  40 klitmus7 is independent of the model provided here.  It has its own
  41 dependency on a target kernel release where converted code is built
  42 and executed.  Any change in kernel APIs essential to klitmus7 will
  43 necessitate an upgrade of klitmus7.
  44
  45 If you find any compatibility issues in klitmus7, please inform the
  46 memory model maintainers.
  47
  48 klitmus7 Compatibility Table
  49 ----------------------------
  50
  51         ============  ==========
  52         target Linux  herdtools7
  53         ------------  ----------
  54              -- 4.18  7.48 --
  55         4.15 -- 4.19  7.49 --
  56         4.20 -- 5.5   7.54 --
  57         5.6  --       7.56 --
  58         ============  ==========
  59
  60
  61 ==================
  62 BASIC USAGE: HERD7
  63 ==================
  64
  65 The memory model is used, in conjunction with "herd7", to exhaustively
  66 explore the state space of small litmus tests.
  67
  68 For example, to run SB+fencembonceonces.litmus against the memory model:
  69
  70   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
  71
  72 Here is the corresponding output:
  73
  74   Test SB+fencembonceonces Allowed
  75   States 3
  76   0:r0=0; 1:r0=1;
  77   0:r0=1; 1:r0=0;
  78   0:r0=1; 1:r0=1;
  79   No
  80   Witnesses
  81   Positive: 0 Negative: 3
  82   Condition exists (0:r0=0 /\ 1:r0=0)
  83   Observation SB+fencembonceonces Never 0 3
  84   Time SB+fencembonceonces 0.01
  85   Hash=d66d99523e2cac6b06e66f4c995ebb48
  86
  87 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
  88 this litmus test's "exists" clause can not be satisfied.
  89
  90 See "herd7 -help" or "herdtools7/doc/" for more information.
  91
  92
  93 =====================
  94 BASIC USAGE: KLITMUS7
  95 =====================
  96
  97 The "klitmus7" tool converts a litmus test into a Linux kernel module,
  98 which may then be loaded and run.
  99
 100 For example, to run SB+fencembonceonces.litmus against hardware:
 101
 102   $ mkdir mymodules
 103   $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
 104   $ cd mymodules ; make
 105   $ sudo sh run.sh
 106
 107 The corresponding output includes:
 108
 109   Test SB+fencembonceonces Allowed
 110   Histogram (3 states)
 111   644580  :>0:r0=1; 1:r0=0;
 112   644328  :>0:r0=0; 1:r0=1;
 113   711092  :>0:r0=1; 1:r0=1;
 114   No
 115   Witnesses
 116   Positive: 0, Negative: 2000000
 117   Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
 118   Hash=d66d99523e2cac6b06e66f4c995ebb48
 119   Observation SB+fencembonceonces Never 0 2000000
 120   Time SB+fencembonceonces 0.16
 121
 122 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
 123 that during two million trials, the state specified in this litmus
 124 test's "exists" clause was not reached.
 125
 126 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
 127 for more information.
 128
 129
 130 ====================
 131 DESCRIPTION OF FILES
 132 ====================
 133
 134 Documentation/cheatsheet.txt
 135         Quick-reference guide to the Linux-kernel memory model.
 136
 137 Documentation/explanation.txt
 138         Describes the memory model in detail.
 139
 140 Documentation/recipes.txt
 141         Lists common memory-ordering patterns.
 142
 143 Documentation/references.txt
 144         Provides background reading.
 145
 146 linux-kernel.bell
 147         Categorizes the relevant instructions, including memory
 148         references, memory barriers, atomic read-modify-write operations,
 149         lock acquisition/release, and RCU operations.
 150
 151         More formally, this file (1) lists the subtypes of the various
 152         event types used by the memory model and (2) performs RCU
 153         read-side critical section nesting analysis.
 154
 155 linux-kernel.cat
 156         Specifies what reorderings are forbidden by memory references,
 157         memory barriers, atomic read-modify-write operations, and RCU.
 158
 159         More formally, this file specifies what executions are forbidden
 160         by the memory model.  Allowed executions are those which
 161         satisfy the model's "coherence", "atomic", "happens-before",
 162         "propagation", and "rcu" axioms, which are defined in the file.
 163
 164 linux-kernel.cfg
 165         Convenience file that gathers the common-case herd7 command-line
 166         arguments.
 167
 168 linux-kernel.def
 169         Maps from C-like syntax to herd7's internal litmus-test
 170         instruction-set architecture.
 171
 172 litmus-tests
 173         Directory containing a few representative litmus tests, which
 174         are listed in litmus-tests/README.  A great deal more litmus
 175         tests are available at https://github.com/paulmckrcu/litmus.
 176
 177 lock.cat
 178         Provides a front-end analysis of lock acquisition and release,
 179         for example, associating a lock acquisition with the preceding
 180         and following releases and checking for self-deadlock.
 181
 182         More formally, this file defines a performance-enhanced scheme
 183         for generation of the possible reads-from and coherence order
 184         relations on the locking primitives.
 185
 186 README
 187         This file.
 188
 189 scripts Various scripts, see scripts/README.
 190
 191
 192 ===========
 193 LIMITATIONS
 194 ===========
 195
 196 The Linux-kernel memory model (LKMM) has the following limitations:
 197
 198 1.      Compiler optimizations are not accurately modeled.  Of course,
 199         the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
 200         ability to optimize, but under some circumstances it is possible
 201         for the compiler to undermine the memory model.  For more
 202         information, see Documentation/explanation.txt (in particular,
 203         the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
 204         sections).
 205
 206         Note that this limitation in turn limits LKMM's ability to
 207         accurately model address, control, and data dependencies.
 208         For example, if the compiler can deduce the value of some variable
 209         carrying a dependency, then the compiler can break that dependency
 210         by substituting a constant of that value.
 211
 212 2.      Multiple access sizes for a single variable are not supported,
 213         and neither are misaligned or partially overlapping accesses.
 214
 215 3.      Exceptions and interrupts are not modeled.  In some cases,
 216         this limitation can be overcome by modeling the interrupt or
 217         exception with an additional process.
 218
 219 4.      I/O such as MMIO or DMA is not supported.
 220
 221 5.      Self-modifying code (such as that found in the kernel's
 222         alternatives mechanism, function tracer, Berkeley Packet Filter
 223         JIT compiler, and module loader) is not supported.
 224
 225 6.      Complete modeling of all variants of atomic read-modify-write
 226         operations, locking primitives, and RCU is not provided.
 227         For example, call_rcu() and rcu_barrier() are not supported.
 228         However, a substantial amount of support is provided for these
 229         operations, as shown in the linux-kernel.def file.
 230
 231         a.      When rcu_assign_pointer() is passed NULL, the Linux
 232                 kernel provides no ordering, but LKMM models this
 233                 case as a store release.
 234
 235         b.      The "unless" RMW operations are not currently modeled:
 236                 atomic_long_add_unless(), atomic_inc_unless_negative(),
 237                 and atomic_dec_unless_positive().  These can be emulated
 238                 in litmus tests, for example, by using atomic_cmpxchg().
 239
 240                 One exception of this limitation is atomic_add_unless(),
 241                 which is provided directly by herd7 (so no corresponding
 242                 definition in linux-kernel.def).  atomic_add_unless() is
 243                 modeled by herd7 therefore it can be used in litmus tests.
 244
 245         c.      The call_rcu() function is not modeled.  It can be
 246                 emulated in litmus tests by adding another process that
 247                 invokes synchronize_rcu() and the body of the callback
 248                 function, with (for example) a release-acquire from
 249                 the site of the emulated call_rcu() to the beginning
 250                 of the additional process.
 251
 252         d.      The rcu_barrier() function is not modeled.  It can be
 253                 emulated in litmus tests emulating call_rcu() via
 254                 (for example) a release-acquire from the end of each
 255                 additional call_rcu() process to the site of the
 256                 emulated rcu-barrier().
 257
 258         e.      Although sleepable RCU (SRCU) is now modeled, there
 259                 are some subtle differences between its semantics and
 260                 those in the Linux kernel.  For example, the kernel
 261                 might interpret the following sequence as two partially
 262                 overlapping SRCU read-side critical sections:
 263
 264                          1  r1 = srcu_read_lock(&my_srcu);
 265                          2  do_something_1();
 266                          3  r2 = srcu_read_lock(&my_srcu);
 267                          4  do_something_2();
 268                          5  srcu_read_unlock(&my_srcu, r1);
 269                          6  do_something_3();
 270                          7  srcu_read_unlock(&my_srcu, r2);
 271
 272                 In contrast, LKMM will interpret this as a nested pair of
 273                 SRCU read-side critical sections, with the outer critical
 274                 section spanning lines 1-7 and the inner critical section
 275                 spanning lines 3-5.
 276
 277                 This difference would be more of a concern had anyone
 278                 identified a reasonable use case for partially overlapping
 279                 SRCU read-side critical sections.  For more information,
 280                 please see: https://paulmck.livejournal.com/40593.html
 281
 282         f.      Reader-writer locking is not modeled.  It can be
 283                 emulated in litmus tests using atomic read-modify-write
 284                 operations.
 285
 286 The "herd7" tool has some additional limitations of its own, apart from
 287 the memory model:
 288
 289 1.      Non-trivial data structures such as arrays or structures are
 290         not supported.  However, pointers are supported, allowing trivial
 291         linked lists to be constructed.
 292
 293 2.      Dynamic memory allocation is not supported, although this can
 294         be worked around in some cases by supplying multiple statically
 295         allocated variables.
 296
 297 Some of these limitations may be overcome in the future, but others are
 298 more likely to be addressed by incorporating the Linux-kernel memory model
 299 into other tools.
 300
 301 Finally, please note that LKMM is subject to change as hardware, use cases,
 302 and compilers evolve.