path: root/tools/memory-model/Documentation/litmus-tests.txt

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 {}
 4
 5 P0(int *x, int *y)
 6 {
 7   WRITE_ONCE(*x, 1);
 8   smp_store_release(y, 1);
 9 }
10
11 P1(int *x, int *y)
12 {
13   int r0;
14   int r1;
15
16   r0 = smp_load_acquire(y);
17   r1 = READ_ONCE(*x);
18 }
19
20 exists (1:r0=1 /\ 1:r1=0)

Line 1 starts with "C", which identifies this file as being in the
LKMM C-language format (which, as we will see, is a small fragment
of the full C language).  The remainder of line 1 is the name of
the test, which by convention is the filename with the ".litmus"
suffix stripped.  In this case, the actual test may be found in
tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
in the Linux-kernel source tree.

Mechanically generated litmus tests will often have an optional
double-quoted comment string on the second line.  Such strings are ignored
when running the test.  Yes, you can add your own comments to litmus
tests, but this is a bit involved due to the use of multiple parsers.
For now, you can use C-language comments in the C code, and these comments
may be in either the "/* */" or the "//" style.  A later section will
cover the full litmus-test commenting story.

Line 3 is the initialization section.  Because the default initialization
to zero suffices for this test, the "{}" syntax is used, which mean the
initialization section is empty.  Litmus tests requiring non-default
initialization must have non-empty initialization sections, as in the
example that will be presented later in this document.

Lines 5-9 show the first process and lines 11-18 the second process.  Each
process corresponds to a Linux-kernel task (or kthread, workqueue, thread,
and so on; LKMM discussions often use these terms interchangeably).
The name of the first process is "P0" and that of the second "P1".
You can name your processes anything you like as long as the names consist
of a single "P" followed by a number, and as long as the numbers are
consecutive starting with zero.  This can actually be quite helpful,
for example, a .litmus file matching "^P1(" but not matching "^P2("
must contain a two-process litmus test.

The argument list for each function are pointers to the global variables
used by that function.  Unlike normal C-language function parameters, the
names are significant.  The fact that both P0() and P1() have a formal
parameter named "x" means that these two processes are working with the
same global variable, also named "x".  So the "int *x, int *y" on P0()
and P1() mean that both processes are working with two shared global
variables, "x" and "y".  Global variables are always passed to processes
by reference, hence "P0(int *x, int *y)", but *never* "P0(int x, int y)".

P0() has no local variables, but P1() has two of them named "r0" and "r1".
These names may be freely chosen, but for historical reasons stemming from
other litmus-test formats, it is conventional to use names consisting of
"r" followed by a number as shown here.  A common bug in litmus tests
is forgetting to add a global variable to a process's parameter list.
This will sometimes result in an error message, but can also cause the
intended global to instead be silently treated as an undeclared local
variable.

Each process's code is similar to Linux-kernel C, as can be seen on lines
7-8 and 13-17.  This code may use many of the Linux kernel's atomic
operations, some of its exclusive-lock functions, and some of its RCU
and SRCU functions.  An approximate list of the currently supported
functions may be found in the linux-kernel.def file.

The P0() process does "WRITE_ONCE(*x, 1)" on line 7.  Because "x" is a
pointer in P0()'s parameter list, this does an unordered store to global
variable "x".  Line 8 does "smp_store_release(y, 1)", and because "y"
is also in P0()'s parameter list, this does a release store to global
variable "y".

The P1() process declares two local variables on lines 13 and 14.
Line 16 does "r0 = smp_load_acquire(y)" which does an acquire load
from global variable "y" into local variable "r0".  Line 17 does a
"r1 = READ_ONCE(*x)", which does an unordered load from "*x" into local
variable "r1".  Both "x" and "y" are in P1()'s parameter list, so both
reference the same global variables that are used by P0().

Line 20 is the "exists" assertion expression to evaluate the final state.
This final state is evaluated after the dust has settled: both processes
have completed and all of their memory references and memory barriers
have propagated to all parts of the system.  The references to the local
variables "r0" and "r1" in line 24 must be prefixed with "1:" to specify
which process they are local to.

