tools/memory-model/Documentation/litmus-tests.txt

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

File Facts

System
Linux kernel
Corpus path
tools/memory-model/Documentation/litmus-tests.txt
Extension
.txt
Size
39936 bytes
Lines
1084
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

Linux-Kernel Memory Model Litmus Tests
======================================

This file describes the LKMM litmus-test format by example, describes
some tricks and traps, and finally outlines LKMM's limitations.  Earlier
versions of this material appeared in a number of LWN articles, including:

https://lwn.net/Articles/720550/
	A formal kernel memory-ordering model (part 2)
https://lwn.net/Articles/608550/
	Axiomatic validation of memory barriers and atomic instructions
https://lwn.net/Articles/470681/
	Validating Memory Barriers and Atomic Instructions

This document presents information in decreasing order of applicability,
so that, where possible, the information that has proven more commonly
useful is shown near the beginning.

For information on installing LKMM, including the underlying "herd7"
tool, please see tools/memory-model/README.


Copy-Pasta
==========

As with other software, it is often better (if less macho) to adapt an
existing litmus test than it is to create one from scratch.  A number
of litmus tests may be found in the kernel source tree:

	tools/memory-model/litmus-tests/
	Documentation/litmus-tests/

Several thousand more example litmus tests are available on github
and kernel.org:

	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

The -l and -L arguments to "git grep" can be quite helpful in identifying
existing litmus tests that are similar to the one you need.  But even if
you start with an existing litmus test, it is still helpful to have a
good understanding of the litmus-test format.


Examples and Format
===================

This section describes the overall format of litmus tests, starting
with a small example of the message-passing pattern and moving on to
more complex examples that illustrate explicit initialization and LKMM's
minimalistic set of flow-control statements.


Message-Passing Example
-----------------------

This section gives an overview of the format of a litmus test using an
example based on the common message-passing use case.  This use case
appears often in the Linux kernel.  For example, a flag (modeled by "y"
below) indicates that a buffer (modeled by "x" below) is now completely
filled in and ready for use.  It would be very bad if the consumer saw the
flag set, but, due to memory misordering, saw old values in the buffer.

This example asks whether smp_store_release() and smp_load_acquire()
suffices to avoid this bad outcome:

 1 C MP+pooncerelease+poacquireonce
 2
 3 {}

Annotation

Implementation Notes