^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1) Linux-Kernel Memory Model Litmus Tests
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 2) ======================================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 3)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 4) This file describes the LKMM litmus-test format by example, describes
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 5) some tricks and traps, and finally outlines LKMM's limitations. Earlier
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 6) versions of this material appeared in a number of LWN articles, including:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 7)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 8) https://lwn.net/Articles/720550/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 9) A formal kernel memory-ordering model (part 2)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 10) https://lwn.net/Articles/608550/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 11) Axiomatic validation of memory barriers and atomic instructions
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 12) https://lwn.net/Articles/470681/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 13) Validating Memory Barriers and Atomic Instructions
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 14)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 15) This document presents information in decreasing order of applicability,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 16) so that, where possible, the information that has proven more commonly
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 17) useful is shown near the beginning.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 18)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 19) For information on installing LKMM, including the underlying "herd7"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 20) tool, please see tools/memory-model/README.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 21)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 22)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 23) Copy-Pasta
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 24) ==========
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 25)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 26) As with other software, it is often better (if less macho) to adapt an
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 27) existing litmus test than it is to create one from scratch. A number
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 28) of litmus tests may be found in the kernel source tree:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 29)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 30) tools/memory-model/litmus-tests/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 31) Documentation/litmus-tests/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 32)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 33) Several thousand more example litmus tests are available on github
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 34) and kernel.org:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 35)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 36) https://github.com/paulmckrcu/litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 37) https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 38) https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 39)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 40) The -l and -L arguments to "git grep" can be quite helpful in identifying
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 41) existing litmus tests that are similar to the one you need. But even if
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 42) you start with an existing litmus test, it is still helpful to have a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 43) good understanding of the litmus-test format.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 44)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 45)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 46) Examples and Format
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 47) ===================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 48)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 49) This section describes the overall format of litmus tests, starting
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 50) with a small example of the message-passing pattern and moving on to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 51) more complex examples that illustrate explicit initialization and LKMM's
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 52) minimalistic set of flow-control statements.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 53)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 54)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 55) Message-Passing Example
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 56) -----------------------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 57)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 58) This section gives an overview of the format of a litmus test using an
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 59) example based on the common message-passing use case. This use case
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 60) appears often in the Linux kernel. For example, a flag (modeled by "y"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 61) below) indicates that a buffer (modeled by "x" below) is now completely
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 62) filled in and ready for use. It would be very bad if the consumer saw the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 63) flag set, but, due to memory misordering, saw old values in the buffer.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 64)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 65) This example asks whether smp_store_release() and smp_load_acquire()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 66) suffices to avoid this bad outcome:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 67)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 68) 1 C MP+pooncerelease+poacquireonce
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 69) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 70) 3 {}
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 71) 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 72) 5 P0(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 73) 6 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 74) 7 WRITE_ONCE(*x, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 75) 8 smp_store_release(y, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 76) 9 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 77) 10
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 78) 11 P1(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 79) 12 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 80) 13 int r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 81) 14 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 82) 15
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 83) 16 r0 = smp_load_acquire(y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 84) 17 r1 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 85) 18 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 86) 19
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 87) 20 exists (1:r0=1 /\ 1:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 88)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 89) Line 1 starts with "C", which identifies this file as being in the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 90) LKMM C-language format (which, as we will see, is a small fragment
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 91) of the full C language). The remainder of line 1 is the name of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 92) the test, which by convention is the filename with the ".litmus"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 93) suffix stripped. In this case, the actual test may be found in
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 94) tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 95) in the Linux-kernel source tree.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 96)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 97) Mechanically generated litmus tests will often have an optional
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 98) double-quoted comment string on the second line. Such strings are ignored
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 99) when running the test. Yes, you can add your own comments to litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 100) tests, but this is a bit involved due to the use of multiple parsers.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 101) For now, you can use C-language comments in the C code, and these comments
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 102) may be in either the "/* */" or the "//" style. A later section will
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 103) cover the full litmus-test commenting story.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 104)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 105) Line 3 is the initialization section. Because the default initialization
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 106) to zero suffices for this test, the "{}" syntax is used, which mean the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 107) initialization section is empty. Litmus tests requiring non-default
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 108) initialization must have non-empty initialization sections, as in the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 109) example that will be presented later in this document.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 110)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 111) Lines 5-9 show the first process and lines 11-18 the second process. Each
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 112) process corresponds to a Linux-kernel task (or kthread, workqueue, thread,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 113) and so on; LKMM discussions often use these terms interchangeably).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 114) The name of the first process is "P0" and that of the second "P1".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 115) You can name your processes anything you like as long as the names consist
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 116) of a single "P" followed by a number, and as long as the numbers are
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 117) consecutive starting with zero. This can actually be quite helpful,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 118) for example, a .litmus file matching "^P1(" but not matching "^P2("
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 119) must contain a two-process litmus test.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 120)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 121) The argument list for each function are pointers to the global variables
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 122) used by that function. Unlike normal C-language function parameters, the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 123) names are significant. The fact that both P0() and P1() have a formal
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 124) parameter named "x" means that these two processes are working with the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 125) same global variable, also named "x". So the "int *x, int *y" on P0()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 126) and P1() mean that both processes are working with two shared global
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 127) variables, "x" and "y". Global variables are always passed to processes
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 128) by reference, hence "P0(int *x, int *y)", but *never* "P0(int x, int y)".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 129)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 130) P0() has no local variables, but P1() has two of them named "r0" and "r1".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 131) These names may be freely chosen, but for historical reasons stemming from
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 132) other litmus-test formats, it is conventional to use names consisting of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 133) "r" followed by a number as shown here. A common bug in litmus tests
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 134) is forgetting to add a global variable to a process's parameter list.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 135) This will sometimes result in an error message, but can also cause the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 136) intended global to instead be silently treated as an undeclared local
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 137) variable.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 138)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 139) Each process's code is similar to Linux-kernel C, as can be seen on lines
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 140) 7-8 and 13-17. This code may use many of the Linux kernel's atomic
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 141) operations, some of its exclusive-lock functions, and some of its RCU
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 142) and SRCU functions. An approximate list of the currently supported
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 143) functions may be found in the linux-kernel.def file.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 144)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 145) The P0() process does "WRITE_ONCE(*x, 1)" on line 7. Because "x" is a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 146) pointer in P0()'s parameter list, this does an unordered store to global
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 147) variable "x". Line 8 does "smp_store_release(y, 1)", and because "y"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 148) is also in P0()'s parameter list, this does a release store to global
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 149) variable "y".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 150)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 151) The P1() process declares two local variables on lines 13 and 14.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 152) Line 16 does "r0 = smp_load_acquire(y)" which does an acquire load
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 153) from global variable "y" into local variable "r0". Line 17 does a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 154) "r1 = READ_ONCE(*x)", which does an unordered load from "*x" into local
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 155) variable "r1". Both "x" and "y" are in P1()'s parameter list, so both
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 156) reference the same global variables that are used by P0().
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 157)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 158) Line 20 is the "exists" assertion expression to evaluate the final state.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 159) This final state is evaluated after the dust has settled: both processes
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 160) have completed and all of their memory references and memory barriers
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 161) have propagated to all parts of the system. The references to the local
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 162) variables "r0" and "r1" in line 24 must be prefixed with "1:" to specify
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 163) which process they are local to.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 164)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 165) Note that the assertion expression is written in the litmus-test
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 166) language rather than in C. For example, single "=" is an equality
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 167) operator rather than an assignment. The "/\" character combination means
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 168) "and". Similarly, "\/" stands for "or". Both of these are ASCII-art
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 169) representations of the corresponding mathematical symbols. Finally,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 170) "~" stands for "logical not", which is "!" in C, and not to be confused
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 171) with the C-language "~" operator which instead stands for "bitwise not".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 172) Parentheses may be used to override precedence.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 173)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 174) The "exists" assertion on line 20 is satisfied if the consumer sees the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 175) flag ("y") set but the buffer ("x") as not yet filled in, that is, if P1()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 176) loaded a value from "x" that was equal to 1 but loaded a value from "y"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 177) that was still equal to zero.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 178)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 179) This example can be checked by running the following command, which
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 180) absolutely must be run from the tools/memory-model directory and from
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 181) this directory only:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 182)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 183) herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 184)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 185) The output is the result of something similar to a full state-space
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 186) search, and is as follows:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 187)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 188) 1 Test MP+pooncerelease+poacquireonce Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 189) 2 States 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 190) 3 1:r0=0; 1:r1=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 191) 4 1:r0=0; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 192) 5 1:r0=1; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 193) 6 No
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 194) 7 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 195) 8 Positive: 0 Negative: 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 196) 9 Condition exists (1:r0=1 /\ 1:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 197) 10 Observation MP+pooncerelease+poacquireonce Never 0 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 198) 11 Time MP+pooncerelease+poacquireonce 0.00
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 199) 12 Hash=579aaa14d8c35a39429b02e698241d09
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 200)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 201) The most pertinent line is line 10, which contains "Never 0 3", which
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 202) indicates that the bad result flagged by the "exists" clause never
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 203) happens. This line might instead say "Sometimes" to indicate that the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 204) bad result happened in some but not all executions, or it might say
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 205) "Always" to indicate that the bad result happened in all executions.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 206) (The herd7 tool doesn't judge, so it is only an LKMM convention that the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 207) "exists" clause indicates a bad result. To see this, invert the "exists"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 208) clause's condition and run the test.) The numbers ("0 3") at the end
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 209) of this line indicate the number of end states satisfying the "exists"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 210) clause (0) and the number not not satisfying that clause (3).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 211)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 212) Another important part of this output is shown in lines 2-5, repeated here:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 213)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 214) 2 States 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 215) 3 1:r0=0; 1:r1=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 216) 4 1:r0=0; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 217) 5 1:r0=1; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 218)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 219) Line 2 gives the total number of end states, and each of lines 3-5 list
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 220) one of these states, with the first ("1:r0=0; 1:r1=0;") indicating that
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 221) both of P1()'s loads returned the value "0". As expected, given the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 222) "Never" on line 10, the state flagged by the "exists" clause is not
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 223) listed. This full list of states can be helpful when debugging a new
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 224) litmus test.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 225)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 226) The rest of the output is not normally needed, either due to irrelevance
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 227) or due to being redundant with the lines discussed above. However, the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 228) following paragraph lists them for the benefit of readers possessed of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 229) an insatiable curiosity. Other readers should feel free to skip ahead.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 230)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 231) Line 1 echos the test name, along with the "Test" and "Allowed". Line 6's
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 232) "No" says that the "exists" clause was not satisfied by any execution,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 233) and as such it has the same meaning as line 10's "Never". Line 7 is a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 234) lead-in to line 8's "Positive: 0 Negative: 3", which lists the number
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 235) of end states satisfying and not satisfying the "exists" clause, just
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 236) like the two numbers at the end of line 10. Line 9 repeats the "exists"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 237) clause so that you don't have to look it up in the litmus-test file.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 238) The number at the end of line 11 (which begins with "Time") gives the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 239) time in seconds required to analyze the litmus test. Small tests such
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 240) as this one complete in a few milliseconds, so "0.00" is quite common.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 241) Line 12 gives a hash of the contents for the litmus-test file, and is used
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 242) by tooling that manages litmus tests and their output. This tooling is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 243) used by people modifying LKMM itself, and among other things lets such
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 244) people know which of the several thousand relevant litmus tests were
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 245) affected by a given change to LKMM.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 246)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 247)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 248) Initialization
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 249) --------------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 250)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 251) The previous example relied on the default zero initialization for
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 252) "x" and "y", but a similar litmus test could instead initialize them
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 253) to some other value:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 254)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 255) 1 C MP+pooncerelease+poacquireonce
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 256) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 257) 3 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 258) 4 x=42;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 259) 5 y=42;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 260) 6 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 261) 7
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 262) 8 P0(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 263) 9 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 264) 10 WRITE_ONCE(*x, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 265) 11 smp_store_release(y, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 266) 12 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 267) 13
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 268) 14 P1(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 269) 15 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 270) 16 int r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 271) 17 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 272) 18
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 273) 19 r0 = smp_load_acquire(y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 274) 20 r1 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 275) 21 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 276) 22
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 277) 23 exists (1:r0=1 /\ 1:r1=42)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 278)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 279) Lines 3-6 now initialize both "x" and "y" to the value 42. This also
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 280) means that the "exists" clause on line 23 must change "1:r1=0" to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 281) "1:r1=42".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 282)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 283) Running the test gives the same overall result as before, but with the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 284) value 42 appearing in place of the value zero:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 285)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 286) 1 Test MP+pooncerelease+poacquireonce Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 287) 2 States 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 288) 3 1:r0=1; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 289) 4 1:r0=42; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 290) 5 1:r0=42; 1:r1=42;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 291) 6 No
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 292) 7 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 293) 8 Positive: 0 Negative: 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 294) 9 Condition exists (1:r0=1 /\ 1:r1=42)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 295) 10 Observation MP+pooncerelease+poacquireonce Never 0 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 296) 11 Time MP+pooncerelease+poacquireonce 0.02
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 297) 12 Hash=ab9a9b7940a75a792266be279a980156
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 298)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 299) It is tempting to avoid the open-coded repetitions of the value "42"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 300) by defining another global variable "initval=42" and replacing all
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 301) occurrences of "42" with "initval". This will not, repeat *not*,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 302) initialize "x" and "y" to 42, but instead to the address of "initval"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 303) (try it!). See the section below on linked lists to learn more about
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 304) why this approach to initialization can be useful.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 305)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 306)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 307) Control Structures
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 308) ------------------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 309)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 310) LKMM supports the C-language "if" statement, which allows modeling of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 311) conditional branches. In LKMM, conditional branches can affect ordering,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 312) but only if you are *very* careful (compilers are surprisingly able
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 313) to optimize away conditional branches). The following example shows
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 314) the "load buffering" (LB) use case that is used in the Linux kernel to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 315) synchronize between ring-buffer producers and consumers. In the example
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 316) below, P0() is one side checking to see if an operation may proceed and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 317) P1() is the other side completing its update.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 318)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 319) 1 C LB+fencembonceonce+ctrlonceonce
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 320) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 321) 3 {}
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 322) 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 323) 5 P0(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 324) 6 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 325) 7 int r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 326) 8
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 327) 9 r0 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 328) 10 if (r0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 329) 11 WRITE_ONCE(*y, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 330) 12 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 331) 13
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 332) 14 P1(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 333) 15 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 334) 16 int r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 335) 17
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 336) 18 r0 = READ_ONCE(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 337) 19 smp_mb();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 338) 20 WRITE_ONCE(*x, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 339) 21 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 340) 22
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 341) 23 exists (0:r0=1 /\ 1:r0=1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 342)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 343) P1()'s "if" statement on line 10 works as expected, so that line 11 is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 344) executed only if line 9 loads a non-zero value from "x". Because P1()'s
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 345) write of "1" to "x" happens only after P1()'s read from "y", one would
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 346) hope that the "exists" clause cannot be satisfied. LKMM agrees:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 347)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 348) 1 Test LB+fencembonceonce+ctrlonceonce Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 349) 2 States 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 350) 3 0:r0=0; 1:r0=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 351) 4 0:r0=1; 1:r0=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 352) 5 No
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 353) 6 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 354) 7 Positive: 0 Negative: 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 355) 8 Condition exists (0:r0=1 /\ 1:r0=1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 356) 9 Observation LB+fencembonceonce+ctrlonceonce Never 0 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 357) 10 Time LB+fencembonceonce+ctrlonceonce 0.00
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 358) 11 Hash=e5260556f6de495fd39b556d1b831c3b
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 359)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 360) However, there is no "while" statement due to the fact that full
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 361) state-space search has some difficulty with iteration. However, there
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 362) are tricks that may be used to handle some special cases, which are
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 363) discussed below. In addition, loop-unrolling tricks may be applied,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 364) albeit sparingly.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 365)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 366)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 367) Tricks and Traps
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 368) ================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 369)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 370) This section covers extracting debug output from herd7, emulating
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 371) spin loops, handling trivial linked lists, adding comments to litmus tests,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 372) emulating call_rcu(), and finally tricks to improve herd7 performance
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 373) in order to better handle large litmus tests.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 374)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 375)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 376) Debug Output
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 377) ------------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 378)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 379) By default, the herd7 state output includes all variables mentioned
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 380) in the "exists" clause. But sometimes debugging efforts are greatly
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 381) aided by the values of other variables. Consider this litmus test
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 382) (tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 383) slightly modified), which probes an obscure corner of hardware memory
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 384) ordering:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 385)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 386) 1 C SB+rfionceonce-poonceonces
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 387) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 388) 3 {}
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 389) 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 390) 5 P0(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 391) 6 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 392) 7 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 393) 8 int r2;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 394) 9
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 395) 10 WRITE_ONCE(*x, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 396) 11 r1 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 397) 12 r2 = READ_ONCE(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 398) 13 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 399) 14
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 400) 15 P1(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 401) 16 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 402) 17 int r3;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 403) 18 int r4;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 404) 19
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 405) 20 WRITE_ONCE(*y, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 406) 21 r3 = READ_ONCE(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 407) 22 r4 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 408) 23 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 409) 24
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 410) 25 exists (0:r2=0 /\ 1:r4=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 411)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 412) The herd7 output is as follows:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 413)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 414) 1 Test SB+rfionceonce-poonceonces Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 415) 2 States 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 416) 3 0:r2=0; 1:r4=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 417) 4 0:r2=0; 1:r4=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 418) 5 0:r2=1; 1:r4=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 419) 6 0:r2=1; 1:r4=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 420) 7 Ok
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 421) 8 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 422) 9 Positive: 1 Negative: 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 423) 10 Condition exists (0:r2=0 /\ 1:r4=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 424) 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 425) 12 Time SB+rfionceonce-poonceonces 0.01
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 426) 13 Hash=c7f30fe0faebb7d565405d55b7318ada
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 427)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 428) (This output indicates that CPUs are permitted to "snoop their own
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 429) store buffers", which all of Linux's CPU families other than s390 will
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 430) happily do. Such snooping results in disagreement among CPUs on the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 431) order of stores from different CPUs, which is rarely an issue.)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 432)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 433) But the herd7 output shows only the two variables mentioned in the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 434) "exists" clause. Someone modifying this test might wish to know the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 435) values of "x", "y", "0:r1", and "0:r3" as well. The "locations"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 436) statement on line 25 shows how to cause herd7 to display additional
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 437) variables:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 438)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 439) 1 C SB+rfionceonce-poonceonces
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 440) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 441) 3 {}
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 442) 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 443) 5 P0(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 444) 6 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 445) 7 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 446) 8 int r2;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 447) 9
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 448) 10 WRITE_ONCE(*x, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 449) 11 r1 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 450) 12 r2 = READ_ONCE(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 451) 13 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 452) 14
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 453) 15 P1(int *x, int *y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 454) 16 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 455) 17 int r3;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 456) 18 int r4;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 457) 19
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 458) 20 WRITE_ONCE(*y, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 459) 21 r3 = READ_ONCE(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 460) 22 r4 = READ_ONCE(*x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 461) 23 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 462) 24
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 463) 25 locations [0:r1; 1:r3; x; y]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 464) 26 exists (0:r2=0 /\ 1:r4=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 465)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 466) The herd7 output then displays the values of all the variables:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 467)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 468) 1 Test SB+rfionceonce-poonceonces Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 469) 2 States 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 470) 3 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=0; x=1; y=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 471) 4 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=1; x=1; y=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 472) 5 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=0; x=1; y=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 473) 6 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=1; x=1; y=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 474) 7 Ok
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 475) 8 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 476) 9 Positive: 1 Negative: 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 477) 10 Condition exists (0:r2=0 /\ 1:r4=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 478) 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 479) 12 Time SB+rfionceonce-poonceonces 0.01
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 480) 13 Hash=40de8418c4b395388f6501cafd1ed38d
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 481)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 482) What if you would like to know the value of a particular global variable
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 483) at some particular point in a given process's execution? One approach
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 484) is to use a READ_ONCE() to load that global variable into a new local
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 485) variable, then add that local variable to the "locations" clause.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 486) But be careful: In some litmus tests, adding a READ_ONCE() will change
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 487) the outcome! For one example, please see the C-READ_ONCE.litmus and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 488) C-READ_ONCE-omitted.litmus tests located here:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 489)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 490) https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 491)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 492)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 493) Spin Loops
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 494) ----------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 495)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 496) The analysis carried out by herd7 explores full state space, which is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 497) at best of exponential time complexity. Adding processes and increasing
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 498) the amount of code in a give process can greatly increase execution time.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 499) Potentially infinite loops, such as those used to wait for locks to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 500) become available, are clearly problematic.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 501)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 502) Fortunately, it is possible to avoid state-space explosion by specially
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 503) modeling such loops. For example, the following litmus tests emulates
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 504) locking using xchg_acquire(), but instead of enclosing xchg_acquire()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 505) in a spin loop, it instead excludes executions that fail to acquire the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 506) lock using a herd7 "filter" clause. Note that for exclusive locking, you
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 507) are better off using the spin_lock() and spin_unlock() that LKMM directly
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 508) models, if for no other reason that these are much faster. However, the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 509) techniques illustrated in this section can be used for other purposes,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 510) such as emulating reader-writer locking, which LKMM does not yet model.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 511)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 512) 1 C C-SB+l-o-o-u+l-o-o-u-X
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 513) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 514) 3 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 515) 4 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 516) 5
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 517) 6 P0(int *sl, int *x0, int *x1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 518) 7 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 519) 8 int r2;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 520) 9 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 521) 10
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 522) 11 r2 = xchg_acquire(sl, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 523) 12 WRITE_ONCE(*x0, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 524) 13 r1 = READ_ONCE(*x1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 525) 14 smp_store_release(sl, 0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 526) 15 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 527) 16
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 528) 17 P1(int *sl, int *x0, int *x1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 529) 18 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 530) 19 int r2;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 531) 20 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 532) 21
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 533) 22 r2 = xchg_acquire(sl, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 534) 23 WRITE_ONCE(*x1, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 535) 24 r1 = READ_ONCE(*x0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 536) 25 smp_store_release(sl, 0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 537) 26 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 538) 27
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 539) 28 filter (0:r2=0 /\ 1:r2=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 540) 29 exists (0:r1=0 /\ 1:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 541)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 542) This litmus test may be found here:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 543)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 544) https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 545)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 546) This test uses two global variables, "x1" and "x2", and also emulates a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 547) single global spinlock named "sl". This spinlock is held by whichever
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 548) process changes the value of "sl" from "0" to "1", and is released when
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 549) that process sets "sl" back to "0". P0()'s lock acquisition is emulated
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 550) on line 11 using xchg_acquire(), which unconditionally stores the value
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 551) "1" to "sl" and stores either "0" or "1" to "r2", depending on whether
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 552) the lock acquisition was successful or unsuccessful (due to "sl" already
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 553) having the value "1"), respectively. P1() operates in a similar manner.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 554)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 555) Rather unconventionally, execution appears to proceed to the critical
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 556) section on lines 12 and 13 in either case. Line 14 then uses an
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 557) smp_store_release() to store zero to "sl", thus emulating lock release.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 558)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 559) The case where xchg_acquire() fails to acquire the lock is handled by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 560) the "filter" clause on line 28, which tells herd7 to keep only those
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 561) executions in which both "0:r2" and "1:r2" are zero, that is to pay
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 562) attention only to those executions in which both locks are actually
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 563) acquired. Thus, the bogus executions that would execute the critical
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 564) sections are discarded and any effects that they might have had are
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 565) ignored. Note well that the "filter" clause keeps those executions
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 566) for which its expression is satisfied, that is, for which the expression
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 567) evaluates to true. In other words, the "filter" clause says what to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 568) keep, not what to discard.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 569)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 570) The result of running this test is as follows:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 571)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 572) 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 573) 2 States 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 574) 3 0:r1=0; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 575) 4 0:r1=1; 1:r1=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 576) 5 No
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 577) 6 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 578) 7 Positive: 0 Negative: 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 579) 8 Condition exists (0:r1=0 /\ 1:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 580) 9 Observation C-SB+l-o-o-u+l-o-o-u-X Never 0 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 581) 10 Time C-SB+l-o-o-u+l-o-o-u-X 0.03
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 582)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 583) The "Never" on line 9 indicates that this use of xchg_acquire() and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 584) smp_store_release() really does correctly emulate locking.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 585)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 586) Why doesn't the litmus test take the simpler approach of using a spin loop
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 587) to handle failed spinlock acquisitions, like the kernel does? The key
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 588) insight behind this litmus test is that spin loops have no effect on the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 589) possible "exists"-clause outcomes of program execution in the absence
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 590) of deadlock. In other words, given a high-quality lock-acquisition
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 591) primitive in a deadlock-free program running on high-quality hardware,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 592) each lock acquisition will eventually succeed. Because herd7 already
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 593) explores the full state space, the length of time required to actually
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 594) acquire the lock does not matter. After all, herd7 already models all
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 595) possible durations of the xchg_acquire() statements.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 596)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 597) Why not just add the "filter" clause to the "exists" clause, thus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 598) avoiding the "filter" clause entirely? This does work, but is slower.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 599) The reason that the "filter" clause is faster is that (in the common case)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 600) herd7 knows to abandon an execution as soon as the "filter" expression
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 601) fails to be satisfied. In contrast, the "exists" clause is evaluated
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 602) only at the end of time, thus requiring herd7 to waste time on bogus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 603) executions in which both critical sections proceed concurrently. In
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 604) addition, some LKMM users like the separation of concerns provided by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 605) using the both the "filter" and "exists" clauses.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 606)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 607) Readers lacking a pathological interest in odd corner cases should feel
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 608) free to skip the remainder of this section.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 609)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 610) But what if the litmus test were to temporarily set "0:r2" to a non-zero
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 611) value? Wouldn't that cause herd7 to abandon the execution prematurely
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 612) due to an early mismatch of the "filter" clause?
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 613)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 614) Why not just try it? Line 4 of the following modified litmus test
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 615) introduces a new global variable "x2" that is initialized to "1". Line 23
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 616) of P1() reads that variable into "1:r2" to force an early mismatch with
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 617) the "filter" clause. Line 24 does a known-true "if" condition to avoid
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 618) and static analysis that herd7 might do. Finally the "exists" clause
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 619) on line 32 is updated to a condition that is alway satisfied at the end
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 620) of the test.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 621)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 622) 1 C C-SB+l-o-o-u+l-o-o-u-X
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 623) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 624) 3 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 625) 4 x2=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 626) 5 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 627) 6
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 628) 7 P0(int *sl, int *x0, int *x1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 629) 8 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 630) 9 int r2;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 631) 10 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 632) 11
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 633) 12 r2 = xchg_acquire(sl, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 634) 13 WRITE_ONCE(*x0, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 635) 14 r1 = READ_ONCE(*x1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 636) 15 smp_store_release(sl, 0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 637) 16 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 638) 17
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 639) 18 P1(int *sl, int *x0, int *x1, int *x2)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 640) 19 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 641) 20 int r2;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 642) 21 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 643) 22
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 644) 23 r2 = READ_ONCE(*x2);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 645) 24 if (r2)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 646) 25 r2 = xchg_acquire(sl, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 647) 26 WRITE_ONCE(*x1, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 648) 27 r1 = READ_ONCE(*x0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 649) 28 smp_store_release(sl, 0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 650) 29 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 651) 30
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 652) 31 filter (0:r2=0 /\ 1:r2=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 653) 32 exists (x1=1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 654)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 655) If the "filter" clause were to check each variable at each point in the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 656) execution, running this litmus test would display no executions because
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 657) all executions would be filtered out at line 23. However, the output
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 658) is instead as follows:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 659)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 660) 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 661) 2 States 1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 662) 3 x1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 663) 4 Ok
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 664) 5 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 665) 6 Positive: 2 Negative: 0
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 666) 7 Condition exists (x1=1)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 667) 8 Observation C-SB+l-o-o-u+l-o-o-u-X Always 2 0
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 668) 9 Time C-SB+l-o-o-u+l-o-o-u-X 0.04
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 669) 10 Hash=080bc508da7f291e122c6de76c0088e3
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 670)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 671) Line 3 shows that there is one execution that did not get filtered out,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 672) so the "filter" clause is evaluated only on the last assignment to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 673) the variables that it checks. In this case, the "filter" clause is a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 674) disjunction, so it might be evaluated twice, once at the final (and only)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 675) assignment to "0:r2" and once at the final assignment to "1:r2".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 676)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 677)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 678) Linked Lists
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 679) ------------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 680)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 681) LKMM can handle linked lists, but only linked lists in which each node
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 682) contains nothing except a pointer to the next node in the list. This is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 683) of course quite restrictive, but there is nevertheless quite a bit that
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 684) can be done within these confines, as can be seen in the litmus test
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 685) at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 686)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 687) 1 C MP+onceassign+derefonce
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 688) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 689) 3 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 690) 4 y=z;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 691) 5 z=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 692) 6 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 693) 7
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 694) 8 P0(int *x, int **y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 695) 9 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 696) 10 WRITE_ONCE(*x, 1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 697) 11 rcu_assign_pointer(*y, x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 698) 12 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 699) 13
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 700) 14 P1(int *x, int **y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 701) 15 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 702) 16 int *r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 703) 17 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 704) 18
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 705) 19 rcu_read_lock();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 706) 20 r0 = rcu_dereference(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 707) 21 r1 = READ_ONCE(*r0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 708) 22 rcu_read_unlock();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 709) 23 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 710) 24
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 711) 25 exists (1:r0=x /\ 1:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 712)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 713) Line 4's "y=z" may seem odd, given that "z" has not yet been initialized.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 714) But "y=z" does not set the value of "y" to that of "z", but instead
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 715) sets the value of "y" to the *address* of "z". Lines 4 and 5 therefore
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 716) create a simple linked list, with "y" pointing to "z" and "z" having a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 717) NULL pointer. A much longer linked list could be created if desired,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 718) and circular singly linked lists can also be created and manipulated.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 719)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 720) The "exists" clause works the same way, with the "1:r0=x" comparing P1()'s
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 721) "r0" not to the value of "x", but again to its address. This term of the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 722) "exists" clause therefore tests whether line 20's load from "y" saw the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 723) value stored by line 11, which is in fact what is required in this case.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 724)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 725) P0()'s line 10 initializes "x" to the value 1 then line 11 links to "x"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 726) from "y", replacing "z".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 727)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 728) P1()'s line 20 loads a pointer from "y", and line 21 dereferences that
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 729) pointer. The RCU read-side critical section spanning lines 19-22 is just
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 730) for show in this example. Note that the address used for line 21's load
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 731) depends on (in this case, "is exactly the same as") the value loaded by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 732) line 20. This is an example of what is called an "address dependency".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 733) This particular address dependency extends from the load on line 20 to the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 734) load on line 21. Address dependencies provide a weak form of ordering.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 735)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 736) Running this test results in the following:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 737)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 738) 1 Test MP+onceassign+derefonce Allowed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 739) 2 States 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 740) 3 1:r0=x; 1:r1=1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 741) 4 1:r0=z; 1:r1=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 742) 5 No
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 743) 6 Witnesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 744) 7 Positive: 0 Negative: 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 745) 8 Condition exists (1:r0=x /\ 1:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 746) 9 Observation MP+onceassign+derefonce Never 0 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 747) 10 Time MP+onceassign+derefonce 0.00
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 748) 11 Hash=49ef7a741563570102448a256a0c8568
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 749)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 750) The only possible outcomes feature P1() loading a pointer to "z"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 751) (which contains zero) on the one hand and P1() loading a pointer to "x"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 752) (which contains the value one) on the other. This should be reassuring
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 753) because it says that RCU readers cannot see the old preinitialization
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 754) values when accessing a newly inserted list node. This undesirable
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 755) scenario is flagged by the "exists" clause, and would occur if P1()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 756) loaded a pointer to "x", but obtained the pre-initialization value of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 757) zero after dereferencing that pointer.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 758)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 759)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 760) Comments
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 761) --------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 762)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 763) Different portions of a litmus test are processed by different parsers,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 764) which has the charming effect of requiring different comment syntax in
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 765) different portions of the litmus test. The C-syntax portions use
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 766) C-language comments (either "/* */" or "//"), while the other portions
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 767) use Ocaml comments "(* *)".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 768)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 769) The following litmus test illustrates the comment style corresponding
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 770) to each syntactic unit of the test:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 771)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 772) 1 C MP+onceassign+derefonce (* A *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 773) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 774) 3 (* B *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 775) 4
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 776) 5 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 777) 6 y=z; (* C *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 778) 7 z=0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 779) 8 } // D
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 780) 9
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 781) 10 // E
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 782) 11
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 783) 12 P0(int *x, int **y) // F
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 784) 13 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 785) 14 WRITE_ONCE(*x, 1); // G
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 786) 15 rcu_assign_pointer(*y, x);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 787) 16 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 788) 17
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 789) 18 // H
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 790) 19
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 791) 20 P1(int *x, int **y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 792) 21 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 793) 22 int *r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 794) 23 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 795) 24
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 796) 25 rcu_read_lock();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 797) 26 r0 = rcu_dereference(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 798) 27 r1 = READ_ONCE(*r0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 799) 28 rcu_read_unlock();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 800) 29 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 801) 30
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 802) 31 // I
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 803) 32
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 804) 33 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) (* L *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 805)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 806) In short, use C-language comments in the C code and Ocaml comments in
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 807) the rest of the litmus test.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 808)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 809) On the other hand, if you prefer C-style comments everywhere, the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 810) C preprocessor is your friend.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 811)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 812)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 813) Asynchronous RCU Grace Periods
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 814) ------------------------------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 815)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 816) The following litmus test is derived from the example show in
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 817) Documentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 818) emulate call_rcu():
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 819)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 820) 1 C RCU+sync+free
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 821) 2
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 822) 3 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 823) 4 int x = 1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 824) 5 int *y = &x;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 825) 6 int z = 1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 826) 7 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 827) 8
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 828) 9 P0(int *x, int *z, int **y)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 829) 10 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 830) 11 int *r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 831) 12 int r1;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 832) 13
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 833) 14 rcu_read_lock();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 834) 15 r0 = rcu_dereference(*y);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 835) 16 r1 = READ_ONCE(*r0);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 836) 17 rcu_read_unlock();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 837) 18 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 838) 19
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 839) 20 P1(int *z, int **y, int *c)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 840) 21 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 841) 22 rcu_assign_pointer(*y, z);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 842) 23 smp_store_release(*c, 1); // Emulate call_rcu().
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 843) 24 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 844) 25
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 845) 26 P2(int *x, int *z, int **y, int *c)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 846) 27 {
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 847) 28 int r0;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 848) 29
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 849) 30 r0 = smp_load_acquire(*c); // Note call_rcu() request.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 850) 31 synchronize_rcu(); // Wait one grace period.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 851) 32 WRITE_ONCE(*x, 0); // Emulate the RCU callback.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 852) 33 }
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 853) 34
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 854) 35 filter (2:r0=1) (* Reject too-early starts. *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 855) 36 exists (0:r0=x /\ 0:r1=0)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 856)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 857) Lines 4-6 initialize a linked list headed by "y" that initially contains
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 858) "x". In addition, "z" is pre-initialized to prepare for P1(), which
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 859) will replace "x" with "z" in this list.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 860)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 861) P0() on lines 9-18 enters an RCU read-side critical section, loads the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 862) list header "y" and dereferences it, leaving the node in "0:r0" and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 863) the node's value in "0:r1".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 864)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 865) P1() on lines 20-24 updates the list header to instead reference "z",
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 866) then emulates call_rcu() by doing a release store into "c".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 867)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 868) P2() on lines 27-33 emulates the behind-the-scenes effect of doing a
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 869) call_rcu(). Line 30 first does an acquire load from "c", then line 31
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 870) waits for an RCU grace period to elapse, and finally line 32 emulates
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 871) the RCU callback, which in turn emulates a call to kfree().
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 872)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 873) Of course, it is possible for P2() to start too soon, so that the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 874) value of "2:r0" is zero rather than the required value of "1".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 875) The "filter" clause on line 35 handles this possibility, rejecting
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 876) all executions in which "2:r0" is not equal to the value "1".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 877)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 878)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 879) Performance
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 880) -----------
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 881)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 882) LKMM's exploration of the full state-space can be extremely helpful,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 883) but it does not come for free. The price is exponential computational
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 884) complexity in terms of the number of processes, the average number
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 885) of statements in each process, and the total number of stores in the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 886) litmus test.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 887)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 888) So it is best to start small and then work up. Where possible, break
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 889) your code down into small pieces each representing a core concurrency
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 890) requirement.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 891)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 892) That said, herd7 is quite fast. On an unprepossessing x86 laptop, it
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 893) was able to analyze the following 10-process RCU litmus test in about
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 894) six seconds.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 895)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 896) https://github.com/paulmckrcu/litmus/blob/master/auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R.litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 897)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 898) One way to make herd7 run faster is to use the "-speedcheck true" option.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 899) This option prevents herd7 from generating all possible end states,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 900) instead causing it to focus solely on whether or not the "exists"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 901) clause can be satisfied. With this option, herd7 evaluates the above
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 902) litmus test in about 300 milliseconds, for more than an order of magnitude
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 903) improvement in performance.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 904)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 905) Larger 16-process litmus tests that would normally consume 15 minutes
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 906) of time complete in about 40 seconds with this option. To be fair,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 907) you do get an extra 65,535 states when you leave off the "-speedcheck
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 908) true" option.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 909)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 910) https://github.com/paulmckrcu/litmus/blob/master/auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R.litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 911)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 912) Nevertheless, litmus-test analysis really is of exponential complexity,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 913) whether with or without "-speedcheck true". Increasing by just three
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 914) processes to a 19-process litmus test requires 2 hours and 40 minutes
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 915) without, and about 8 minutes with "-speedcheck true". Each of these
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 916) results represent roughly an order of magnitude slowdown compared to the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 917) 16-process litmus test. Again, to be fair, the multi-hour run explores
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 918) no fewer than 524,287 additional states compared to the shorter one.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 919)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 920) https://github.com/paulmckrcu/litmus/blob/master/auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R+RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R.litmus
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 921)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 922) If you don't like command-line arguments, you can obtain a similar speedup
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 923) by adding a "filter" clause with exactly the same expression as your
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 924) "exists" clause.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 925)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 926) However, please note that seeing the full set of states can be extremely
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 927) helpful when developing and debugging litmus tests.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 928)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 929)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 930) LIMITATIONS
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 931) ===========
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 932)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 933) Limitations of the Linux-kernel memory model (LKMM) include:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 934)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 935) 1. Compiler optimizations are not accurately modeled. Of course,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 936) the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 937) ability to optimize, but under some circumstances it is possible
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 938) for the compiler to undermine the memory model. For more
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 939) information, see Documentation/explanation.txt (in particular,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 940) the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 941) sections).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 942)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 943) Note that this limitation in turn limits LKMM's ability to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 944) accurately model address, control, and data dependencies.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 945) For example, if the compiler can deduce the value of some variable
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 946) carrying a dependency, then the compiler can break that dependency
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 947) by substituting a constant of that value.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 948)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 949) 2. Multiple access sizes for a single variable are not supported,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 950) and neither are misaligned or partially overlapping accesses.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 951)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 952) 3. Exceptions and interrupts are not modeled. In some cases,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 953) this limitation can be overcome by modeling the interrupt or
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 954) exception with an additional process.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 955)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 956) 4. I/O such as MMIO or DMA is not supported.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 957)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 958) 5. Self-modifying code (such as that found in the kernel's
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 959) alternatives mechanism, function tracer, Berkeley Packet Filter
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 960) JIT compiler, and module loader) is not supported.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 961)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 962) 6. Complete modeling of all variants of atomic read-modify-write
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 963) operations, locking primitives, and RCU is not provided.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 964) For example, call_rcu() and rcu_barrier() are not supported.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 965) However, a substantial amount of support is provided for these
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 966) operations, as shown in the linux-kernel.def file.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 967)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 968) Here are specific limitations:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 969)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 970) a. When rcu_assign_pointer() is passed NULL, the Linux
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 971) kernel provides no ordering, but LKMM models this
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 972) case as a store release.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 973)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 974) b. The "unless" RMW operations are not currently modeled:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 975) atomic_long_add_unless(), atomic_inc_unless_negative(),
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 976) and atomic_dec_unless_positive(). These can be emulated
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 977) in litmus tests, for example, by using atomic_cmpxchg().
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 978)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 979) One exception of this limitation is atomic_add_unless(),
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 980) which is provided directly by herd7 (so no corresponding
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 981) definition in linux-kernel.def). atomic_add_unless() is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 982) modeled by herd7 therefore it can be used in litmus tests.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 983)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 984) c. The call_rcu() function is not modeled. As was shown above,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 985) it can be emulated in litmus tests by adding another
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 986) process that invokes synchronize_rcu() and the body of the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 987) callback function, with (for example) a release-acquire
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 988) from the site of the emulated call_rcu() to the beginning
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 989) of the additional process.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 990)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 991) d. The rcu_barrier() function is not modeled. It can be
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 992) emulated in litmus tests emulating call_rcu() via
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 993) (for example) a release-acquire from the end of each
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 994) additional call_rcu() process to the site of the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 995) emulated rcu-barrier().
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 996)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 997) e. Although sleepable RCU (SRCU) is now modeled, there
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 998) are some subtle differences between its semantics and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 999) those in the Linux kernel. For example, the kernel
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1000) might interpret the following sequence as two partially
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1001) overlapping SRCU read-side critical sections:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1002)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1003) 1 r1 = srcu_read_lock(&my_srcu);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1004) 2 do_something_1();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1005) 3 r2 = srcu_read_lock(&my_srcu);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1006) 4 do_something_2();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1007) 5 srcu_read_unlock(&my_srcu, r1);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1008) 6 do_something_3();
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1009) 7 srcu_read_unlock(&my_srcu, r2);
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1010)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1011) In contrast, LKMM will interpret this as a nested pair of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1012) SRCU read-side critical sections, with the outer critical
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1013) section spanning lines 1-7 and the inner critical section
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1014) spanning lines 3-5.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1015)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1016) This difference would be more of a concern had anyone
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1017) identified a reasonable use case for partially overlapping
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1018) SRCU read-side critical sections. For more information
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1019) on the trickiness of such overlapping, please see:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1020) https://paulmck.livejournal.com/40593.html
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1021)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1022) f. Reader-writer locking is not modeled. It can be
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1023) emulated in litmus tests using atomic read-modify-write
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1024) operations.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1025)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1026) The fragment of the C language supported by these litmus tests is quite
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1027) limited and in some ways non-standard:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1028)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1029) 1. There is no automatic C-preprocessor pass. You can of course
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1030) run it manually, if you choose.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1031)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1032) 2. There is no way to create functions other than the Pn() functions
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1033) that model the concurrent processes.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1034)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1035) 3. The Pn() functions' formal parameters must be pointers to the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1036) global shared variables. Nothing can be passed by value into
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1037) these functions.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1038)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1039) 4. The only functions that can be invoked are those built directly
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1040) into herd7 or that are defined in the linux-kernel.def file.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1041)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1042) 5. The "switch", "do", "for", "while", and "goto" C statements are
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1043) not supported. The "switch" statement can be emulated by the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1044) "if" statement. The "do", "for", and "while" statements can
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1045) often be emulated by manually unrolling the loop, or perhaps by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1046) enlisting the aid of the C preprocessor to minimize the resulting
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1047) code duplication. Some uses of "goto" can be emulated by "if",
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1048) and some others by unrolling.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1049)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1050) 6. Although you can use a wide variety of types in litmus-test
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1051) variable declarations, and especially in global-variable
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1052) declarations, the "herd7" tool understands only int and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1053) pointer types. There is no support for floating-point types,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1054) enumerations, characters, strings, arrays, or structures.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1055)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1056) 7. Parsing of variable declarations is very loose, with almost no
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1057) type checking.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1058)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1059) 8. Initializers differ from their C-language counterparts.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1060) For example, when an initializer contains the name of a shared
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1061) variable, that name denotes a pointer to that variable, not
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1062) the current value of that variable. For example, "int x = y"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1063) is interpreted the way "int x = &y" would be in C.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1064)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1065) 9. Dynamic memory allocation is not supported, although this can
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1066) be worked around in some cases by supplying multiple statically
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1067) allocated variables.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1068)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1069) Some of these limitations may be overcome in the future, but others are
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1070) more likely to be addressed by incorporating the Linux-kernel memory model
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1071) into other tools.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1072)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1073) Finally, please note that LKMM is subject to change as hardware, use cases,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1074) and compilers evolve.
Orange Pi5 kernel
Deprecated Linux kernel 5.10.110 for OrangePi 5/5B/5+ boards
3 Commits
0 Branches
0 Tags