Note that the assertion expression is written in the litmus-test
language rather than in C.  For example, single "=" is an equality
operator rather than an assignment.  The "/\" character combination means
"and".  Similarly, "\/" stands for "or".  Both of these are ASCII-art
representations of the corresponding mathematical symbols.  Finally,
"~" stands for "logical not", which is "!" in C, and not to be confused
with the C-language "~" operator which instead stands for "bitwise not".
Parentheses may be used to override precedence.

The "exists" assertion on line 20 is satisfied if the consumer sees the
flag ("y") set but the buffer ("x") as not yet filled in, that is, if P1()
loaded a value from "x" that was equal to 1 but loaded a value from "y"
that was still equal to zero.

This example can be checked by running the following command, which
absolutely must be run from the tools/memory-model directory and from
this directory only:

herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus

The output is the result of something similar to a full state-space
search, and is as follows:

 1 Test MP+pooncerelease+poacquireonce Allowed
 2 States 3
 3 1:r0=0; 1:r1=0;
 4 1:r0=0; 1:r1=1;
 5 1:r0=1; 1:r1=1;
 6 No
 7 Witnesses
 8 Positive: 0 Negative: 3
 9 Condition exists (1:r0=1 /\ 1:r1=0)
10 Observation MP+pooncerelease+poacquireonce Never 0 3
11 Time MP+pooncerelease+poacquireonce 0.00
12 Hash=579aaa14d8c35a39429b02e698241d09

