linux-stable.git/tools/memory-model/Documentation, branch v6.11

Merge tag 'kcsan.2024.07.12a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu

2024-07-15T22:44:40+00:00

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

tools/memory-model: Add access-marking.txt to README

2024-06-06T18:24:58+00:00

Given that access-marking.txt exists, this commit makes it easier to find.

Reported-by: Akira Yokosawa 
Signed-off-by: Paul E. McKenney

tools/memory-model: Add KCSAN LF mentorship session citation

2024-06-06T18:23:35+00:00

Add a citation to Marco's LF mentorship session presentation entitled
"The Kernel Concurrency Sanitizer"

[ paulmck: Apply Marco Elver feedback. ]

Reported-by: Marco Elver 
Signed-off-by: Paul E. McKenney 
Acked-by: Andrea Parri 
Reviewed-by: Akira Yokosawa 
Acked-by: Marco Elver 
Cc: Alan Stern 
Cc: Will Deacon 
Cc: Peter Zijlstra 
Cc: Boqun Feng 
Cc: Nicholas Piggin 
Cc: David Howells 
Cc: Jade Alglave 
Cc: Luc Maranget 
Cc: Daniel Lustig 
Cc: Joel Fernandes 
Cc:

kcsan: Add example to data_race() kerneldoc header

2024-05-30T22:06:26+00:00

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 
Signed-off-by: Paul E. McKenney 
Cc: Marco Elver 
Cc: Breno Leitao 
Cc: Jens Axboe

Merge tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu

2023-04-24T19:02:25+00:00

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
  ...

tools/memory-model: Remove out-of-date SRCU documentation

2023-03-24T17:24:48+00:00

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 
Reviewed-by: Joel Fernandes (Google) 
Acked-by: Alan Stern 
Signed-off-by: Paul E. McKenney

tools/memory-model: Document locking corner cases

2023-03-24T17:22:25+00:00

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 
Signed-off-by: Paul E. McKenney

tools/memory-model: Add documentation about SRCU read-side critical sections

2023-03-22T19:02:21+00:00

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 
Co-developed-by: Joel Fernandes (Google) 
Signed-off-by: Joel Fernandes (Google) 
Reviewed-by: Akira Yokosawa 
Cc: Andrea Parri 
Cc: Boqun Feng 
Cc: Jade Alglave 
Cc: Jonas Oberhauser 
Cc: Luc Maranget 
Cc: "Paul E. McKenney" 
Cc: Peter Zijlstra 
CC: Will Deacon 
Signed-off-by: Paul E. McKenney

tools: memory-model: Make plain accesses carry dependencies

2023-01-04T04:47:04+00:00

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 
Signed-off-by: Jonas Oberhauser 
Reviewed-by: Alan Stern 
Signed-off-by: Paul E. McKenney

tools: memory-model: Add rmw-sequences to the LKMM

2023-01-04T04:47:04+00:00

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 
Signed-off-by: Alan Stern 
Reviewed-by: Jonas Oberhauser 
Signed-off-by: Paul E. McKenney