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 ...
This commit is contained in:
@@ -2,9 +2,9 @@
|
||||
#ifndef _LIBLOCKDEP_LINUX_TRACE_IRQFLAGS_H_
|
||||
#define _LIBLOCKDEP_LINUX_TRACE_IRQFLAGS_H_
|
||||
|
||||
# define lockdep_hardirq_context(p) 0
|
||||
# define lockdep_hardirq_context() 0
|
||||
# define lockdep_softirq_context(p) 0
|
||||
# define lockdep_hardirqs_enabled(p) 0
|
||||
# define lockdep_hardirqs_enabled() 0
|
||||
# define lockdep_softirqs_enabled(p) 0
|
||||
# define lockdep_hardirq_enter() do { } while (0)
|
||||
# define lockdep_hardirq_exit() do { } while (0)
|
||||
|
@@ -1985,28 +1985,36 @@ outcome undefined.
|
||||
|
||||
In technical terms, the compiler is allowed to assume that when the
|
||||
program executes, there will not be any data races. A "data race"
|
||||
occurs when two conflicting memory accesses execute concurrently;
|
||||
two memory accesses "conflict" if:
|
||||
occurs when there are two memory accesses such that:
|
||||
|
||||
they access the same location,
|
||||
1. they access the same location,
|
||||
|
||||
they occur on different CPUs (or in different threads on the
|
||||
same CPU),
|
||||
2. at least one of them is a store,
|
||||
|
||||
at least one of them is a plain access,
|
||||
3. at least one of them is plain,
|
||||
|
||||
and at least one of them is a store.
|
||||
4. they occur on different CPUs (or in different threads on the
|
||||
same CPU), and
|
||||
|
||||
The LKMM tries to determine whether a program contains two conflicting
|
||||
accesses which may execute concurrently; if it does then the LKMM says
|
||||
there is a potential data race and makes no predictions about the
|
||||
program's outcome.
|
||||
5. they execute concurrently.
|
||||
|
||||
Determining whether two accesses conflict is easy; you can see that
|
||||
all the concepts involved in the definition above are already part of
|
||||
the memory model. The hard part is telling whether they may execute
|
||||
concurrently. The LKMM takes a conservative attitude, assuming that
|
||||
accesses may be concurrent unless it can prove they cannot.
|
||||
In the literature, two accesses are said to "conflict" if they satisfy
|
||||
1 and 2 above. We'll go a little farther and say that two accesses
|
||||
are "race candidates" if they satisfy 1 - 4. Thus, whether or not two
|
||||
race candidates actually do race in a given execution depends on
|
||||
whether they are concurrent.
|
||||
|
||||
The LKMM tries to determine whether a program contains race candidates
|
||||
which may execute concurrently; if it does then the LKMM says there is
|
||||
a potential data race and makes no predictions about the program's
|
||||
outcome.
|
||||
|
||||
Determining whether two accesses are race candidates is easy; you can
|
||||
see that all the concepts involved in the definition above are already
|
||||
part of the memory model. The hard part is telling whether they may
|
||||
execute concurrently. The LKMM takes a conservative attitude,
|
||||
assuming that accesses may be concurrent unless it can prove they
|
||||
are not.
|
||||
|
||||
If two memory accesses aren't concurrent then one must execute before
|
||||
the other. Therefore the LKMM decides two accesses aren't concurrent
|
||||
@@ -2169,8 +2177,8 @@ again, now using plain accesses for buf:
|
||||
}
|
||||
|
||||
This program does not contain a data race. Although the U and V
|
||||
accesses conflict, the LKMM can prove they are not concurrent as
|
||||
follows:
|
||||
accesses are race candidates, the LKMM can prove they are not
|
||||
concurrent as follows:
|
||||
|
||||
The smp_wmb() fence in P0 is both a compiler barrier and a
|
||||
cumul-fence. It guarantees that no matter what hash of
|
||||
@@ -2324,12 +2332,11 @@ could now perform the load of x before the load of ptr (there might be
|
||||
a control dependency but no address dependency at the machine level).
|
||||
|
||||
Finally, it turns out there is a situation in which a plain write does
|
||||
not need to be w-post-bounded: when it is separated from the
|
||||
conflicting access by a fence. At first glance this may seem
|
||||
impossible. After all, to be conflicting the second access has to be
|
||||
on a different CPU from the first, and fences don't link events on
|
||||
different CPUs. Well, normal fences don't -- but rcu-fence can!
|
||||
Here's an example:
|
||||
not need to be w-post-bounded: when it is separated from the other
|
||||
race-candidate access by a fence. At first glance this may seem
|
||||
impossible. After all, to be race candidates the two accesses must
|
||||
be on different CPUs, and fences don't link events on different CPUs.
|
||||
Well, normal fences don't -- but rcu-fence can! Here's an example:
|
||||
|
||||
int x, y;
|
||||
|
||||
@@ -2365,7 +2372,7 @@ concurrent and there is no race, even though P1's plain store to y
|
||||
isn't w-post-bounded by any marked accesses.
|
||||
|
||||
Putting all this material together yields the following picture. For
|
||||
two conflicting stores W and W', where W ->co W', the LKMM says the
|
||||
race-candidate stores W and W', where W ->co W', the LKMM says the
|
||||
stores don't race if W can be linked to W' by a
|
||||
|
||||
w-post-bounded ; vis ; w-pre-bounded
|
||||
@@ -2378,8 +2385,8 @@ sequence, and if W' is plain then they also have to be linked by a
|
||||
|
||||
w-post-bounded ; vis ; r-pre-bounded
|
||||
|
||||
sequence. For a conflicting load R and store W, the LKMM says the two
|
||||
accesses don't race if R can be linked to W by an
|
||||
sequence. For race-candidate load R and store W, the LKMM says the
|
||||
two accesses don't race if R can be linked to W by an
|
||||
|
||||
r-post-bounded ; xb* ; w-pre-bounded
|
||||
|
||||
@@ -2411,20 +2418,20 @@ is, the rules governing the memory subsystem's choice of a store to
|
||||
satisfy a load request and its determination of where a store will
|
||||
fall in the coherence order):
|
||||
|
||||
If R and W conflict and it is possible to link R to W by one
|
||||
of the xb* sequences listed above, then W ->rfe R is not
|
||||
allowed (i.e., a load cannot read from a store that it
|
||||
If R and W are race candidates and it is possible to link R to
|
||||
W by one of the xb* sequences listed above, then W ->rfe R is
|
||||
not allowed (i.e., a load cannot read from a store that it
|
||||
executes before, even if one or both is plain).
|
||||
|
||||
If W and R conflict and it is possible to link W to R by one
|
||||
of the vis sequences listed above, then R ->fre W is not
|
||||
allowed (i.e., if a store is visible to a load then the load
|
||||
must read from that store or one coherence-after it).
|
||||
If W and R are race candidates and it is possible to link W to
|
||||
R by one of the vis sequences listed above, then R ->fre W is
|
||||
not allowed (i.e., if a store is visible to a load then the
|
||||
load must read from that store or one coherence-after it).
|
||||
|
||||
If W and W' conflict and it is possible to link W to W' by one
|
||||
of the vis sequences listed above, then W' ->co W is not
|
||||
allowed (i.e., if one store is visible to a second then the
|
||||
second must come after the first in the coherence order).
|
||||
If W and W' are race candidates and it is possible to link W
|
||||
to W' by one of the vis sequences listed above, then W' ->co W
|
||||
is not allowed (i.e., if one store is visible to a second then
|
||||
the second must come after the first in the coherence order).
|
||||
|
||||
This is the extent to which the LKMM deals with plain accesses.
|
||||
Perhaps it could say more (for example, plain accesses might
|
||||
|
@@ -126,7 +126,7 @@ However, it is not necessarily the case that accesses ordered by
|
||||
locking will be seen as ordered by CPUs not holding that lock.
|
||||
Consider this example:
|
||||
|
||||
/* See Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus. */
|
||||
/* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
|
@@ -73,6 +73,18 @@ o Christopher Pulte, Shaked Flur, Will Deacon, Jon French,
|
||||
Linux-kernel memory model
|
||||
=========================
|
||||
|
||||
o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
|
||||
Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
|
||||
Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
|
||||
2019. "Calibrating your fear of big bad optimizing compilers"
|
||||
Linux Weekly News. https://lwn.net/Articles/799218/
|
||||
|
||||
o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
|
||||
Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
|
||||
Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
|
||||
2019. "Who's afraid of a big bad optimizing compiler?"
|
||||
Linux Weekly News. https://lwn.net/Articles/793253/
|
||||
|
||||
o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
|
||||
Alan Stern. 2018. "Frightening small children and disconcerting
|
||||
grown-ups: Concurrency in the Linux kernel". In Proceedings of
|
||||
@@ -88,6 +100,11 @@ o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
|
||||
Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)"
|
||||
Linux Weekly News. https://lwn.net/Articles/720550/
|
||||
|
||||
o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
|
||||
Alan Stern. 2017-2019. "A Formal Model of Linux-Kernel Memory
|
||||
Ordering" (backup material for the LWN articles)
|
||||
https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
|
||||
|
||||
|
||||
Memory-model tooling
|
||||
====================
|
||||
@@ -110,5 +127,5 @@ Memory-model comparisons
|
||||
========================
|
||||
|
||||
o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
|
||||
Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016).
|
||||
http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html.
|
||||
Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
|
||||
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
|
||||
|
@@ -28,8 +28,34 @@ downloaded separately:
|
||||
See "herdtools7/INSTALL.md" for installation instructions.
|
||||
|
||||
Note that although these tools usually provide backwards compatibility,
|
||||
this is not absolutely guaranteed. Therefore, if a later version does
|
||||
not work, please try using the exact version called out above.
|
||||
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 --
|
||||
============ ==========
|
||||
|
||||
|
||||
==================
|
||||
@@ -207,11 +233,15 @@ The Linux-kernel memory model (LKMM) has the following limitations:
|
||||
case as a store release.
|
||||
|
||||
b. The "unless" RMW operations are not currently modeled:
|
||||
atomic_long_add_unless(), atomic_add_unless(),
|
||||
atomic_inc_unless_negative(), and
|
||||
atomic_dec_unless_positive(). These can be emulated
|
||||
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
|
||||
|
Reference in New Issue
Block a user