~ [ source navigation ] ~ [ diff markup ] ~ [ identifier search ] ~

TOMOYO Linux Cross Reference
Linux/tools/memory-model/README

Version: ~ [ linux-6.11.5 ] ~ [ linux-6.10.14 ] ~ [ linux-6.9.12 ] ~ [ linux-6.8.12 ] ~ [ linux-6.7.12 ] ~ [ linux-6.6.58 ] ~ [ linux-6.5.13 ] ~ [ linux-6.4.16 ] ~ [ linux-6.3.13 ] ~ [ linux-6.2.16 ] ~ [ linux-6.1.114 ] ~ [ linux-6.0.19 ] ~ [ linux-5.19.17 ] ~ [ linux-5.18.19 ] ~ [ linux-5.17.15 ] ~ [ linux-5.16.20 ] ~ [ linux-5.15.169 ] ~ [ linux-5.14.21 ] ~ [ linux-5.13.19 ] ~ [ linux-5.12.19 ] ~ [ linux-5.11.22 ] ~ [ linux-5.10.228 ] ~ [ linux-5.9.16 ] ~ [ linux-5.8.18 ] ~ [ linux-5.7.19 ] ~ [ linux-5.6.19 ] ~ [ linux-5.5.19 ] ~ [ linux-5.4.284 ] ~ [ linux-5.3.18 ] ~ [ linux-5.2.21 ] ~ [ linux-5.1.21 ] ~ [ linux-5.0.21 ] ~ [ linux-4.20.17 ] ~ [ linux-4.19.322 ] ~ [ linux-4.18.20 ] ~ [ linux-4.17.19 ] ~ [ linux-4.16.18 ] ~ [ linux-4.15.18 ] ~ [ linux-4.14.336 ] ~ [ linux-4.13.16 ] ~ [ linux-4.12.14 ] ~ [ linux-4.11.12 ] ~ [ linux-4.10.17 ] ~ [ linux-4.9.337 ] ~ [ linux-4.4.302 ] ~ [ linux-3.10.108 ] ~ [ linux-2.6.32.71 ] ~ [ linux-2.6.0 ] ~ [ linux-2.4.37.11 ] ~ [ unix-v6-master ] ~ [ ccs-tools-1.8.9 ] ~ [ policy-sample ] ~
Architecture: ~ [ i386 ] ~ [ alpha ] ~ [ m68k ] ~ [ mips ] ~ [ ppc ] ~ [ sparc ] ~ [ sparc64 ] ~

Diff markup

