mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/next/linux-next.git
synced 2025-01-01 10:42:11 +00:00
55ea0b074d
A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7 behavior of simply ignoring any softcoded tags in the .def and .bell files. We port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg and reporting an error if the LKMM is used without this switch. To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic RMW which do not return a value and define atomic_add_unless with an Mb tag in linux-kernel.def. We update the herd-representation.txt accordingly and clarify some of the resulting combinations. Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> Tested-by: Boqun Feng <boqun.feng@gmail.com>
224 lines
7.2 KiB
Plaintext
224 lines
7.2 KiB
Plaintext
=====================================
|
|
LINUX KERNEL MEMORY CONSISTENCY MODEL
|
|
=====================================
|
|
|
|
============
|
|
INTRODUCTION
|
|
============
|
|
|
|
This directory contains the memory consistency model (memory model, for
|
|
short) of the Linux kernel, written in the "cat" language and executable
|
|
by the externally provided "herd7" simulator, which exhaustively explores
|
|
the state space of small litmus tests.
|
|
|
|
In addition, the "klitmus7" tool (also externally provided) may be used
|
|
to convert a litmus test to a Linux kernel module, which in turn allows
|
|
that litmus test to be exercised within the Linux kernel.
|
|
|
|
|
|
============
|
|
REQUIREMENTS
|
|
============
|
|
|
|
Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
|
|
downloaded separately:
|
|
|
|
https://github.com/herd/herdtools7
|
|
|
|
See "herdtools7/INSTALL.md" for installation instructions.
|
|
|
|
Note that although these tools usually provide backwards compatibility,
|
|
this is not absolutely guaranteed.
|
|
|
|
For example, a future version of herd7 might not work with the model
|
|
in this release. A compatible model will likely be made available in
|
|
a later release of Linux kernel.
|
|
|
|
If you absolutely need to run the model in this particular release,
|
|
please try using the exact version called out above.
|
|
|
|
klitmus7 is independent of the model provided here. It has its own
|
|
dependency on a target kernel release where converted code is built
|
|
and executed. Any change in kernel APIs essential to klitmus7 will
|
|
necessitate an upgrade of klitmus7.
|
|
|
|
If you find any compatibility issues in klitmus7, please inform the
|
|
memory model maintainers.
|
|
|
|
klitmus7 Compatibility Table
|
|
----------------------------
|
|
|
|
============ ==========
|
|
target Linux herdtools7
|
|
------------ ----------
|
|
-- 4.14 7.48 --
|
|
4.15 -- 4.19 7.49 --
|
|
4.20 -- 5.5 7.54 --
|
|
5.6 -- 5.16 7.56 --
|
|
5.17 -- 7.56.1 --
|
|
============ ==========
|
|
|
|
|
|
==================
|
|
BASIC USAGE: HERD7
|
|
==================
|
|
|
|
The memory model is used, in conjunction with "herd7", to exhaustively
|
|
explore the state space of small litmus tests. Documentation describing
|
|
the format, features, capabilities and limitations of these litmus
|
|
tests is available in tools/memory-model/Documentation/litmus-tests.txt.
|
|
|
|
Example litmus tests may be found in the Linux-kernel source tree:
|
|
|
|
tools/memory-model/litmus-tests/
|
|
Documentation/litmus-tests/
|
|
|
|
Several thousand more example litmus tests are available here:
|
|
|
|
https://github.com/paulmckrcu/litmus
|
|
https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
|
|
https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
|
|
|
|
Documentation describing litmus tests and now to use them may be found
|
|
here:
|
|
|
|
tools/memory-model/Documentation/litmus-tests.txt
|
|
|
|
The remainder of this section uses the SB+fencembonceonces.litmus test
|
|
located in the tools/memory-model directory.
|
|
|
|
To run SB+fencembonceonces.litmus against the memory model:
|
|
|
|
$ cd $LINUX_SOURCE_TREE/tools/memory-model
|
|
$ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
|
|
|
|
Here is the corresponding output:
|
|
|
|
Test SB+fencembonceonces Allowed
|
|
States 3
|
|
0:r0=0; 1:r0=1;
|
|
0:r0=1; 1:r0=0;
|
|
0:r0=1; 1:r0=1;
|
|
No
|
|
Witnesses
|
|
Positive: 0 Negative: 3
|
|
Condition exists (0:r0=0 /\ 1:r0=0)
|
|
Observation SB+fencembonceonces Never 0 3
|
|
Time SB+fencembonceonces 0.01
|
|
Hash=d66d99523e2cac6b06e66f4c995ebb48
|
|
|
|
The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
|
|
this litmus test's "exists" clause can not be satisfied.
|
|
|
|
See "herd7 -help" or "herdtools7/doc/" for more information on running the
|
|
tool itself, but please be aware that this documentation is intended for
|
|
people who work on the memory model itself, that is, people making changes
|
|
to the tools/memory-model/linux-kernel.* files. It is not intended for
|
|
people focusing on writing, understanding, and running LKMM litmus tests.
|
|
|
|
|
|
=====================
|
|
BASIC USAGE: KLITMUS7
|
|
=====================
|
|
|
|
The "klitmus7" tool converts a litmus test into a Linux kernel module,
|
|
which may then be loaded and run.
|
|
|
|
For example, to run SB+fencembonceonces.litmus against hardware:
|
|
|
|
$ mkdir mymodules
|
|
$ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
|
|
$ cd mymodules ; make
|
|
$ sudo sh run.sh
|
|
|
|
The corresponding output includes:
|
|
|
|
Test SB+fencembonceonces Allowed
|
|
Histogram (3 states)
|
|
644580 :>0:r0=1; 1:r0=0;
|
|
644328 :>0:r0=0; 1:r0=1;
|
|
711092 :>0:r0=1; 1:r0=1;
|
|
No
|
|
Witnesses
|
|
Positive: 0, Negative: 2000000
|
|
Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
|
|
Hash=d66d99523e2cac6b06e66f4c995ebb48
|
|
Observation SB+fencembonceonces Never 0 2000000
|
|
Time SB+fencembonceonces 0.16
|
|
|
|
The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
|
|
that during two million trials, the state specified in this litmus
|
|
test's "exists" clause was not reached.
|
|
|
|
And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
|
|
for more information. And again, please be aware that this documentation
|
|
is intended for people who work on the memory model itself, that is,
|
|
people making changes to the tools/memory-model/linux-kernel.* files.
|
|
It is not intended for people focusing on writing, understanding, and
|
|
running LKMM litmus tests.
|
|
|
|
|
|
====================
|
|
DESCRIPTION OF FILES
|
|
====================
|
|
|
|
Documentation/README
|
|
Guide to the other documents in the Documentation/ directory.
|
|
|
|
linux-kernel.bell
|
|
Categorizes the relevant instructions, including memory
|
|
references, memory barriers, atomic read-modify-write operations,
|
|
lock acquisition/release, and RCU operations.
|
|
|
|
More formally, this file (1) lists the subtypes of the various
|
|
event types used by the memory model and (2) performs RCU
|
|
read-side critical section nesting analysis.
|
|
|
|
linux-kernel.cat
|
|
Specifies what reorderings are forbidden by memory references,
|
|
memory barriers, atomic read-modify-write operations, and RCU.
|
|
|
|
More formally, this file specifies what executions are forbidden
|
|
by the memory model. Allowed executions are those which
|
|
satisfy the model's "coherence", "atomic", "happens-before",
|
|
"propagation", and "rcu" axioms, which are defined in the file.
|
|
|
|
linux-kernel.cfg
|
|
Convenience file that gathers the common-case herd7 command-line
|
|
arguments.
|
|
|
|
linux-kernel.def
|
|
Maps from C-like syntax to herd7's internal litmus-test
|
|
instruction-set architecture.
|
|
|
|
litmus-tests
|
|
Directory containing a few representative litmus tests, which
|
|
are listed in litmus-tests/README. A great deal more litmus
|
|
tests are available at https://github.com/paulmckrcu/litmus.
|
|
|
|
By "representative", it means the one in the litmus-tests
|
|
directory is:
|
|
|
|
1) simple, the number of threads should be relatively
|
|
small and each thread function should be relatively
|
|
simple.
|
|
2) orthogonal, there should be no two litmus tests
|
|
describing the same aspect of the memory model.
|
|
3) textbook, developers can easily copy-paste-modify
|
|
the litmus tests to use the patterns on their own
|
|
code.
|
|
|
|
lock.cat
|
|
Provides a front-end analysis of lock acquisition and release,
|
|
for example, associating a lock acquisition with the preceding
|
|
and following releases and checking for self-deadlock.
|
|
|
|
More formally, this file defines a performance-enhanced scheme
|
|
for generation of the possible reads-from and coherence order
|
|
relations on the locking primitives.
|
|
|
|
README
|
|
This file.
|
|
|
|
scripts Various scripts, see scripts/README.
|