linux/tools/memory-model/Documentation/litmus-tests.txt
<<
>>
Prefs
   1Linux-Kernel Memory Model Litmus Tests
   2======================================
   3
   4This file describes the LKMM litmus-test format by example, describes
   5some tricks and traps, and finally outlines LKMM's limitations.  Earlier
   6versions 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 instructions
  12https://lwn.net/Articles/470681/
  13        Validating Memory Barriers and Atomic Instructions
  14
  15This document presents information in decreasing order of applicability,
  16so that, where possible, the information that has proven more commonly
  17useful 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-Pasta
  24==========
  25
  26As with other software, it is often better (if less macho) to adapt an
  27existing litmus test than it is to create one from scratch.  A number
  28of 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 github
  34and kernel.org:
  35
  36        https://github.com/paulmckrcu/litmus
  37        https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
  38        https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
  39
  40The -l and -L arguments to "git grep" can be quite helpful in identifying
  41existing litmus tests that are similar to the one you need.  But even if
  42you start with an existing litmus test, it is still helpful to have a
  43good understanding of the litmus-test format.
  44
  45
  46Examples and Format
  47===================
  48
  49This section describes the overall format of litmus tests, starting
  50with a small example of the message-passing pattern and moving on to
  51more complex examples that illustrate explicit initialization and LKMM's
  52minimalistic set of flow-control statements.
  53
  54
  55Message-Passing Example
  56-----------------------
  57
  58This section gives an overview of the format of a litmus test using an
  59example based on the common message-passing use case.  This use case
  60appears often in the Linux kernel.  For example, a flag (modeled by "y"
  61below) indicates that a buffer (modeled by "x" below) is now completely
  62filled in and ready for use.  It would be very bad if the consumer saw the
  63flag 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+poacquireonce
  69 2
  70 3 {}
  71 4
  72 5 P0(int *x, int *y)
  73 6 {
  74 7   WRITE_ONCE(*x, 1);
  75 8   smp_store_release(y, 1);
  76 9 }
  7710
  7811 P1(int *x, int *y)
  7912 {
  8013   int r0;
  8114   int r1;
  8215
  8316   r0 = smp_load_acquire(y);
  8417   r1 = READ_ONCE(*x);
  8518 }
  8619
  8720 exists (1:r0=1 /\ 1:r1=0)
  88
  89Line 1 starts with "C", which identifies this file as being in the
  90LKMM C-language format (which, as we will see, is a small fragment
  91of the full C language).  The remainder of line 1 is the name of
  92the test, which by convention is the filename with the ".litmus"
  93suffix stripped.  In this case, the actual test may be found in
  94tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
  95in the Linux-kernel source tree.
  96
  97Mechanically generated litmus tests will often have an optional
  98double-quoted comment string on the second line.  Such strings are ignored
  99when running the test.  Yes, you can add your own comments to litmus
 100tests, 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 comments
 102may be in either the "/* */" or the "//" style.  A later section will
 103cover the full litmus-test commenting story.
 104
 105Line 3 is the initialization section.  Because the default initialization
 106to zero suffices for this test, the "{}" syntax is used, which mean the
 107initialization section is empty.  Litmus tests requiring non-default
 108initialization must have non-empty initialization sections, as in the
 109example that will be presented later in this document.
 110
 111Lines 5-9 show the first process and lines 11-18 the second process.  Each
 112process 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 consist
 116of a single "P" followed by a number, and as long as the numbers are
 117consecutive 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 variables
 122used by that function.  Unlike normal C-language function parameters, the
 123names are significant.  The fact that both P0() and P1() have a formal
 124parameter named "x" means that these two processes are working with the
 125same global variable, also named "x".  So the "int *x, int *y" on P0()
 126and P1() mean that both processes are working with two shared global
 127variables, "x" and "y".  Global variables are always passed to processes
 128by 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 from
 132other litmus-test formats, it is conventional to use names consisting of
 133"r" followed by a number as shown here.  A common bug in litmus tests
 134is forgetting to add a global variable to a process's parameter list.
 135This will sometimes result in an error message, but can also cause the
 136intended global to instead be silently treated as an undeclared local
 137variable.
 138
 139Each process's code is similar to Linux-kernel C, as can be seen on lines
 1407-8 and 13-17.  This code may use many of the Linux kernel's atomic
 141operations, some of its exclusive-lock functions, and some of its RCU
 142and SRCU functions.  An approximate list of the currently supported
 143functions may be found in the linux-kernel.def file.
 144
 145The P0() process does "WRITE_ONCE(*x, 1)" on line 7.  Because "x" is a
 146pointer in P0()'s parameter list, this does an unordered store to global
 147variable "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 global
 149variable "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 load
 153from global variable "y" into local variable "r0".  Line 17 does a
 154"r1 = READ_ONCE(*x)", which does an unordered load from "*x" into local
 155variable "r1".  Both "x" and "y" are in P1()'s parameter list, so both
 156reference 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 processes
 160have completed and all of their memory references and memory barriers
 161have propagated to all parts of the system.  The references to the local
 162variables "r0" and "r1" in line 24 must be prefixed with "1:" to specify
 163which process they are local to.
 164
 165Note that the assertion expression is written in the litmus-test
 166language rather than in C.  For example, single "=" is an equality
 167operator rather than an assignment.  The "/\" character combination means
 168"and".  Similarly, "\/" stands for "or".  Both of these are ASCII-art
 169representations of the corresponding mathematical symbols.  Finally,
 170"~" stands for "logical not", which is "!" in C, and not to be confused
 171with 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 the
 175flag ("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, which
 180absolutely must be run from the tools/memory-model directory and from
 181this directory only:
 182
 183herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus
 184
 185The output is the result of something similar to a full state-space
 186search, and is as follows:
 187
 188 1 Test MP+pooncerelease+poacquireonce Allowed
 189 2 States 3
 190 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 No
 194 7 Witnesses
 195 8 Positive: 0 Negative: 3
 196 9 Condition exists (1:r0=1 /\ 1:r1=0)
 19710 Observation MP+pooncerelease+poacquireonce Never 0 3
 19811 Time MP+pooncerelease+poacquireonce 0.00
 19912 Hash=579aaa14d8c35a39429b02e698241d09
 200
 201The most pertinent line is line 10, which contains "Never 0 3", which
 202indicates that the bad result flagged by the "exists" clause never
 203happens.  This line might instead say "Sometimes" to indicate that the
 204bad result happened in some but not all executions, or it might say
 205"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 the
 207"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 end
 209of 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 3
 215 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 list
 220one of these states, with the first ("1:r0=0; 1:r1=0;") indicating that
 221both of P1()'s loads returned the value "0".  As expected, given the
 222"Never" on line 10, the state flagged by the "exists" clause is not
 223listed.  This full list of states can be helpful when debugging a new
 224litmus test.
 225
 226The rest of the output is not normally needed, either due to irrelevance
 227or due to being redundant with the lines discussed above.  However, the
 228following paragraph lists them for the benefit of readers possessed of
 229an 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's
 232"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 a
 234lead-in to line 8's "Positive: 0 Negative: 3", which lists the number
 235of end states satisfying and not satisfying the "exists" clause, just
 236like 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 the
 239time in seconds required to analyze the litmus test.  Small tests such
 240as 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 used
 242by tooling that manages litmus tests and their output.  This tooling is
 243used by people modifying LKMM itself, and among other things lets such
 244people know which of the several thousand relevant litmus tests were
 245affected by a given change to LKMM.
 246
 247
 248Initialization
 249--------------
 250
 251The previous example relied on the default zero initialization for
 252"x" and "y", but a similar litmus test could instead initialize them
 253to some other value:
 254
 255 1 C MP+pooncerelease+poacquireonce
 256 2
 257 3 {
 258 4   x=42;
 259 5   y=42;
 260 6 }
 261 7
 262 8 P0(int *x, int *y)
 263 9 {
 26410   WRITE_ONCE(*x, 1);
 26511   smp_store_release(y, 1);
 26612 }
 26713
 26814 P1(int *x, int *y)
 26915 {
 27016   int r0;
 27117   int r1;
 27218
 27319   r0 = smp_load_acquire(y);
 27420   r1 = READ_ONCE(*x);
 27521 }
 27622
 27723 exists (1:r0=1 /\ 1:r1=42)
 278
 279Lines 3-6 now initialize both "x" and "y" to the value 42.  This also
 280means that the "exists" clause on line 23 must change "1:r1=0" to
 281"1:r1=42".
 282
 283Running the test gives the same overall result as before, but with the
 284value 42 appearing in place of the value zero:
 285
 286 1 Test MP+pooncerelease+poacquireonce Allowed
 287 2 States 3
 288 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 No
 292 7 Witnesses
 293 8 Positive: 0 Negative: 3
 294 9 Condition exists (1:r0=1 /\ 1:r1=42)
 29510 Observation MP+pooncerelease+poacquireonce Never 0 3
 29611 Time MP+pooncerelease+poacquireonce 0.02
 29712 Hash=ab9a9b7940a75a792266be279a980156
 298
 299It is tempting to avoid the open-coded repetitions of the value "42"
 300by defining another global variable "initval=42" and replacing all
 301occurrences 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 about
 304why this approach to initialization can be useful.
 305
 306
 307Control Structures
 308------------------
 309
 310LKMM supports the C-language "if" statement, which allows modeling of
 311conditional branches.  In LKMM, conditional branches can affect ordering,
 312but only if you are *very* careful (compilers are surprisingly able
 313to optimize away conditional branches).  The following example shows
 314the "load buffering" (LB) use case that is used in the Linux kernel to
 315synchronize between ring-buffer producers and consumers.  In the example
 316below, P0() is one side checking to see if an operation may proceed and
 317P1() is the other side completing its update.
 318
 319 1 C LB+fencembonceonce+ctrlonceonce
 320 2
 321 3 {}
 322 4
 323 5 P0(int *x, int *y)
 324 6 {
 325 7   int r0;
 326 8
 327 9   r0 = READ_ONCE(*x);
 32810   if (r0)
 32911     WRITE_ONCE(*y, 1);
 33012 }
 33113
 33214 P1(int *x, int *y)
 33315 {
 33416   int r0;
 33517
 33618   r0 = READ_ONCE(*y);
 33719   smp_mb();
 33820   WRITE_ONCE(*x, 1);
 33921 }
 34022
 34123 exists (0:r0=1 /\ 1:r0=1)
 342
 343P1()'s "if" statement on line 10 works as expected, so that line 11 is
 344executed only if line 9 loads a non-zero value from "x".  Because P1()'s
 345write of "1" to "x" happens only after P1()'s read from "y", one would
 346hope that the "exists" clause cannot be satisfied.  LKMM agrees:
 347
 348 1 Test LB+fencembonceonce+ctrlonceonce Allowed
 349 2 States 2
 350 3 0:r0=0; 1:r0=0;
 351 4 0:r0=1; 1:r0=0;
 352 5 No
 353 6 Witnesses
 354 7 Positive: 0 Negative: 2
 355 8 Condition exists (0:r0=1 /\ 1:r0=1)
 356 9 Observation LB+fencembonceonce+ctrlonceonce Never 0 2
 35710 Time LB+fencembonceonce+ctrlonceonce 0.00
 35811 Hash=e5260556f6de495fd39b556d1b831c3b
 359
 360However, there is no "while" statement due to the fact that full
 361state-space search has some difficulty with iteration.  However, there
 362are tricks that may be used to handle some special cases, which are
 363discussed below.  In addition, loop-unrolling tricks may be applied,
 364albeit sparingly.
 365
 366
 367Tricks and Traps
 368================
 369
 370This section covers extracting debug output from herd7, emulating
 371spin loops, handling trivial linked lists, adding comments to litmus tests,
 372emulating call_rcu(), and finally tricks to improve herd7 performance
 373in order to better handle large litmus tests.
 374
 375
 376Debug Output
 377------------
 378
 379By default, the herd7 state output includes all variables mentioned
 380in the "exists" clause.  But sometimes debugging efforts are greatly
 381aided by the values of other variables.  Consider this litmus test
 382(tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
 383slightly modified), which probes an obscure corner of hardware memory
 384ordering:
 385
 386 1 C SB+rfionceonce-poonceonces
 387 2
 388 3 {}
 389 4
 390 5 P0(int *x, int *y)
 391 6 {
 392 7   int r1;
 393 8   int r2;
 394 9
 39510   WRITE_ONCE(*x, 1);
 39611   r1 = READ_ONCE(*x);
 39712   r2 = READ_ONCE(*y);
 39813 }
 39914
 40015 P1(int *x, int *y)
 40116 {
 40217   int r3;
 40318   int r4;
 40419
 40520   WRITE_ONCE(*y, 1);
 40621   r3 = READ_ONCE(*y);
 40722   r4 = READ_ONCE(*x);
 40823 }
 40924
 41025 exists (0:r2=0 /\ 1:r4=0)
 411
 412The herd7 output is as follows:
 413
 414 1 Test SB+rfionceonce-poonceonces Allowed
 415 2 States 4
 416 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 Ok
 421 8 Witnesses
 422 9 Positive: 1 Negative: 3
 42310 Condition exists (0:r2=0 /\ 1:r4=0)
 42411 Observation SB+rfionceonce-poonceonces Sometimes 1 3
 42512 Time SB+rfionceonce-poonceonces 0.01
 42613 Hash=c7f30fe0faebb7d565405d55b7318ada
 427
 428(This output indicates that CPUs are permitted to "snoop their own
 429store buffers", which all of Linux's CPU families other than s390 will
 430happily do.  Such snooping results in disagreement among CPUs on the
 431order of stores from different CPUs, which is rarely an issue.)
 432
 433But the herd7 output shows only the two variables mentioned in the
 434"exists" clause.  Someone modifying this test might wish to know the
 435values of "x", "y", "0:r1", and "0:r3" as well.  The "locations"
 436statement on line 25 shows how to cause herd7 to display additional
 437variables:
 438
 439 1 C SB+rfionceonce-poonceonces
 440 2
 441 3 {}
 442 4
 443 5 P0(int *x, int *y)
 444 6 {
 445 7   int r1;
 446 8   int r2;
 447 9
 44810   WRITE_ONCE(*x, 1);
 44911   r1 = READ_ONCE(*x);
 45012   r2 = READ_ONCE(*y);
 45113 }
 45214
 45315 P1(int *x, int *y)
 45416 {
 45517   int r3;
 45618   int r4;
 45719
 45820   WRITE_ONCE(*y, 1);
 45921   r3 = READ_ONCE(*y);
 46022   r4 = READ_ONCE(*x);
 46123 }
 46224
 46325 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 Allowed
 469 2 States 4
 470 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 Ok
 475 8 Witnesses
 476 9 Positive: 1 Negative: 3
 47710 Condition exists (0:r2=0 /\ 1:r4=0)
 47811 Observation SB+rfionceonce-poonceonces Sometimes 1 3
 47912 Time SB+rfionceonce-poonceonces 0.01
 48013 Hash=40de8418c4b395388f6501cafd1ed38d
 481
 482What if you would like to know the value of a particular global variable
 483at some particular point in a given process's execution?  One approach
 484is to use a READ_ONCE() to load that global variable into a new local
 485variable, then add that local variable to the "locations" clause.
 486But be careful:  In some litmus tests, adding a READ_ONCE() will change
 487the outcome!  For one example, please see the C-READ_ONCE.litmus and
 488C-READ_ONCE-omitted.litmus tests located here:
 489
 490        https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/
 491
 492
 493Spin Loops
 494----------
 495
 496The analysis carried out by herd7 explores full state space, which is
 497at best of exponential time complexity.  Adding processes and increasing
 498the amount of code in a give process can greatly increase execution time.
 499Potentially infinite loops, such as those used to wait for locks to
 500become available, are clearly problematic.
 501
 502Fortunately, it is possible to avoid state-space explosion by specially
 503modeling such loops.  For example, the following litmus tests emulates
 504locking using xchg_acquire(), but instead of enclosing xchg_acquire()
 505in a spin loop, it instead excludes executions that fail to acquire the
 506lock using a herd7 "filter" clause.  Note that for exclusive locking, you
 507are better off using the spin_lock() and spin_unlock() that LKMM directly
 508models, if for no other reason that these are much faster.  However, the
 509techniques 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-X
 513 2
 514 3 {
 515 4 }
 516 5
 517 6 P0(int *sl, int *x0, int *x1)
 518 7 {
 519 8   int r2;
 520 9   int r1;
 52110
 52211   r2 = xchg_acquire(sl, 1);
 52312   WRITE_ONCE(*x0, 1);
 52413   r1 = READ_ONCE(*x1);
 52514   smp_store_release(sl, 0);
 52615 }
 52716
 52817 P1(int *sl, int *x0, int *x1)
 52918 {
 53019   int r2;
 53120   int r1;
 53221
 53322   r2 = xchg_acquire(sl, 1);
 53423   WRITE_ONCE(*x1, 1);
 53524   r1 = READ_ONCE(*x0);
 53625   smp_store_release(sl, 0);
 53726 }
 53827
 53928 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.litmus
 545
 546This test uses two global variables, "x1" and "x2", and also emulates a
 547single global spinlock named "sl".  This spinlock is held by whichever
 548process changes the value of "sl" from "0" to "1", and is released when
 549that process sets "sl" back to "0".  P0()'s lock acquisition is emulated
 550on line 11 using xchg_acquire(), which unconditionally stores the value
 551"1" to "sl" and stores either "0" or "1" to "r2", depending on whether
 552the lock acquisition was successful or unsuccessful (due to "sl" already
 553having the value "1"), respectively.  P1() operates in a similar manner.
 554
 555Rather unconventionally, execution appears to proceed to the critical
 556section on lines 12 and 13 in either case.  Line 14 then uses an
 557smp_store_release() to store zero to "sl", thus emulating lock release.
 558
 559The case where xchg_acquire() fails to acquire the lock is handled by
 560the "filter" clause on line 28, which tells herd7 to keep only those
 561executions in which both "0:r2" and "1:r2" are zero, that is to pay
 562attention only to those executions in which both locks are actually
 563acquired.  Thus, the bogus executions that would execute the critical
 564sections are discarded and any effects that they might have had are
 565ignored.  Note well that the "filter" clause keeps those executions
 566for which its expression is satisfied, that is, for which the expression
 567evaluates to true.  In other words, the "filter" clause says what to
 568keep, 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 Allowed
 573 2 States 2
 574 3 0:r1=0; 1:r1=1;
 575 4 0:r1=1; 1:r1=0;
 576 5 No
 577 6 Witnesses
 578 7 Positive: 0 Negative: 2
 579 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 2
 58110 Time C-SB+l-o-o-u+l-o-o-u-X 0.03
 582
 583The "Never" on line 9 indicates that this use of xchg_acquire() and
 584smp_store_release() really does correctly emulate locking.
 585
 586Why doesn't the litmus test take the simpler approach of using a spin loop
 587to handle failed spinlock acquisitions, like the kernel does?  The key
 588insight behind this litmus test is that spin loops have no effect on the
 589possible "exists"-clause outcomes of program execution in the absence
 590of deadlock.  In other words, given a high-quality lock-acquisition
 591primitive in a deadlock-free program running on high-quality hardware,
 592each lock acquisition will eventually succeed.  Because herd7 already
 593explores the full state space, the length of time required to actually
 594acquire the lock does not matter.  After all, herd7 already models all
 595possible durations of the xchg_acquire() statements.
 596
 597Why not just add the "filter" clause to the "exists" clause, thus
 598avoiding 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" expression
 601fails to be satisfied.  In contrast, the "exists" clause is evaluated
 602only at the end of time, thus requiring herd7 to waste time on bogus
 603executions in which both critical sections proceed concurrently.  In
 604addition, some LKMM users like the separation of concerns provided by
 605using the both the "filter" and "exists" clauses.
 606
 607Readers lacking a pathological interest in odd corner cases should feel
 608free to skip the remainder of this section.
 609
 610But what if the litmus test were to temporarily set "0:r2" to a non-zero
 611value?  Wouldn't that cause herd7 to abandon the execution prematurely
 612due to an early mismatch of the "filter" clause?
 613
 614Why not just try it?  Line 4 of the following modified litmus test
 615introduces a new global variable "x2" that is initialized to "1".  Line 23
 616of P1() reads that variable into "1:r2" to force an early mismatch with
 617the "filter" clause.  Line 24 does a known-true "if" condition to avoid
 618and static analysis that herd7 might do.  Finally the "exists" clause
 619on line 32 is updated to a condition that is alway satisfied at the end
 620of the test.
 621
 622 1 C C-SB+l-o-o-u+l-o-o-u-X
 623 2
 624 3 {
 625 4   x2=1;
 626 5 }
 627 6
 628 7 P0(int *sl, int *x0, int *x1)
 629 8 {
 630 9   int r2;
 63110   int r1;
 63211
 63312   r2 = xchg_acquire(sl, 1);
 63413   WRITE_ONCE(*x0, 1);
 63514   r1 = READ_ONCE(*x1);
 63615   smp_store_release(sl, 0);
 63716 }
 63817
 63918 P1(int *sl, int *x0, int *x1, int *x2)
 64019 {
 64120   int r2;
 64221   int r1;
 64322
 64423   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 }
 65130
 65231 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 the
 656execution, running this litmus test would display no executions because
 657all executions would be filtered out at line 23.  However, the output
 658is instead as follows:
 659
 660 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
 661 2 States 1
 662 3 x1=1;
 663 4 Ok
 664 5 Witnesses
 665 6 Positive: 2 Negative: 0
 666 7 Condition exists (x1=1)
 667 8 Observation C-SB+l-o-o-u+l-o-o-u-X Always 2 0
 668 9 Time C-SB+l-o-o-u+l-o-o-u-X 0.04
 66910 Hash=080bc508da7f291e122c6de76c0088e3
 670
 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 to
 673the variables that it checks.  In this case, the "filter" clause is a
 674disjunction, 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 Lists
 679------------
 680
 681LKMM can handle linked lists, but only linked lists in which each node
 682contains nothing except a pointer to the next node in the list.  This is
 683of course quite restrictive, but there is nevertheless quite a bit that
 684can be done within these confines, as can be seen in the litmus test
 685at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
 686
 687 1 C MP+onceassign+derefonce
 688 2
 689 3 {
 690 4 y=z;
 691 5 z=0;
 692 6 }
 693 7
 694 8 P0(int *x, int **y)
 695 9 {
 69610   WRITE_ONCE(*x, 1);
 69711   rcu_assign_pointer(*y, x);
 69812 }
 69913
 70014 P1(int *x, int **y)
 70115 {
 70216   int *r0;
 70317   int r1;
 70418
 70519   rcu_read_lock();
 70620   r0 = rcu_dereference(*y);
 70721   r1 = READ_ONCE(*r0);
 70822   rcu_read_unlock();
 70923 }
 71024
 71125 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 instead
 715sets the value of "y" to the *address* of "z".  Lines 4 and 5 therefore
 716create a simple linked list, with "y" pointing to "z" and "z" having a
 717NULL 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()'s
 721"r0" not to the value of "x", but again to its address.  This term of the
 722"exists" clause therefore tests whether line 20's load from "y" saw the
 723value 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 that
 729pointer.  The RCU read-side critical section spanning lines 19-22 is just
 730for show in this example.  Note that the address used for line 21's load
 731depends on (in this case, "is exactly the same as") the value loaded by
 732line 20.  This is an example of what is called an "address dependency".
 733This particular address dependency extends from the load on line 20 to the
 734load 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 Allowed
 739 2 States 2
 740 3 1:r0=x; 1:r1=1;
 741 4 1:r0=z; 1:r1=0;
 742 5 No
 743 6 Witnesses
 744 7 Positive: 0 Negative: 2
 745 8 Condition exists (1:r0=x /\ 1:r1=0)
 746 9 Observation MP+onceassign+derefonce Never 0 2
 74710 Time MP+onceassign+derefonce 0.00
 74811 Hash=49ef7a741563570102448a256a0c8568
 749
 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 reassuring
 753because it says that RCU readers cannot see the old preinitialization
 754values when accessing a newly inserted list node.  This undesirable
 755scenario is flagged by the "exists" clause, and would occur if P1()
 756loaded a pointer to "x", but obtained the pre-initialization value of
 757zero after dereferencing that pointer.
 758
 759
 760Comments
 761--------
 762
 763Different portions of a litmus test are processed by different parsers,
 764which has the charming effect of requiring different comment syntax in
 765different portions of the litmus test.  The C-syntax portions use
 766C-language comments (either "/* */" or "//"), while the other portions
 767use Ocaml comments "(* *)".
 768
 769The following litmus test illustrates the comment style corresponding
 770to each syntactic unit of the test:
 771
 772 1 C MP+onceassign+derefonce (* A *)
 773 2
 774 3 (* B *)
 775 4
 776 5 {
 777 6 y=z; (* C *)
 778 7 z=0;
 779 8 } // D
 780 9
 78110 // E
 78211
 78312 P0(int *x, int **y) // F
 78413 {
 78514   WRITE_ONCE(*x, 1);  // G
 78615   rcu_assign_pointer(*y, x);
 78716 }
 78817
 78918 // H
 79019
 79120 P1(int *x, int **y)
 79221 {
 79322   int *r0;
 79423   int r1;
 79524
 79625   rcu_read_lock();
 79726   r0 = rcu_dereference(*y);
 79827   r1 = READ_ONCE(*r0);
 79928   rcu_read_unlock();
 80029 }
 80130
 80231 // I
 80332
 80433 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) (* L *)
 805
 806In short, use C-language comments in the C code and Ocaml comments in
 807the rest of the litmus test.
 808
 809On the other hand, if you prefer C-style comments everywhere, the
 810C preprocessor is your friend.
 811
 812
 813Asynchronous RCU Grace Periods
 814------------------------------
 815
 816The following litmus test is derived from the example show in
 817Documentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted to
 818emulate call_rcu():
 819
 820 1 C RCU+sync+free
 821 2
 822 3 {
 823 4 int x = 1;
 824 5 int *y = &x;
 825 6 int z = 1;
 826 7 }
 827 8
 828 9 P0(int *x, int *z, int **y)
 82910 {
 83011   int *r0;
 83112   int r1;
 83213
 83314   rcu_read_lock();
 83415   r0 = rcu_dereference(*y);
 83516   r1 = READ_ONCE(*r0);
 83617   rcu_read_unlock();
 83718 }
 83819
 83920 P1(int *z, int **y, int *c)
 84021 {
 84122   rcu_assign_pointer(*y, z);
 84223   smp_store_release(*c, 1); // Emulate call_rcu().
 84324 }
 84425
 84526 P2(int *x, int *z, int **y, int *c)
 84627 {
 84728   int r0;
 84829
 84930   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 }
 85334
 85435 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 contains
 858"x".  In addition, "z" is pre-initialized to prepare for P1(), which
 859will replace "x" with "z" in this list.
 860
 861P0() on lines 9-18 enters an RCU read-side critical section, loads the
 862list header "y" and dereferences it, leaving the node in "0:r0" and
 863the 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 a
 869call_rcu().  Line 30 first does an acquire load from "c", then line 31
 870waits for an RCU grace period to elapse, and finally line 32 emulates
 871the RCU callback, which in turn emulates a call to kfree().
 872
 873Of course, it is possible for P2() to start too soon, so that the
 874value of "2:r0" is zero rather than the required value of "1".
 875The "filter" clause on line 35 handles this possibility, rejecting
 876all executions in which "2:r0" is not equal to the value "1".
 877
 878
 879Performance
 880-----------
 881
 882LKMM's exploration of the full state-space can be extremely helpful,
 883but it does not come for free.  The price is exponential computational
 884complexity in terms of the number of processes, the average number
 885of statements in each process, and the total number of stores in the
 886litmus test.
 887
 888So it is best to start small and then work up.  Where possible, break
 889your code down into small pieces each representing a core concurrency
 890requirement.
 891
 892That said, herd7 is quite fast.  On an unprepossessing x86 laptop, it
 893was able to analyze the following 10-process RCU litmus test in about
 894six 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.litmus
 897
 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 above
 902litmus test in about 300 milliseconds, for more than an order of magnitude
 903improvement in performance.
 904
 905Larger 16-process litmus tests that would normally consume 15 minutes
 906of 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 "-speedcheck
 908true" 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.litmus
 911
 912Nevertheless, litmus-test analysis really is of exponential complexity,
 913whether with or without "-speedcheck true".  Increasing by just three
 914processes to a 19-process litmus test requires 2 hours and 40 minutes
 915without, and about 8 minutes with "-speedcheck true".  Each of these
 916results represent roughly an order of magnitude slowdown compared to the
 91716-process litmus test.  Again, to be fair, the multi-hour run explores
 918no 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.litmus
 921
 922If you don't like command-line arguments, you can obtain a similar speedup
 923by adding a "filter" clause with exactly the same expression as your
 924"exists" clause.
 925
 926However, please note that seeing the full set of states can be extremely
 927helpful when developing and debugging litmus tests.
 928
 929
 930LIMITATIONS
 931===========
 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's
 937        ability to optimize, but under some circumstances it is possible
 938        for the compiler to undermine the memory model.  For more
 939        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 to
 944        accurately model address, control, and data dependencies.
 945        For example, if the compiler can deduce the value of some variable
 946        carrying a dependency, then the compiler can break that dependency
 947        by substituting a constant of that value.
 948
 949        Conversely, LKMM sometimes doesn't recognize that a particular
 950        optimization is not allowed, and as a result, thinks that a
 951        dependency is not present (because the optimization would break it).
 952        The memory model misses some pretty obvious control dependencies
 953        because of this limitation.  A simple example is:
 954
 955                r1 = READ_ONCE(x);
 956                if (r1 == 0)
 957                        smp_mb();
 958                WRITE_ONCE(y, 1);
 959
 960        There is a control dependency from the READ_ONCE to the WRITE_ONCE,
 961        even when r1 is nonzero, but LKMM doesn't realize this and thinks
 962        that the write may execute before the read if r1 != 0.  (Yes, that
 963        doesn't make sense if you think about it, but the memory model's
 964        intelligence is limited.)
 965
 9662.      Multiple access sizes for a single variable are not supported,
 967        and neither are misaligned or partially overlapping accesses.
 968
 9693.      Exceptions and interrupts are not modeled.  In some cases,
 970        this limitation can be overcome by modeling the interrupt or
 971        exception with an additional process.
 972
 9734.      I/O such as MMIO or DMA is not supported.
 974
 9755.      Self-modifying code (such as that found in the kernel's
 976        alternatives mechanism, function tracer, Berkeley Packet Filter
 977        JIT compiler, and module loader) is not supported.
 978
 9796.      Complete modeling of all variants of atomic read-modify-write
 980        operations, locking primitives, and RCU is not provided.
 981        For example, call_rcu() and rcu_barrier() are not supported.
 982        However, a substantial amount of support is provided for these
 983        operations, as shown in the linux-kernel.def file.
 984
 985        Here are specific limitations:
 986
 987        a.      When rcu_assign_pointer() is passed NULL, the Linux
 988                kernel provides no ordering, but LKMM models this
 989                case as a store release.
 990
 991        b.      The "unless" RMW operations are not currently modeled:
 992                atomic_long_add_unless(), atomic_inc_unless_negative(),
 993                and atomic_dec_unless_positive().  These can be emulated
 994                in litmus tests, for example, by using atomic_cmpxchg().
 995
 996                One exception of this limitation is atomic_add_unless(),
 997                which is provided directly by herd7 (so no corresponding
 998                definition in linux-kernel.def).  atomic_add_unless() is
 999                modeled by herd7 therefore it can be used in litmus tests.
