~ [ 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.9.16)


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

~ [ 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