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.  Documentation describing
  67 the format, features, capabilities and limitations of these litmus
  68 tests is available in tools/memory-model/Documentation/litmus-tests.txt.
  69
  70 Example litmus tests may be found in the Linux-kernel source tree:
  71
  72         tools/memory-model/litmus-tests/
  73         Documentation/litmus-tests/
  74
  75 Several thousand more example litmus tests are available here:
  76
  77         https://github.com/paulmckrcu/litmus
  78         https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
  79         https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
  80
  81 Documentation describing litmus tests and now to use them may be found
  82 here:
  83
  84         tools/memory-model/Documentation/litmus-tests.txt
  85
  86 The remainder of this section uses the SB+fencembonceonces.litmus test
  87 located in the tools/memory-model directory.
  88
  89 To run SB+fencembonceonces.litmus against the memory model:
  90
  91   $ cd $LINUX_SOURCE_TREE/tools/memory-model
  92   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
  93
  94 Here is the corresponding output:
  95
  96   Test SB+fencembonceonces Allowed
  97   States 3
  98   0:r0=0; 1:r0=1;
  99   0:r0=1; 1:r0=0;
 100   0:r0=1; 1:r0=1;
 101   No
 102   Witnesses
 103   Positive: 0 Negative: 3
 104   Condition exists (0:r0=0 /\ 1:r0=0)
 105   Observation SB+fencembonceonces Never 0 3
 106   Time SB+fencembonceonces 0.01
 107   Hash=d66d99523e2cac6b06e66f4c995ebb48
 108
 109 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
 110 this litmus test's "exists" clause can not be satisfied.
 111
 112 See "herd7 -help" or "herdtools7/doc/" for more information on running the
 113 tool itself, but please be aware that this documentation is intended for
 114 people who work on the memory model itself, that is, people making changes
 115 to the tools/memory-model/linux-kernel.* files.  It is not intended for
 116 people focusing on writing, understanding, and running LKMM litmus tests.
 117
 118
 119 =====================
 120 BASIC USAGE: KLITMUS7
 121 =====================
 122
 123 The "klitmus7" tool converts a litmus test into a Linux kernel module,
 124 which may then be loaded and run.
 125
 126 For example, to run SB+fencembonceonces.litmus against hardware:
 127
 128   $ mkdir mymodules
 129   $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
 130   $ cd mymodules ; make
 131   $ sudo sh run.sh
 132
 133 The corresponding output includes:
 134
 135   Test SB+fencembonceonces Allowed
 136   Histogram (3 states)
 137   644580  :>0:r0=1; 1:r0=0;
 138   644328  :>0:r0=0; 1:r0=1;
 139   711092  :>0:r0=1; 1:r0=1;
 140   No
 141   Witnesses
 142   Positive: 0, Negative: 2000000
 143   Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
 144   Hash=d66d99523e2cac6b06e66f4c995ebb48
 145   Observation SB+fencembonceonces Never 0 2000000
 146   Time SB+fencembonceonces 0.16
 147
 148 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
 149 that during two million trials, the state specified in this litmus
 150 test's "exists" clause was not reached.
 151
 152 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
 153 for more information.  And again, please be aware that this documentation
 154 is intended for people who work on the memory model itself, that is,
 155 people making changes to the tools/memory-model/linux-kernel.* files.
 156 It is not intended for people focusing on writing, understanding, and
 157 running LKMM litmus tests.
 158
 159
 160 ====================
 161 DESCRIPTION OF FILES
 162 ====================
 163
 164 Documentation/cheatsheet.txt
 165         Quick-reference guide to the Linux-kernel memory model.
 166
 167 Documentation/explanation.txt
 168         Describes the memory model in detail.
 169
 170 Documentation/litmus-tests.txt
 171         Describes the format, features, capabilities, and limitations
 172         of the litmus tests that LKMM can evaluate.
 173
 174 Documentation/recipes.txt
 175         Lists common memory-ordering patterns.
 176
 177 Documentation/references.txt
 178         Provides background reading.
 179
 180 Documentation/simple.txt
 181         Starting point for someone new to Linux-kernel concurrency.
 182         And also for those needing a reminder of the simpler approaches
 183         to concurrency!
 184
 185 linux-kernel.bell
 186         Categorizes the relevant instructions, including memory
 187         references, memory barriers, atomic read-modify-write operations,
 188         lock acquisition/release, and RCU operations.
 189
 190         More formally, this file (1) lists the subtypes of the various
 191         event types used by the memory model and (2) performs RCU
 192         read-side critical section nesting analysis.
 193
 194 linux-kernel.cat
 195         Specifies what reorderings are forbidden by memory references,
 196         memory barriers, atomic read-modify-write operations, and RCU.
 197
 198         More formally, this file specifies what executions are forbidden
 199         by the memory model.  Allowed executions are those which
 200         satisfy the model's "coherence", "atomic", "happens-before",
 201         "propagation", and "rcu" axioms, which are defined in the file.
 202
 203 linux-kernel.cfg
 204         Convenience file that gathers the common-case herd7 command-line
 205         arguments.
 206
 207 linux-kernel.def
 208         Maps from C-like syntax to herd7's internal litmus-test
 209         instruction-set architecture.
 210
 211 litmus-tests
 212         Directory containing a few representative litmus tests, which
 213         are listed in litmus-tests/README.  A great deal more litmus
 214         tests are available at https://github.com/paulmckrcu/litmus.
 215
 216 lock.cat
 217         Provides a front-end analysis of lock acquisition and release,
 218         for example, associating a lock acquisition with the preceding
 219         and following releases and checking for self-deadlock.
 220
 221         More formally, this file defines a performance-enhanced scheme
 222         for generation of the possible reads-from and coherence order
 223         relations on the locking primitives.
 224
 225 README
 226         This file.
 227
 228 scripts Various scripts, see scripts/README.