1
0
Fork 0

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>
alistair/sunxi64-5.4-dsi
Andrea Parri 2019-06-29 23:10:44 +02:00 committed by Paul E. McKenney
parent 6240973e56
commit 6738ff85c3
2 changed files with 27 additions and 32 deletions

View File

@ -42,7 +42,8 @@ linux-kernel.bell and linux-kernel.cat files that make up the formal
version of the model; they are extremely terse and their meanings are version of the model; they are extremely terse and their meanings are
far from clear. far from clear.
This document describes the ideas underlying the LKMM. It is meant This document describes the ideas underlying the LKMM, but excluding
the modeling of bare C (or plain) shared memory accesses. It is meant
for people who want to understand how the model was designed. It does for people who want to understand how the model was designed. It does
not go into the details of the code in the .bell and .cat files; not go into the details of the code in the .bell and .cat files;
rather, it explains in English what the code expresses symbolically. rather, it explains in English what the code expresses symbolically.
@ -354,31 +355,25 @@ be extremely complex.
Optimizing compilers have great freedom in the way they translate Optimizing compilers have great freedom in the way they translate
source code to object code. They are allowed to apply transformations source code to object code. They are allowed to apply transformations
that add memory accesses, eliminate accesses, combine them, split them that add memory accesses, eliminate accesses, combine them, split them
into pieces, or move them around. Faced with all these possibilities, into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(),
the LKMM basically gives up. It insists that the code it analyzes or one of the other atomic or synchronization primitives prevents a
must contain no ordinary accesses to shared memory; all accesses must large number of compiler optimizations. In particular, it is guaranteed
be performed using READ_ONCE(), WRITE_ONCE(), or one of the other that the compiler will not remove such accesses from the generated code
atomic or synchronization primitives. These primitives prevent a (unless it can prove the accesses will never be executed), it will not
large number of compiler optimizations. In particular, it is change the order in which they occur in the code (within limits imposed
guaranteed that the compiler will not remove such accesses from the by the C standard), and it will not introduce extraneous accesses.
generated code (unless it can prove the accesses will never be
executed), it will not change the order in which they occur in the
code (within limits imposed by the C standard), and it will not
introduce extraneous accesses.
This explains why the MP and SB examples above used READ_ONCE() and The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather
WRITE_ONCE() rather than ordinary memory accesses. Thanks to this than ordinary memory accesses. Thanks to this usage, we can be certain
usage, we can be certain that in the MP example, P0's write event to that in the MP example, the compiler won't reorder P0's write event to
buf really is po-before its write event to flag, and similarly for the buf and P0's write event to flag, and similarly for the other shared
other shared memory accesses in the examples. memory accesses in the examples.
Private variables are not subject to this restriction. Since they are Since private variables are not shared between CPUs, they can be
not shared between CPUs, they can be accessed normally without accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they
READ_ONCE() or WRITE_ONCE(), and there will be no ill effects. In need not even be stored in normal memory at all -- in principle a
fact, they need not even be stored in normal memory at all -- in private variable could be stored in a CPU register (hence the convention
principle a private variable could be stored in a CPU register (hence that these variables have names starting with the letter 'r').
the convention that these variables have names starting with the
letter 'r').
A WARNING A WARNING

View File

@ -167,15 +167,15 @@ scripts Various scripts, see scripts/README.
LIMITATIONS LIMITATIONS
=========== ===========
The Linux-kernel memory model has the following limitations: The Linux-kernel memory model (LKMM) has the following limitations:
1. Compiler optimizations are not modeled. Of course, the use 1. Compiler optimizations are not accurately modeled. Of course,
of READ_ONCE() and WRITE_ONCE() limits the compiler's ability the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
to optimize, but there is Linux-kernel code that uses bare C ability to optimize, but under some circumstances it is possible
memory accesses. Handling this code is on the to-do list. for the compiler to undermine the memory model. For more
For more information, see Documentation/explanation.txt (in information, see Documentation/explanation.txt (in particular,
particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
and "A WARNING" sections). sections).
Note that this limitation in turn limits LKMM's ability to Note that this limitation in turn limits LKMM's ability to
accurately model address, control, and data dependencies. accurately model address, control, and data dependencies.