mirror_ubuntu-kernels/tools/memory-model/Documentation
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
..
access-marking.txt tools/memory-model: Document data_race(READ_ONCE()) 2021-07-27 11:48:55 -07:00
cheatsheet.txt tools/memory-model: Expand the cheatsheet.txt notion of relaxed 2020-09-04 11:58:15 -07:00
control-dependencies.txt tools/memory-model: Document categories of ordering primitives 2020-11-06 17:24:50 -08:00
explanation.txt tools: memory-model: Add rmw-sequences to the LKMM 2023-01-03 20:47:04 -08:00
glossary.txt doc: Update rcu_dereference.rst reference 2021-03-08 14:29:22 -08:00
litmus-tests.txt tools/memory-model: Clarify LKMM's limitations in litmus-tests.txt 2022-08-31 05:15:31 -07:00
ordering.txt tools/memory-model: Document categories of ordering primitives 2020-11-06 17:24:50 -08:00
README tools/memory-model: Document categories of ordering primitives 2020-11-06 17:24:50 -08:00
recipes.txt tools/memory-model: Update recipes.txt prime_numbers.c path 2020-09-03 09:51:00 -07:00
references.txt Replace HTTP links with HTTPS ones: LKMM 2020-09-03 09:51:00 -07:00
simple.txt tools/memory-model: Remove reference to atomic_ops.rst 2021-03-08 14:29:22 -08:00

It has been said that successful communication requires first identifying
what your audience knows and then building a bridge from their current
knowledge to what they need to know.  Unfortunately, the expected
Linux-kernel memory model (LKMM) audience might be anywhere from novice
to expert both in kernel hacking and in understanding LKMM.

This document therefore points out a number of places to start reading,
depending on what you know and what you would like to learn.  Please note
that the documents later in this list assume that the reader understands
the material provided by documents earlier in this list.

o	You are new to Linux-kernel concurrency: simple.txt

o	You have some background in Linux-kernel concurrency, and would
	like an overview of the types of low-level concurrency primitives
	that the Linux kernel provides:  ordering.txt

	Here, "low level" means atomic operations to single variables.

o	You are familiar with the Linux-kernel concurrency primitives
	that you need, and just want to get started with LKMM litmus
	tests:  litmus-tests.txt

o	You are familiar with Linux-kernel concurrency, and would
	like a detailed intuitive understanding of LKMM, including
	situations involving more than two threads:  recipes.txt

o	You would like a detailed understanding of what your compiler can
	and cannot do to control dependencies:  control-dependencies.txt

o	You are familiar with Linux-kernel concurrency and the use of
	LKMM, and would like a quick reference:  cheatsheet.txt

o	You are familiar with Linux-kernel concurrency and the use
	of LKMM, and would like to learn about LKMM's requirements,
	rationale, and implementation:	explanation.txt

o	You are interested in the publications related to LKMM, including
	hardware manuals, academic literature, standards-committee
	working papers, and LWN articles:  references.txt


====================
DESCRIPTION OF FILES
====================

README
	This file.

cheatsheet.txt
	Quick-reference guide to the Linux-kernel memory model.

control-dependencies.txt
	Guide to preventing compiler optimizations from destroying
	your control dependencies.

explanation.txt
	Detailed description of the memory model.

litmus-tests.txt
	The format, features, capabilities, and limitations of the litmus
	tests that LKMM can evaluate.

ordering.txt
	Overview of the Linux kernel's low-level memory-ordering
	primitives by category.

recipes.txt
	Common memory-ordering patterns.

references.txt
	Background information.

simple.txt
	Starting point for someone new to Linux-kernel concurrency.
	And also a reminder of the simpler approaches to concurrency!