=====================================
|
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.49 of the "herd7" and "klitmus7" tools must be downloaded
|
separately:
|
|
https://github.com/herd/herdtools7
|
|
See "herdtools7/INSTALL.md" for installation instructions.
|
|
|
==================
|
BASIC USAGE: HERD7
|
==================
|
|
The memory model is used, in conjunction with "herd7", to exhaustively
|
explore the state space of small litmus tests.
|
|
For example, to run SB+fencembonceonces.litmus against the 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.
|
|
|
=====================
|
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.
|
|
|
====================
|
DESCRIPTION OF FILES
|
====================
|
|
Documentation/cheatsheet.txt
|
Quick-reference guide to the Linux-kernel memory model.
|
|
Documentation/explanation.txt
|
Describes the memory model in detail.
|
|
Documentation/recipes.txt
|
Lists common memory-ordering patterns.
|
|
Documentation/references.txt
|
Provides background reading.
|
|
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.
|
|
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.
|
|
|
===========
|
LIMITATIONS
|
===========
|
|
The Linux-kernel memory model has the following limitations:
|
|
1. Compiler optimizations are not modeled. Of course, the use
|
of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
|
to optimize, but there is Linux-kernel code that uses bare C
|
memory accesses. Handling this code is on the to-do list.
|
For more information, see Documentation/explanation.txt (in
|
particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
|
and "A WARNING" sections).
|
|
2. Multiple access sizes for a single variable are not supported,
|
and neither are misaligned or partially overlapping accesses.
|
|
3. Exceptions and interrupts are not modeled. In some cases,
|
this limitation can be overcome by modeling the interrupt or
|
exception with an additional process.
|
|
4. I/O such as MMIO or DMA is not supported.
|
|
5. Self-modifying code (such as that found in the kernel's
|
alternatives mechanism, function tracer, Berkeley Packet Filter
|
JIT compiler, and module loader) is not supported.
|
|
6. Complete modeling of all variants of atomic read-modify-write
|
operations, locking primitives, and RCU is not provided.
|
For example, call_rcu() and rcu_barrier() are not supported.
|
However, a substantial amount of support is provided for these
|
operations, as shown in the linux-kernel.def file.
|
|
The "herd7" tool has some additional limitations of its own, apart from
|
the memory model:
|
|
1. Non-trivial data structures such as arrays or structures are
|
not supported. However, pointers are supported, allowing trivial
|
linked lists to be constructed.
|
|
2. Dynamic memory allocation is not supported, although this can
|
be worked around in some cases by supplying multiple statically
|
allocated variables.
|
|
Some of these limitations may be overcome in the future, but others are
|
more likely to be addressed by incorporating the Linux-kernel memory model
|
into other tools.
|
