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


  1                 ==============================    
  2                 LINUX KERNEL MEMORY CONSISTENC    
  3                 ==============================    
  4                                                   
  5 ============                                      
  6 INTRODUCTION                                      
  7 ============                                      
  8                                                   
  9 This directory contains the memory consistency    
 10 short) of the Linux kernel, written in the "ca    
 11 by the externally provided "herd7" simulator,     
 12 the state space of small litmus tests.            
 13                                                   
 14 In addition, the "klitmus7" tool (also externa    
 15 to convert a litmus test to a Linux kernel mod    
 16 that litmus test to be exercised within the Li    
 17                                                   
 18                                                   
 19 ============                                      
 20 REQUIREMENTS                                      
 21 ============                                      
 22                                                   
 23 Version 7.52 or higher of the "herd7" and "kli    
 24 downloaded separately:                            
 25                                                   
 26   https://github.com/herd/herdtools7              
 27                                                   
 28 See "herdtools7/INSTALL.md" for installation i    
 29                                                   
 30 Note that although these tools usually provide    
 31 this is not absolutely guaranteed.                
 32                                                   
 33 For example, a future version of herd7 might n    
 34 in this release.  A compatible model will like    
 35 a later release of Linux kernel.                  
 36                                                   
 37 If you absolutely need to run the model in thi    
 38 please try using the exact version called out     
 39                                                   
 40 klitmus7 is independent of the model provided     
 41 dependency on a target kernel release where co    
 42 and executed.  Any change in kernel APIs essen    
 43 necessitate an upgrade of klitmus7.               
 44                                                   
 45 If you find any compatibility issues in klitmu    
 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     
 67 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                                                   
 71 Example litmus tests may be found in the Linux    
 72                                                   
 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/    
 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    
111 this litmus test's "exists" clause can not be     
112                                                   
113 See "herd7 -help" or "herdtools7/doc/" for mor    
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                                                   
119                                                   
120 =====================                             
121 BASIC USAGE: KLITMUS7                             
122 =====================                             
123                                                   
124 The "klitmus7" tool converts a litmus test int    
125 which may then be loaded and run.                 
126                                                   
127 For example, to run SB+fencembonceonces.litmus    
128                                                   
129   $ mkdir mymodules                               
130   $ klitmus7 -o mymodules litmus-tests/SB+fenc    
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 v    
145   Hash=d66d99523e2cac6b06e66f4c995ebb48           
146   Observation SB+fencembonceonces Never 0 2000    
147   Time SB+fencembonceonces 0.16                   
148                                                   
149 The "Positive: 0 Negative: 2000000" and the "N    
150 that during two million trials, the state spec    
151 test's "exists" clause was not reached.           
152                                                   
153 And, as with "herd7", please see "klitmus7 -he    
154 for more information.  And again, please be aw    
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                                                   
160                                                   
161 ====================                              
162 DESCRIPTION OF FILES                              
163 ====================                              
164                                                   
165 Documentation/README                              
166         Guide to the other documents in the Do    
167                                                   
168 linux-kernel.bell                                 
169         Categorizes the relevant instructions,    
170         references, memory barriers, atomic re    
171         lock acquisition/release, and RCU oper    
172                                                   
173         More formally, this file (1) lists the    
174         event types used by the memory model a    
175         read-side critical section nesting ana    
176                                                   
177 linux-kernel.cat                                  
178         Specifies what reorderings are forbidd    
179         memory barriers, atomic read-modify-wr    
180                                                   
181         More formally, this file specifies wha    
182         by the memory model.  Allowed executio    
183         satisfy the model's "coherence", "atom    
184         "propagation", and "rcu" axioms, which    
185                                                   
186 linux-kernel.cfg                                  
187         Convenience file that gathers the comm    
188         arguments.                                
189                                                   
190 linux-kernel.def                                  
191         Maps from C-like syntax to herd7's int    
192         instruction-set architecture.             
193                                                   
194 litmus-tests                                      
195         Directory containing a few representat    
196         are listed in litmus-tests/README.  A     
197         tests are available at https://github.    
198                                                   
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                                          
212         Provides a front-end analysis of lock     
213         for example, associating a lock acquis    
214         and following releases and checking fo    
215                                                   
216         More formally, this file defines a per    
217         for generation of the possible reads-f    
218         relations on the locking primitives.      
219                                                   
220 README                                            
221         This file.                                
222                                                   
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