mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux.git
synced 2024-08-27 03:10:12 +00:00
![]() - LKMM updates: mostly documentation changes, but also some new litmus tests for atomic ops. - KCSAN updates: the most important change is that GCC 11 now has all fixes in place to support KCSAN, so GCC support can be enabled again. Also more annotations. - futex updates: minor cleanups and simplifications - seqlock updates: merge preparatory changes/cleanups for the 'associated locks' facilities. - lockdep updates: - simplify IRQ trace event handling - add various new debug checks - simplify header dependencies, split out <linux/lockdep_types.h>, decouple lockdep from other low level headers some more - fix NMI handling - misc cleanups and smaller fixes Signed-off-by: Ingo Molnar <mingo@kernel.org> -----BEGIN PGP SIGNATURE----- iQJFBAABCgAvFiEEBpT5eoXrXCwVQwEKEnMQ0APhK1gFAl8n9/wRHG1pbmdvQGtl cm5lbC5vcmcACgkQEnMQ0APhK1hZFQ//dD+AKw9Nym+WbylovmeD0qxWxPyeN/jG vBVDTOJIJLtZTkZf6YHcYOJlPwaMDYUQluqTPQhsaQZy/NoEb5NM2cFAj2R9gjyT O8665T1dvhW9Sh353mBpuwviqdrnvCeHTBEcglSlFY7hxToYAflUN0+DXGVtNys8 PFNf3L9SHT0GLVC8+di/eJzQaRqxiB0Pq7kvh2RvPJM/dcQNA9Ho3CCNO5j6qGoY u7OnMT8xJXkgbdjjUO4RO0v9VjMuNthZ2JiONDgvgKtJfIL2wt5YXIv1EYX0GuWp WZgIzE4o1G7GJOOzKpFfZFyK8grHu2fWgK1plvodWjlLkBmltJZ1qyOM+wngd/m2 TgtPo73/YFbxFUbbBpkb0eiIaH2t99kMvfCWd05+GiPCtzn9UL9GfFRWd42vonwc sQWjFrHKlnuzifUfNcLmKg7R2nUtF3Dm/SydiTJ+9NtH/QA17YJKWnlE1moulNtQ p7H7+8UdcvSQ7F38A74v2IYNIyDsv5qcE8ar4QHdaanBBX/LCyD0UlfgsgxEReXf GDKkpx7LFQlI6Y2YB+dZgkCwhNBl3/OQ3v6hC95B37fA67dAIQyPIWHiHbaM+029 gghqU4GcUcbjSnHPzl9PPL+hi9MyXrMjpb7CBXytg4NI4EE1waHR+0kX14V8ndRj MkWQOKPUgB0= =3MTT -----END PGP SIGNATURE----- Merge tag 'locking-core-2020-08-03' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip Pull locking updates from Ingo Molnar: - LKMM updates: mostly documentation changes, but also some new litmus tests for atomic ops. - KCSAN updates: the most important change is that GCC 11 now has all fixes in place to support KCSAN, so GCC support can be enabled again. Also more annotations. - futex updates: minor cleanups and simplifications - seqlock updates: merge preparatory changes/cleanups for the 'associated locks' facilities. - lockdep updates: - simplify IRQ trace event handling - add various new debug checks - simplify header dependencies, split out <linux/lockdep_types.h>, decouple lockdep from other low level headers some more - fix NMI handling - misc cleanups and smaller fixes * tag 'locking-core-2020-08-03' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip: (60 commits) kcsan: Improve IRQ state trace reporting lockdep: Refactor IRQ trace events fields into struct seqlock: lockdep assert non-preemptibility on seqcount_t write lockdep: Add preemption enabled/disabled assertion APIs seqlock: Implement raw_seqcount_begin() in terms of raw_read_seqcount() seqlock: Add kernel-doc for seqcount_t and seqlock_t APIs seqlock: Reorder seqcount_t and seqlock_t API definitions seqlock: seqcount_t latch: End read sections with read_seqcount_retry() seqlock: Properly format kernel-doc code samples Documentation: locking: Describe seqlock design and usage locking/qspinlock: Do not include atomic.h from qspinlock_types.h locking/atomic: Move ATOMIC_INIT into linux/types.h lockdep: Move list.h inclusion into lockdep.h locking/lockdep: Fix TRACE_IRQFLAGS vs. NMIs futex: Remove unused or redundant includes futex: Consistently use fshared as boolean futex: Remove needless goto's futex: Remove put_futex_key() rwsem: fix commas in initialisation docs: locking: Replace HTTP links with HTTPS ones ... |
||
---|---|---|
.. | ||
Documentation | ||
litmus-tests | ||
scripts | ||
.gitignore | ||
linux-kernel.bell | ||
linux-kernel.cat | ||
linux-kernel.cfg | ||
linux-kernel.def | ||
lock.cat | ||
README |
===================================== LINUX KERNEL MEMORY CONSISTENCY MODEL ===================================== ============ INTRODUCTION ============ This directory contains the memory consistency model (memory model, for short) of the Linux kernel, written in the "cat" language and executable by the externally provided "herd7" simulator, which exhaustively explores the state space of small litmus tests. In addition, the "klitmus7" tool (also externally provided) may be used to convert a litmus test to a Linux kernel module, which in turn allows that litmus test to be exercised within the Linux kernel. ============ REQUIREMENTS ============ Version 7.52 or higher of the "herd7" and "klitmus7" tools must be downloaded separately: https://github.com/herd/herdtools7 See "herdtools7/INSTALL.md" for installation instructions. Note that although these tools usually provide backwards compatibility, this is not absolutely guaranteed. For example, a future version of herd7 might not work with the model in this release. A compatible model will likely be made available in a later release of Linux kernel. If you absolutely need to run the model in this particular release, please try using the exact version called out above. klitmus7 is independent of the model provided here. It has its own dependency on a target kernel release where converted code is built and executed. Any change in kernel APIs essential to klitmus7 will necessitate an upgrade of klitmus7. If you find any compatibility issues in klitmus7, please inform the memory model maintainers. klitmus7 Compatibility Table ---------------------------- ============ ========== target Linux herdtools7 ------------ ---------- -- 4.18 7.48 -- 4.15 -- 4.19 7.49 -- 4.20 -- 5.5 7.54 -- 5.6 -- 7.56 -- ============ ========== ================== BASIC USAGE: HERD7 ================== The memory model is used, in conjunction with "herd7", to exhaustively explore the state space of small litmus tests. For example, to run SB+fencembonceonces.litmus against the memory model: $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus Here is the corresponding output: Test SB+fencembonceonces Allowed States 3 0:r0=0; 1:r0=1; 0:r0=1; 1:r0=0; 0:r0=1; 1:r0=1; No Witnesses Positive: 0 Negative: 3 Condition exists (0:r0=0 /\ 1:r0=0) Observation SB+fencembonceonces Never 0 3 Time SB+fencembonceonces 0.01 Hash=d66d99523e2cac6b06e66f4c995ebb48 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that this litmus test's "exists" clause can not be satisfied. See "herd7 -help" or "herdtools7/doc/" for more information. ===================== BASIC USAGE: KLITMUS7 ===================== The "klitmus7" tool converts a litmus test into a Linux kernel module, which may then be loaded and run. For example, to run SB+fencembonceonces.litmus against hardware: $ mkdir mymodules $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus $ cd mymodules ; make $ sudo sh run.sh The corresponding output includes: Test SB+fencembonceonces Allowed Histogram (3 states) 644580 :>0:r0=1; 1:r0=0; 644328 :>0:r0=0; 1:r0=1; 711092 :>0:r0=1; 1:r0=1; No Witnesses Positive: 0, Negative: 2000000 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated Hash=d66d99523e2cac6b06e66f4c995ebb48 Observation SB+fencembonceonces Never 0 2000000 Time SB+fencembonceonces 0.16 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate that during two million trials, the state specified in this litmus test's "exists" clause was not reached. And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" for more information. ==================== DESCRIPTION OF FILES ==================== Documentation/cheatsheet.txt Quick-reference guide to the Linux-kernel memory model. Documentation/explanation.txt Describes the memory model in detail. Documentation/recipes.txt Lists common memory-ordering patterns. Documentation/references.txt Provides background reading. linux-kernel.bell Categorizes the relevant instructions, including memory references, memory barriers, atomic read-modify-write operations, lock acquisition/release, and RCU operations. More formally, this file (1) lists the subtypes of the various event types used by the memory model and (2) performs RCU read-side critical section nesting analysis. linux-kernel.cat Specifies what reorderings are forbidden by memory references, memory barriers, atomic read-modify-write operations, and RCU. More formally, this file specifies what executions are forbidden by the memory model. Allowed executions are those which satisfy the model's "coherence", "atomic", "happens-before", "propagation", and "rcu" axioms, which are defined in the file. linux-kernel.cfg Convenience file that gathers the common-case herd7 command-line arguments. linux-kernel.def Maps from C-like syntax to herd7's internal litmus-test instruction-set architecture. litmus-tests Directory containing a few representative litmus tests, which are listed in litmus-tests/README. A great deal more litmus tests are available at https://github.com/paulmckrcu/litmus. lock.cat Provides a front-end analysis of lock acquisition and release, for example, associating a lock acquisition with the preceding and following releases and checking for self-deadlock. More formally, this file defines a performance-enhanced scheme for generation of the possible reads-from and coherence order relations on the locking primitives. README This file. scripts Various scripts, see scripts/README. =========== LIMITATIONS =========== The Linux-kernel memory model (LKMM) has the following limitations: 1. Compiler optimizations are not accurately modeled. Of course, the use of READ_ONCE() and WRITE_ONCE() limits the compiler's ability to optimize, but under some circumstances it is possible for the compiler to undermine the memory model. For more information, see Documentation/explanation.txt (in particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING" sections). Note that this limitation in turn limits LKMM's ability to accurately model address, control, and data dependencies. For example, if the compiler can deduce the value of some variable carrying a dependency, then the compiler can break that dependency by substituting a constant of that value. 2. Multiple access sizes for a single variable are not supported, and neither are misaligned or partially overlapping accesses. 3. Exceptions and interrupts are not modeled. In some cases, this limitation can be overcome by modeling the interrupt or exception with an additional process. 4. I/O such as MMIO or DMA is not supported. 5. Self-modifying code (such as that found in the kernel's alternatives mechanism, function tracer, Berkeley Packet Filter JIT compiler, and module loader) is not supported. 6. Complete modeling of all variants of atomic read-modify-write operations, locking primitives, and RCU is not provided. For example, call_rcu() and rcu_barrier() are not supported. However, a substantial amount of support is provided for these operations, as shown in the linux-kernel.def file. a. When rcu_assign_pointer() is passed NULL, the Linux kernel provides no ordering, but LKMM models this case as a store release. b. The "unless" RMW operations are not currently modeled: atomic_long_add_unless(), atomic_inc_unless_negative(), and atomic_dec_unless_positive(). These can be emulated in litmus tests, for example, by using atomic_cmpxchg(). One exception of this limitation is atomic_add_unless(), which is provided directly by herd7 (so no corresponding definition in linux-kernel.def). atomic_add_unless() is modeled by herd7 therefore it can be used in litmus tests. c. The call_rcu() function is not modeled. It can be emulated in litmus tests by adding another process that invokes synchronize_rcu() and the body of the callback function, with (for example) a release-acquire from the site of the emulated call_rcu() to the beginning of the additional process. d. The rcu_barrier() function is not modeled. It can be emulated in litmus tests emulating call_rcu() via (for example) a release-acquire from the end of each additional call_rcu() process to the site of the emulated rcu-barrier(). e. Although sleepable RCU (SRCU) is now modeled, there are some subtle differences between its semantics and those in the Linux kernel. For example, the kernel might interpret the following sequence as two partially overlapping SRCU read-side critical sections: 1 r1 = srcu_read_lock(&my_srcu); 2 do_something_1(); 3 r2 = srcu_read_lock(&my_srcu); 4 do_something_2(); 5 srcu_read_unlock(&my_srcu, r1); 6 do_something_3(); 7 srcu_read_unlock(&my_srcu, r2); In contrast, LKMM will interpret this as a nested pair of SRCU read-side critical sections, with the outer critical section spanning lines 1-7 and the inner critical section spanning lines 3-5. This difference would be more of a concern had anyone identified a reasonable use case for partially overlapping SRCU read-side critical sections. For more information, please see: https://paulmck.livejournal.com/40593.html f. Reader-writer locking is not modeled. It can be emulated in litmus tests using atomic read-modify-write operations. The "herd7" tool has some additional limitations of its own, apart from the memory model: 1. Non-trivial data structures such as arrays or structures are not supported. However, pointers are supported, allowing trivial linked lists to be constructed. 2. Dynamic memory allocation is not supported, although this can be worked around in some cases by supplying multiple statically allocated variables. Some of these limitations may be overcome in the future, but others are more likely to be addressed by incorporating the Linux-kernel memory model into other tools. Finally, please note that LKMM is subject to change as hardware, use cases, and compilers evolve.