148d44d4eSAndrea Parri ===================================== 248d44d4eSAndrea Parri LINUX KERNEL MEMORY CONSISTENCY MODEL 348d44d4eSAndrea Parri ===================================== 41c27b644SPaul E. McKenney 51c27b644SPaul E. McKenney============ 61c27b644SPaul E. McKenneyINTRODUCTION 71c27b644SPaul E. McKenney============ 81c27b644SPaul E. McKenney 948d44d4eSAndrea ParriThis directory contains the memory consistency model (memory model, for 1048d44d4eSAndrea Parrishort) of the Linux kernel, written in the "cat" language and executable 1148d44d4eSAndrea Parriby the externally provided "herd7" simulator, which exhaustively explores 1248d44d4eSAndrea Parrithe state space of small litmus tests. 131c27b644SPaul E. McKenney 141c27b644SPaul E. McKenneyIn addition, the "klitmus7" tool (also externally provided) may be used 151c27b644SPaul E. McKenneyto convert a litmus test to a Linux kernel module, which in turn allows 161c27b644SPaul E. McKenneythat litmus test to be exercised within the Linux kernel. 171c27b644SPaul E. McKenney 181c27b644SPaul E. McKenney 191c27b644SPaul E. McKenney============ 201c27b644SPaul E. McKenneyREQUIREMENTS 211c27b644SPaul E. McKenney============ 221c27b644SPaul E. McKenney 23034fb712SAndrea ParriVersion 7.52 or higher of the "herd7" and "klitmus7" tools must be 24034fb712SAndrea Parridownloaded separately: 251c27b644SPaul E. McKenney 261c27b644SPaul E. McKenney https://github.com/herd/herdtools7 271c27b644SPaul E. McKenney 281c27b644SPaul E. McKenneySee "herdtools7/INSTALL.md" for installation instructions. 291c27b644SPaul E. McKenney 30034fb712SAndrea ParriNote that although these tools usually provide backwards compatibility, 31d075a78aSAkira Yokosawathis is not absolutely guaranteed. 32d075a78aSAkira Yokosawa 33d075a78aSAkira YokosawaFor example, a future version of herd7 might not work with the model 34d075a78aSAkira Yokosawain this release. A compatible model will likely be made available in 35d075a78aSAkira Yokosawaa later release of Linux kernel. 36d075a78aSAkira Yokosawa 37d075a78aSAkira YokosawaIf you absolutely need to run the model in this particular release, 38d075a78aSAkira Yokosawaplease try using the exact version called out above. 39d075a78aSAkira Yokosawa 40d075a78aSAkira Yokosawaklitmus7 is independent of the model provided here. It has its own 41d075a78aSAkira Yokosawadependency on a target kernel release where converted code is built 42d075a78aSAkira Yokosawaand executed. Any change in kernel APIs essential to klitmus7 will 43d075a78aSAkira Yokosawanecessitate an upgrade of klitmus7. 44d075a78aSAkira Yokosawa 45d075a78aSAkira YokosawaIf you find any compatibility issues in klitmus7, please inform the 46d075a78aSAkira Yokosawamemory model maintainers. 47d075a78aSAkira Yokosawa 48d075a78aSAkira Yokosawaklitmus7 Compatibility Table 49d075a78aSAkira Yokosawa---------------------------- 50d075a78aSAkira Yokosawa 51d075a78aSAkira Yokosawa ============ ========== 52d075a78aSAkira Yokosawa target Linux herdtools7 53d075a78aSAkira Yokosawa ------------ ---------- 54d075a78aSAkira Yokosawa -- 4.18 7.48 -- 55d075a78aSAkira Yokosawa 4.15 -- 4.19 7.49 -- 56d075a78aSAkira Yokosawa 4.20 -- 5.5 7.54 -- 572bfa5c62SAkira Yokosawa 5.6 -- 7.56 -- 58d075a78aSAkira Yokosawa ============ ========== 59034fb712SAndrea Parri 601c27b644SPaul E. McKenney 611c27b644SPaul E. McKenney================== 621c27b644SPaul E. McKenneyBASIC USAGE: HERD7 631c27b644SPaul E. McKenney================== 641c27b644SPaul E. McKenney 651c27b644SPaul E. McKenneyThe memory model is used, in conjunction with "herd7", to exhaustively 661c27b644SPaul E. McKenneyexplore the state space of small litmus tests. 671c27b644SPaul E. McKenney 6871b7ff5eSAndrea ParriFor example, to run SB+fencembonceonces.litmus against the memory model: 691c27b644SPaul E. McKenney 7071b7ff5eSAndrea Parri $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus 711c27b644SPaul E. McKenney 721c27b644SPaul E. McKenneyHere is the corresponding output: 731c27b644SPaul E. McKenney 7471b7ff5eSAndrea Parri Test SB+fencembonceonces Allowed 751c27b644SPaul E. McKenney States 3 761c27b644SPaul E. McKenney 0:r0=0; 1:r0=1; 771c27b644SPaul E. McKenney 0:r0=1; 1:r0=0; 781c27b644SPaul E. McKenney 0:r0=1; 1:r0=1; 791c27b644SPaul E. McKenney No 801c27b644SPaul E. McKenney Witnesses 811c27b644SPaul E. McKenney Positive: 0 Negative: 3 821c27b644SPaul E. McKenney Condition exists (0:r0=0 /\ 1:r0=0) 8371b7ff5eSAndrea Parri Observation SB+fencembonceonces Never 0 3 8471b7ff5eSAndrea Parri Time SB+fencembonceonces 0.01 851c27b644SPaul E. McKenney Hash=d66d99523e2cac6b06e66f4c995ebb48 861c27b644SPaul E. McKenney 871c27b644SPaul E. McKenneyThe "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 881c27b644SPaul E. McKenneythis litmus test's "exists" clause can not be satisfied. 891c27b644SPaul E. McKenney 901c27b644SPaul E. McKenneySee "herd7 -help" or "herdtools7/doc/" for more information. 911c27b644SPaul E. McKenney 921c27b644SPaul E. McKenney 931c27b644SPaul E. McKenney===================== 941c27b644SPaul E. McKenneyBASIC USAGE: KLITMUS7 951c27b644SPaul E. McKenney===================== 961c27b644SPaul E. McKenney 971c27b644SPaul E. McKenneyThe "klitmus7" tool converts a litmus test into a Linux kernel module, 981c27b644SPaul E. McKenneywhich may then be loaded and run. 991c27b644SPaul E. McKenney 10071b7ff5eSAndrea ParriFor example, to run SB+fencembonceonces.litmus against hardware: 1011c27b644SPaul E. McKenney 1021c27b644SPaul E. McKenney $ mkdir mymodules 10371b7ff5eSAndrea Parri $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus 1041c27b644SPaul E. McKenney $ cd mymodules ; make 1051c27b644SPaul E. McKenney $ sudo sh run.sh 1061c27b644SPaul E. McKenney 1071c27b644SPaul E. McKenneyThe corresponding output includes: 1081c27b644SPaul E. McKenney 10971b7ff5eSAndrea Parri Test SB+fencembonceonces Allowed 1101c27b644SPaul E. McKenney Histogram (3 states) 1111c27b644SPaul E. McKenney 644580 :>0:r0=1; 1:r0=0; 1121c27b644SPaul E. McKenney 644328 :>0:r0=0; 1:r0=1; 1131c27b644SPaul E. McKenney 711092 :>0:r0=1; 1:r0=1; 1141c27b644SPaul E. McKenney No 1151c27b644SPaul E. McKenney Witnesses 1161c27b644SPaul E. McKenney Positive: 0, Negative: 2000000 1171c27b644SPaul E. McKenney Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 1181c27b644SPaul E. McKenney Hash=d66d99523e2cac6b06e66f4c995ebb48 11971b7ff5eSAndrea Parri Observation SB+fencembonceonces Never 0 2000000 12071b7ff5eSAndrea Parri Time SB+fencembonceonces 0.16 1211c27b644SPaul E. McKenney 1221c27b644SPaul E. McKenneyThe "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 1231c27b644SPaul E. McKenneythat during two million trials, the state specified in this litmus 1241c27b644SPaul E. McKenneytest's "exists" clause was not reached. 1251c27b644SPaul E. McKenney 1261c27b644SPaul E. McKenneyAnd, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 1271c27b644SPaul E. McKenneyfor more information. 1281c27b644SPaul E. McKenney 1291c27b644SPaul E. McKenney 1301c27b644SPaul E. McKenney==================== 1311c27b644SPaul E. McKenneyDESCRIPTION OF FILES 1321c27b644SPaul E. McKenney==================== 1331c27b644SPaul E. McKenney 1341c27b644SPaul E. McKenneyDocumentation/cheatsheet.txt 1351c27b644SPaul E. McKenney Quick-reference guide to the Linux-kernel memory model. 1361c27b644SPaul E. McKenney 1371c27b644SPaul E. McKenneyDocumentation/explanation.txt 1381c27b644SPaul E. McKenney Describes the memory model in detail. 1391c27b644SPaul E. McKenney 1401c27b644SPaul E. McKenneyDocumentation/recipes.txt 1411c27b644SPaul E. McKenney Lists common memory-ordering patterns. 1421c27b644SPaul E. McKenney 1431c27b644SPaul E. McKenneyDocumentation/references.txt 1441c27b644SPaul E. McKenney Provides background reading. 1451c27b644SPaul E. McKenney 1461c27b644SPaul E. McKenneylinux-kernel.bell 1471c27b644SPaul E. McKenney Categorizes the relevant instructions, including memory 1481c27b644SPaul E. McKenney references, memory barriers, atomic read-modify-write operations, 1491c27b644SPaul E. McKenney lock acquisition/release, and RCU operations. 1501c27b644SPaul E. McKenney 1511c27b644SPaul E. McKenney More formally, this file (1) lists the subtypes of the various 1521c27b644SPaul E. McKenney event types used by the memory model and (2) performs RCU 1531c27b644SPaul E. McKenney read-side critical section nesting analysis. 1541c27b644SPaul E. McKenney 1551c27b644SPaul E. McKenneylinux-kernel.cat 1561c27b644SPaul E. McKenney Specifies what reorderings are forbidden by memory references, 1571c27b644SPaul E. McKenney memory barriers, atomic read-modify-write operations, and RCU. 1581c27b644SPaul E. McKenney 1591c27b644SPaul E. McKenney More formally, this file specifies what executions are forbidden 1601c27b644SPaul E. McKenney by the memory model. Allowed executions are those which 1611c27b644SPaul E. McKenney satisfy the model's "coherence", "atomic", "happens-before", 1621c27b644SPaul E. McKenney "propagation", and "rcu" axioms, which are defined in the file. 1631c27b644SPaul E. McKenney 1641c27b644SPaul E. McKenneylinux-kernel.cfg 1651c27b644SPaul E. McKenney Convenience file that gathers the common-case herd7 command-line 1661c27b644SPaul E. McKenney arguments. 1671c27b644SPaul E. McKenney 1681c27b644SPaul E. McKenneylinux-kernel.def 1691c27b644SPaul E. McKenney Maps from C-like syntax to herd7's internal litmus-test 1701c27b644SPaul E. McKenney instruction-set architecture. 1711c27b644SPaul E. McKenney 1721c27b644SPaul E. McKenneylitmus-tests 1731c27b644SPaul E. McKenney Directory containing a few representative litmus tests, which 1741c27b644SPaul E. McKenney are listed in litmus-tests/README. A great deal more litmus 1751c27b644SPaul E. McKenney tests are available at https://github.com/paulmckrcu/litmus. 1761c27b644SPaul E. McKenney 1771c27b644SPaul E. McKenneylock.cat 1781c27b644SPaul E. McKenney Provides a front-end analysis of lock acquisition and release, 1791c27b644SPaul E. McKenney for example, associating a lock acquisition with the preceding 1801c27b644SPaul E. McKenney and following releases and checking for self-deadlock. 1811c27b644SPaul E. McKenney 1821c27b644SPaul E. McKenney More formally, this file defines a performance-enhanced scheme 1831c27b644SPaul E. McKenney for generation of the possible reads-from and coherence order 1841c27b644SPaul E. McKenney relations on the locking primitives. 1851c27b644SPaul E. McKenney 1861c27b644SPaul E. McKenneyREADME 1871c27b644SPaul E. McKenney This file. 1881c27b644SPaul E. McKenney 189b02eb5b0SPaul E. McKenneyscripts Various scripts, see scripts/README. 190b02eb5b0SPaul E. McKenney 1911c27b644SPaul E. McKenney 1921c27b644SPaul E. McKenney=========== 1931c27b644SPaul E. McKenneyLIMITATIONS 1941c27b644SPaul E. McKenney=========== 1951c27b644SPaul E. McKenney 1966738ff85SAndrea ParriThe Linux-kernel memory model (LKMM) has the following limitations: 1971c27b644SPaul E. McKenney 1986738ff85SAndrea Parri1. Compiler optimizations are not accurately modeled. Of course, 1996738ff85SAndrea Parri the use of READ_ONCE() and WRITE_ONCE() limits the compiler's 2006738ff85SAndrea Parri ability to optimize, but under some circumstances it is possible 2016738ff85SAndrea Parri for the compiler to undermine the memory model. For more 2026738ff85SAndrea Parri information, see Documentation/explanation.txt (in particular, 2036738ff85SAndrea Parri the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING" 2046738ff85SAndrea Parri sections). 2051c27b644SPaul E. McKenney 206d8fa25c4SPaul E. McKenney Note that this limitation in turn limits LKMM's ability to 207d8fa25c4SPaul E. McKenney accurately model address, control, and data dependencies. 208d8fa25c4SPaul E. McKenney For example, if the compiler can deduce the value of some variable 209d8fa25c4SPaul E. McKenney carrying a dependency, then the compiler can break that dependency 210d8fa25c4SPaul E. McKenney by substituting a constant of that value. 211d8fa25c4SPaul E. McKenney 2121c27b644SPaul E. McKenney2. Multiple access sizes for a single variable are not supported, 2131c27b644SPaul E. McKenney and neither are misaligned or partially overlapping accesses. 2141c27b644SPaul E. McKenney 2151c27b644SPaul E. McKenney3. Exceptions and interrupts are not modeled. In some cases, 2161c27b644SPaul E. McKenney this limitation can be overcome by modeling the interrupt or 2171c27b644SPaul E. McKenney exception with an additional process. 2181c27b644SPaul E. McKenney 2191c27b644SPaul E. McKenney4. I/O such as MMIO or DMA is not supported. 2201c27b644SPaul E. McKenney 2211c27b644SPaul E. McKenney5. Self-modifying code (such as that found in the kernel's 2221c27b644SPaul E. McKenney alternatives mechanism, function tracer, Berkeley Packet Filter 2231c27b644SPaul E. McKenney JIT compiler, and module loader) is not supported. 2241c27b644SPaul E. McKenney 2251c27b644SPaul E. McKenney6. Complete modeling of all variants of atomic read-modify-write 2261c27b644SPaul E. McKenney operations, locking primitives, and RCU is not provided. 2271c27b644SPaul E. McKenney For example, call_rcu() and rcu_barrier() are not supported. 2281c27b644SPaul E. McKenney However, a substantial amount of support is provided for these 2291c27b644SPaul E. McKenney operations, as shown in the linux-kernel.def file. 2301c27b644SPaul E. McKenney 231d8fa25c4SPaul E. McKenney a. When rcu_assign_pointer() is passed NULL, the Linux 232d8fa25c4SPaul E. McKenney kernel provides no ordering, but LKMM models this 233d8fa25c4SPaul E. McKenney case as a store release. 234d8fa25c4SPaul E. McKenney 235d8fa25c4SPaul E. McKenney b. The "unless" RMW operations are not currently modeled: 2364a9cc65fSBoqun Feng atomic_long_add_unless(), atomic_inc_unless_negative(), 2374a9cc65fSBoqun Feng and atomic_dec_unless_positive(). These can be emulated 238d8fa25c4SPaul E. McKenney in litmus tests, for example, by using atomic_cmpxchg(). 239d8fa25c4SPaul E. McKenney 2404a9cc65fSBoqun Feng One exception of this limitation is atomic_add_unless(), 2414a9cc65fSBoqun Feng which is provided directly by herd7 (so no corresponding 2424a9cc65fSBoqun Feng definition in linux-kernel.def). atomic_add_unless() is 2434a9cc65fSBoqun Feng modeled by herd7 therefore it can be used in litmus tests. 2444a9cc65fSBoqun Feng 245d8fa25c4SPaul E. McKenney c. The call_rcu() function is not modeled. It can be 246d8fa25c4SPaul E. McKenney emulated in litmus tests by adding another process that 247d8fa25c4SPaul E. McKenney invokes synchronize_rcu() and the body of the callback 248d8fa25c4SPaul E. McKenney function, with (for example) a release-acquire from 249d8fa25c4SPaul E. McKenney the site of the emulated call_rcu() to the beginning 250d8fa25c4SPaul E. McKenney of the additional process. 251d8fa25c4SPaul E. McKenney 252d8fa25c4SPaul E. McKenney d. The rcu_barrier() function is not modeled. It can be 253d8fa25c4SPaul E. McKenney emulated in litmus tests emulating call_rcu() via 254d8fa25c4SPaul E. McKenney (for example) a release-acquire from the end of each 255d8fa25c4SPaul E. McKenney additional call_rcu() process to the site of the 256d8fa25c4SPaul E. McKenney emulated rcu-barrier(). 257d8fa25c4SPaul E. McKenney 258ad9fd20bSPaul E. McKenney e. Although sleepable RCU (SRCU) is now modeled, there 259ad9fd20bSPaul E. McKenney are some subtle differences between its semantics and 260ad9fd20bSPaul E. McKenney those in the Linux kernel. For example, the kernel 261ad9fd20bSPaul E. McKenney might interpret the following sequence as two partially 262ad9fd20bSPaul E. McKenney overlapping SRCU read-side critical sections: 263ad9fd20bSPaul E. McKenney 264ad9fd20bSPaul E. McKenney 1 r1 = srcu_read_lock(&my_srcu); 265ad9fd20bSPaul E. McKenney 2 do_something_1(); 266ad9fd20bSPaul E. McKenney 3 r2 = srcu_read_lock(&my_srcu); 267ad9fd20bSPaul E. McKenney 4 do_something_2(); 268ad9fd20bSPaul E. McKenney 5 srcu_read_unlock(&my_srcu, r1); 269ad9fd20bSPaul E. McKenney 6 do_something_3(); 270ad9fd20bSPaul E. McKenney 7 srcu_read_unlock(&my_srcu, r2); 271ad9fd20bSPaul E. McKenney 272ad9fd20bSPaul E. McKenney In contrast, LKMM will interpret this as a nested pair of 273ad9fd20bSPaul E. McKenney SRCU read-side critical sections, with the outer critical 274ad9fd20bSPaul E. McKenney section spanning lines 1-7 and the inner critical section 275ad9fd20bSPaul E. McKenney spanning lines 3-5. 276ad9fd20bSPaul E. McKenney 277ad9fd20bSPaul E. McKenney This difference would be more of a concern had anyone 278ad9fd20bSPaul E. McKenney identified a reasonable use case for partially overlapping 279ad9fd20bSPaul E. McKenney SRCU read-side critical sections. For more information, 280ad9fd20bSPaul E. McKenney please see: https://paulmck.livejournal.com/40593.html 281d8fa25c4SPaul E. McKenney 282d8fa25c4SPaul E. McKenney f. Reader-writer locking is not modeled. It can be 283d8fa25c4SPaul E. McKenney emulated in litmus tests using atomic read-modify-write 284d8fa25c4SPaul E. McKenney operations. 285d8fa25c4SPaul E. McKenney 2861c27b644SPaul E. McKenneyThe "herd7" tool has some additional limitations of its own, apart from 2871c27b644SPaul E. McKenneythe memory model: 2881c27b644SPaul E. McKenney 2891c27b644SPaul E. McKenney1. Non-trivial data structures such as arrays or structures are 2901c27b644SPaul E. McKenney not supported. However, pointers are supported, allowing trivial 2911c27b644SPaul E. McKenney linked lists to be constructed. 2921c27b644SPaul E. McKenney 2931c27b644SPaul E. McKenney2. Dynamic memory allocation is not supported, although this can 2941c27b644SPaul E. McKenney be worked around in some cases by supplying multiple statically 2951c27b644SPaul E. McKenney allocated variables. 2961c27b644SPaul E. McKenney 2971c27b644SPaul E. McKenneySome of these limitations may be overcome in the future, but others are 2981c27b644SPaul E. McKenneymore likely to be addressed by incorporating the Linux-kernel memory model 2991c27b644SPaul E. McKenneyinto other tools. 300d8fa25c4SPaul E. McKenney 301d8fa25c4SPaul E. McKenneyFinally, please note that LKMM is subject to change as hardware, use cases, 302d8fa25c4SPaul E. McKenneyand compilers evolve. 303