1000
1001        c.      The call_rcu() function is not modeled.  As was shown above,
1002                it can be emulated in litmus tests by adding another
1003                process that invokes synchronize_rcu() and the body of the
1004                callback function, with (for example) a release-acquire
1005                from the site of the emulated call_rcu() to the beginning
1006                of the additional process.
1007
1008        d.      The rcu_barrier() function is not modeled.  It can be
1009                emulated in litmus tests emulating call_rcu() via
1010                (for example) a release-acquire from the end of each
1011                additional call_rcu() process to the site of the
1012                emulated rcu-barrier().
1013
1014        e.      Although sleepable RCU (SRCU) is now modeled, there
1015                are some subtle differences between its semantics and
1016                those in the Linux kernel.  For example, the kernel
1017                might interpret the following sequence as two partially
1018                overlapping SRCU read-side critical sections:
1019
1020                         1  r1 = srcu_read_lock(&my_srcu);
1021                         2  do_something_1();
1022                         3  r2 = srcu_read_lock(&my_srcu);
1023                         4  do_something_2();
1024                         5  srcu_read_unlock(&my_srcu, r1);
1025                         6  do_something_3();
1026                         7  srcu_read_unlock(&my_srcu, r2);
1027
1028                In contrast, LKMM will interpret this as a nested pair of
1029                SRCU read-side critical sections, with the outer critical
1030                section spanning lines 1-7 and the inner critical section
1031                spanning lines 3-5.
1032
1033                This difference would be more of a concern had anyone
1034                identified a reasonable use case for partially overlapping
1035                SRCU read-side critical sections.  For more information
1036                on the trickiness of such overlapping, please see:
1037                https://paulmck.livejournal.com/40593.html
1038
1039        f.      Reader-writer locking is not modeled.  It can be
1040                emulated in litmus tests using atomic read-modify-write
1041                operations.
1042
1043The fragment of the C language supported by these litmus tests is quite
1044limited and in some ways non-standard:
1045
10461.      There is no automatic C-preprocessor pass.  You can of course
1047        run it manually, if you choose.
1048
10492.      There is no way to create functions other than the Pn() functions
1050        that model the concurrent processes.
1051
10523.      The Pn() functions' formal parameters must be pointers to the
1053        global shared variables.  Nothing can be passed by value into
1054        these functions.
1055
10564.      The only functions that can be invoked are those built directly
1057        into herd7 or that are defined in the linux-kernel.def file.
1058
10595.      The "switch", "do", "for", "while", and "goto" C statements are
1060        not supported.  The "switch" statement can be emulated by the
1061        "if" statement.  The "do", "for", and "while" statements can
1062        often be emulated by manually unrolling the loop, or perhaps by
1063        enlisting the aid of the C preprocessor to minimize the resulting
1064        code duplication.  Some uses of "goto" can be emulated by "if",
1065        and some others by unrolling.
1066
10676.      Although you can use a wide variety of types in litmus-test
1068        variable declarations, and especially in global-variable
1069        declarations, the "herd7" tool understands only int and
1070        pointer types.  There is no support for floating-point types,
1071        enumerations, characters, strings, arrays, or structures.
1072
10737.      Parsing of variable declarations is very loose, with almost no
1074        type checking.
1075
10768.      Initializers differ from their C-language counterparts.
1077        For example, when an initializer contains the name of a shared
1078        variable, that name denotes a pointer to that variable, not
1079        the current value of that variable.  For example, "int x = y"
1080        is interpreted the way "int x = &y" would be in C.
1081
10829.      Dynamic memory allocation is not supported, although this can
1083        be worked around in some cases by supplying multiple statically
1084        allocated variables.
1085
1086Some of these limitations may be overcome in the future, but others are
1087more likely to be addressed by incorporating the Linux-kernel memory model
1088into other tools.
1089
1090Finally, please note that LKMM is subject to change as hardware, use cases,
1091and compilers evolve.
1092