1084 lines · plain
1Linux-Kernel Memory Model Litmus Tests2======================================3 4This file describes the LKMM litmus-test format by example, describes5some tricks and traps, and finally outlines LKMM's limitations. Earlier6versions of this material appeared in a number of LWN articles, including:7 8https://lwn.net/Articles/720550/9 A formal kernel memory-ordering model (part 2)10https://lwn.net/Articles/608550/11 Axiomatic validation of memory barriers and atomic instructions12https://lwn.net/Articles/470681/13 Validating Memory Barriers and Atomic Instructions14 15This document presents information in decreasing order of applicability,16so that, where possible, the information that has proven more commonly17useful is shown near the beginning.18 19For information on installing LKMM, including the underlying "herd7"20tool, please see tools/memory-model/README.21 22 23Copy-Pasta24==========25 26As with other software, it is often better (if less macho) to adapt an27existing litmus test than it is to create one from scratch. A number28of litmus tests may be found in the kernel source tree:29 30 tools/memory-model/litmus-tests/31 Documentation/litmus-tests/32 33Several thousand more example litmus tests are available on github34and kernel.org:35 36 https://github.com/paulmckrcu/litmus37 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd38 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus39 40The -l and -L arguments to "git grep" can be quite helpful in identifying41existing litmus tests that are similar to the one you need. But even if42you start with an existing litmus test, it is still helpful to have a43good understanding of the litmus-test format.44 45 46Examples and Format47===================48 49This section describes the overall format of litmus tests, starting50with a small example of the message-passing pattern and moving on to51more complex examples that illustrate explicit initialization and LKMM's52minimalistic set of flow-control statements.53 54 55Message-Passing Example56-----------------------57 58This section gives an overview of the format of a litmus test using an59example based on the common message-passing use case. This use case60appears often in the Linux kernel. For example, a flag (modeled by "y"61below) indicates that a buffer (modeled by "x" below) is now completely62filled in and ready for use. It would be very bad if the consumer saw the63flag set, but, due to memory misordering, saw old values in the buffer.64 65This example asks whether smp_store_release() and smp_load_acquire()66suffices to avoid this bad outcome:67 68 1 C MP+pooncerelease+poacquireonce69 270 3 {}71 472 5 P0(int *x, int *y)73 6 {74 7 WRITE_ONCE(*x, 1);75 8 smp_store_release(y, 1);76 9 }77107811 P1(int *x, int *y)7912 {8013 int r0;8114 int r1;82158316 r0 = smp_load_acquire(y);8417 r1 = READ_ONCE(*x);8518 }86198720 exists (1:r0=1 /\ 1:r1=0)88 89Line 1 starts with "C", which identifies this file as being in the90LKMM C-language format (which, as we will see, is a small fragment91of the full C language). The remainder of line 1 is the name of92the test, which by convention is the filename with the ".litmus"93suffix stripped. In this case, the actual test may be found in94tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus95in the Linux-kernel source tree.96 97Mechanically generated litmus tests will often have an optional98double-quoted comment string on the second line. Such strings are ignored99when running the test. Yes, you can add your own comments to litmus100tests, but this is a bit involved due to the use of multiple parsers.101For now, you can use C-language comments in the C code, and these comments102may be in either the "/* */" or the "//" style. A later section will103cover the full litmus-test commenting story.104 105Line 3 is the initialization section. Because the default initialization106to zero suffices for this test, the "{}" syntax is used, which mean the107initialization section is empty. Litmus tests requiring non-default108initialization must have non-empty initialization sections, as in the109example that will be presented later in this document.110 111Lines 5-9 show the first process and lines 11-18 the second process. Each112process corresponds to a Linux-kernel task (or kthread, workqueue, thread,113and so on; LKMM discussions often use these terms interchangeably).114The name of the first process is "P0" and that of the second "P1".115You can name your processes anything you like as long as the names consist116of a single "P" followed by a number, and as long as the numbers are117consecutive starting with zero. This can actually be quite helpful,118for example, a .litmus file matching "^P1(" but not matching "^P2("119must contain a two-process litmus test.120 121The argument list for each function are pointers to the global variables122used by that function. Unlike normal C-language function parameters, the123names are significant. The fact that both P0() and P1() have a formal124parameter named "x" means that these two processes are working with the125same global variable, also named "x". So the "int *x, int *y" on P0()126and P1() mean that both processes are working with two shared global127variables, "x" and "y". Global variables are always passed to processes128by reference, hence "P0(int *x, int *y)", but *never* "P0(int x, int y)".129 130P0() has no local variables, but P1() has two of them named "r0" and "r1".131These names may be freely chosen, but for historical reasons stemming from132other litmus-test formats, it is conventional to use names consisting of133"r" followed by a number as shown here. A common bug in litmus tests134is forgetting to add a global variable to a process's parameter list.135This will sometimes result in an error message, but can also cause the136intended global to instead be silently treated as an undeclared local137variable.138 139Each process's code is similar to Linux-kernel C, as can be seen on lines1407-8 and 13-17. This code may use many of the Linux kernel's atomic141operations, some of its exclusive-lock functions, and some of its RCU142and SRCU functions. An approximate list of the currently supported143functions may be found in the linux-kernel.def file.144 145The P0() process does "WRITE_ONCE(*x, 1)" on line 7. Because "x" is a146pointer in P0()'s parameter list, this does an unordered store to global147variable "x". Line 8 does "smp_store_release(y, 1)", and because "y"148is also in P0()'s parameter list, this does a release store to global149variable "y".150 151The P1() process declares two local variables on lines 13 and 14.152Line 16 does "r0 = smp_load_acquire(y)" which does an acquire load153from global variable "y" into local variable "r0". Line 17 does a154"r1 = READ_ONCE(*x)", which does an unordered load from "*x" into local155variable "r1". Both "x" and "y" are in P1()'s parameter list, so both156reference the same global variables that are used by P0().157 158Line 20 is the "exists" assertion expression to evaluate the final state.159This final state is evaluated after the dust has settled: both processes160have completed and all of their memory references and memory barriers161have propagated to all parts of the system. The references to the local162variables "r0" and "r1" in line 24 must be prefixed with "1:" to specify163which process they are local to.164 165Note that the assertion expression is written in the litmus-test166language rather than in C. For example, single "=" is an equality167operator rather than an assignment. The "/\" character combination means168"and". Similarly, "\/" stands for "or". Both of these are ASCII-art169representations of the corresponding mathematical symbols. Finally,170"~" stands for "logical not", which is "!" in C, and not to be confused171with the C-language "~" operator which instead stands for "bitwise not".172Parentheses may be used to override precedence.173 174The "exists" assertion on line 20 is satisfied if the consumer sees the175flag ("y") set but the buffer ("x") as not yet filled in, that is, if P1()176loaded a value from "x" that was equal to 1 but loaded a value from "y"177that was still equal to zero.178 179This example can be checked by running the following command, which180absolutely must be run from the tools/memory-model directory and from181this directory only:182 183herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus184 185The output is the result of something similar to a full state-space186search, and is as follows:187 188 1 Test MP+pooncerelease+poacquireonce Allowed189 2 States 3190 3 1:r0=0; 1:r1=0;191 4 1:r0=0; 1:r1=1;192 5 1:r0=1; 1:r1=1;193 6 No194 7 Witnesses195 8 Positive: 0 Negative: 3196 9 Condition exists (1:r0=1 /\ 1:r1=0)19710 Observation MP+pooncerelease+poacquireonce Never 0 319811 Time MP+pooncerelease+poacquireonce 0.0019912 Hash=579aaa14d8c35a39429b02e698241d09200 201The most pertinent line is line 10, which contains "Never 0 3", which202indicates that the bad result flagged by the "exists" clause never203happens. This line might instead say "Sometimes" to indicate that the204bad result happened in some but not all executions, or it might say205"Always" to indicate that the bad result happened in all executions.206(The herd7 tool doesn't judge, so it is only an LKMM convention that the207"exists" clause indicates a bad result. To see this, invert the "exists"208clause's condition and run the test.) The numbers ("0 3") at the end209of this line indicate the number of end states satisfying the "exists"210clause (0) and the number not not satisfying that clause (3).211 212Another important part of this output is shown in lines 2-5, repeated here:213 214 2 States 3215 3 1:r0=0; 1:r1=0;216 4 1:r0=0; 1:r1=1;217 5 1:r0=1; 1:r1=1;218 219Line 2 gives the total number of end states, and each of lines 3-5 list220one of these states, with the first ("1:r0=0; 1:r1=0;") indicating that221both of P1()'s loads returned the value "0". As expected, given the222"Never" on line 10, the state flagged by the "exists" clause is not223listed. This full list of states can be helpful when debugging a new224litmus test.225 226The rest of the output is not normally needed, either due to irrelevance227or due to being redundant with the lines discussed above. However, the228following paragraph lists them for the benefit of readers possessed of229an insatiable curiosity. Other readers should feel free to skip ahead.230 231Line 1 echos the test name, along with the "Test" and "Allowed". Line 6's232"No" says that the "exists" clause was not satisfied by any execution,233and as such it has the same meaning as line 10's "Never". Line 7 is a234lead-in to line 8's "Positive: 0 Negative: 3", which lists the number235of end states satisfying and not satisfying the "exists" clause, just236like the two numbers at the end of line 10. Line 9 repeats the "exists"237clause so that you don't have to look it up in the litmus-test file.238The number at the end of line 11 (which begins with "Time") gives the239time in seconds required to analyze the litmus test. Small tests such240as this one complete in a few milliseconds, so "0.00" is quite common.241Line 12 gives a hash of the contents for the litmus-test file, and is used242by tooling that manages litmus tests and their output. This tooling is243used by people modifying LKMM itself, and among other things lets such244people know which of the several thousand relevant litmus tests were245affected by a given change to LKMM.246 247 248Initialization249--------------250 251The previous example relied on the default zero initialization for252"x" and "y", but a similar litmus test could instead initialize them253to some other value:254 255 1 C MP+pooncerelease+poacquireonce256 2257 3 {258 4 x=42;259 5 y=42;260 6 }261 7262 8 P0(int *x, int *y)263 9 {26410 WRITE_ONCE(*x, 1);26511 smp_store_release(y, 1);26612 }2671326814 P1(int *x, int *y)26915 {27016 int r0;27117 int r1;2721827319 r0 = smp_load_acquire(y);27420 r1 = READ_ONCE(*x);27521 }2762227723 exists (1:r0=1 /\ 1:r1=42)278 279Lines 3-6 now initialize both "x" and "y" to the value 42. This also280means that the "exists" clause on line 23 must change "1:r1=0" to281"1:r1=42".282 283Running the test gives the same overall result as before, but with the284value 42 appearing in place of the value zero:285 286 1 Test MP+pooncerelease+poacquireonce Allowed287 2 States 3288 3 1:r0=1; 1:r1=1;289 4 1:r0=42; 1:r1=1;290 5 1:r0=42; 1:r1=42;291 6 No292 7 Witnesses293 8 Positive: 0 Negative: 3294 9 Condition exists (1:r0=1 /\ 1:r1=42)29510 Observation MP+pooncerelease+poacquireonce Never 0 329611 Time MP+pooncerelease+poacquireonce 0.0229712 Hash=ab9a9b7940a75a792266be279a980156298 299It is tempting to avoid the open-coded repetitions of the value "42"300by defining another global variable "initval=42" and replacing all301occurrences of "42" with "initval". This will not, repeat *not*,302initialize "x" and "y" to 42, but instead to the address of "initval"303(try it!). See the section below on linked lists to learn more about304why this approach to initialization can be useful.305 306 307Control Structures308------------------309 310LKMM supports the C-language "if" statement, which allows modeling of311conditional branches. In LKMM, conditional branches can affect ordering,312but only if you are *very* careful (compilers are surprisingly able313to optimize away conditional branches). The following example shows314the "load buffering" (LB) use case that is used in the Linux kernel to315synchronize between ring-buffer producers and consumers. In the example316below, P0() is one side checking to see if an operation may proceed and317P1() is the other side completing its update.318 319 1 C LB+fencembonceonce+ctrlonceonce320 2321 3 {}322 4323 5 P0(int *x, int *y)324 6 {325 7 int r0;326 8327 9 r0 = READ_ONCE(*x);32810 if (r0)32911 WRITE_ONCE(*y, 1);33012 }3311333214 P1(int *x, int *y)33315 {33416 int r0;3351733618 r0 = READ_ONCE(*y);33719 smp_mb();33820 WRITE_ONCE(*x, 1);33921 }3402234123 exists (0:r0=1 /\ 1:r0=1)342 343P1()'s "if" statement on line 10 works as expected, so that line 11 is344executed only if line 9 loads a non-zero value from "x". Because P1()'s345write of "1" to "x" happens only after P1()'s read from "y", one would346hope that the "exists" clause cannot be satisfied. LKMM agrees:347 348 1 Test LB+fencembonceonce+ctrlonceonce Allowed349 2 States 2350 3 0:r0=0; 1:r0=0;351 4 0:r0=1; 1:r0=0;352 5 No353 6 Witnesses354 7 Positive: 0 Negative: 2355 8 Condition exists (0:r0=1 /\ 1:r0=1)356 9 Observation LB+fencembonceonce+ctrlonceonce Never 0 235710 Time LB+fencembonceonce+ctrlonceonce 0.0035811 Hash=e5260556f6de495fd39b556d1b831c3b359 360However, there is no "while" statement due to the fact that full361state-space search has some difficulty with iteration. However, there362are tricks that may be used to handle some special cases, which are363discussed below. In addition, loop-unrolling tricks may be applied,364albeit sparingly.365 366 367Tricks and Traps368================369 370This section covers extracting debug output from herd7, emulating371spin loops, handling trivial linked lists, adding comments to litmus tests,372emulating call_rcu(), and finally tricks to improve herd7 performance373in order to better handle large litmus tests.374 375 376Debug Output377------------378 379By default, the herd7 state output includes all variables mentioned380in the "exists" clause. But sometimes debugging efforts are greatly381aided by the values of other variables. Consider this litmus test382(tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but383slightly modified), which probes an obscure corner of hardware memory384ordering:385 386 1 C SB+rfionceonce-poonceonces387 2388 3 {}389 4390 5 P0(int *x, int *y)391 6 {392 7 int r1;393 8 int r2;394 939510 WRITE_ONCE(*x, 1);39611 r1 = READ_ONCE(*x);39712 r2 = READ_ONCE(*y);39813 }3991440015 P1(int *x, int *y)40116 {40217 int r3;40318 int r4;4041940520 WRITE_ONCE(*y, 1);40621 r3 = READ_ONCE(*y);40722 r4 = READ_ONCE(*x);40823 }4092441025 exists (0:r2=0 /\ 1:r4=0)411 412The herd7 output is as follows:413 414 1 Test SB+rfionceonce-poonceonces Allowed415 2 States 4416 3 0:r2=0; 1:r4=0;417 4 0:r2=0; 1:r4=1;418 5 0:r2=1; 1:r4=0;419 6 0:r2=1; 1:r4=1;420 7 Ok421 8 Witnesses422 9 Positive: 1 Negative: 342310 Condition exists (0:r2=0 /\ 1:r4=0)42411 Observation SB+rfionceonce-poonceonces Sometimes 1 342512 Time SB+rfionceonce-poonceonces 0.0142613 Hash=c7f30fe0faebb7d565405d55b7318ada427 428(This output indicates that CPUs are permitted to "snoop their own429store buffers", which all of Linux's CPU families other than s390 will430happily do. Such snooping results in disagreement among CPUs on the431order of stores from different CPUs, which is rarely an issue.)432 433But the herd7 output shows only the two variables mentioned in the434"exists" clause. Someone modifying this test might wish to know the435values of "x", "y", "0:r1", and "0:r3" as well. The "locations"436statement on line 25 shows how to cause herd7 to display additional437variables:438 439 1 C SB+rfionceonce-poonceonces440 2441 3 {}442 4443 5 P0(int *x, int *y)444 6 {445 7 int r1;446 8 int r2;447 944810 WRITE_ONCE(*x, 1);44911 r1 = READ_ONCE(*x);45012 r2 = READ_ONCE(*y);45113 }4521445315 P1(int *x, int *y)45416 {45517 int r3;45618 int r4;4571945820 WRITE_ONCE(*y, 1);45921 r3 = READ_ONCE(*y);46022 r4 = READ_ONCE(*x);46123 }4622446325 locations [0:r1; 1:r3; x; y]46426 exists (0:r2=0 /\ 1:r4=0)465 466The herd7 output then displays the values of all the variables:467 468 1 Test SB+rfionceonce-poonceonces Allowed469 2 States 4470 3 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=0; x=1; y=1;471 4 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=1; x=1; y=1;472 5 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=0; x=1; y=1;473 6 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=1; x=1; y=1;474 7 Ok475 8 Witnesses476 9 Positive: 1 Negative: 347710 Condition exists (0:r2=0 /\ 1:r4=0)47811 Observation SB+rfionceonce-poonceonces Sometimes 1 347912 Time SB+rfionceonce-poonceonces 0.0148013 Hash=40de8418c4b395388f6501cafd1ed38d481 482What if you would like to know the value of a particular global variable483at some particular point in a given process's execution? One approach484is to use a READ_ONCE() to load that global variable into a new local485variable, then add that local variable to the "locations" clause.486But be careful: In some litmus tests, adding a READ_ONCE() will change487the outcome! For one example, please see the C-READ_ONCE.litmus and488C-READ_ONCE-omitted.litmus tests located here:489 490 https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/491 492 493Spin Loops494----------495 496The analysis carried out by herd7 explores full state space, which is497at best of exponential time complexity. Adding processes and increasing498the amount of code in a give process can greatly increase execution time.499Potentially infinite loops, such as those used to wait for locks to500become available, are clearly problematic.501 502Fortunately, it is possible to avoid state-space explosion by specially503modeling such loops. For example, the following litmus tests emulates504locking using xchg_acquire(), but instead of enclosing xchg_acquire()505in a spin loop, it instead excludes executions that fail to acquire the506lock using a herd7 "filter" clause. Note that for exclusive locking, you507are better off using the spin_lock() and spin_unlock() that LKMM directly508models, if for no other reason that these are much faster. However, the509techniques illustrated in this section can be used for other purposes,510such as emulating reader-writer locking, which LKMM does not yet model.511 512 1 C C-SB+l-o-o-u+l-o-o-u-X513 2514 3 {515 4 }516 5517 6 P0(int *sl, int *x0, int *x1)518 7 {519 8 int r2;520 9 int r1;5211052211 r2 = xchg_acquire(sl, 1);52312 WRITE_ONCE(*x0, 1);52413 r1 = READ_ONCE(*x1);52514 smp_store_release(sl, 0);52615 }5271652817 P1(int *sl, int *x0, int *x1)52918 {53019 int r2;53120 int r1;5322153322 r2 = xchg_acquire(sl, 1);53423 WRITE_ONCE(*x1, 1);53524 r1 = READ_ONCE(*x0);53625 smp_store_release(sl, 0);53726 }5382753928 filter (0:r2=0 /\ 1:r2=0)54029 exists (0:r1=0 /\ 1:r1=0)541 542This litmus test may be found here:543 544https://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.litmus545 546This test uses two global variables, "x1" and "x2", and also emulates a547single global spinlock named "sl". This spinlock is held by whichever548process changes the value of "sl" from "0" to "1", and is released when549that process sets "sl" back to "0". P0()'s lock acquisition is emulated550on line 11 using xchg_acquire(), which unconditionally stores the value551"1" to "sl" and stores either "0" or "1" to "r2", depending on whether552the lock acquisition was successful or unsuccessful (due to "sl" already553having the value "1"), respectively. P1() operates in a similar manner.554 555Rather unconventionally, execution appears to proceed to the critical556section on lines 12 and 13 in either case. Line 14 then uses an557smp_store_release() to store zero to "sl", thus emulating lock release.558 559The case where xchg_acquire() fails to acquire the lock is handled by560the "filter" clause on line 28, which tells herd7 to keep only those561executions in which both "0:r2" and "1:r2" are zero, that is to pay562attention only to those executions in which both locks are actually563acquired. Thus, the bogus executions that would execute the critical564sections are discarded and any effects that they might have had are565ignored. Note well that the "filter" clause keeps those executions566for which its expression is satisfied, that is, for which the expression567evaluates to true. In other words, the "filter" clause says what to568keep, not what to discard.569 570The result of running this test is as follows:571 572 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed573 2 States 2574 3 0:r1=0; 1:r1=1;575 4 0:r1=1; 1:r1=0;576 5 No577 6 Witnesses578 7 Positive: 0 Negative: 2579 8 Condition exists (0:r1=0 /\ 1:r1=0)580 9 Observation C-SB+l-o-o-u+l-o-o-u-X Never 0 258110 Time C-SB+l-o-o-u+l-o-o-u-X 0.03582 583The "Never" on line 9 indicates that this use of xchg_acquire() and584smp_store_release() really does correctly emulate locking.585 586Why doesn't the litmus test take the simpler approach of using a spin loop587to handle failed spinlock acquisitions, like the kernel does? The key588insight behind this litmus test is that spin loops have no effect on the589possible "exists"-clause outcomes of program execution in the absence590of deadlock. In other words, given a high-quality lock-acquisition591primitive in a deadlock-free program running on high-quality hardware,592each lock acquisition will eventually succeed. Because herd7 already593explores the full state space, the length of time required to actually594acquire the lock does not matter. After all, herd7 already models all595possible durations of the xchg_acquire() statements.596 597Why not just add the "filter" clause to the "exists" clause, thus598avoiding the "filter" clause entirely? This does work, but is slower.599The reason that the "filter" clause is faster is that (in the common case)600herd7 knows to abandon an execution as soon as the "filter" expression601fails to be satisfied. In contrast, the "exists" clause is evaluated602only at the end of time, thus requiring herd7 to waste time on bogus603executions in which both critical sections proceed concurrently. In604addition, some LKMM users like the separation of concerns provided by605using the both the "filter" and "exists" clauses.606 607Readers lacking a pathological interest in odd corner cases should feel608free to skip the remainder of this section.609 610But what if the litmus test were to temporarily set "0:r2" to a non-zero611value? Wouldn't that cause herd7 to abandon the execution prematurely612due to an early mismatch of the "filter" clause?613 614Why not just try it? Line 4 of the following modified litmus test615introduces a new global variable "x2" that is initialized to "1". Line 23616of P1() reads that variable into "1:r2" to force an early mismatch with617the "filter" clause. Line 24 does a known-true "if" condition to avoid618and static analysis that herd7 might do. Finally the "exists" clause619on line 32 is updated to a condition that is alway satisfied at the end620of the test.621 622 1 C C-SB+l-o-o-u+l-o-o-u-X623 2624 3 {625 4 x2=1;626 5 }627 6628 7 P0(int *sl, int *x0, int *x1)629 8 {630 9 int r2;63110 int r1;6321163312 r2 = xchg_acquire(sl, 1);63413 WRITE_ONCE(*x0, 1);63514 r1 = READ_ONCE(*x1);63615 smp_store_release(sl, 0);63716 }6381763918 P1(int *sl, int *x0, int *x1, int *x2)64019 {64120 int r2;64221 int r1;6432264423 r2 = READ_ONCE(*x2);64524 if (r2)64625 r2 = xchg_acquire(sl, 1);64726 WRITE_ONCE(*x1, 1);64827 r1 = READ_ONCE(*x0);64928 smp_store_release(sl, 0);65029 }6513065231 filter (0:r2=0 /\ 1:r2=0)65332 exists (x1=1)654 655If the "filter" clause were to check each variable at each point in the656execution, running this litmus test would display no executions because657all executions would be filtered out at line 23. However, the output658is instead as follows:659 660 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed661 2 States 1662 3 x1=1;663 4 Ok664 5 Witnesses665 6 Positive: 2 Negative: 0666 7 Condition exists (x1=1)667 8 Observation C-SB+l-o-o-u+l-o-o-u-X Always 2 0668 9 Time C-SB+l-o-o-u+l-o-o-u-X 0.0466910 Hash=080bc508da7f291e122c6de76c0088e3670 671Line 3 shows that there is one execution that did not get filtered out,672so the "filter" clause is evaluated only on the last assignment to673the variables that it checks. In this case, the "filter" clause is a674disjunction, so it might be evaluated twice, once at the final (and only)675assignment to "0:r2" and once at the final assignment to "1:r2".676 677 678Linked Lists679------------680 681LKMM can handle linked lists, but only linked lists in which each node682contains nothing except a pointer to the next node in the list. This is683of course quite restrictive, but there is nevertheless quite a bit that684can be done within these confines, as can be seen in the litmus test685at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:686 687 1 C MP+onceassign+derefonce688 2689 3 {690 4 y=z;691 5 z=0;692 6 }693 7694 8 P0(int *x, int **y)695 9 {69610 WRITE_ONCE(*x, 1);69711 rcu_assign_pointer(*y, x);69812 }6991370014 P1(int *x, int **y)70115 {70216 int *r0;70317 int r1;7041870519 rcu_read_lock();70620 r0 = rcu_dereference(*y);70721 r1 = READ_ONCE(*r0);70822 rcu_read_unlock();70923 }7102471125 exists (1:r0=x /\ 1:r1=0)712 713Line 4's "y=z" may seem odd, given that "z" has not yet been initialized.714But "y=z" does not set the value of "y" to that of "z", but instead715sets the value of "y" to the *address* of "z". Lines 4 and 5 therefore716create a simple linked list, with "y" pointing to "z" and "z" having a717NULL pointer. A much longer linked list could be created if desired,718and circular singly linked lists can also be created and manipulated.719 720The "exists" clause works the same way, with the "1:r0=x" comparing P1()'s721"r0" not to the value of "x", but again to its address. This term of the722"exists" clause therefore tests whether line 20's load from "y" saw the723value stored by line 11, which is in fact what is required in this case.724 725P0()'s line 10 initializes "x" to the value 1 then line 11 links to "x"726from "y", replacing "z".727 728P1()'s line 20 loads a pointer from "y", and line 21 dereferences that729pointer. The RCU read-side critical section spanning lines 19-22 is just730for show in this example. Note that the address used for line 21's load731depends on (in this case, "is exactly the same as") the value loaded by732line 20. This is an example of what is called an "address dependency".733This particular address dependency extends from the load on line 20 to the734load on line 21. Address dependencies provide a weak form of ordering.735 736Running this test results in the following:737 738 1 Test MP+onceassign+derefonce Allowed739 2 States 2740 3 1:r0=x; 1:r1=1;741 4 1:r0=z; 1:r1=0;742 5 No743 6 Witnesses744 7 Positive: 0 Negative: 2745 8 Condition exists (1:r0=x /\ 1:r1=0)746 9 Observation MP+onceassign+derefonce Never 0 274710 Time MP+onceassign+derefonce 0.0074811 Hash=49ef7a741563570102448a256a0c8568749 750The only possible outcomes feature P1() loading a pointer to "z"751(which contains zero) on the one hand and P1() loading a pointer to "x"752(which contains the value one) on the other. This should be reassuring753because it says that RCU readers cannot see the old preinitialization754values when accessing a newly inserted list node. This undesirable755scenario is flagged by the "exists" clause, and would occur if P1()756loaded a pointer to "x", but obtained the pre-initialization value of757zero after dereferencing that pointer.758 759 760Comments761--------762 763Different portions of a litmus test are processed by different parsers,764which has the charming effect of requiring different comment syntax in765different portions of the litmus test. The C-syntax portions use766C-language comments (either "/* */" or "//"), while the other portions767use Ocaml comments "(* *)".768 769The following litmus test illustrates the comment style corresponding770to each syntactic unit of the test:771 772 1 C MP+onceassign+derefonce (* A *)773 2774 3 (* B *)775 4776 5 {777 6 y=z; (* C *)778 7 z=0;779 8 } // D780 978110 // E7821178312 P0(int *x, int **y) // F78413 {78514 WRITE_ONCE(*x, 1); // G78615 rcu_assign_pointer(*y, x);78716 }7881778918 // H7901979120 P1(int *x, int **y)79221 {79322 int *r0;79423 int r1;7952479625 rcu_read_lock();79726 r0 = rcu_dereference(*y);79827 r1 = READ_ONCE(*r0);79928 rcu_read_unlock();80029 }8013080231 // I8033280433 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) (* L *)805 806In short, use C-language comments in the C code and Ocaml comments in807the rest of the litmus test.808 809On the other hand, if you prefer C-style comments everywhere, the810C preprocessor is your friend.811 812 813Asynchronous RCU Grace Periods814------------------------------815 816The following litmus test is derived from the example show in817Documentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted to818emulate call_rcu():819 820 1 C RCU+sync+free821 2822 3 {823 4 int x = 1;824 5 int *y = &x;825 6 int z = 1;826 7 }827 8828 9 P0(int *x, int *z, int **y)82910 {83011 int *r0;83112 int r1;8321383314 rcu_read_lock();83415 r0 = rcu_dereference(*y);83516 r1 = READ_ONCE(*r0);83617 rcu_read_unlock();83718 }8381983920 P1(int *z, int **y, int *c)84021 {84122 rcu_assign_pointer(*y, z);84223 smp_store_release(*c, 1); // Emulate call_rcu().84324 }8442584526 P2(int *x, int *z, int **y, int *c)84627 {84728 int r0;8482984930 r0 = smp_load_acquire(*c); // Note call_rcu() request.85031 synchronize_rcu(); // Wait one grace period.85132 WRITE_ONCE(*x, 0); // Emulate the RCU callback.85233 }8533485435 filter (2:r0=1) (* Reject too-early starts. *)85536 exists (0:r0=x /\ 0:r1=0)856 857Lines 4-6 initialize a linked list headed by "y" that initially contains858"x". In addition, "z" is pre-initialized to prepare for P1(), which859will replace "x" with "z" in this list.860 861P0() on lines 9-18 enters an RCU read-side critical section, loads the862list header "y" and dereferences it, leaving the node in "0:r0" and863the node's value in "0:r1".864 865P1() on lines 20-24 updates the list header to instead reference "z",866then emulates call_rcu() by doing a release store into "c".867 868P2() on lines 27-33 emulates the behind-the-scenes effect of doing a869call_rcu(). Line 30 first does an acquire load from "c", then line 31870waits for an RCU grace period to elapse, and finally line 32 emulates871the RCU callback, which in turn emulates a call to kfree().872 873Of course, it is possible for P2() to start too soon, so that the874value of "2:r0" is zero rather than the required value of "1".875The "filter" clause on line 35 handles this possibility, rejecting876all executions in which "2:r0" is not equal to the value "1".877 878 879Performance880-----------881 882LKMM's exploration of the full state-space can be extremely helpful,883but it does not come for free. The price is exponential computational884complexity in terms of the number of processes, the average number885of statements in each process, and the total number of stores in the886litmus test.887 888So it is best to start small and then work up. Where possible, break889your code down into small pieces each representing a core concurrency890requirement.891 892That said, herd7 is quite fast. On an unprepossessing x86 laptop, it893was able to analyze the following 10-process RCU litmus test in about894six seconds.895 896https://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.litmus897 898One way to make herd7 run faster is to use the "-speedcheck true" option.899This option prevents herd7 from generating all possible end states,900instead causing it to focus solely on whether or not the "exists"901clause can be satisfied. With this option, herd7 evaluates the above902litmus test in about 300 milliseconds, for more than an order of magnitude903improvement in performance.904 905Larger 16-process litmus tests that would normally consume 15 minutes906of time complete in about 40 seconds with this option. To be fair,907you do get an extra 65,535 states when you leave off the "-speedcheck908true" option.909 910https://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.litmus911 912Nevertheless, litmus-test analysis really is of exponential complexity,913whether with or without "-speedcheck true". Increasing by just three914processes to a 19-process litmus test requires 2 hours and 40 minutes915without, and about 8 minutes with "-speedcheck true". Each of these916results represent roughly an order of magnitude slowdown compared to the91716-process litmus test. Again, to be fair, the multi-hour run explores918no fewer than 524,287 additional states compared to the shorter one.919 920https://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.litmus921 922If you don't like command-line arguments, you can obtain a similar speedup923by adding a "filter" clause with exactly the same expression as your924"exists" clause.925 926However, please note that seeing the full set of states can be extremely927helpful when developing and debugging litmus tests.928 929 930LIMITATIONS931===========932 933Limitations of the Linux-kernel memory model (LKMM) include:934 9351. Compiler optimizations are not accurately modeled. Of course,936 the use of READ_ONCE() and WRITE_ONCE() limits the compiler's937 ability to optimize, but under some circumstances it is possible938 for the compiler to undermine the memory model. For more939 information, see Documentation/explanation.txt (in particular,940 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"941 sections).942 943 Note that this limitation in turn limits LKMM's ability to944 accurately model address, control, and data dependencies.945 For example, if the compiler can deduce the value of some variable946 carrying a dependency, then the compiler can break that dependency947 by substituting a constant of that value.948 949 Conversely, LKMM will sometimes overestimate the amount of950 reordering compilers and CPUs can carry out, leading it to miss951 some pretty obvious cases of ordering. A simple example is:952 953 r1 = READ_ONCE(x);954 if (r1 == 0)955 smp_mb();956 WRITE_ONCE(y, 1);957 958 The WRITE_ONCE() does not depend on the READ_ONCE(), and as a959 result, LKMM does not claim ordering. However, even though no960 dependency is present, the WRITE_ONCE() will not be executed before961 the READ_ONCE(). There are two reasons for this:962 963 The presence of the smp_mb() in one of the branches964 prevents the compiler from moving the WRITE_ONCE()965 up before the "if" statement, since the compiler has966 to assume that r1 will sometimes be 0 (but see the967 comment below);968 969 CPUs do not execute stores before po-earlier conditional970 branches, even in cases where the store occurs after the971 two arms of the branch have recombined.972 973 It is clear that it is not dangerous in the slightest for LKMM to974 make weaker guarantees than architectures. In fact, it is975 desirable, as it gives compilers room for making optimizations.976 For instance, suppose that a 0 value in r1 would trigger undefined977 behavior elsewhere. Then a clever compiler might deduce that r1978 can never be 0 in the if condition. As a result, said clever979 compiler might deem it safe to optimize away the smp_mb(),980 eliminating the branch and any ordering an architecture would981 guarantee otherwise.982 9832. Multiple access sizes for a single variable are not supported,984 and neither are misaligned or partially overlapping accesses.985 9863. Exceptions and interrupts are not modeled. In some cases,987 this limitation can be overcome by modeling the interrupt or988 exception with an additional process.989 9904. I/O such as MMIO or DMA is not supported.991 9925. Self-modifying code (such as that found in the kernel's993 alternatives mechanism, function tracer, Berkeley Packet Filter994 JIT compiler, and module loader) is not supported.995 9966. Complete modeling of all variants of atomic read-modify-write997 operations, locking primitives, and RCU is not provided.998 For example, call_rcu() and rcu_barrier() are not supported.999 However, a substantial amount of support is provided for these1000 operations, as shown in the linux-kernel.def file.1001 1002 Here are specific limitations:1003 1004 a. When rcu_assign_pointer() is passed NULL, the Linux1005 kernel provides no ordering, but LKMM models this1006 case as a store release.1007 1008 b. The "unless" RMW operations are not currently modeled:1009 atomic_long_add_unless(), atomic_inc_unless_negative(),1010 and atomic_dec_unless_positive(). These can be emulated1011 in litmus tests, for example, by using atomic_cmpxchg().1012 1013 One exception of this limitation is atomic_add_unless(),1014 which is provided directly by herd7 (so no corresponding1015 definition in linux-kernel.def). atomic_add_unless() is1016 modeled by herd7 therefore it can be used in litmus tests.1017 1018 c. The call_rcu() function is not modeled. As was shown above,1019 it can be emulated in litmus tests by adding another1020 process that invokes synchronize_rcu() and the body of the1021 callback function, with (for example) a release-acquire1022 from the site of the emulated call_rcu() to the beginning1023 of the additional process.1024 1025 d. The rcu_barrier() function is not modeled. It can be1026 emulated in litmus tests emulating call_rcu() via1027 (for example) a release-acquire from the end of each1028 additional call_rcu() process to the site of the1029 emulated rcu-barrier().1030 1031 e. Reader-writer locking is not modeled. It can be1032 emulated in litmus tests using atomic read-modify-write1033 operations.1034 1035The fragment of the C language supported by these litmus tests is quite1036limited and in some ways non-standard:1037 10381. There is no automatic C-preprocessor pass. You can of course1039 run it manually, if you choose.1040 10412. There is no way to create functions other than the Pn() functions1042 that model the concurrent processes.1043 10443. The Pn() functions' formal parameters must be pointers to the1045 global shared variables. Nothing can be passed by value into1046 these functions.1047 10484. The only functions that can be invoked are those built directly1049 into herd7 or that are defined in the linux-kernel.def file.1050 10515. The "switch", "do", "for", "while", and "goto" C statements are1052 not supported. The "switch" statement can be emulated by the1053 "if" statement. The "do", "for", and "while" statements can1054 often be emulated by manually unrolling the loop, or perhaps by1055 enlisting the aid of the C preprocessor to minimize the resulting1056 code duplication. Some uses of "goto" can be emulated by "if",1057 and some others by unrolling.1058 10596. Although you can use a wide variety of types in litmus-test1060 variable declarations, and especially in global-variable1061 declarations, the "herd7" tool understands only int and1062 pointer types. There is no support for floating-point types,1063 enumerations, characters, strings, arrays, or structures.1064 10657. Parsing of variable declarations is very loose, with almost no1066 type checking.1067 10688. Initializers differ from their C-language counterparts.1069 For example, when an initializer contains the name of a shared1070 variable, that name denotes a pointer to that variable, not1071 the current value of that variable. For example, "int x = y"1072 is interpreted the way "int x = &y" would be in C.1073 10749. Dynamic memory allocation is not supported, although this can1075 be worked around in some cases by supplying multiple statically1076 allocated variables.1077 1078Some of these limitations may be overcome in the future, but others are1079more likely to be addressed by incorporating the Linux-kernel memory model1080into other tools.1081 1082Finally, please note that LKMM is subject to change as hardware, use cases,1083and compilers evolve.1084