Граф коммитов

108 Коммитов

Автор SHA1 Сообщение Дата
Jonas Oberhauser 9ba7d3b3b8 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>
2023-01-03 20:47:04 -08:00
Alan Stern ebd50e2947 tools: memory-model: Add rmw-sequences to the LKMM
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 <viktor@mpi-sws.org>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reviewed-by: Jonas Oberhauser <jonas.oberhauser@huawei.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2023-01-03 20:47:04 -08:00
Paul Heidekrüger fc13b47692 tools/memory-model: Weaken ctrl dependency definition in explanation.txt
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/20220615114330.2573952-1-paul.heidekrueger@in.tum.de/
Cc: Marco Elver <elver@google.com>
Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
Cc: Martin Fink <martin.fink@in.tum.de>
Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2022-10-18 15:14:52 -07:00
Paul Heidekrüger be94ecf760 tools/memory-model: Clarify LKMM's limitations in litmus-tests.txt
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%2FQeeszO1@ethstick13.dse.in.tum.de/T/#u
Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
Reviewed-by: Marco Elver <elver@google.com>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
Cc: Martin Fink <martin.fink@in.tum.de>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2022-08-31 05:15:31 -07:00
Akira Yokosawa 5b759db441 tools/memory-model/README: Update klitmus7 compat table
EXPORT_SYMBOL of do_exec() was removed in v5.17.  Unfortunately,
kernel modules from klitmus7 7.56 have do_exec() at the end of
each kthread.

herdtools7 7.56.1 has addressed the issue.

Update the compatibility table accordingly.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: stable@vger.kernel.org # v5.17+
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2022-05-03 10:12:48 -07:00
Alan Stern e2b665f612 tools/memory-model: Explain syntactic and semantic dependencies
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 <paul.heidekrueger@in.tum.de>
Reviewed-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2022-02-01 17:32:30 -08:00
Boqun Feng c438b7d860 tools/memory-model: litmus: Add two tests for unlock(A)+lock(B) ordering
The memory model has been updated to provide a stronger ordering
guarantee for unlock(A)+lock(B) on the same CPU/thread. Therefore add
two litmus tests describing this new guarantee, these tests are simple
yet can clearly show the usage of the new guarantee, also they can serve
as the self tests for the modification in the model.

Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Peter Zijlstra (Intel) <peterz@infradead.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-11-30 17:47:08 -08:00
Boqun Feng b47c05ecf6 tools/memory-model: doc: Describe the requirement of the litmus-tests directory
It's better that we have some "standard" about which test should be put
in the litmus-tests directory because it helps future contributors
understand whether they should work on litmus-tests in kernel or Paul's
GitHub repo. Therefore explain a little bit on what a "representative"
litmus test is.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Peter Zijlstra (Intel) <peterz@infradead.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-11-30 17:47:08 -08:00
Boqun Feng ddfe12944e tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU
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/20210909185937.GA12379@rowland.harvard.edu/

Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Reviewed-by: Michael Ellerman <mpe@ellerman.id.au> (powerpc)
Acked-by: Palmer Dabbelt <palmerdabbelt@google.com> (RISC-V)
Acked-by: Peter Zijlstra (Intel) <peterz@infradead.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-11-30 17:47:08 -08:00
Paul E. McKenney 87859a8e3f 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>
2021-07-27 11:48:55 -07:00
Manfred Spraul f92975d76d 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>
2021-07-27 11:48:55 -07:00
Paul E. McKenney 436eef23c4 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>
2021-07-27 11:47:34 -07:00
Paul E. McKenney 1846a7fa76 tools/memory-model: Make read_foo_diagnostic() more clearly diagnostic
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 <manfred@colorfullife.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-07-20 13:52:03 -07:00
Björn Töpel d25fba0e34 tools/memory-model: Fix smp_mb__after_spinlock() spelling
A misspelled git-grep regex revealed that smp_mb__after_spinlock()
was misspelled in explanation.txt.  This commit adds the missing "_".

