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.14  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/README
 165         Guide to the other documents in the Documentation/ directory.
 166
 167 linux-kernel.bell
 168         Categorizes the relevant instructions, including memory
 169         references, memory barriers, atomic read-modify-write operations,
 170         lock acquisition/release, and RCU operations.
 171
 172         More formally, this file (1) lists the subtypes of the various
 173         event types used by the memory model and (2) performs RCU
 174         read-side critical section nesting analysis.
 175
 176 linux-kernel.cat
 177         Specifies what reorderings are forbidden by memory references,
 178         memory barriers, atomic read-modify-write operations, and RCU.
 179
 180         More formally, this file specifies what executions are forbidden
 181         by the memory model.  Allowed executions are those which
 182         satisfy the model's "coherence", "atomic", "happens-before",
 183         "propagation", and "rcu" axioms, which are defined in the file.
 184
 185 linux-kernel.cfg
 186         Convenience file that gathers the common-case herd7 command-line
 187         arguments.
 188
 189 linux-kernel.def
 190         Maps from C-like syntax to herd7's internal litmus-test
 191         instruction-set architecture.
 192
 193 litmus-tests
 194         Directory containing a few representative litmus tests, which
 195         are listed in litmus-tests/README.  A great deal more litmus
 196         tests are available at https://github.com/paulmckrcu/litmus.
 197
 198 lock.cat
 199         Provides a front-end analysis of lock acquisition and release,
 200         for example, associating a lock acquisition with the preceding
 201         and following releases and checking for self-deadlock.
 202
 203         More formally, this file defines a performance-enhanced scheme
 204         for generation of the possible reads-from and coherence order
 205         relations on the locking primitives.
 206
 207 README
 208         This file.
 209
 210 scripts Various scripts, see scripts/README.