| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
There has never been recipes-paris.txt at least since v5.11.
Fix the typo.
Signed-off-by: Akira Yokosawa <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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]>
|
|
The Linux-kernel memory model (LKMM) source code and the herd7 tool are
closely linked in that the latter is responsible for (pre)processing
each C-like macro of a litmus test, and for providing the LKMM with a
set of events, or "representation", corresponding to the given macro.
This commit therefore provides herd-representation.txt to document
the representations of the concurrency macros, following their
"classification" in Documentation/atomic_t.txt.
Link: https://lore.kernel.org/all/ZnFZPJlILp5B9scN@andrea/
Suggested-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Andrea Parri <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Reviewed-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu
Pull KCSAN updates from Paul McKenney:
- improve the documentation for the new __data_racy type qualifier
to the data_race() macro's kernel-doc header and to the LKMM's
access-marking documentation
- add missing MODULE_DESCRIPTION
* tag 'kcsan.2024.07.12a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu:
kcsan: Add missing MODULE_DESCRIPTION() macro
kcsan: Add example to data_race() kerneldoc header
|
|
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]>
|
|
Add a citation to Marco's LF mentorship session presentation entitled
"The Kernel Concurrency Sanitizer"
[ paulmck: Apply Marco Elver feedback. ]
Reported-by: Marco Elver <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Reviewed-by: Akira Yokosawa <[email protected]>
Acked-by: Marco Elver <[email protected]>
Cc: Alan Stern <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: Joel Fernandes <[email protected]>
Cc: <[email protected]>
|
|
Although the data_race() kerneldoc header accurately states what it does,
some of the implications and usage patterns are non-obvious. Therefore,
add a brief locking example and also state how to have KCSAN ignore
accesses while also preventing the compiler from folding, spindling,
or otherwise mutilating the access.
[ paulmck: Apply Bart Van Assche feedback. ]
[ paulmck: Apply feedback from Marco Elver. ]
Reported-by: Bart Van Assche <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Breno Leitao <[email protected]>
Cc: Jens Axboe <[email protected]>
|
|
git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu
Pull Linux Kernel Memory Model scripting updates from Paul McKenney:
"This improves litmus-test documentation and improves the ability to do
before/after tests on the https://github.com/paulmckrcu/litmus repo"
* tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: (32 commits)
tools/memory-model: Remove out-of-date SRCU documentation
tools/memory-model: Document LKMM test procedure
tools/memory-model: Use "grep -E" instead of "egrep"
tools/memory-model: Use "-unroll 0" to keep --hw runs finite
tools/memory-model: Make judgelitmus.sh handle scripted Result: tag
tools/memory-model: Add data-race capabilities to judgelitmus.sh
tools/memory-model: Add checktheselitmus.sh to run specified litmus tests
tools/memory-model: Repair parseargs.sh header comment
tools/memory-model: Add "--" to parseargs.sh for additional arguments
tools/memory-model: Make history-check scripts use mselect7
tools/memory-model: Make checkghlitmus.sh use mselect7
tools/memory-model: Fix scripting --jobs argument
tools/memory-model: Implement --hw support for checkghlitmus.sh
tools/memory-model: Add -v flag to jingle7 runs
tools/memory-model: Make runlitmus.sh check for jingle errors
tools/memory-model: Allow herd to deduce CPU type
tools/memory-model: Keep assembly-language litmus tests
tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out
tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw
tools/memory-model: Split runlitmus.sh out of checklitmus.sh
...
|
|
Commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics")
changed the semantics of partially overlapping SRCU read-side critical
sections (among other things), making such documentation out-of-date.
The new, semantic changes are discussed in explanation.txt. Remove the
out-of-date documentation.
Signed-off-by: Andrea Parri <[email protected]>
Reviewed-by: Joel Fernandes (Google) <[email protected]>
Acked-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
Most Linux-kernel uses of locking are straightforward, but there are
corner-case uses that rely on less well-known aspects of the lock and
unlock primitives. This commit therefore adds a locking.txt and litmus
tests in Documentation/litmus-tests/locking to explain these corner-case
uses.
[ paulmck: Apply Andrea Parri feedback for klitmus7. ]
[ paulmck: Apply Akira Yokosawa example-consistency feedback. ]
Reviewed-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
Expand the discussion of SRCU and its read-side critical sections in
the Linux Kernel Memory Model documentation file explanation.txt. The
new material discusses recent changes to the memory model made in
commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU
semantics").
Signed-off-by: Alan Stern <[email protected]>
Co-developed-by: Joel Fernandes (Google) <[email protected]>
Signed-off-by: Joel Fernandes (Google) <[email protected]>
Reviewed-by: Akira Yokosawa <[email protected]>
Cc: Andrea Parri <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Jonas Oberhauser <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Peter Zijlstra <[email protected]>
CC: Will Deacon <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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]>
|
|
Viktor (as relayed by Jonas) has pointed out a weakness in the Linux
Kernel Memory Model. Namely, the memory ordering properties of atomic
operations are not monotonic: An atomic op with full-barrier semantics
does not always provide ordering as strong as one with release-barrier
semantics.
The following litmus test illustrates the problem:
--------------------------------------------------
C atomics-not-monotonic
{}
P0(int *x, atomic_t *y)
{
WRITE_ONCE(*x, 1);
smp_wmb();
atomic_set(y, 1);
}
P1(atomic_t *y)
{
int r1;
r1 = atomic_inc_return(y);
}
P2(int *x, atomic_t *y)
{
int r2;
int r3;
r2 = atomic_read(y);
smp_rmb();
r3 = READ_ONCE(*x);
}
exists (2:r2=2 /\ 2:r3=0)
--------------------------------------------------
The litmus test is allowed as shown with atomic_inc_return(), which
has full-barrier semantics. But if the operation is changed to
atomic_inc_return_release(), which only has release-barrier semantics,
the litmus test is forbidden. Clearly this violates monotonicity.
The reason is because the LKMM treats full-barrier atomic ops as if
they were written:
mb();
load();
store();
mb();
(where the load() and store() are the two parts of an atomic RMW op),
whereas it treats release-barrier atomic ops as if they were written:
load();
release_barrier();
store();
The difference is that here the release barrier orders the load part
of the atomic op before the store part with A-cumulativity, whereas
the mb()'s above do not. This means that release-barrier atomics can
effectively extend the cumul-fence relation but full-barrier atomics
cannot.
To resolve this problem we introduce the rmw-sequence relation,
representing an arbitrarily long sequence of atomic RMW operations in
which each operation reads from the previous one, and explicitly allow
it to extend cumul-fence. This modification of the memory model is
sound; it holds for PPC because of B-cumulativity, it holds for TSO
and ARM64 because of other-multicopy atomicity, and we can assume that
atomic ops on all other architectures will be implemented so as to
make it hold for them.
For similar reasons we also allow rmw-sequence to extend the
w-post-bounded relation, which is analogous to cumul-fence in some
ways.
Reported-by: Viktor Vafeiadis <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Reviewed-by: Jonas Oberhauser <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
The current informal control dependency definition in explanation.txt is
too broad and, as discussed, needs to be updated.
Consider the following example:
> if(READ_ONCE(x))
> return 42;
>
> WRITE_ONCE(y, 42);
>
> return 21;
The read event determines whether the write event will be executed "at all"
- as per the current definition - but the formal LKMM does not recognize
this as a control dependency.
Introduce a new definition which includes the requirement for the second
memory access event to syntactically lie within the arm of a non-loop
conditional.
Link: https://lore.kernel.org/all/[email protected]/
Cc: Marco Elver <[email protected]>
Cc: Charalampos Mainas <[email protected]>
Cc: Pramod Bhatotia <[email protected]>
Cc: Soham Chakraborty <[email protected]>
Cc: Martin Fink <[email protected]>
Co-developed-by: Alan Stern <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul Heidekrüger <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
As discussed, clarify LKMM not recognizing certain kinds of orderings.
In particular, highlight the fact that LKMM might deliberately make
weaker guarantees than compilers and architectures.
[ paulmck: Fix whitespace issue noted by checkpatch.pl. ]
Link: https://lore.kernel.org/all/YpoW1deb%[email protected]/T/#u
Co-developed-by: Alan Stern <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul Heidekrüger <[email protected]>
Reviewed-by: Marco Elver <[email protected]>
Reviewed-by: Joel Fernandes (Google) <[email protected]>
Cc: Charalampos Mainas <[email protected]>
Cc: Pramod Bhatotia <[email protected]>
Cc: Soham Chakraborty <[email protected]>
Cc: Martin Fink <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
Paul Heidekrüger pointed out that the Linux Kernel Memory Model
documentation doesn't mention the distinction between syntactic and
semantic dependencies. This is an important difference, because the
compiler can easily break dependencies that are only syntactic, not
semantic.
This patch adds a few paragraphs to the LKMM documentation explaining
these issues and illustrating how they can matter.
Suggested-by: Paul Heidekrüger <[email protected]>
Reviewed-by: Akira Yokosawa <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
A recent discussion[1] shows that we are in favor of strengthening the
ordering of unlock + lock on the same CPU: a unlock and a po-after lock
should provide the so-called RCtso ordering, that is a memory access S
po-before the unlock should be ordered against a memory access R
po-after the lock, unless S is a store and R is a load.
The strengthening meets programmers' expection that "sequence of two
locked regions to be ordered wrt each other" (from Linus), and can
reduce the mental burden when using locks. Therefore add it in LKMM.
[1]: https://lore.kernel.org/lkml/[email protected]/
Co-developed-by: Alan Stern <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Boqun Feng <[email protected]>
Reviewed-by: Michael Ellerman <[email protected]> (powerpc)
Acked-by: Palmer Dabbelt <[email protected]> (RISC-V)
Acked-by: Peter Zijlstra (Intel) <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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]>
|
|
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]>
|
|
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]>
|
|
The current definition of read_foo_diagnostic() in the "Lock Protection
With Lockless Diagnostic Access" section returns a value, which could
be use for any purpose. This could mislead people into incorrectly
using data_race() in cases where READ_ONCE() is required. This commit
therefore makes read_foo_diagnostic() simply print the value read.
Reported-by: Manfred Spraul <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
A misspelled git-grep regex revealed that smp_mb__after_spinlock()
was misspelled in explanation.txt. This commit adds the missing "_".
Fixes: 1c27b644c0fd ("Automate memory-barriers.txt; provide Linux-kernel memory model")
[ paulmck: Apply Alan Stern commit-log feedback. ]
Signed-off-by: Björn Töpel <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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]>
|
|
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]>
|
|
Changeset b00aedf978aa ("doc: Convert to rcu_dereference.txt to rcu_dereference.rst")
renamed: Documentation/RCU/rcu_dereference.txt
to: Documentation/RCU/rcu_dereference.rst.
Update its cross-reference accordingly.
Signed-off-by: Mauro Carvalho Chehab <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
This commit explicitly makes the connection between acquire loads and
the reads-from relation. It also adds an entry for happens-before,
and refers to the corresponding section of explanation.txt.
Reported-by: Boqun Feng <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
[ paulmck: Apply Alan Stern feedback. ]
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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 <[email protected]>
|
|
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 <[email protected]>
|
|
Add a small section to the litmus-tests.txt documentation file for
the Linux Kernel Memory Model explaining that the memory model often
fails to recognize certain control dependencies.
Suggested-by: Akira Yokosawa <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Reviewed-by: Joel Fernandes (Google) <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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 <[email protected]>
Signed-off-by: Dave Chinner <[email protected]>
Co-developed-by: Paul E. McKenney <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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 <[email protected]>
Acked-by: Peter Zijlstra (Intel) <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
The expand_to_next_prime() and next_prime_number() functions have moved
from lib/prime_numbers.c to lib/math/prime_numbers.c, so this commit
updates recipes.txt to reflect this change.
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
Rationale:
Reduces attack surface on kernel devs opening the links for MITM
as HTTPS traffic is much harder to manipulate.
Deterministic algorithm:
For each file:
If not .svg:
For each line:
If doesn't contain `\bxmlns\b`:
For each link, `\bhttp://[^# \t\r\n]*(?:\w|/)`:
If both the HTTP and HTTPS versions
return 200 OK and serve the same content:
Replace HTTP with HTTPS.
Signed-off-by: Alexander A. Klimov <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
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
...
|
|
smp_read_barrier_depends() has gone the way of mmiowb() and so many
esoteric memory barriers before it. Drop the two mentions of this
deceased barrier from the LKMM informal explanation document.
Acked-by: Peter Zijlstra (Intel) <[email protected]>
Acked-by: Alan Stern <[email protected]>
Acked-by: Paul E. McKenney <[email protected]>
Signed-off-by: Will Deacon <[email protected]>
|
|
The name of litmus test doesn't match the one described below.
Fix the name of litmus test.
Acked-by: Andrea Parri <[email protected]>
Acked-by: Joel Fernandes (Google) <[email protected]>
Signed-off-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
The definition of "conflict" should not include the type of access nor
whether the accesses are concurrent or not, which this patch addresses.
The definition of "data race" remains unchanged.
The definition of "conflict" as we know it and is cited by various
papers on memory consistency models appeared in [1]: "Two accesses to
the same variable conflict if at least one is a write; two operations
conflict if they execute conflicting accesses."
The LKMM as well as the C11 memory model are adaptations of
data-race-free, which are based on the work in [2]. Necessarily, we need
both conflicting data operations (plain) and synchronization operations
(marked). For example, C11's definition is based on [3], which defines a
"data race" as: "Two memory operations conflict if they access the same
memory location, and at least one of them is a store, atomic store, or
atomic read-modify-write operation. In a sequentially consistent
execution, two memory operations from different threads form a type 1
data race if they conflict, at least one of them is a data operation,
and they are adjacent in <T (i.e., they may be executed concurrently)."
[1] D. Shasha, M. Snir, "Efficient and Correct Execution of Parallel
Programs that Share Memory", 1988.
URL: http://snir.cs.illinois.edu/listed/J21.pdf
[2] S. Adve, "Designing Memory Consistency Models for Shared-Memory
Multiprocessors", 1993.
URL: http://sadve.cs.illinois.edu/Publications/thesis.pdf
[3] H.-J. Boehm, S. Adve, "Foundations of the C++ Concurrency Memory
Model", 2008.
URL: https://www.hpl.hp.com/techreports/2008/HPL-2008-56.pdf
Signed-off-by: Marco Elver <[email protected]>
Co-developed-by: Alan Stern <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
This commit updates the list of LKMM-related publications in
Documentation/references.txt.
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Andrea Parri <[email protected]>
|
|
explanation.txt
This patch updates the Linux Kernel Memory Model's explanation.txt
file by adding a section devoted to the model's handling of plain
accesses and data-race detection.
Signed-off-by: Alan Stern <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
explanation.txt
This patch updates the Linux Kernel Memory Model's explanation.txt
file to incorporate the introduction of the rcu-order relation and
the redefinition of rcu-fence made by commit 15aa25cbf0cc
("tools/memory-model: Change definition of rcu-fence").
Signed-off-by: Alan Stern <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
This patch fixes a few minor typos and improves word usage in a few
places in the Linux Kernel Memory Model's explanation.txt file.
Signed-off-by: Alan Stern <[email protected]>
Reviewed-by: Joel Fernandes (Google) <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
The formal memory consistency model has added support for plain accesses
(and data races). While updating the informal documentation to describe
this addition to the model is highly desirable and important future work,
update the informal documentation to at least acknowledge such addition.
Signed-off-by: Andrea Parri <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Alan Stern <[email protected]>
|
|
To reduce ambiguity in the more exotic ->prop ordering example, this
commit uses the term cumul-fence instead of the term fence for the two
fences, so that the implict ->rfe on loads/stores to Y are covered by
the description.
Link: https://lore.kernel.org/lkml/[email protected]
Suggested-by: Alan Stern <[email protected]>
Signed-off-by: Joel Fernandes (Google) <[email protected]>
Acked-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
|
|
The recent commit adding support for SRCU to the Linux Kernel Memory
Model ended up changing the names and meanings of several relations.
This patch updates the explanation.txt documentation file to reflect
those changes.
It also revises the statement of the RCU Guarantee to a more accurate
form, and it adds a short paragraph mentioning the new support for SRCU.
Signed-off-by: Alan Stern <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Andrea Parri <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Andrea Parri <[email protected]>
|
|
This commit fixes a duplicate-"the" typo in README.
Signed-off-by: SeongJae Park <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Alan Stern <[email protected]>
Cc: Alexander Shishkin <[email protected]>
Cc: Arnaldo Carvalho de Melo <[email protected]>
Cc: Jiri Olsa <[email protected]>
Cc: Linus Torvalds <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Stephane Eranian <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Vince Weaver <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Link: http://lkml.kernel.org/r/[email protected]
Signed-off-by: Ingo Molnar <[email protected]>
|
|
release/acquire
More than one kernel developer has expressed the opinion that the LKMM
should enforce ordering of writes by locking. In other words, given
the following code:
WRITE_ONCE(x, 1);
spin_unlock(&s):
spin_lock(&s);
WRITE_ONCE(y, 1);
the stores to x and y should be propagated in order to all other CPUs,
even though those other CPUs might not access the lock s. In terms of
the memory model, this means expanding the cumul-fence relation.
Locks should also provide read-read (and read-write) ordering in a
similar way. Given:
READ_ONCE(x);
spin_unlock(&s);
spin_lock(&s);
READ_ONCE(y); // or WRITE_ONCE(y, 1);
the load of x should be executed before the load of (or store to) y.
The LKMM already provides this ordering, but it provides it even in
the case where the two accesses are separated by a release/acquire
pair of fences rather than unlock/lock. This would prevent
architectures from using weakly ordered implementations of release and
acquire, which seems like an unnecessary restriction. The patch
therefore removes the ordering requirement from the LKMM for that
case.
There are several arguments both for and against this change. Let us
refer to these enhanced ordering properties by saying that the LKMM
would require locks to be RCtso (a bit of a misnomer, but analogous to
RCpc and RCsc) and it would require ordinary acquire/release only to
be RCpc. (Note: In the following, the phrase "all supported
architectures" is meant not to include RISC-V. Although RISC-V is
indeed supported by the kernel, the implementation is still somewhat
in a state of flux and therefore statements about it would be
premature.)
Pros:
The kernel already provides RCtso ordering for locks on all
supported architectures, even though this is not stated
explicitly anywhere. Therefore the LKMM should formalize it.
In theory, guaranteeing RCtso ordering would reduce the need
for additional barrier-like constructs meant to increase the
ordering strength of locks.
Will Deacon and Peter Zijlstra are strongly in favor of
formalizing the RCtso requirement. Linus Torvalds and Will
would like to go even further, requiring locks to have RCsc
behavior (ordering preceding writes against later reads), but
they recognize that this would incur a noticeable performance
degradation on the POWER architecture. Linus also points out
that people have made the mistake, in the past, of assuming
that locking has stronger ordering properties than is
currently guaranteed, and this change would reduce the
likelihood of such mistakes.
Not requiring ordinary acquire/release to be any stronger than
RCpc may prove advantageous for future architectures, allowing
them to implement smp_load_acquire() and smp_store_release()
with more efficient machine instructions than would be
possible if the operations had to be RCtso. Will and Linus
approve this rationale, hypothetical though it is at the
moment (it may end up affecting the RISC-V implementation).
The same argument may or may not apply to RMW-acquire/release;
see also the second Con entry below.
Linus feels that locks should be easy for people to use
without worrying about memory consistency issues, since they
are so pervasive in the kernel, whereas acquire/release is
much more of an "experts only" tool. Requiring locks to be
RCtso is a step in this direction.
Cons:
Andrea Parri and Luc Maranget think that locks should have the
same ordering properties as ordinary acquire/release (indeed,
Luc points out that the names "acquire" and "release" derive
from the usage of locks). Andrea points out that having
different ordering properties for different forms of acquires
and releases is not only unnecessary, it would also be
confusing and unmaintainable.
Locks are constructed from lower-level primitives, typically
RMW-acquire (for locking) and ordinary release (for unlock).
It is illogical to require stronger ordering properties from
the high-level operations than from the low-level operations
they comprise. Thus, this change would make
while (cmpxchg_acquire(&s, 0, 1) != 0)
cpu_relax();
an incorrect implementation of spin_lock(&s) as far as the
LKMM is concerned. In theory this weakness can be ameliorated
by changing the LKMM even further, requiring
RMW-acquire/release also to be RCtso (which it already is on
all supported architectures).
As far as I know, nobody has singled out any examples of code
in the kernel that actually relies on locks being RCtso.
(People mumble about RCU and the scheduler, but nobody has
pointed to any actual code. If there are any real cases,
their number is likely quite small.) If RCtso ordering is not
needed, why require it?
A handful of locking constructs (qspinlocks, qrwlocks, and
mcs_spinlocks) are built on top of smp_cond_load_acquire()
instead of an RMW-acquire instruction. It currently provides
only the ordinary acquire semantics, not the stronger ordering
this patch would require of locks. In theory this could be
ameliorated by requiring smp_cond_load_acquire() in
combination with ordinary release also to be RCtso (which is
currently true on all supported architectures).
On future weakly ordered architectures, people may be able to
implement locks in a non-RCtso fashion with significant
performance improvement. Meeting the RCtso requirement would
necessarily add run-time overhead.
Overall, the technical aspects of these arguments seem relatively
minor, and it appears mostly to boil down to a matter of opinion.
Since the opinions of senior kernel maintainers such as Linus,
Peter, and Will carry more weight than those of Luc and Andrea, this
patch changes the model in accordance with the maintainers' wishes.
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Reviewed-by: Will Deacon <[email protected]>
Reviewed-by: Andrea Parri <[email protected]>
Acked-by: Peter Zijlstra (Intel) <[email protected]>
Cc: Alexander Shishkin <[email protected]>
Cc: Arnaldo Carvalho de Melo <[email protected]>
Cc: Jiri Olsa <[email protected]>
Cc: Linus Torvalds <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Stephane Eranian <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Vince Weaver <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Link: http://lkml.kernel.org/r/[email protected]
Signed-off-by: Ingo Molnar <[email protected]>
|
|
norm7 produces the 'normalized' name of a litmus test, when the test
can be generated from a single cycle that passes through each process
exactly once. The commit renames such tests in order to comply to the
naming scheme implemented by this tool.
Signed-off-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Alan Stern <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Linus Torvalds <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: [email protected]
Cc: [email protected]
Link: http://lkml.kernel.org/r/[email protected]
Signed-off-by: Ingo Molnar <[email protected]>
|
|
The tools/memory-model/Documentation/explanation.txt file says
"For each other CPU C', smb_wmb() forces all po-earlier stores"
This commit therefore replaces the "smb_wmb()" with "smp_wmb()".
Signed-off-by: Yauheni Kaliuta <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Alan Stern <[email protected]>
Cc: Linus Torvalds <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Link: http://lkml.kernel.org/r/[email protected]
Signed-off-by: Ingo Molnar <[email protected]>
|