Fixes: 1c27b644c0 ("Automate memory-barriers.txt; provide Linux-kernel memory model")
[ paulmck: Apply Alan Stern commit-log feedback. ]
Signed-off-by: Björn Töpel <bjorn.topel@intel.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-05-10 16:27:20 -07:00
Paul E. McKenney 49ab51b01e 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>
2021-03-15 13:59:47 -07:00
Akira Yokosawa 9146658cc4 tools/memory-model: Remove reference to atomic_ops.rst
atomic_ops.rst was removed by commit f0400a77eb ("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>
2021-03-08 14:29:22 -08:00
Mauro Carvalho Chehab ba46b21bbd doc: Update rcu_dereference.rst reference
Changeset b00aedf978 ("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 <mchehab+huawei@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-03-08 14:29:22 -08:00
Akira Yokosawa 3d5c70329b tools/memory-model: Fix typo in klitmus7 compatibility table
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: d075a78a5a ("tools/memory-model/README: Expand dependency of klitmus7")
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-01-04 14:40:50 -08:00
Akira Yokosawa 5c587f9b9c tools/memory-model: Remove redundant initialization in litmus tests
This is a revert of commit 1947bfcf81 ("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 <paulmck@kernel.org>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-01-04 14:40:49 -08:00
Paul E. McKenney 8881e7a774 tools/memory-model: Tie acquire loads to reads-from
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 <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2021-01-04 14:40:49 -08:00
Paul E. McKenney b6ff30849c tools/memory-model: Label MP tests' producers and consumers
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 <hannes@cmpxchg.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-11-06 17:25:17 -08:00
Paul E. McKenney acc4bdc55d tools/memory-model: Use "buf" and "flag" for message-passing tests
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 <hannes@cmpxchg.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-11-06 17:25:16 -08:00
Paul E. McKenney 1947bfcf81 tools/memory-model: Add types to litmus tests
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@kernel.org>
2020-11-06 17:25:16 -08:00
Paul E. McKenney 0a27ce6b69 tools/memory-model: Add a glossary of LKMM terms
[ paulmck: Apply Alan Stern feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-11-06 17:24:53 -08:00
Paul E. McKenney ebb477cb2f 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>
2020-11-06 17:24:50 -08:00
Paul E. McKenney ab8bcad67b 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>
2020-10-26 16:18:53 -07:00
Alan Stern 9270e1a744 tools: memory-model: Document that the LKMM can easily miss control dependencies
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 <akiyks@gmail.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-10-26 16:18:53 -07:00
Paul E. McKenney 0ce0c78eff 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>
2020-09-04 11:58:15 -07:00
Paul E. McKenney 0b8c06b75e 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>
2020-09-03 09:51:01 -07:00
Paul E. McKenney 984f272be9 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>
2020-09-03 09:51:01 -07:00
Paul E. McKenney cc9628b45c tools/memory-model: Update recipes.txt prime_numbers.c path
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 <paulmck@kernel.org>
2020-09-03 09:51:00 -07:00
Alexander A. Klimov 1e44e6e82e Replace HTTP links with HTTPS ones: LKMM
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 <grandmaster@al2klimov.de>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-09-03 09:51:00 -07:00
Linus Torvalds 9ba19ccd2d These were the main changes in this cycle:
- 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
 
 Signed-off-by: Ingo Molnar <mingo@kernel.org>
 -----BEGIN PGP SIGNATURE-----
 
 iQJFBAABCgAvFiEEBpT5eoXrXCwVQwEKEnMQ0APhK1gFAl8n9/wRHG1pbmdvQGtl
 cm5lbC5vcmcACgkQEnMQ0APhK1hZFQ//dD+AKw9Nym+WbylovmeD0qxWxPyeN/jG
 vBVDTOJIJLtZTkZf6YHcYOJlPwaMDYUQluqTPQhsaQZy/NoEb5NM2cFAj2R9gjyT
 O8665T1dvhW9Sh353mBpuwviqdrnvCeHTBEcglSlFY7hxToYAflUN0+DXGVtNys8
 PFNf3L9SHT0GLVC8+di/eJzQaRqxiB0Pq7kvh2RvPJM/dcQNA9Ho3CCNO5j6qGoY
 u7OnMT8xJXkgbdjjUO4RO0v9VjMuNthZ2JiONDgvgKtJfIL2wt5YXIv1EYX0GuWp
 WZgIzE4o1G7GJOOzKpFfZFyK8grHu2fWgK1plvodWjlLkBmltJZ1qyOM+wngd/m2
 TgtPo73/YFbxFUbbBpkb0eiIaH2t99kMvfCWd05+GiPCtzn9UL9GfFRWd42vonwc
 sQWjFrHKlnuzifUfNcLmKg7R2nUtF3Dm/SydiTJ+9NtH/QA17YJKWnlE1moulNtQ
 p7H7+8UdcvSQ7F38A74v2IYNIyDsv5qcE8ar4QHdaanBBX/LCyD0UlfgsgxEReXf
 GDKkpx7LFQlI6Y2YB+dZgkCwhNBl3/OQ3v6hC95B37fA67dAIQyPIWHiHbaM+029
 gghqU4GcUcbjSnHPzl9PPL+hi9MyXrMjpb7CBXytg4NI4EE1waHR+0kX14V8ndRj
 MkWQOKPUgB0=
 =3MTT
 -----END PGP SIGNATURE-----

Merge tag 'locking-core-2020-08-03' of 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
  ...
2020-08-03 14:39:35 -07:00
Will Deacon 628fd55671 tools/memory-model: Remove smp_read_barrier_depends() from informal doc
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) <peterz@infradead.org>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Paul E. McKenney <paulmck@kernel.org>
Signed-off-by: Will Deacon <will@kernel.org>
2020-07-21 10:50:37 +01:00
Akira Yokosawa 2bfa5c62de tools/memory-model/README: Mention herdtools7 7.56 in compatibility table
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 <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-06-29 12:05:18 -07:00
Akira Yokosawa d075a78a5a tools/memory-model/README: Expand dependency of klitmus7
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]: b899a85043 ("compiler.h: Remove ACCESS_ONCE()")
[2]: 0bb95f80a3 ("Makefile: Globally enable VLA warning")
[3]: d56c0d45f0 ("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 <parri.andrea@gmail.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-06-29 12:05:18 -07:00
Akira Yokosawa 9725dd5551 tools/memory-model: Fix reference to litmus test in recipes.txt
The name of litmus test doesn't match the one described below.
Fix the name of litmus test.

Acked-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-06-29 12:05:18 -07:00
Boqun Feng 4a9cc65f7a tools/memory-model: Add an exception for limitations on _unless() family
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 <luc.maranget@inria.fr>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-06-29 12:05:18 -07:00
Marco Elver c1b1460901 tools/memory-model: Fix "conflict" definition
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 <elver@google.com>
Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-06-29 12:05:17 -07:00
Paul E. McKenney 38908de90a tools/memory-model: Add recent references
This commit updates the list of LKMM-related publications in
Documentation/references.txt.

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
2020-06-29 12:05:17 -07:00
Masahiro Yamada d198b34f38 .gitignore: add SPDX License Identifier
Add SPDX License Identifier to all .gitignore files.

Signed-off-by: Masahiro Yamada <masahiroy@kernel.org>
Signed-off-by: Greg Kroah-Hartman <gregkh@linuxfoundation.org>
2020-03-25 11:50:48 +01:00
Alan Stern c58a801701 tools/memory-model/Documentation: Add plain accesses and data races to 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 <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2019-10-05 11:59:44 -07:00
Alan Stern ddc82999f0 tools/memory-model/Documentation: Put redefinition of rcu-fence into 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 15aa25cbf0
("tools/memory-model: Change definition of rcu-fence").

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2019-10-05 11:59:23 -07:00
Alan Stern 3321ea1290 tools/memory-model/Documentation: Fix typos in explanation.txt
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 <stern@rowland.harvard.edu>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2019-10-05 11:58:55 -07:00
Alan Stern daebf24a8e tools/memory-model: Fix data race detection for unordered store and load
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 <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2019-10-05 11:58:14 -07:00
Andrea Parri 6738ff85c3 tools/memory-model: Update the informal documentation
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 <andrea.parri@amarulasolutions.com>
Cc: Will Deacon <will.deacon@arm.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@linux.ibm.com>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
2019-08-09 10:28:57 -07:00
Joel Fernandes (Google) 6240973e56 tools/memory-model: Use cumul-fence instead of fence in ->prop example
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 <stern@rowland.harvard.edu>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
2019-08-09 10:28:57 -07:00
Paul E. McKenney 7455cdd1a0 tools/memory-model: Make scripts be executable
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 <paulmck@linux.ibm.com>
2019-08-01 08:40:07 -07:00
Alan Stern 4289ee7d5a tools/memory-model: Improve data-race detection
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.litmus

Reported-by: Herbert Xu <herbert@gondor.apana.org.au>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Tested-by: Akira Yokosawa <akiyks@gmail.com>
2019-06-24 09:08:54 -07:00
Alan Stern 15aa25cbf0 tools/memory-model: Change definition of rcu-fence
The rcu-fence relation in the Linux Kernel Memory Model is not well
named.  It doesn't act like any other fence relation, in that it does
not relate events before a fence to events after that fence.  All it
does is relate certain RCU events to one another (those that are
ordered by the RCU Guarantee); this induces an actual
strong-fence-like relation linking events preceding the first RCU
event to those following the second.

This patch renames rcu-fence, now called rcu-order.  It adds a new
definition of rcu-fence, something which should have been present all
along because it is used in the rb relation.  And it modifies the
fence and strong-fence relations by making them incorporate the new
rcu-fence.

As a result of this change, there is no longer any need to define
full-fence in the section for detecting data races.  It can simply be
replaced by the updated strong-fence relation.

This change should have no effect on the operation of the memory model.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
2019-06-21 16:20:49 -07:00