mirror of
https://github.com/torvalds/linux
synced 2024-09-06 18:01:05 +00:00
kcsan: Document modeling of weak memory
Document how KCSAN models a subset of weak memory and the subset of missing memory barriers it can detect as a result. Signed-off-by: Marco Elver <elver@google.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit is contained in:
parent
be3f6967ec
commit
82eb6911d9
|
@ -204,17 +204,17 @@ Ultimately this allows to determine the possible executions of concurrent code,
|
|||
and if that code is free from data races.
|
||||
|
||||
KCSAN is aware of *marked atomic operations* (``READ_ONCE``, ``WRITE_ONCE``,
|
||||
``atomic_*``, etc.), but is oblivious of any ordering guarantees and simply
|
||||
assumes that memory barriers are placed correctly. In other words, KCSAN
|
||||
assumes that as long as a plain access is not observed to race with another
|
||||
conflicting access, memory operations are correctly ordered.
|
||||
``atomic_*``, etc.), and a subset of ordering guarantees implied by memory
|
||||
barriers. With ``CONFIG_KCSAN_WEAK_MEMORY=y``, KCSAN models load or store
|
||||
buffering, and can detect missing ``smp_mb()``, ``smp_wmb()``, ``smp_rmb()``,
|
||||
``smp_store_release()``, and all ``atomic_*`` operations with equivalent
|
||||
implied barriers.
|
||||
|
||||
This means that KCSAN will not report *potential* data races due to missing
|
||||
memory ordering. Developers should therefore carefully consider the required
|
||||
memory ordering requirements that remain unchecked. If, however, missing
|
||||
memory ordering (that is observable with a particular compiler and
|
||||
architecture) leads to an observable data race (e.g. entering a critical
|
||||
section erroneously), KCSAN would report the resulting data race.
|
||||
Note, KCSAN will not report all data races due to missing memory ordering,
|
||||
specifically where a memory barrier would be required to prohibit subsequent
|
||||
memory operation from reordering before the barrier. Developers should
|
||||
therefore carefully consider the required memory ordering requirements that
|
||||
remain unchecked.
|
||||
|
||||
Race Detection Beyond Data Races
|
||||
--------------------------------
|
||||
|
@ -268,6 +268,56 @@ marked operations, if all accesses to a variable that is accessed concurrently
|
|||
are properly marked, KCSAN will never trigger a watchpoint and therefore never
|
||||
report the accesses.
|
||||
|
||||
Modeling Weak Memory
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
KCSAN's approach to detecting data races due to missing memory barriers is
|
||||
based on modeling access reordering (with ``CONFIG_KCSAN_WEAK_MEMORY=y``).
|
||||
Each plain memory access for which a watchpoint is set up, is also selected for
|
||||
simulated reordering within the scope of its function (at most 1 in-flight
|
||||
access).
|
||||
|
||||
Once an access has been selected for reordering, it is checked along every
|
||||
other access until the end of the function scope. If an appropriate memory
|
||||
barrier is encountered, the access will no longer be considered for simulated
|
||||
reordering.
|
||||
|
||||
When the result of a memory operation should be ordered by a barrier, KCSAN can
|
||||
then detect data races where the conflict only occurs as a result of a missing
|
||||
barrier. Consider the example::
|
||||
|
||||
int x, flag;
|
||||
void T1(void)
|
||||
{
|
||||
x = 1; // data race!
|
||||
WRITE_ONCE(flag, 1); // correct: smp_store_release(&flag, 1)
|
||||
}
|
||||
void T2(void)
|
||||
{
|
||||
while (!READ_ONCE(flag)); // correct: smp_load_acquire(&flag)
|
||||
... = x; // data race!
|
||||
}
|
||||
|
||||
When weak memory modeling is enabled, KCSAN can consider ``x`` in ``T1`` for
|
||||
simulated reordering. After the write of ``flag``, ``x`` is again checked for
|
||||
concurrent accesses: because ``T2`` is able to proceed after the write of
|
||||
``flag``, a data race is detected. With the correct barriers in place, ``x``
|
||||
would not be considered for reordering after the proper release of ``flag``,
|
||||
and no data race would be detected.
|
||||
|
||||
Deliberate trade-offs in complexity but also practical limitations mean only a
|
||||
subset of data races due to missing memory barriers can be detected. With
|
||||
currently available compiler support, the implementation is limited to modeling
|
||||
the effects of "buffering" (delaying accesses), since the runtime cannot
|
||||
"prefetch" accesses. Also recall that watchpoints are only set up for plain
|
||||
accesses, and the only access type for which KCSAN simulates reordering. This
|
||||
means reordering of marked accesses is not modeled.
|
||||
|
||||
A consequence of the above is that acquire operations do not require barrier
|
||||
instrumentation (no prefetching). Furthermore, marked accesses introducing
|
||||
address or control dependencies do not require special handling (the marked
|
||||
access cannot be reordered, later dependent accesses cannot be prefetched).
|
||||
|
||||
Key Properties
|
||||
~~~~~~~~~~~~~~
|
||||
|
||||
|
@ -290,8 +340,8 @@ Key Properties
|
|||
4. **Detects Racy Writes from Devices:** Due to checking data values upon
|
||||
setting up watchpoints, racy writes from devices can also be detected.
|
||||
|
||||
5. **Memory Ordering:** KCSAN is *not* explicitly aware of the LKMM's ordering
|
||||
rules; this may result in missed data races (false negatives).
|
||||
5. **Memory Ordering:** KCSAN is aware of only a subset of LKMM ordering rules;
|
||||
this may result in missed data races (false negatives).
|
||||
|
||||
6. **Analysis Accuracy:** For observed executions, due to using a sampling
|
||||
strategy, the analysis is *unsound* (false negatives possible), but aims to
|
||||
|
|
Loading…
Reference in a new issue