| dcc51978 | 05-Nov-2024 |
Jonas Oberhauser <[email protected]> |
tools/memory-model: Distinguish between syntactic and semantic tags
Not all annotated accesses provide the semantics their syntactic tags
would imply. For example, an 'acquire tag on a write does no
tools/memory-model: Distinguish between syntactic and semantic tags
Not all annotated accesses provide the semantics their syntactic tags
would imply. For example, an 'acquire tag on a write does not imply that
the write is finally in the Acquire set and provides acquire ordering.
To distinguish in those cases between the syntactic tags and actual
sets, we capitalize the former, so 'ACQUIRE tags may be present on both
reads and writes, but only reads will appear in the Acquire set.
For tags where the two concepts are the same we do not use specific
capitalization to make this distinction.
Reported-by: Boqun Feng <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Tested-by: Boqun Feng <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Tested-by: Akira Yokosawa <[email protected]> # herdtools7.7.58
show more ...
|
| 9bc931e9 | 25-Jun-2024 |
Akira Yokosawa <[email protected]> |
tools/memory-model: Add locking.txt and glossary.txt to README
locking.txt and glossary.txt have been in LKMM's documentation for
quite a while.
Add them in README's introduction of docs and the li
tools/memory-model: Add locking.txt and glossary.txt to README
locking.txt and glossary.txt have been in LKMM's documentation for
quite a while.
Add them in README's introduction of docs and the list of docs at the
bottom. Add access-marking.txt in the former as well.
Signed-off-by: Akira Yokosawa <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Cc: Marco Elver <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 520c637b | 05-Jun-2024 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Add access-marking.txt to README
Given that access-marking.txt exists, this commit makes it easier to find.
Reported-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E.
tools/memory-model: Add access-marking.txt to README
Given that access-marking.txt exists, this commit makes it easier to find.
Reported-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 9ba7d3b3 | 02-Dec-2022 |
Jonas Oberhauser <[email protected]> |
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/[email protected]/
Reported-by: Viktor Vafeiadis <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
Reviewed-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 87859a8e | 18-May-2021 |
Paul E. McKenney <[email protected]> |
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 <[email protected]>
show more ...
|
| f92975d7 | 14-May-2021 |
Manfred Spraul <[email protected]> |
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 436eef23 | 13-May-2021 |
Paul E. McKenney <[email protected]> |
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 <[email protected]>
[ paulmck: Update per Manfred Spraul and Hillf Danton feedback. ]
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 49ab51b0 | 11-Feb-2021 |
Paul E. McKenney <[email protected]> |
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 <[email protected]>
[ paulmck: Apply Marco Elver feedback. ]
[ paulmck: Update per Akira Yokosawa feedback. ]
Reviewed-by: Marco Elver <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 9146658c | 14-Jan-2021 |
Akira Yokosawa <[email protected]> |
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 <[email protected]>
Signed-off-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|