tools/memory-model/Documentation/explanation.txt

Source file repositories/reference/linux-study-clean/tools/memory-model/Documentation/explanation.txt

File Facts

System
Linux kernel
Corpus path
tools/memory-model/Documentation/explanation.txt
Extension
.txt
Size
109224 bytes
Lines
2811
Domain
Support Tooling And Documentation
Bucket
tools
Inferred role
Support Tooling And Documentation: documentation
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

if (r1) {
			   smp_rmb();
			V: r2 = buf;
		   }
	}

This program does not contain a data race.  Although the U and V
accesses are race candidates, the LKMM can prove they are not
concurrent as follows:

	The smp_wmb() fence in P0 is both a compiler barrier and a
	cumul-fence.  It guarantees that no matter what hash of
	machine instructions the compiler generates for the plain
	access U, all those instructions will be po-before the fence.
	Consequently U's store to buf, no matter how it is carried out
	at the machine level, must propagate to P1 before X's store to
	flag does.

	X and Y are both marked accesses.  Hence an rfe link from X to
	Y is a valid indicator that X propagated to P1 before Y
	executed, i.e., X ->vis Y.  (And if there is no rfe link then
	r1 will be 0, so V will not be executed and ipso facto won't
	race with U.)

	The smp_rmb() fence in P1 is a compiler barrier as well as a
	fence.  It guarantees that all the machine-level instructions
	corresponding to the access V will be po-after the fence, and
	therefore any loads among those instructions will execute
	after the fence does and hence after Y does.

Thus U's store to buf is forced to propagate to P1 before V's load
executes (assuming V does execute), ruling out the possibility of a
data race between them.

This analysis illustrates how the LKMM deals with plain accesses in
general.  Suppose R is a plain load and we want to show that R
executes before some marked access E.  We can do this by finding a
marked access X such that R and X are ordered by a suitable fence and
X ->xb* E.  If E was also a plain access, we would also look for a
marked access Y such that X ->xb* Y, and Y and E are ordered by a
fence.  We describe this arrangement by saying that R is
"post-bounded" by X and E is "pre-bounded" by Y.

In fact, we go one step further: Since R is a read, we say that R is
"r-post-bounded" by X.  Similarly, E would be "r-pre-bounded" or
"w-pre-bounded" by Y, depending on whether E was a store or a load.
This distinction is needed because some fences affect only loads
(i.e., smp_rmb()) and some affect only stores (smp_wmb()); otherwise
the two types of bounds are the same.  And as a degenerate case, we
say that a marked access pre-bounds and post-bounds itself (e.g., if R
above were a marked load then X could simply be taken to be R itself.)

The need to distinguish between r- and w-bounding raises yet another
issue.  When the source code contains a plain store, the compiler is
allowed to put plain loads of the same location into the object code.
For example, given the source code:

	x = 1;

the compiler is theoretically allowed to generate object code that
looks like:

	if (x != 1)
		x = 1;

thereby adding a load (and possibly replacing the store entirely).
For this reason, whenever the LKMM requires a plain store to be
w-pre-bounded or w-post-bounded by a marked access, it also requires
the store to be r-pre-bounded or r-post-bounded, so as to handle cases
where the compiler adds a load.

Annotation

Implementation Notes