Litmus Tests¶
Literal include oftools/memory-model/Documentation/litmus-tests.txt.
Linux-Kernel Memory Model Litmus Tests======================================This file describes the LKMM litmus-test format by example, describessome tricks and traps, and finally outlines LKMM's limitations. Earlierversions 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 instructionshttps://lwn.net/Articles/470681/ Validating Memory Barriers and Atomic InstructionsThis document presents information in decreasing order of applicability,so that, where possible, the information that has proven more commonlyuseful 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 anexisting litmus test than it is to create one from scratch. A numberof 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 githuband 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/litmusThe -l and -L arguments to "git grep" can be quite helpful in identifyingexisting litmus tests that are similar to the one you need. But even ifyou start with an existing litmus test, it is still helpful to have agood understanding of the litmus-test format.Examples and Format===================This section describes the overall format of litmus tests, startingwith a small example of the message-passing pattern and moving on tomore complex examples that illustrate explicit initialization and LKMM'sminimalistic set of flow-control statements.Message-Passing Example-----------------------This section gives an overview of the format of a litmus test using anexample based on the common message-passing use case. This use caseappears often in the Linux kernel. For example, a flag (modeled by "y"below) indicates that a buffer (modeled by "x" below) is now completelyfilled in and ready for use. It would be very bad if the consumer saw theflag 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 }1011 P1(int *x, int *y)12 {13 int r0;14 int r1;1516 r0 = smp_load_acquire(y);17 r1 = READ_ONCE(*x);18 }1920 exists (1:r0=1 /\ 1:r1=0)Line 1 starts with "C", which identifies this file as being in theLKMM C-language format (which, as we will see, is a small fragmentof the full C language). The remainder of line 1 is the name ofthe test, which by convention is the filename with the ".litmus"suffix stripped. In this case, the actual test may be found intools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmusin the Linux-kernel source tree.Mechanically generated litmus tests will often have an optionaldouble-quoted comment string on the second line. Such strings are ignoredwhen running the test. Yes, you can add your own comments to litmustests, 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 commentsmay be in either the "/* */" or the "//" style. A later section willcover the full litmus-test commenting story.Line 3 is the initialization section. Because the default initializationto zero suffices for this test, the "{}" syntax is used, which mean theinitialization section is empty. Litmus tests requiring non-defaultinitialization must have non-empty initialization sections, as in theexample that will be presented later in this document.Lines 5-9 show the first process and lines 11-18 the second process. Eachprocess 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 consistof a single "P" followed by a number, and as long as the numbers areconsecutive 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 variablesused by that function. Unlike normal C-language function parameters, thenames are significant. The fact that both P0() and P1() have a formalparameter named "x" means that these two processes are working with thesame global variable, also named "x". So the "int *x, int *y" on P0()and P1() mean that both processes are working with two shared globalvariables, "x" and "y". Global variables are always passed to processesby 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 fromother litmus-test formats, it is conventional to use names consisting of"r" followed by a number as shown here. A common bug in litmus testsis forgetting to add a global variable to a process's parameter list.This will sometimes result in an error message, but can also cause theintended global to instead be silently treated as an undeclared localvariable.Each process's code is similar to Linux-kernel C, as can be seen on lines7-8 and 13-17. This code may use many of the Linux kernel's atomicoperations, some of its exclusive-lock functions, and some of its RCUand SRCU functions. An approximate list of the currently supportedfunctions may be found in the linux-kernel.def file.The P0() process does "WRITE_ONCE(*x, 1)" on line 7. Because "x" is apointer in P0()'s parameter list, this does an unordered store to globalvariable "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 globalvariable "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 loadfrom global variable "y" into local variable "r0". Line 17 does a"r1 = READ_ONCE(*x)", which does an unordered load from "*x" into localvariable "r1". Both "x" and "y" are in P1()'s parameter list, so bothreference 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 processeshave completed and all of their memory references and memory barriershave propagated to all parts of the system. The references to the localvariables "r0" and "r1" in line 24 must be prefixed with "1:" to specifywhich process they are local to.Note that the assertion expression is written in the litmus-testlanguage rather than in C. For example, single "=" is an equalityoperator rather than an assignment. The "/\" character combination means"and". Similarly, "\/" stands for "or". Both of these are ASCII-artrepresentations of the corresponding mathematical symbols. Finally,"~" stands for "logical not", which is "!" in C, and not to be confusedwith 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 theflag ("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, whichabsolutely must be run from the tools/memory-model directory and fromthis directory only:herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmusThe output is the result of something similar to a full state-spacesearch, 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 311 Time MP+pooncerelease+poacquireonce 0.0012 Hash=579aaa14d8c35a39429b02e698241d09The most pertinent line is line 10, which contains "Never 0 3", whichindicates that the bad result flagged by the "exists" clause neverhappens. This line might instead say "Sometimes" to indicate that thebad 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 endof 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 listone of these states, with the first ("1:r0=0; 1:r1=0;") indicating thatboth of P1()'s loads returned the value "0". As expected, given the"Never" on line 10, the state flagged by the "exists" clause is notlisted. This full list of states can be helpful when debugging a newlitmus test.The rest of the output is not normally needed, either due to irrelevanceor due to being redundant with the lines discussed above. However, thefollowing paragraph lists them for the benefit of readers possessed ofan 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 alead-in to line 8's "Positive: 0 Negative: 3", which lists the numberof end states satisfying and not satisfying the "exists" clause, justlike 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 thetime in seconds required to analyze the litmus test. Small tests suchas 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 usedby tooling that manages litmus tests and their output. This tooling isused by people modifying LKMM itself, and among other things lets suchpeople know which of the several thousand relevant litmus tests wereaffected 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 themto 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 }1314 P1(int *x, int *y)15 {16 int r0;17 int r1;1819 r0 = smp_load_acquire(y);20 r1 = READ_ONCE(*x);21 }2223 exists (1:r0=1 /\ 1:r1=42)Lines 3-6 now initialize both "x" and "y" to the value 42. This alsomeans 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 thevalue 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 311 Time MP+pooncerelease+poacquireonce 0.0212 Hash=ab9a9b7940a75a792266be279a980156It is tempting to avoid the open-coded repetitions of the value "42"by defining another global variable "initval=42" and replacing alloccurrences 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 aboutwhy this approach to initialization can be useful.Control Structures------------------LKMM supports the C-language "if" statement, which allows modeling ofconditional branches. In LKMM, conditional branches can affect ordering,but only if you are *very* careful (compilers are surprisingly ableto optimize away conditional branches). The following example showsthe "load buffering" (LB) use case that is used in the Linux kernel tosynchronize between ring-buffer producers and consumers. In the examplebelow, P0() is one side checking to see if an operation may proceed andP1() 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 }1314 P1(int *x, int *y)15 {16 int r0;1718 r0 = READ_ONCE(*y);19 smp_mb();20 WRITE_ONCE(*x, 1);21 }2223 exists (0:r0=1 /\ 1:r0=1)P1()'s "if" statement on line 10 works as expected, so that line 11 isexecuted only if line 9 loads a non-zero value from "x". Because P1()'swrite of "1" to "x" happens only after P1()'s read from "y", one wouldhope 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 210 Time LB+fencembonceonce+ctrlonceonce 0.0011 Hash=e5260556f6de495fd39b556d1b831c3bHowever, there is no "while" statement due to the fact that fullstate-space search has some difficulty with iteration. However, thereare tricks that may be used to handle some special cases, which arediscussed below. In addition, loop-unrolling tricks may be applied,albeit sparingly.Tricks and Traps================This section covers extracting debug output from herd7, emulatingspin loops, handling trivial linked lists, adding comments to litmus tests,emulating call_rcu(), and finally tricks to improve herd7 performancein order to better handle large litmus tests.Debug Output------------By default, the herd7 state output includes all variables mentionedin the "exists" clause. But sometimes debugging efforts are greatlyaided by the values of other variables. Consider this litmus test(tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus butslightly modified), which probes an obscure corner of hardware memoryordering: 1 C SB+rfionceonce-poonceonces 2 3 {} 4 5 P0(int *x, int *y) 6 { 7 int r1; 8 int r2; 910 WRITE_ONCE(*x, 1);11 r1 = READ_ONCE(*x);12 r2 = READ_ONCE(*y);13 }1415 P1(int *x, int *y)16 {17 int r3;18 int r4;1920 WRITE_ONCE(*y, 1);21 r3 = READ_ONCE(*y);22 r4 = READ_ONCE(*x);23 }2425 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: 310 Condition exists (0:r2=0 /\ 1:r4=0)11 Observation SB+rfionceonce-poonceonces Sometimes 1 312 Time SB+rfionceonce-poonceonces 0.0113 Hash=c7f30fe0faebb7d565405d55b7318ada(This output indicates that CPUs are permitted to "snoop their ownstore buffers", which all of Linux's CPU families other than s390 willhappily do. Such snooping results in disagreement among CPUs on theorder 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 thevalues of "x", "y", "0:r1", and "0:r3" as well. The "locations"statement on line 25 shows how to cause herd7 to display additionalvariables: 1 C SB+rfionceonce-poonceonces 2 3 {} 4 5 P0(int *x, int *y) 6 { 7 int r1; 8 int r2; 910 WRITE_ONCE(*x, 1);11 r1 = READ_ONCE(*x);12 r2 = READ_ONCE(*y);13 }1415 P1(int *x, int *y)16 {17 int r3;18 int r4;1920 WRITE_ONCE(*y, 1);21 r3 = READ_ONCE(*y);22 r4 = READ_ONCE(*x);23 }2425 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: 310 Condition exists (0:r2=0 /\ 1:r4=0)11 Observation SB+rfionceonce-poonceonces Sometimes 1 312 Time SB+rfionceonce-poonceonces 0.0113 Hash=40de8418c4b395388f6501cafd1ed38dWhat if you would like to know the value of a particular global variableat some particular point in a given process's execution? One approachis to use a READ_ONCE() to load that global variable into a new localvariable, then add that local variable to the "locations" clause.But be careful: In some litmus tests, adding a READ_ONCE() will changethe outcome! For one example, please see the C-READ_ONCE.litmus andC-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 isat best of exponential time complexity. Adding processes and increasingthe amount of code in a give process can greatly increase execution time.Potentially infinite loops, such as those used to wait for locks tobecome available, are clearly problematic.Fortunately, it is possible to avoid state-space explosion by speciallymodeling such loops. For example, the following litmus tests emulateslocking using xchg_acquire(), but instead of enclosing xchg_acquire()in a spin loop, it instead excludes executions that fail to acquire thelock using a herd7 "filter" clause. Note that for exclusive locking, youare better off using the spin_lock() and spin_unlock() that LKMM directlymodels, if for no other reason that these are much faster. However, thetechniques illustrated in this section can be used for other purposes,such as emulating reader-writer locking, which LKMM does not yet model. 1 C C-SB+l-o-o-u+l-o-o-u-X 2 3 { 4 } 5 6 P0(int *sl, int *x0, int *x1) 7 { 8 int r2; 9 int r1;1011 r2 = xchg_acquire(sl, 1);12 WRITE_ONCE(*x0, 1);13 r1 = READ_ONCE(*x1);14 smp_store_release(sl, 0);15 }1617 P1(int *sl, int *x0, int *x1)18 {19 int r2;20 int r1;2122 r2 = xchg_acquire(sl, 1);23 WRITE_ONCE(*x1, 1);24 r1 = READ_ONCE(*x0);25 smp_store_release(sl, 0);26 }2728 filter (0:r2=0 /\ 1:r2=0)29 exists (0:r1=0 /\ 1:r1=0)This litmus test may be found here: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.litmusThis test uses two global variables, "x1" and "x2", and also emulates asingle global spinlock named "sl". This spinlock is held by whicheverprocess changes the value of "sl" from "0" to "1", and is released whenthat process sets "sl" back to "0". P0()'s lock acquisition is emulatedon line 11 using xchg_acquire(), which unconditionally stores the value"1" to "sl" and stores either "0" or "1" to "r2", depending on whetherthe lock acquisition was successful or unsuccessful (due to "sl" alreadyhaving the value "1"), respectively. P1() operates in a similar manner.Rather unconventionally, execution appears to proceed to the criticalsection on lines 12 and 13 in either case. Line 14 then uses ansmp_store_release() to store zero to "sl", thus emulating lock release.The case where xchg_acquire() fails to acquire the lock is handled bythe "filter" clause on line 28, which tells herd7 to keep only thoseexecutions in which both "0:r2" and "1:r2" are zero, that is to payattention only to those executions in which both locks are actuallyacquired. Thus, the bogus executions that would execute the criticalsections are discarded and any effects that they might have had areignored. Note well that the "filter" clause keeps those executionsfor which its expression is satisfied, that is, for which the expressionevaluates to true. In other words, the "filter" clause says what tokeep, not what to discard.The result of running this test is as follows: 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed 2 States 2 3 0:r1=0; 1:r1=1; 4 0:r1=1; 1:r1=0; 5 No 6 Witnesses 7 Positive: 0 Negative: 2 8 Condition exists (0:r1=0 /\ 1:r1=0) 9 Observation C-SB+l-o-o-u+l-o-o-u-X Never 0 210 Time C-SB+l-o-o-u+l-o-o-u-X 0.03The "Never" on line 9 indicates that this use of xchg_acquire() andsmp_store_release() really does correctly emulate locking.Why doesn't the litmus test take the simpler approach of using a spin loopto handle failed spinlock acquisitions, like the kernel does? The keyinsight behind this litmus test is that spin loops have no effect on thepossible "exists"-clause outcomes of program execution in the absenceof deadlock. In other words, given a high-quality lock-acquisitionprimitive in a deadlock-free program running on high-quality hardware,each lock acquisition will eventually succeed. Because herd7 alreadyexplores the full state space, the length of time required to actuallyacquire the lock does not matter. After all, herd7 already models allpossible durations of the xchg_acquire() statements.Why not just add the "filter" clause to the "exists" clause, thusavoiding the "filter" clause entirely? This does work, but is slower.The reason that the "filter" clause is faster is that (in the common case)herd7 knows to abandon an execution as soon as the "filter" expressionfails to be satisfied. In contrast, the "exists" clause is evaluatedonly at the end of time, thus requiring herd7 to waste time on bogusexecutions in which both critical sections proceed concurrently. Inaddition, some LKMM users like the separation of concerns provided byusing the both the "filter" and "exists" clauses.Readers lacking a pathological interest in odd corner cases should feelfree to skip the remainder of this section.But what if the litmus test were to temporarily set "0:r2" to a non-zerovalue? Wouldn't that cause herd7 to abandon the execution prematurelydue to an early mismatch of the "filter" clause?Why not just try it? Line 4 of the following modified litmus testintroduces a new global variable "x2" that is initialized to "1". Line 23of P1() reads that variable into "1:r2" to force an early mismatch withthe "filter" clause. Line 24 does a known-true "if" condition to avoidand static analysis that herd7 might do. Finally the "exists" clauseon line 32 is updated to a condition that is alway satisfied at the endof the test. 1 C C-SB+l-o-o-u+l-o-o-u-X 2 3 { 4 x2=1; 5 } 6 7 P0(int *sl, int *x0, int *x1) 8 { 9 int r2;10 int r1;1112 r2 = xchg_acquire(sl, 1);13 WRITE_ONCE(*x0, 1);14 r1 = READ_ONCE(*x1);15 smp_store_release(sl, 0);16 }1718 P1(int *sl, int *x0, int *x1, int *x2)19 {20 int r2;21 int r1;2223 r2 = READ_ONCE(*x2);24 if (r2)25 r2 = xchg_acquire(sl, 1);26 WRITE_ONCE(*x1, 1);27 r1 = READ_ONCE(*x0);28 smp_store_release(sl, 0);29 }3031 filter (0:r2=0 /\ 1:r2=0)32 exists (x1=1)If the "filter" clause were to check each variable at each point in theexecution, running this litmus test would display no executions becauseall executions would be filtered out at line 23. However, the outputis instead as follows: 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed 2 States 1 3 x1=1; 4 Ok 5 Witnesses 6 Positive: 2 Negative: 0 7 Condition exists (x1=1) 8 Observation C-SB+l-o-o-u+l-o-o-u-X Always 2 0 9 Time C-SB+l-o-o-u+l-o-o-u-X 0.0410 Hash=080bc508da7f291e122c6de76c0088e3Line 3 shows that there is one execution that did not get filtered out,so the "filter" clause is evaluated only on the last assignment tothe variables that it checks. In this case, the "filter" clause is adisjunction, so it might be evaluated twice, once at the final (and only)assignment to "0:r2" and once at the final assignment to "1:r2".Linked Lists------------LKMM can handle linked lists, but only linked lists in which each nodecontains nothing except a pointer to the next node in the list. This isof course quite restrictive, but there is nevertheless quite a bit thatcan be done within these confines, as can be seen in the litmus testat tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus: 1 C MP+onceassign+derefonce 2 3 { 4 y=z; 5 z=0; 6 } 7 8 P0(int *x, int **y) 9 {10 WRITE_ONCE(*x, 1);11 rcu_assign_pointer(*y, x);12 }1314 P1(int *x, int **y)15 {16 int *r0;17 int r1;1819 rcu_read_lock();20 r0 = rcu_dereference(*y);21 r1 = READ_ONCE(*r0);22 rcu_read_unlock();23 }2425 exists (1:r0=x /\ 1:r1=0)Line 4's "y=z" may seem odd, given that "z" has not yet been initialized.But "y=z" does not set the value of "y" to that of "z", but insteadsets the value of "y" to the *address* of "z". Lines 4 and 5 thereforecreate a simple linked list, with "y" pointing to "z" and "z" having aNULL pointer. A much longer linked list could be created if desired,and circular singly linked lists can also be created and manipulated.The "exists" clause works the same way, with the "1:r0=x" comparing P1()'s"r0" not to the value of "x", but again to its address. This term of the"exists" clause therefore tests whether line 20's load from "y" saw thevalue stored by line 11, which is in fact what is required in this case.P0()'s line 10 initializes "x" to the value 1 then line 11 links to "x"from "y", replacing "z".P1()'s line 20 loads a pointer from "y", and line 21 dereferences thatpointer. The RCU read-side critical section spanning lines 19-22 is justfor show in this example. Note that the address used for line 21's loaddepends on (in this case, "is exactly the same as") the value loaded byline 20. This is an example of what is called an "address dependency".This particular address dependency extends from the load on line 20 to theload on line 21. Address dependencies provide a weak form of ordering.Running this test results in the following: 1 Test MP+onceassign+derefonce Allowed 2 States 2 3 1:r0=x; 1:r1=1; 4 1:r0=z; 1:r1=0; 5 No 6 Witnesses 7 Positive: 0 Negative: 2 8 Condition exists (1:r0=x /\ 1:r1=0) 9 Observation MP+onceassign+derefonce Never 0 210 Time MP+onceassign+derefonce 0.0011 Hash=49ef7a741563570102448a256a0c8568The only possible outcomes feature P1() loading a pointer to "z"(which contains zero) on the one hand and P1() loading a pointer to "x"(which contains the value one) on the other. This should be reassuringbecause it says that RCU readers cannot see the old preinitializationvalues when accessing a newly inserted list node. This undesirablescenario is flagged by the "exists" clause, and would occur if P1()loaded a pointer to "x", but obtained the pre-initialization value ofzero after dereferencing that pointer.Comments--------Different portions of a litmus test are processed by different parsers,which has the charming effect of requiring different comment syntax indifferent portions of the litmus test. The C-syntax portions useC-language comments (either "/* */" or "//"), while the other portionsuse Ocaml comments "(* *)".The following litmus test illustrates the comment style correspondingto each syntactic unit of the test: 1 C MP+onceassign+derefonce (* A *) 2 3 (* B *) 4 5 { 6 y=z; (* C *) 7 z=0; 8 } // D 910 // E1112 P0(int *x, int **y) // F13 {14 WRITE_ONCE(*x, 1); // G15 rcu_assign_pointer(*y, x);16 }1718 // H1920 P1(int *x, int **y)21 {22 int *r0;23 int r1;2425 rcu_read_lock();26 r0 = rcu_dereference(*y);27 r1 = READ_ONCE(*r0);28 rcu_read_unlock();29 }3031 // I3233 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) (* L *)In short, use C-language comments in the C code and Ocaml comments inthe rest of the litmus test.On the other hand, if you prefer C-style comments everywhere, theC preprocessor is your friend.Asynchronous RCU Grace Periods------------------------------The following litmus test is derived from the example show inDocumentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted toemulate call_rcu(): 1 C RCU+sync+free 2 3 { 4 int x = 1; 5 int *y = &x; 6 int z = 1; 7 } 8 9 P0(int *x, int *z, int **y)10 {11 int *r0;12 int r1;1314 rcu_read_lock();15 r0 = rcu_dereference(*y);16 r1 = READ_ONCE(*r0);17 rcu_read_unlock();18 }1920 P1(int *z, int **y, int *c)21 {22 rcu_assign_pointer(*y, z);23 smp_store_release(*c, 1); // Emulate call_rcu().24 }2526 P2(int *x, int *z, int **y, int *c)27 {28 int r0;2930 r0 = smp_load_acquire(*c); // Note call_rcu() request.31 synchronize_rcu(); // Wait one grace period.32 WRITE_ONCE(*x, 0); // Emulate the RCU callback.33 }3435 filter (2:r0=1) (* Reject too-early starts. *)36 exists (0:r0=x /\ 0:r1=0)Lines 4-6 initialize a linked list headed by "y" that initially contains"x". In addition, "z" is pre-initialized to prepare for P1(), whichwill replace "x" with "z" in this list.P0() on lines 9-18 enters an RCU read-side critical section, loads thelist header "y" and dereferences it, leaving the node in "0:r0" andthe node's value in "0:r1".P1() on lines 20-24 updates the list header to instead reference "z",then emulates call_rcu() by doing a release store into "c".P2() on lines 27-33 emulates the behind-the-scenes effect of doing acall_rcu(). Line 30 first does an acquire load from "c", then line 31waits for an RCU grace period to elapse, and finally line 32 emulatesthe RCU callback, which in turn emulates a call to kfree().Of course, it is possible for P2() to start too soon, so that thevalue of "2:r0" is zero rather than the required value of "1".The "filter" clause on line 35 handles this possibility, rejectingall executions in which "2:r0" is not equal to the value "1".Performance-----------LKMM's exploration of the full state-space can be extremely helpful,but it does not come for free. The price is exponential computationalcomplexity in terms of the number of processes, the average numberof statements in each process, and the total number of stores in thelitmus test.So it is best to start small and then work up. Where possible, breakyour code down into small pieces each representing a core concurrencyrequirement.That said, herd7 is quite fast. On an unprepossessing x86 laptop, itwas able to analyze the following 10-process RCU litmus test in aboutsix seconds.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.litmusOne way to make herd7 run faster is to use the "-speedcheck true" option.This option prevents herd7 from generating all possible end states,instead causing it to focus solely on whether or not the "exists"clause can be satisfied. With this option, herd7 evaluates the abovelitmus test in about 300 milliseconds, for more than an order of magnitudeimprovement in performance.Larger 16-process litmus tests that would normally consume 15 minutesof time complete in about 40 seconds with this option. To be fair,you do get an extra 65,535 states when you leave off the "-speedchecktrue" option.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.litmusNevertheless, litmus-test analysis really is of exponential complexity,whether with or without "-speedcheck true". Increasing by just threeprocesses to a 19-process litmus test requires 2 hours and 40 minuteswithout, and about 8 minutes with "-speedcheck true". Each of theseresults represent roughly an order of magnitude slowdown compared to the16-process litmus test. Again, to be fair, the multi-hour run exploresno fewer than 524,287 additional states compared to the shorter one.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.litmusIf you don't like command-line arguments, you can obtain a similar speedupby adding a "filter" clause with exactly the same expression as your"exists" clause.However, please note that seeing the full set of states can be extremelyhelpful when developing and debugging litmus tests.LIMITATIONS===========Limitations of the Linux-kernel memory model (LKMM) include:1. Compiler optimizations are not accurately modeled. Of course, the use of READ_ONCE() and WRITE_ONCE() limits the compiler's ability to optimize, but under some circumstances it is possible for the compiler to undermine the memory model. For more information, see Documentation/explanation.txt (in particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING" sections). Note that this limitation in turn limits LKMM's ability to accurately model address, control, and data dependencies. For example, if the compiler can deduce the value of some variable carrying a dependency, then the compiler can break that dependency by substituting a constant of that value. Conversely, LKMM will sometimes overestimate the amount of reordering compilers and CPUs can carry out, leading it to miss some pretty obvious cases of ordering. A simple example is: r1 = READ_ONCE(x); if (r1 == 0) smp_mb(); WRITE_ONCE(y, 1); The WRITE_ONCE() does not depend on the READ_ONCE(), and as a result, LKMM does not claim ordering. However, even though no dependency is present, the WRITE_ONCE() will not be executed before the READ_ONCE(). There are two reasons for this: The presence of the smp_mb() in one of the branches prevents the compiler from moving the WRITE_ONCE() up before the "if" statement, since the compiler has to assume that r1 will sometimes be 0 (but see the comment below); CPUs do not execute stores before po-earlier conditional branches, even in cases where the store occurs after the two arms of the branch have recombined. It is clear that it is not dangerous in the slightest for LKMM to make weaker guarantees than architectures. In fact, it is desirable, as it gives compilers room for making optimizations. For instance, suppose that a 0 value in r1 would trigger undefined behavior elsewhere. Then a clever compiler might deduce that r1 can never be 0 in the if condition. As a result, said clever compiler might deem it safe to optimize away the smp_mb(), eliminating the branch and any ordering an architecture would guarantee otherwise.2. Multiple access sizes for a single variable are not supported, and neither are misaligned or partially overlapping accesses.3. Exceptions and interrupts are not modeled. In some cases, this limitation can be overcome by modeling the interrupt or exception with an additional process.4. I/O such as MMIO or DMA is not supported.5. Self-modifying code (such as that found in the kernel's alternatives mechanism, function tracer, Berkeley Packet Filter JIT compiler, and module loader) is not supported.6. Complete modeling of all variants of atomic read-modify-write operations, locking primitives, and RCU is not provided. For example, call_rcu() and rcu_barrier() are not supported. However, a substantial amount of support is provided for these operations, as shown in the linux-kernel.def file. Here are specific limitations: a. When rcu_assign_pointer() is passed NULL, the Linux kernel provides no ordering, but LKMM models this case as a store release. b. The "unless" RMW operations are not currently modeled: atomic_long_add_unless(), atomic_inc_unless_negative(), and atomic_dec_unless_positive(). These can be emulated in litmus tests, for example, by using atomic_cmpxchg(). One exception of this limitation is atomic_add_unless(), which is provided directly by herd7 (so no corresponding definition in linux-kernel.def). atomic_add_unless() is modeled by herd7 therefore it can be used in litmus tests. c. The call_rcu() function is not modeled. As was shown above, it can be emulated in litmus tests by adding another process that invokes synchronize_rcu() and the body of the callback function, with (for example) a release-acquire from the site of the emulated call_rcu() to the beginning of the additional process. d. The rcu_barrier() function is not modeled. It can be emulated in litmus tests emulating call_rcu() via (for example) a release-acquire from the end of each additional call_rcu() process to the site of the emulated rcu-barrier(). e. Reader-writer locking is not modeled. It can be emulated in litmus tests using atomic read-modify-write operations.The fragment of the C language supported by these litmus tests is quitelimited and in some ways non-standard:1. There is no automatic C-preprocessor pass. You can of course run it manually, if you choose.2. There is no way to create functions other than the Pn() functions that model the concurrent processes.3. The Pn() functions' formal parameters must be pointers to the global shared variables. Nothing can be passed by value into these functions.4. The only functions that can be invoked are those built directly into herd7 or that are defined in the linux-kernel.def file.5. The "switch", "do", "for", "while", and "goto" C statements are not supported. The "switch" statement can be emulated by the "if" statement. The "do", "for", and "while" statements can often be emulated by manually unrolling the loop, or perhaps by enlisting the aid of the C preprocessor to minimize the resulting code duplication. Some uses of "goto" can be emulated by "if", and some others by unrolling.6. Although you can use a wide variety of types in litmus-test variable declarations, and especially in global-variable declarations, the "herd7" tool understands only int and pointer types. There is no support for floating-point types, enumerations, characters, strings, arrays, or structures.7. Parsing of variable declarations is very loose, with almost no type checking.8. Initializers differ from their C-language counterparts. For example, when an initializer contains the name of a shared variable, that name denotes a pointer to that variable, not the current value of that variable. For example, "int x = y" is interpreted the way "int x = &y" would be in C.9. Dynamic memory allocation is not supported, although this can be worked around in some cases by supplying multiple statically allocated variables.Some of these limitations may be overcome in the future, but others aremore likely to be addressed by incorporating the Linux-kernel memory modelinto other tools.Finally, please note that LKMM is subject to change as hardware, use cases,and compilers evolve.