forked from ~ljy/RK356X_SDK_RELEASE
blame | history | patch | commit | commitdiff
hc
2024-10-09 244b2c5ca8b14627e4a17755e5922221e121c771 
 kernel/tools/memory-model/README
....@@ -20,12 +20,42 @@
2020 REQUIREMENTS
2121 ============
2222 
23
-Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
24
-separately:
23
+Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
24
+downloaded separately:
2525 
2626   https://github.com/herd/herdtools7
2727 
2828 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
+	============  ==========
2959 
3060 
3161 ==================
....@@ -33,10 +63,32 @@
3363 ==================
3464 
3565 The memory model is used, in conjunction with "herd7", to exhaustively
36
-explore the state space of small litmus tests.
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.
3769 
38
-For example, to run SB+fencembonceonces.litmus against the memory model:
70
+Example litmus tests may be found in the Linux-kernel source tree:
3971 
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
4092   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
4193 
4294 Here is the corresponding output:
....@@ -57,7 +109,11 @@
57109 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
58110 this litmus test's "exists" clause can not be satisfied.
59111 
60
-See "herd7 -help" or "herdtools7/doc/" for more information.
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.
61117 
62118 
63119 =====================
....@@ -94,7 +150,11 @@
94150 test's "exists" clause was not reached.
95151 
96152 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
97
-for more information.
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.
98158 
99159 
100160 ====================
....@@ -107,11 +167,20 @@
107167 Documentation/explanation.txt
108168 	Describes the memory model in detail.
109169 
170
+Documentation/litmus-tests.txt
171
+	Describes the format, features, capabilities, and limitations
172
+	of the litmus tests that LKMM can evaluate.
173
+
110174 Documentation/recipes.txt
111175 	Lists common memory-ordering patterns.
112176 
113177 Documentation/references.txt
114178 	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!
115184 
116185 linux-kernel.bell
117186 	Categorizes the relevant instructions, including memory
....@@ -156,51 +225,4 @@
156225 README
157226 	This file.
158227 
159
-
160
-===========
161
-LIMITATIONS
162
-===========
163
-
164
-The Linux-kernel memory model has the following limitations:
165
-
166
-1.	Compiler optimizations are not modeled.  Of course, the use
167
-	of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
168
-	to optimize, but there is Linux-kernel code that uses bare C
169
-	memory accesses.  Handling this code is on the to-do list.
170
-	For more information, see Documentation/explanation.txt (in
171
-	particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
172
-	and "A WARNING" sections).
173
-
174
-2.	Multiple access sizes for a single variable are not supported,
175
-	and neither are misaligned or partially overlapping accesses.
176
-
177
-3.	Exceptions and interrupts are not modeled.  In some cases,
178
-	this limitation can be overcome by modeling the interrupt or
179
-	exception with an additional process.
180
-
181
-4.	I/O such as MMIO or DMA is not supported.
182
-
183
-5.	Self-modifying code (such as that found in the kernel's
184
-	alternatives mechanism, function tracer, Berkeley Packet Filter
185
-	JIT compiler, and module loader) is not supported.
186
-
187
-6.	Complete modeling of all variants of atomic read-modify-write
188
-	operations, locking primitives, and RCU is not provided.
189
-	For example, call_rcu() and rcu_barrier() are not supported.
190
-	However, a substantial amount of support is provided for these
191
-	operations, as shown in the linux-kernel.def file.
192
-
193
-The "herd7" tool has some additional limitations of its own, apart from
194
-the memory model:
195
-
196
-1.	Non-trivial data structures such as arrays or structures are
197
-	not supported.	However, pointers are supported, allowing trivial
198
-	linked lists to be constructed.
199
-
200
-2.	Dynamic memory allocation is not supported, although this can
201
-	be worked around in some cases by supplying multiple statically
202
-	allocated variables.
203
-
204
-Some of these limitations may be overcome in the future, but others are
205
-more likely to be addressed by incorporating the Linux-kernel memory model
206
-into other tools.
228
+scripts	Various scripts, see scripts/README.