Differences between /tools/memory-model/README (Version linux-6.11.5) and /tools/memory-model/README (Version linux-5.18.19)


  1                 ==============================      1                 =====================================
  2                 LINUX KERNEL MEMORY CONSISTENC      2                 LINUX KERNEL MEMORY CONSISTENCY MODEL
  3                 ==============================      3                 =====================================
  4                                                     4 
  5 ============                                        5 ============
  6 INTRODUCTION                                        6 INTRODUCTION
  7 ============                                        7 ============
  8                                                     8 
  9 This directory contains the memory consistency      9 This directory contains the memory consistency model (memory model, for
 10 short) of the Linux kernel, written in the "ca     10 short) of the Linux kernel, written in the "cat" language and executable
 11 by the externally provided "herd7" simulator,      11 by the externally provided "herd7" simulator, which exhaustively explores
 12 the state space of small litmus tests.             12 the state space of small litmus tests.
 13                                                    13 
 14 In addition, the "klitmus7" tool (also externa     14 In addition, the "klitmus7" tool (also externally provided) may be used
 15 to convert a litmus test to a Linux kernel mod     15 to convert a litmus test to a Linux kernel module, which in turn allows
 16 that litmus test to be exercised within the Li     16 that litmus test to be exercised within the Linux kernel.
 17                                                    17 
 18                                                    18 
 19 ============                                       19 ============
 20 REQUIREMENTS                                       20 REQUIREMENTS
 21 ============                                       21 ============
 22                                                    22 
 23 Version 7.52 or higher of the "herd7" and "kli     23 Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
 24 downloaded separately:                             24 downloaded separately:
 25                                                    25 
 26   https://github.com/herd/herdtools7               26   https://github.com/herd/herdtools7
 27                                                    27 
 28 See "herdtools7/INSTALL.md" for installation i     28 See "herdtools7/INSTALL.md" for installation instructions.
 29                                                    29 
 30 Note that although these tools usually provide     30 Note that although these tools usually provide backwards compatibility,
 31 this is not absolutely guaranteed.                 31 this is not absolutely guaranteed.
 32                                                    32 
 33 For example, a future version of herd7 might n     33 For example, a future version of herd7 might not work with the model
 34 in this release.  A compatible model will like     34 in this release.  A compatible model will likely be made available in
 35 a later release of Linux kernel.                   35 a later release of Linux kernel.
 36                                                    36 
 37 If you absolutely need to run the model in thi     37 If you absolutely need to run the model in this particular release,
 38 please try using the exact version called out      38 please try using the exact version called out above.
 39                                                    39 
 40 klitmus7 is independent of the model provided      40 klitmus7 is independent of the model provided here.  It has its own
 41 dependency on a target kernel release where co     41 dependency on a target kernel release where converted code is built
 42 and executed.  Any change in kernel APIs essen     42 and executed.  Any change in kernel APIs essential to klitmus7 will
 43 necessitate an upgrade of klitmus7.                43 necessitate an upgrade of klitmus7.
 44                                                    44 
 45 If you find any compatibility issues in klitmu     45 If you find any compatibility issues in klitmus7, please inform the
 46 memory model maintainers.                          46 memory model maintainers.
 47                                                    47 
 48 klitmus7 Compatibility Table                       48 klitmus7 Compatibility Table
 49 ----------------------------                       49 ----------------------------
 50                                                    50 
 51         ============  ==========                   51         ============  ==========
 52         target Linux  herdtools7                   52         target Linux  herdtools7
 53         ------------  ----------                   53         ------------  ----------
 54              -- 4.14  7.48 --                      54              -- 4.14  7.48 --
 55         4.15 -- 4.19  7.49 --                      55         4.15 -- 4.19  7.49 --
 56         4.20 -- 5.5   7.54 --                      56         4.20 -- 5.5   7.54 --
 57         5.6  -- 5.16  7.56 --                      57         5.6  -- 5.16  7.56 --
 58         5.17 --       7.56.1 --                    58         5.17 --       7.56.1 --
 59         ============  ==========                   59         ============  ==========
 60                                                    60 
 61                                                    61 
 62 ==================                                 62 ==================
 63 BASIC USAGE: HERD7                                 63 BASIC USAGE: HERD7
 64 ==================                                 64 ==================
 65                                                    65 
 66 The memory model is used, in conjunction with      66 The memory model is used, in conjunction with "herd7", to exhaustively
 67 explore the state space of small litmus tests.     67 explore the state space of small litmus tests.  Documentation describing
 68 the format, features, capabilities and limitat     68 the format, features, capabilities and limitations of these litmus
 69 tests is available in tools/memory-model/Docum     69 tests is available in tools/memory-model/Documentation/litmus-tests.txt.
 70                                                    70 
 71 Example litmus tests may be found in the Linux     71 Example litmus tests may be found in the Linux-kernel source tree:
 72                                                    72 
 73         tools/memory-model/litmus-tests/           73         tools/memory-model/litmus-tests/
 74         Documentation/litmus-tests/                74         Documentation/litmus-tests/
 75                                                    75 
 76 Several thousand more example litmus tests are     76 Several thousand more example litmus tests are available here:
 77                                                    77 
 78         https://github.com/paulmckrcu/litmus       78         https://github.com/paulmckrcu/litmus
 79         https://git.kernel.org/pub/scm/linux/k     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/k     80         https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
 81                                                    81 
 82 Documentation describing litmus tests and now      82 Documentation describing litmus tests and now to use them may be found
 83 here:                                              83 here:
 84                                                    84 
 85         tools/memory-model/Documentation/litmu     85         tools/memory-model/Documentation/litmus-tests.txt
 86                                                    86 
 87 The remainder of this section uses the SB+fenc     87 The remainder of this section uses the SB+fencembonceonces.litmus test
 88 located in the tools/memory-model directory.       88 located in the tools/memory-model directory.
 89                                                    89 
 90 To run SB+fencembonceonces.litmus against the      90 To run SB+fencembonceonces.litmus against the memory model:
 91                                                    91 
 92   $ cd $LINUX_SOURCE_TREE/tools/memory-model       92   $ cd $LINUX_SOURCE_TREE/tools/memory-model
 93   $ herd7 -conf linux-kernel.cfg litmus-tests/     93   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
 94                                                    94 
 95 Here is the corresponding output:                  95 Here is the corresponding output:
 96                                                    96 
 97   Test SB+fencembonceonces Allowed                 97   Test SB+fencembonceonces Allowed
 98   States 3                                         98   States 3
 99   0:r0=0; 1:r0=1;                                  99   0:r0=0; 1:r0=1;
100   0:r0=1; 1:r0=0;                                 100   0:r0=1; 1:r0=0;
101   0:r0=1; 1:r0=1;                                 101   0:r0=1; 1:r0=1;
102   No                                              102   No
103   Witnesses                                       103   Witnesses
104   Positive: 0 Negative: 3                         104   Positive: 0 Negative: 3
105   Condition exists (0:r0=0 /\ 1:r0=0)             105   Condition exists (0:r0=0 /\ 1:r0=0)
106   Observation SB+fencembonceonces Never 0 3       106   Observation SB+fencembonceonces Never 0 3
107   Time SB+fencembonceonces 0.01                   107   Time SB+fencembonceonces 0.01
108   Hash=d66d99523e2cac6b06e66f4c995ebb48           108   Hash=d66d99523e2cac6b06e66f4c995ebb48
109                                                   109 
110 The "Positive: 0 Negative: 3" and the "Never 0    110 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
111 this litmus test's "exists" clause can not be     111 this litmus test's "exists" clause can not be satisfied.
112                                                   112 
113 See "herd7 -help" or "herdtools7/doc/" for mor    113 See "herd7 -help" or "herdtools7/doc/" for more information on running the
114 tool itself, but please be aware that this doc    114 tool itself, but please be aware that this documentation is intended for
115 people who work on the memory model itself, th    115 people who work on the memory model itself, that is, people making changes
116 to the tools/memory-model/linux-kernel.* files    116 to the tools/memory-model/linux-kernel.* files.  It is not intended for
117 people focusing on writing, understanding, and    117 people focusing on writing, understanding, and running LKMM litmus tests.
118                                                   118 
119                                                   119 
120 =====================                             120 =====================
121 BASIC USAGE: KLITMUS7                             121 BASIC USAGE: KLITMUS7
122 =====================                             122 =====================
123                                                   123 
124 The "klitmus7" tool converts a litmus test int    124 The "klitmus7" tool converts a litmus test into a Linux kernel module,
125 which may then be loaded and run.                 125 which may then be loaded and run.
126                                                   126 
127 For example, to run SB+fencembonceonces.litmus    127 For example, to run SB+fencembonceonces.litmus against hardware:
128                                                   128 
129   $ mkdir mymodules                               129   $ mkdir mymodules
130   $ klitmus7 -o mymodules litmus-tests/SB+fenc    130   $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
131   $ cd mymodules ; make                           131   $ cd mymodules ; make
132   $ sudo sh run.sh                                132   $ sudo sh run.sh
133                                                   133 
134 The corresponding output includes:                134 The corresponding output includes:
135                                                   135 
136   Test SB+fencembonceonces Allowed                136   Test SB+fencembonceonces Allowed
137   Histogram (3 states)                            137   Histogram (3 states)
138   644580  :>0:r0=1; 1:r0=0;                       138   644580  :>0:r0=1; 1:r0=0;
139   644328  :>0:r0=0; 1:r0=1;                       139   644328  :>0:r0=0; 1:r0=1;
140   711092  :>0:r0=1; 1:r0=1;                       140   711092  :>0:r0=1; 1:r0=1;
141   No                                              141   No
142   Witnesses                                       142   Witnesses
143   Positive: 0, Negative: 2000000                  143   Positive: 0, Negative: 2000000
144   Condition exists (0:r0=0 /\ 1:r0=0) is NOT v    144   Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
145   Hash=d66d99523e2cac6b06e66f4c995ebb48           145   Hash=d66d99523e2cac6b06e66f4c995ebb48
146   Observation SB+fencembonceonces Never 0 2000    146   Observation SB+fencembonceonces Never 0 2000000
147   Time SB+fencembonceonces 0.16                   147   Time SB+fencembonceonces 0.16
148                                                   148 
149 The "Positive: 0 Negative: 2000000" and the "N    149 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
150 that during two million trials, the state spec    150 that during two million trials, the state specified in this litmus
151 test's "exists" clause was not reached.           151 test's "exists" clause was not reached.
152                                                   152 
153 And, as with "herd7", please see "klitmus7 -he    153 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
154 for more information.  And again, please be aw    154 for more information.  And again, please be aware that this documentation
155 is intended for people who work on the memory     155 is intended for people who work on the memory model itself, that is,
156 people making changes to the tools/memory-mode    156 people making changes to the tools/memory-model/linux-kernel.* files.
157 It is not intended for people focusing on writ    157 It is not intended for people focusing on writing, understanding, and
158 running LKMM litmus tests.                        158 running LKMM litmus tests.
159                                                   159 
160                                                   160 
161 ====================                              161 ====================
162 DESCRIPTION OF FILES                              162 DESCRIPTION OF FILES
163 ====================                              163 ====================
164                                                   164 
165 Documentation/README                              165 Documentation/README
166         Guide to the other documents in the Do    166         Guide to the other documents in the Documentation/ directory.
167                                                   167 
168 linux-kernel.bell                                 168 linux-kernel.bell
169         Categorizes the relevant instructions,    169         Categorizes the relevant instructions, including memory
170         references, memory barriers, atomic re    170         references, memory barriers, atomic read-modify-write operations,
171         lock acquisition/release, and RCU oper    171         lock acquisition/release, and RCU operations.
172                                                   172 
173         More formally, this file (1) lists the    173         More formally, this file (1) lists the subtypes of the various
174         event types used by the memory model a    174         event types used by the memory model and (2) performs RCU
175         read-side critical section nesting ana    175         read-side critical section nesting analysis.
176                                                   176 
177 linux-kernel.cat                                  177 linux-kernel.cat
178         Specifies what reorderings are forbidd    178         Specifies what reorderings are forbidden by memory references,
179         memory barriers, atomic read-modify-wr    179         memory barriers, atomic read-modify-write operations, and RCU.
180                                                   180 
181         More formally, this file specifies wha    181         More formally, this file specifies what executions are forbidden
182         by the memory model.  Allowed executio    182         by the memory model.  Allowed executions are those which
183         satisfy the model's "coherence", "atom    183         satisfy the model's "coherence", "atomic", "happens-before",
184         "propagation", and "rcu" axioms, which    184         "propagation", and "rcu" axioms, which are defined in the file.
185                                                   185 
186 linux-kernel.cfg                                  186 linux-kernel.cfg
187         Convenience file that gathers the comm    187         Convenience file that gathers the common-case herd7 command-line
188         arguments.                                188         arguments.
189                                                   189 
190 linux-kernel.def                                  190 linux-kernel.def
191         Maps from C-like syntax to herd7's int    191         Maps from C-like syntax to herd7's internal litmus-test
192         instruction-set architecture.             192         instruction-set architecture.
193                                                   193 
194 litmus-tests                                      194 litmus-tests
195         Directory containing a few representat    195         Directory containing a few representative litmus tests, which
196         are listed in litmus-tests/README.  A     196         are listed in litmus-tests/README.  A great deal more litmus
197         tests are available at https://github.    197         tests are available at https://github.com/paulmckrcu/litmus.
198                                                   198 
199         By "representative", it means the one     199         By "representative", it means the one in the litmus-tests
200         directory is:                             200         directory is:
201                                                   201 
202                 1) simple, the number of threa    202                 1) simple, the number of threads should be relatively
203                    small and each thread funct    203                    small and each thread function should be relatively
204                    simple.                        204                    simple.
205                 2) orthogonal, there should be    205                 2) orthogonal, there should be no two litmus tests
206                    describing the same aspect     206                    describing the same aspect of the memory model.
207                 3) textbook, developers can ea    207                 3) textbook, developers can easily copy-paste-modify
208                    the litmus tests to use the    208                    the litmus tests to use the patterns on their own
209                    code.                          209                    code.
210                                                   210 
211 lock.cat                                          211 lock.cat
212         Provides a front-end analysis of lock     212         Provides a front-end analysis of lock acquisition and release,
213         for example, associating a lock acquis    213         for example, associating a lock acquisition with the preceding
214         and following releases and checking fo    214         and following releases and checking for self-deadlock.
215                                                   215 
216         More formally, this file defines a per    216         More formally, this file defines a performance-enhanced scheme
217         for generation of the possible reads-f    217         for generation of the possible reads-from and coherence order
218         relations on the locking primitives.      218         relations on the locking primitives.
219                                                   219 
220 README                                            220 README
221         This file.                                221         This file.
222                                                   222 
223 scripts Various scripts, see scripts/README.      223 scripts Various scripts, see scripts/README.
                                                      

~ [ source navigation ] ~ [ diff markup ] ~ [ identifier search ] ~

kernel.org | git.kernel.org | LWN.net | Project Home | SVN repository | Mail admin

Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.

sflogo.php