The most pertinent line is line 10, which contains "Never 0 3", which
indicates that the bad result flagged by the "exists" clause never
happens.  This line might instead say "Sometimes" to indicate that the
bad result happened in some but not all executions, or it might say
"Always" to indicate that the bad result happened in all executions.
(The herd7 tool doesn't judge, so it is only an LKMM convention that the
"exists" clause indicates a bad result.  To see this, invert the "exists"
clause's condition and run the test.)  The numbers ("0 3") at the end
of this line indicate the number of end states satisfying the "exists"
clause (0) and the number not not satisfying that clause (3).

Another important part of this output is shown in lines 2-5, repeated here:

 2 States 3
 3 1:r0=0; 1:r1=0;
 4 1:r0=0; 1:r1=1;
 5 1:r0=1; 1:r1=1;

Line 2 gives the total number of end states, and each of lines 3-5 list
one of these states, with the first ("1:r0=0; 1:r1=0;") indicating that
both of P1()'s loads returned the value "0".  As expected, given the
"Never" on line 10, the state flagged by the "exists" clause is not
listed.  This full list of states can be helpful when debugging a new
litmus test.

The rest of the output is not normally needed, either due to irrelevance
or due to being redundant with the lines discussed above.  However, the
following paragraph lists them for the benefit of readers possessed of
an insatiable curiosity.  Other readers should feel free to skip ahead.

Line 1 echos the test name, along with the "Test" and "Allowed".  Line 6's
"No" says that the "exists" clause was not satisfied by any execution,
and as such it has the same meaning as line 10's "Never".  Line 7 is a
lead-in to line 8's "Positive: 0 Negative: 3", which lists the number
of end states satisfying and not satisfying the "exists" clause, just
like the two numbers at the end of line 10.  Line 9 repeats the "exists"
clause so that you don't have to look it up in the litmus-test file.
The number at the end of line 11 (which begins with "Time") gives the
time in seconds required to analyze the litmus test.  Small tests such
as this one complete in a few milliseconds, so "0.00" is quite common.
Line 12 gives a hash of the contents for the litmus-test file, and is used
by tooling that manages litmus tests and their output.  This tooling is
used by people modifying LKMM itself, and among other things lets such
people know which of the several thousand relevant litmus tests were
affected by a given change to LKMM.


Initialization
--------------

The previous example relied on the default zero initialization for
"x" and "y", but a similar litmus test could instead initialize them
to some other value:

 1 C MP+pooncerelease+poacquireonce
 2
 3 {
 4   x=42;
 5   y=42;
 6 }
 7
 8 P0(int *x, int *y)
 9 {
10   WRITE_ONCE(*x, 1);
11   smp_store_release(y, 1);
12 }
13
14 P1(int *x, int *y)
15 {
16   int r0;
17   int r1;
18
19   r0 = smp_load_acquire(y);
20   r1 = READ_ONCE(*x);
21 }
22
23 exists (1:r0=1 /\ 1:r1=42)

Lines 3-6 now initialize both "x" and "y" to the value 42.  This also
means that the "exists" clause on line 23 must change "1:r1=0" to
"1:r1=42".

Running the test gives the same overall result as before, but with the
value 42 appearing in place of the value zero:

 1 Test MP+pooncerelease+poacquireonce Allowed
 2 States 3
 3 1:r0=1; 1:r1=1;
 4 1:r0=42; 1:r1=1;
 5 1:r0=42; 1:r1=42;
 6 No
 7 Witnesses
 8 Positive: 0 Negative: 3
 9 Condition exists (1:r0=1 /\ 1:r1=42)
10 Observation MP+pooncerelease+poacquireonce Never 0 3
11 Time MP+pooncerelease+poacquireonce 0.02
12 Hash=ab9a9b7940a75a792266be279a980156

It is tempting to avoid the open-coded repetitions of the value "42"
by defining another global variable "initval=42" and replacing all
occurrences of "42" with "initval".  This will not, repeat *not*,
initialize "x" and "y" to 42, but instead to the address of "initval"
(try it!).  See the section below on linked lists to learn more about
why this approach to initialization can be useful.


Control Structures
------------------

LKMM supports the C-language "if" statement, which allows modeling of
conditional branches.  In LKMM, conditional branches can affect ordering,
but only if you are *very* careful (compilers are surprisingly able
to optimize away conditional branches).  The following example shows
the "load buffering" (LB) use case that is used in the Linux kernel to
synchronize between ring-buffer producers and consumers.  In the example
below, P0() is one side checking to see if an operation may proceed and
P1() is the other side completing its update.

 1 C LB+fencembonceonce+ctrlonceonce
 2
 3 {}
 4
 5 P0(int *x, int *y)
 6 {
 7   int r0;
 8
 9   r0 = READ_ONCE(*x);
10   if (r0)
11     WRITE_ONCE(*y, 1);
12 }
13
14 P1(int *x, int *y)
15 {
16   int r0;
17
18   r0 = READ_ONCE(*y);
19   smp_mb();
20   WRITE_ONCE(*x, 1);
21 }
22
23 exists (0:r0=1 /\ 1:r0=1)

P1()'s "if" statement on line 10 works as expected, so that line 11 is
executed only if line 9 loads a non-zero value from "x".  Because P1()'s
write of "1" to "x" happens only after P1()'s read from "y", one would
hope that the "exists" clause cannot be satisfied.  LKMM agrees:

 1 Test LB+fencembonceonce+ctrlonceonce Allowed
 2 States 2
 3 0:r0=0; 1:r0=0;
 4 0:r0=1; 1:r0=0;
 5 No
 6 Witnesses
 7 Positive: 0 Negative: 2
 8 Condition exists (0:r0=1 /\ 1:r0=1)
 9 Observation LB+fencembonceonce+ctrlonceonce Never 0 2
10 Time LB+fencembonceonce+ctrlonceonce 0.00
11 Hash=e5260556f6de495fd39b556d1b831c3b

However, there is no "while" statement due to the fact that full
state-space search has some difficulty with iteration.  However, there
are tricks that may be used to handle some special cases, which are
discussed below.  In addition, loop-unrolling tricks may be applied,
albeit sparingly.


Tricks and Traps
================

This section covers extracting debug output from herd7, emulating
spin loops, handling trivial linked lists, adding comments to litmus tests,
emulating call_rcu(), and finally tricks to improve herd7 performance
in order to better handle large litmus tests.


Debug Output
------------

By default, the herd7 state output includes all variables mentioned
in the "exists" clause.  But sometimes debugging efforts are greatly
aided by the values of other variables.  Consider this litmus test
(tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
slightly modified), which probes an obscure corner of hardware memory
ordering:

 1 C SB+rfionceonce-poonceonces
 2
 3 {}
 4
 5 P0(int *x, int *y)
 6 {
 7   int r1;
 8   int r2;
 9
10   WRITE_ONCE(*x, 1);
11   r1 = READ_ONCE(*x);
12   r2 = READ_ONCE(*y);
13 }
14
15 P1(int *x, int *y)
16 {
17   int r3;
18   int r4;
19
20   WRITE_ONCE(*y, 1);
21   r3 = READ_ONCE(*y);
22   r4 = READ_ONCE(*x);
23 }
24
25 exists (0:r2=0 /\ 1:r4=0)

The herd7 output is as follows:

 1 Test SB+rfionceonce-poonceonces Allowed
 2 States 4
 3 0:r2=0; 1:r4=0;
 4 0:r2=0; 1:r4=1;
 5 0:r2=1; 1:r4=0;
 6 0:r2=1; 1:r4=1;
 7 Ok
 8 Witnesses
 9 Positive: 1 Negative: 3
10 Condition exists (0:r2=0 /\ 1:r4=0)
11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
12 Time SB+rfionceonce-poonceonces 0.01
13 Hash=c7f30fe0faebb7d565405d55b7318ada

(This output indicates that CPUs are permitted to "snoop their own
store buffers", which all of Linux's CPU families other than s390 will
happily do.  Such snooping results in disagreement among CPUs on the
order of stores from different CPUs, which is rarely an issue.)

But the herd7 output shows only the two variables mentioned in the
"exists" clause.  Someone modifying this test might wish to know the
values of "x", "y", "0:r1", and "0:r3" as well.  The "locations"
statement on line 25 shows how to cause herd7 to display additional
variables:

 1 C SB+rfionceonce-poonceonces
 2
 3 {}
 4
 5 P0(int *x, int *y)
 6 {
 7   int r1;
 8   int r2;
 9
10   WRITE_ONCE(*x, 1);
11   r1 = READ_ONCE(*x);
12   r2 = READ_ONCE(*y);
13 }
14
15 P1(int *x, int *y)
16 {
17   int r3;
18   int r4;
19
20   WRITE_ONCE(*y, 1);
21   r3 = READ_ONCE(*y);
22   r4 = READ_ONCE(*x);
23 }
24
25 locations [0:r1; 1:r3; x; y]
26 exists (0:r2=0 /\ 1:r4=0)

The herd7 output then displays the values of all the variables:

 1 Test SB+rfionceonce-poonceonces Allowed
 2 States 4
 3 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=0; x=1; y=1;
 4 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=1; x=1; y=1;
 5 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=0; x=1; y=1;
 6 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=1; x=1; y=1;
 7 Ok
 8 Witnesses
 9 Positive: 1 Negative: 3
10 Condition exists (0:r2=0 /\ 1:r4=0)
11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
12 Time SB+rfionceonce-poonceonces 0.01
13 Hash=40de8418c4b395388f6501cafd1ed38d

What if you would like to know the value of a particular global variable
at some particular point in a given process's execution?  One approach
is to use a READ_ONCE() to load that global variable into a new local
variable, then add that local variable to the "locations" clause.
But be careful:  In some litmus tests, adding a READ_ONCE() will change
the outcome!  For one example, please see the C-READ_ONCE.litmus and
C-READ_ONCE-omitted.litmus tests located here:

	https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/


Spin Loops
----------

The analysis carried out by herd7 explores full state space, which is
at best of exponential time complexity.  Adding processes and increasing
the amount of code in a give process can greatly increase execution time.
Potentially infinite loops, such as those used to wait for locks to
become available, are clearly problematic.

Fortunately, it is possible to avoid state-space explosion by specially
modeling such loops.  For example, the following litmus tests emulates
locking using xchg_acquire(), but instead of enclosing xchg_acquire()
in a spin loop, it instead excludes executions that fail to acquire the
lock using a herd7 "filter" clause.  Note that for exclusive locking, you
are better off using the spin_