9ba7d3b3 | 02-Dec-2022 |
Jonas Oberhauser <jonas.oberhauser@huawei.com> |
tools: memory-model: Make plain accesses carry dependencies
As reported by Viktor, plain accesses in LKMM are weaker than accesses to registers: the latter carry dependencies but the former do not.
tools: memory-model: Make plain accesses carry dependencies
As reported by Viktor, plain accesses in LKMM are weaker than accesses to registers: the latter carry dependencies but the former do not. This is exemplified in the following snippet:
int r = READ_ONCE(*x); WRITE_ONCE(*y, r);
Here a data dependency links the READ_ONCE() to the WRITE_ONCE(), preserving their order, because the model treats r as a register. If r is turned into a memory location accessed by plain accesses, however, the link is broken and the order between READ_ONCE() and WRITE_ONCE() is no longer preserved.
This is too conservative, since any optimizations on plain accesses that might break dependencies are also possible on registers; it also contradicts the intuitive notion of "dependency" as the data stored by the WRITE_ONCE() does depend on the data read by the READ_ONCE(), independently of whether r is a register or a memory location.
This is resolved by redefining all dependencies to include dependencies carried by memory accesses; a dependency is said to be carried by memory accesses (in the model: carry-dep) from one load to another load if the initial load is followed by an arbitrarily long sequence alternating between stores and loads of the same thread, where the data of each store depends on the previous load, and is read by the next load.
Any dependency linking the final load in the sequence to another access also links the initial load in the sequence to that access.
More deep details can be found in this LKML discussion:
https://lore.kernel.org/lkml/d86295788ad14a02874ab030ddb8a6f8@huawei.com/
Reported-by: Viktor Vafeiadis <viktor@mpi-sws.org> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huawei.com> Reviewed-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
87859a8e | 18-May-2021 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Document data_race(READ_ONCE())
It is possible to cause KCSAN to ignore marked accesses by applying __no_kcsan to the function or applying data_race() to the marked accesses. The
tools/memory-model: Document data_race(READ_ONCE())
It is possible to cause KCSAN to ignore marked accesses by applying __no_kcsan to the function or applying data_race() to the marked accesses. These approaches allow the developer to restrict compiler optimizations while also causing KCSAN to ignore diagnostic accesses.
This commit therefore updates the documentation accordingly.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
f92975d7 | 14-May-2021 |
Manfred Spraul <manfred@colorfullife.com> |
tools/memory-model: Heuristics using data_race() must handle all values
Data loaded for use by some sorts of heuristics can tolerate the occasional erroneous value. In this case the loads may use d
tools/memory-model: Heuristics using data_race() must handle all values
Data loaded for use by some sorts of heuristics can tolerate the occasional erroneous value. In this case the loads may use data_race() to give the compiler full freedom to optimize while also informing KCSAN of the intent. However, for this to work, the heuristic needs to be able to tolerate any erroneous value that could possibly arise. This commit therefore adds a paragraph spelling this out.
Signed-off-by: Manfred Spraul <manfred@colorfullife.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
436eef23 | 13-May-2021 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Add example for heuristic lockless reads
This commit adds example code for heuristic lockless reads, based loosely on the sem_lock() and sem_unlock() functions.
[ paulmck: Apply
tools/memory-model: Add example for heuristic lockless reads
This commit adds example code for heuristic lockless reads, based loosely on the sem_lock() and sem_unlock() functions.
[ paulmck: Apply Alan Stern and Manfred Spraul feedback. ]
Reported-by: Manfred Spraul <manfred@colorfullife.com> [ paulmck: Update per Manfred Spraul and Hillf Danton feedback. ] Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
49ab51b0 | 11-Feb-2021 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Add access-marking documentation
This commit adapts the "Concurrency bugs should fear the big bad data-race detector (part 2)" LWN article (https://lwn.net/Articles/816854/) to k
tools/memory-model: Add access-marking documentation
This commit adapts the "Concurrency bugs should fear the big bad data-race detector (part 2)" LWN article (https://lwn.net/Articles/816854/) to kernel-documentation form. This allows more easily updating the material as needed.
Suggested-by: Thomas Gleixner <tglx@linutronix.de> [ paulmck: Apply Marco Elver feedback. ] [ paulmck: Update per Akira Yokosawa feedback. ] Reviewed-by: Marco Elver <elver@google.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
9146658c | 14-Jan-2021 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: Remove reference to atomic_ops.rst
atomic_ops.rst was removed by commit f0400a77ebdc ("atomic: Delete obsolete documentation"). Remove the broken link in tools/memory-model/Docum
tools/memory-model: Remove reference to atomic_ops.rst
atomic_ops.rst was removed by commit f0400a77ebdc ("atomic: Delete obsolete documentation"). Remove the broken link in tools/memory-model/Documentation/simple.txt.
Cc: Peter Zijlstra <peterz@infradead.org> Signed-off-by: Akira Yokosawa <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
ebb477cb | 11-Aug-2020 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Document categories of ordering primitives
The Linux kernel has a number of categories of ordering primitives, which are recorded in the LKMM implementation and hinted at by chea
tools/memory-model: Document categories of ordering primitives
The Linux kernel has a number of categories of ordering primitives, which are recorded in the LKMM implementation and hinted at by cheatsheet.txt. But there is no overview of these categories, and such an overview is needed in order to understand multithreaded LKMM litmus tests. This commit therefore adds an ordering.txt as well as extracting a control-dependencies.txt from memory-barriers.txt. It also updates the README file.
[ paulmck: Apply Akira Yokosawa file-placement feedback. ] [ paulmck: Apply Alan Stern feedback. ] [ paulmck: Apply self-review feedback. ] Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
ab8bcad6 | 04-Aug-2020 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Move Documentation description to Documentation/README
This commit moves the descriptions of the files residing in tools/memory-model/Documentation to a README file in that direc
tools/memory-model: Move Documentation description to Documentation/README
This commit moves the descriptions of the files residing in tools/memory-model/Documentation to a README file in that directory, leaving behind the description of tools/memory-model/Documentation/README itself. After this change, tools/memory-model/Documentation/README provides a guide to the files in the tools/memory-model/Documentation directory, guiding people with different skills and needs to the most appropriate starting point.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
0ce0c78e | 04-Aug-2020 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Expand the cheatsheet.txt notion of relaxed
This commit adds a key entry enumerating the various types of relaxed operations. While in the area, it also renames the relaxed rows
tools/memory-model: Expand the cheatsheet.txt notion of relaxed
This commit adds a key entry enumerating the various types of relaxed operations. While in the area, it also renames the relaxed rows.
[ paulmck: Apply Boqun Feng feedback. ] Acked-by: Boqun Feng <boqun.feng@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
0b8c06b7 | 04-Aug-2020 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Add a simple entry point document
Current LKMM documentation assumes that the reader already understands concurrency in the Linux kernel, which won't necessarily always be the ca
tools/memory-model: Add a simple entry point document
Current LKMM documentation assumes that the reader already understands concurrency in the Linux kernel, which won't necessarily always be the case. This commit supplies a simple.txt file that provides a starting point for someone who is new to concurrency in the Linux kernel. That said, this file might also useful as a reminder to experienced developers of simpler approaches to dealing with concurrency.
Link: Link: https://lwn.net/Articles/827180/ [ paulmck: Apply feedback from Joel Fernandes. ] Co-developed-by: Dave Chinner <dchinner@redhat.com> Signed-off-by: Dave Chinner <dchinner@redhat.com> Co-developed-by: Paul E. McKenney <paulmck@kernel.org> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
984f272b | 03-Aug-2020 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Improve litmus-test documentation
The current LKMM documentation says very little about litmus tests, and worse yet directs people to the herd7 documentation for more information
tools/memory-model: Improve litmus-test documentation
The current LKMM documentation says very little about litmus tests, and worse yet directs people to the herd7 documentation for more information. Now, the herd7 documentation is quite voluminous and educational, but it is intended for people creating and modifying memory models, not those attempting to use them.
This commit therefore updates README and creates a litmus-tests.txt file that gives an overview of litmus-test format and describes ways of modeling various special cases, illustrated with numerous examples.
[ paulmck: Add Alan Stern feedback. ] [ paulmck: Apply Dave Chinner feedback. ] [ paulmck: Apply Andrii Nakryiko feedback. ] [ paulmck: Apply Johannes Weiner feedback. ] Link: https://lwn.net/Articles/827180/ Reported-by: Dave Chinner <david@fromorbit.com> Acked-by: Peter Zijlstra (Intel) <peterz@infradead.org> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|