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