28 Jul, 2021
3 commits
-
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
-
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
Signed-off-by: Paul E. McKenney -
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
[ paulmck: Update per Manfred Spraul and Hillf Danton feedback. ]
Signed-off-by: Paul E. McKenney
21 Jul, 2021
1 commit
-
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
Signed-off-by: Paul E. McKenney
11 May, 2021
1 commit
-
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
Signed-off-by: Paul E. McKenney
16 Mar, 2021
1 commit
-
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
[ paulmck: Apply Marco Elver feedback. ]
[ paulmck: Update per Akira Yokosawa feedback. ]
Reviewed-by: Marco Elver
Signed-off-by: Paul E. McKenney
09 Mar, 2021
2 commits
-
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
Signed-off-by: Akira Yokosawa
Signed-off-by: Paul E. McKenney -
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
Signed-off-by: Paul E. McKenney
05 Jan, 2021
3 commits
-
klitmus7 of herdtools7 7.48 or earlier depends on ACCESS_ONCE(),
which was removed in Linux v4.15.
Fix the obvious typo in the table.Fixes: d075a78a5ab1 ("tools/memory-model/README: Expand dependency of klitmus7")
Signed-off-by: Akira Yokosawa
Signed-off-by: Paul E. McKenney -
This is a revert of commit 1947bfcf81a9 ("tools/memory-model: Add types
to litmus tests") with conflict resolutions.klitmus7 [1] is aware of default types of "int" and "int*".
It accepts litmus tests for herd7 without extra type info unless
non-"int" variables are referenced by an "exists", "locations",
or "filter" directive.[1]: Tested with klitmus7 versions 7.49 or later.
Suggested-by: Paul E. McKenney
Signed-off-by: Akira Yokosawa
Signed-off-by: Paul E. McKenney -
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
Signed-off-by: Paul E. McKenney
07 Nov, 2020
5 commits
-
This commit adds comments that label the MP tests' producer and consumer
processes, and also that label the "exists" clause as the bad outcome.Reported-by: Johannes Weiner
Signed-off-by: Paul E. McKenney -
The use of "x" and "y" for message-passing tests is fine for people
familiar with memory models and litmus-test nomenclature, but is a bit
obtuse for others. This commit therefore substitutes "buf" for "x" and
"flag" for "y" for the MP tests. There are a few special-case MP tests
that use locks and these are unchanged. There is another MP test that
uses pointers, and this is changed to name the pointer "p".Reported-by: Johannes Weiner
Signed-off-by: Paul E. McKenney -
This commit adds type information for global variables in the litmus
tests in order to allow easier use with klitmus7.Signed-off-by: Paul E. McKenney
-
[ paulmck: Apply Alan Stern feedback. ]
Signed-off-by: Paul E. McKenney -
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
27 Oct, 2020
2 commits
-
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
-
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
Signed-off-by: Alan Stern
Reviewed-by: Joel Fernandes (Google)
Signed-off-by: Paul E. McKenney
05 Sep, 2020
1 commit
-
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
Signed-off-by: Paul E. McKenney
04 Sep, 2020
4 commits
-
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
Signed-off-by: Dave Chinner
Co-developed-by: Paul E. McKenney
Signed-off-by: Paul E. McKenney -
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
Acked-by: Peter Zijlstra (Intel)
Signed-off-by: Paul E. McKenney -
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
-
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
Signed-off-by: Paul E. McKenney
04 Aug, 2020
1 commit
-
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 ,
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
...
21 Jul, 2020
1 commit
-
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)
Acked-by: Alan Stern
Acked-by: Paul E. McKenney
Signed-off-by: Will Deacon
30 Jun, 2020
6 commits
-
herdtools7 7.56 is going to be released in the week of 22 Jun 2020.
This commit therefore adds the exact version in the compatibility table.Acked-by: Andrea Parri
Signed-off-by: Akira Yokosawa
Signed-off-by: Paul E. McKenney -
klitmus7 is independent of the memory model but depends on the
build-target kernel release.
It occasionally lost compatibility due to kernel API changes [1, 2, 3].
It was remedied in a backwards-compatible manner respectively [4, 5, 6].Reflect this fact in README.
[1]: b899a850431e ("compiler.h: Remove ACCESS_ONCE()")
[2]: 0bb95f80a38f ("Makefile: Globally enable VLA warning")
[3]: d56c0d45f0e2 ("proc: decouple proc from VFS with "struct proc_ops"")
[4]: https://github.com/herd/herdtools7/commit/e87d7f9287d1
("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated ACCESS_ONCE")
[5]: https://github.com/herd/herdtools7/commit/a0cbb10d02be
("klitmus: Avoid variable length array")
[6]: https://github.com/herd/herdtools7/commit/46b9412d3a58
("klitmus: Linux kernel v5.6.x compat")NOTE: [5] was ahead of herdtools7 7.53, which did not make an
official release. Code generated by klitmus7 without [5] can still be
built targeting Linux 4.20--5.5 if you don't care VLA warnings.Acked-by: Andrea Parri
Signed-off-by: Akira Yokosawa
Signed-off-by: Paul E. McKenney -
The name of litmus test doesn't match the one described below.
Fix the name of litmus test.Acked-by: Andrea Parri
Acked-by: Joel Fernandes (Google)
Signed-off-by: Akira Yokosawa
Signed-off-by: Paul E. McKenney -
According to Luc, atomic_add_unless() is directly provided by herd7,
therefore it can be used in litmus tests. So change the limitation
section in README to unlimit the use of atomic_add_unless().Cc: Luc Maranget
Acked-by: Andrea Parri
Reviewed-by: Joel Fernandes (Google)
Signed-off-by: Boqun Feng
Signed-off-by: Paul E. McKenney -
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
Co-developed-by: Alan Stern
Signed-off-by: Alan Stern
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney -
This commit updates the list of LKMM-related publications in
Documentation/references.txt.Signed-off-by: Paul E. McKenney
Acked-by: Andrea Parri
25 Mar, 2020
1 commit
-
Add SPDX License Identifier to all .gitignore files.
Signed-off-by: Masahiro Yamada
Signed-off-by: Greg Kroah-Hartman
06 Oct, 2019
4 commits
-
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
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney -
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
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney -
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
Reviewed-by: Joel Fernandes (Google)
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney -
Currently the Linux Kernel Memory Model gives an incorrect response
for the following litmus test:C plain-WWC
{}
P0(int *x)
{
WRITE_ONCE(*x, 2);
}P1(int *x, int *y)
{
int r1;
int r2;
int r3;r1 = READ_ONCE(*x);
if (r1 == 2) {
smp_rmb();
r2 = *x;
}
smp_rmb();
r3 = READ_ONCE(*x);
WRITE_ONCE(*y, r3 - 1);
}P2(int *x, int *y)
{
int r4;r4 = READ_ONCE(*y);
if (r4 > 0)
WRITE_ONCE(*x, 1);
}exists (x=2 /\ 1:r2=2 /\ 2:r4=1)
The memory model says that the plain read of *x in P1 races with the
WRITE_ONCE(*x) in P2.The problem is that we have a write W and a read R related by neither
fre or rfe, but rather W ->coe W' ->rfe R, where W' is an intermediate
write (the WRITE_ONCE() in P0). In this situation there is no
particular ordering between W and R, so either a wr-vis link from W to
R or an rw-xbstar link from R to W would prove that the accesses
aren't concurrent.But the LKMM only looks for a wr-vis link, which is equivalent to
assuming that W must execute before R. This is not necessarily true
on non-multicopy-atomic systems, as the WWC pattern demonstrates.This patch changes the LKMM to accept either a wr-vis or a reverse
rw-xbstar link as a proof of non-concurrency.Signed-off-by: Alan Stern
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney
10 Aug, 2019
2 commits
-
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
Cc: Will Deacon
Cc: Peter Zijlstra
Cc: Boqun Feng
Cc: Nicholas Piggin
Cc: David Howells
Cc: Jade Alglave
Cc: Luc Maranget
Cc: "Paul E. McKenney"
Cc: Akira Yokosawa
Cc: Daniel Lustig
Signed-off-by: Paul E. McKenney
Acked-by: Alan Stern -
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/20190729121745.GA140682@google.com
Suggested-by: Alan Stern
Signed-off-by: Joel Fernandes (Google)
Acked-by: Alan Stern
Signed-off-by: Paul E. McKenney
01 Aug, 2019
1 commit
-
This commit simplifies life a bit by making all of the scripts in
tools/memory-model/scripts be executable.Signed-off-by: Paul E. McKenney
25 Jun, 2019
1 commit
-
Herbert Xu recently reported a problem concerning RCU and compiler
barriers. In the course of discussing the problem, he put forth a
litmus test which illustrated a serious defect in the Linux Kernel
Memory Model's data-race-detection code [1].The defect was that the LKMM assumed visibility and executes-before
ordering of plain accesses had to be mediated by marked accesses. In
Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
test was allowed and contained a data race although neither is true.In fact, plain accesses can be ordered by fences even in the absence
of marked accesses. In most cases this doesn't matter, because most
fences only order accesses within a single thread. But the rcu-fence
relation is different; it can order (and induce visibility between)
accesses in different threads -- events which otherwise might be
concurrent. This makes it relevant to data-race detection.This patch makes two changes to the memory model to incorporate the
new insight:If a store is separated by a fence from another access,
the store is necessarily visible to the other access (as
reflected in the ww-vis and wr-vis relations). Similarly,
if a load is separated by a fence from another access then
the load necessarily executes before the other access (as
reflected in the rw-xbstar relation).If a store is separated by a strong fence from a marked access
then it is necessarily visible to any access that executes
after the marked access (as reflected in the ww-vis and wr-vis
relations).With these changes, the LKMM gives the desired result for Herbert's
litmus test and other related ones [2].[1] https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
[2] https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmusReported-by: Herbert Xu
Signed-off-by: Alan Stern
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney
Tested-by: Akira Yokosawa