mirror of
https://github.com/torvalds/linux.git
synced 2024-11-22 12:11:40 +00:00
614e40faf5
LKMM has long provided only approximate handling of SRCU read-side
critical sections. This has not been a pressing problem because LKMM's
traditional handling is correct for the common cases of non-overlapping
and properly nested critical sections. However, LKMM's traditional
handling of partially overlapping critical sections incorrectly fuses
them into one large critical section.
For example, consider the following litmus test:
------------------------------------------------------------------------
C C-srcu-nest-5
(*
* Result: Sometimes
*
* This demonstrates non-nested overlapping of SRCU read-side critical
* sections. Unlike RCU, SRCU critical sections do not unconditionally
* nest.
*)
{}
P0(int *x, int *y, struct srcu_struct *s1)
{
int r1;
int r2;
int r3;
int r4;
r3 = srcu_read_lock(s1);
r2 = READ_ONCE(*y);
r4 = srcu_read_lock(s1);
srcu_read_unlock(s1, r3);
r1 = READ_ONCE(*x);
srcu_read_unlock(s1, r4);
}
P1(int *x, int *y, struct srcu_struct *s1)
{
WRITE_ONCE(*y, 1);
synchronize_srcu(s1);
WRITE_ONCE(*x, 1);
}
locations [0:r1]
exists (0:r1=1 /\ 0:r2=0)
------------------------------------------------------------------------
Current mainline incorrectly flattens the two critical sections into
one larger critical section, giving "Never" instead of the correct
"Sometimes":
------------------------------------------------------------------------
$ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus
Test C-srcu-nest-5 Allowed
States 3
0:r1=0; 0:r2=0;
0:r1=0; 0:r2=1;
0:r1=1; 0:r2=1;
No
Witnesses
Positive: 0 Negative: 3
Flag srcu-bad-nesting
Condition exists (0:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-5 Never 0 3
Time C-srcu-nest-5 0.01
Hash=e692c106cf3e84e20f12991dc438ff1b
------------------------------------------------------------------------
To its credit, it does complain about bad nesting. But with this
commit we get the following result, which has the virtue of being
correct:
------------------------------------------------------------------------
$ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus
Test C-srcu-nest-5 Allowed
States 4
0:r1=0; 0:r2=0;
0:r1=0; 0:r2=1;
0:r1=1; 0:r2=0;
0:r1=1; 0:r2=1;
Ok
Witnesses
Positive: 1 Negative: 3
Condition exists (0:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-5 Sometimes 1 3
Time C-srcu-nest-5 0.05
Hash=e692c106cf3e84e20f12991dc438ff1b
------------------------------------------------------------------------
In addition, there are new srcu_down_read() and srcu_up_read()
functions on their way to mainline. Roughly speaking, these are to
srcu_read_lock() and srcu_read_unlock() as down() and up() are to
mutex_lock() and mutex_unlock(). The key point is that
srcu_down_read() can execute in one process and the matching
srcu_up_read() in another, as shown in this litmus test:
------------------------------------------------------------------------
C C-srcu-nest-6
(*
* Result: Never
*
* This would be valid for srcu_down_read() and srcu_up_read().
*)
{}
P0(int *x, int *y, struct srcu_struct *s1, int *idx, int *f)
{
int r2;
int r3;
r3 = srcu_down_read(s1);
WRITE_ONCE(*idx, r3);
r2 = READ_ONCE(*y);
smp_store_release(f, 1);
}
P1(int *x, int *y, struct srcu_struct *s1, int *idx, int *f)
{
int r1;
int r3;
int r4;
r4 = smp_load_acquire(f);
r1 = READ_ONCE(*x);
r3 = READ_ONCE(*idx);
srcu_up_read(s1, r3);
}
P2(int *x, int *y, struct srcu_struct *s1)
{
WRITE_ONCE(*y, 1);
synchronize_srcu(s1);
WRITE_ONCE(*x, 1);
}
locations [0:r1]
filter (1:r4=1)
exists (1:r1=1 /\ 0:r2=0)
------------------------------------------------------------------------
When run on current mainline, this litmus test gets a complaint about
an unknown macro srcu_down_read(). With this commit:
------------------------------------------------------------------------
herd7 -conf linux-kernel.cfg C-srcu-nest-6.litmus
Test C-srcu-nest-6 Allowed
States 3
0:r1=0; 0:r2=0; 1:r1=0;
0:r1=0; 0:r2=1; 1:r1=0;
0:r1=0; 0:r2=1; 1:r1=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (1:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-6 Never 0 3
Time C-srcu-nest-6 0.02
Hash=c1f20257d052ca5e899be508bedcb2a1
------------------------------------------------------------------------
Note that the user must supply the flag "f" and the "filter" clause,
similar to what must be done to emulate call_rcu().
The commit works by treating srcu_read_lock()/srcu_down_read() as
loads and srcu_read_unlock()/srcu_up_read() as stores. This allows us
to determine which unlock matches which lock by looking for a data
dependency between them. In order for this to work properly, the data
dependencies have to be tracked through stores to intermediate
variables such as "idx" in the litmus test above; this is handled by
the new carry-srcu-data relation. But it's important here (and in the
existing carry-dep relation) to avoid tracking the dependencies
through SRCU unlock stores. Otherwise, in situations resembling:
A: r1 = srcu_read_lock(s);
B: srcu_read_unlock(s, r1);
C: r2 = srcu_read_lock(s);
D: srcu_read_unlock(s, r2);
it would look as if D was dependent on both A and C, because "s" would
appear to be an intermediate variable written by B and read by C.
This explains the complications in the definitions of carry-srcu-dep
and carry-dep.
As a debugging aid, the commit adds a check for errors in which the
value returned by one call to srcu_read_lock()/srcu_down_read() is
passed to more than one instance of srcu_read_unlock()/srcu_up_read().
Finally, since these SRCU-related primitives are now treated as
ordinary reads and writes, we have to add them into the lists of
marked accesses (i.e., not subject to data races) and lock-related
accesses (i.e., one shouldn't try to access an srcu_struct with a
non-lock-related primitive such as READ_ONCE() or a plain write).
Portions of this approach were suggested by Boqun Feng and Jonas
Oberhauser.
[ paulmck: Fix space-before-tab whitespace nit. ]
Reported-by: Paul E. McKenney <paulmck@kernel.org>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reviewed-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
|
||
|---|---|---|
| .. | ||
| 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.14 7.48 -- 4.15 -- 4.19 7.49 -- 4.20 -- 5.5 7.54 -- 5.6 -- 5.16 7.56 -- 5.17 -- 7.56.1 -- ============ ========== ================== BASIC USAGE: HERD7 ================== The memory model is used, in conjunction with "herd7", to exhaustively explore the state space of small litmus tests. Documentation describing the format, features, capabilities and limitations of these litmus tests is available in tools/memory-model/Documentation/litmus-tests.txt. Example litmus tests may be found in the Linux-kernel source tree: tools/memory-model/litmus-tests/ Documentation/litmus-tests/ Several thousand more example litmus tests are available here: https://github.com/paulmckrcu/litmus https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus Documentation describing litmus tests and now to use them may be found here: tools/memory-model/Documentation/litmus-tests.txt The remainder of this section uses the SB+fencembonceonces.litmus test located in the tools/memory-model directory. To run SB+fencembonceonces.litmus against the memory model: $ cd $LINUX_SOURCE_TREE/tools/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 on running the tool itself, but please be aware that this documentation is intended for people who work on the memory model itself, that is, people making changes to the tools/memory-model/linux-kernel.* files. It is not intended for people focusing on writing, understanding, and running LKMM litmus tests. ===================== 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. And again, please be aware that this documentation is intended for people who work on the memory model itself, that is, people making changes to the tools/memory-model/linux-kernel.* files. It is not intended for people focusing on writing, understanding, and running LKMM litmus tests. ==================== DESCRIPTION OF FILES ==================== Documentation/README Guide to the other documents in the Documentation/ directory. 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. By "representative", it means the one in the litmus-tests directory is: 1) simple, the number of threads should be relatively small and each thread function should be relatively simple. 2) orthogonal, there should be no two litmus tests describing the same aspect of the memory model. 3) textbook, developers can easily copy-paste-modify the litmus tests to use the patterns on their own code. 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.