summaryrefslogtreecommitdiffstats
path: root/tools/memory-model/README
diff options
context:
space:
mode:
Diffstat (limited to 'tools/memory-model/README')
-rw-r--r--tools/memory-model/README223
1 files changed, 223 insertions, 0 deletions
diff --git a/tools/memory-model/README b/tools/memory-model/README
new file mode 100644
index 0000000000..dab3890420
--- /dev/null
+++ b/tools/memory-model/README
@@ -0,0 +1,223 @@
+ =====================================
+ 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.52 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.