Adding SRCU to the Linux-Kernel Memory Model

March 8, 2019

This article was contributed by Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra

Introduction

The Linux-kernel memory model (LKMM) (described here and here) was accepted into the Linux kernel in early 2018 and has seen continued development since. One item of development is the addition of Sleepable RCU (SRCU), as described in this article.

SRCU is similar to RCU in having read-side critical sections (which begin with srcu_read_lock() and end with srcu_read_unlock()) and grace periods (which may be waited on by invoking synchronize_srcu()). Although the most distinctive attribute of SRCU is the fact that SRCU readers are allowed to block arbitrarily, LKMM does not model the scheduler in general or blocking in particular. Therefore, the most pertinent aspects of SRCU are: (1) Passing the return value from srcu_read_lock() into the corresponding srcu_read_unlock(), and (2) The domains provided by the srcu_struct structure. However, these two SRCU aspects are actually consequences of safe and efficient support of sleeping readers, so we have come full circle.

The domain is specified by a pointer to an srcu_struct structure that is passed to srcu_read_lock(), srcu_read_unlock(), and synchronize_srcu(). Each call to synchronize_srcu() is required to wait only for those SRCU read-side critical sections using the same srcu_struct structure. This means that an SRCU reader that blocks for an excessive time period only impedes those grace periods in the same domain. This in turn allows each domain to choose its own definition of “excessively long”.

The need to pass the return value from srcu_read_lock() to the matching srcu_read_unlock() stems from the implementation-level need to avoid avoid explicitly tracking the state of up to O(N*M) SRCU readers, where N is the number of tasks and M is the number of instances of srcu_struct structures. Passing the return value from srcu_read_lock() to the matching srcu_read_unlock() allows this state to be stored on the stack, and to not be represented at all for tasks not in an SRCU read-side critical section.

To the best of our knowledge, LKMM provides the first realistic automated representation of Linux-kernel SRCU's ordering properties.

This article is organized as follows:

  1. Invoking LKMM
  2. Modeling SRCU
  3. Multiple srcu_struct Structures
  4. Approximating SRCU: Why and How?
  5. Adding SRCU to LKMM
  6. Conclusions

This is followed by the ineludible answers to the quick quizzes.

Invoking LKMM

LKMM was accepted into version v4.17 of the Linux kernel, so if you have a recent Linux-kernel source tree, you have LKMM! Actually running LKMM requires installing herdtools as described in tools/memory-model/README. Once you have these tools installed, given a litmus test in “/path/to/file.litmus” and the Linux-kernel source tree in “/path/to/Linux/kernel”, you can run that litmus test as follows: 

	cd /path/to/Linux/kernel/tools/memory-model
	herd7 -conf linux-kernel.cfg /path/to/file.litmus

This will result in output analyzing file.litmus similar to that shown below.

Modeling SRCU

SRCU is normally used in a manner similar to RCU, as illustrated by this litmus test:

Litmus Test #1 
  1 C C-s1
  2
  3 {}
  4
  5 P0(struct srcu_struct *ssp1, int *a, int *b)
  6 {
  7   int i1;
  8   int r0;
  9
 10   i1 = srcu_read_lock(ssp1);
 11   r0 = READ_ONCE(*b);
 12   WRITE_ONCE(*a, 1);
 13   srcu_read_unlock(ssp1, i1);
 14 }
 15
 16 P1(struct srcu_struct *ssp1, int *a, int *b)
 17 {
 18   int r1;
 19
 20   r1 = READ_ONCE(*a);
 21   synchronize_srcu(ssp1);
 22   WRITE_ONCE(*b, 1);
 23 }
 24
 25 exists (0:r0=1 /\ 1:r1=1)

Here, P0() is the SRCU reader and P1() is the SRCU updater, and as noted earlier, the usage is quite similar to that of RCU. Therefore, in the usual RCU manner, P0()'s SRCU read-side critical section spanning lines 10-13 must be ordered either entirely before the end of or after the beginning of P1()'s grace period on line 21. Because Litmus Test #1 has (trivially) properly nested SRCU read-side critical sections and a pointer to the same srcu_struct structure ssp1 used everywhere, the exists clause cannot be satisfied:

Outcome for Litmus Test #1 (linux-kernel model) 
 1 Test C-s1 Allowed
 2 States 3
 3 0:r0=0; 1:r1=0;
 4 0:r0=0; 1:r1=1;
 5 0:r0=1; 1:r1=0;
 6 No
 7 Witnesses
 8 Positive: 0 Negative: 3
 9 Condition exists (0:r0=1 /\ 1:r1=1)
10 Observation C-s1 Never 0 3
11 Time C-s1 0.01
12 Hash=4e6ad6544498deb56ed8f5823f591bba

Assuming use of a single srcu_struct structure, the SRCU guarantee can be extended to multiple SRCU read-side critical sections and multiple grace periods in the same way RCU's guarantee can be extended.

Quick Quiz 1: What if a pair of SRCU read-side critical sections using the same srcu_struct structure partially overlap instead of being properly nested?
Answer

Multiple srcu_struct Structures

Suppose P0() and P1() use different srcu_struct structures, as shown below:

Litmus Test #2 
  1 C C-s1-mismatch
  2
  3 {}
  4
  5 P0(struct srcu_struct *ssp1, int *a, int *b)
  6 {
  7   int i1;
  8   int r0;
  9
 10   i1 = srcu_read_lock(ssp1);
 11   r0 = READ_ONCE(*b);
 12   WRITE_ONCE(*a, 1);
 13   srcu_read_unlock(ssp1, i1);
 14 }
 15
 16 P1(struct srcu_struct *ssp2, int *a, int *b)
 17 {
 18   int r1;
 19
 20   r1 = READ_ONCE(*a);
 21   synchronize_srcu(ssp2);
 22   WRITE_ONCE(*b, 1);
 23 }
 24
 25 exists (0:r0=1 /\ 1:r1=1)

In this case, P0()'s SRCU read-side critical section has no relation to P1()'s SRCU grace period, which means that the exists clause can be satisfied:

Outcome for Litmus Test #2 (linux-kernel model) 
 1 Test C-s1-mismatch Allowed
 2 States 4
 3 0:r0=0; 1:r1=0;
 4 0:r0=0; 1:r1=1;
 5 0:r0=1; 1:r1=0;
 6 0:r0=1; 1:r1=1;
 7 Ok
 8 Witnesses
 9 Positive: 1 Negative: 3
10 Condition exists (0:r0=1 /\ 1:r1=1)
11 Observation C-s1-mismatch Sometimes 1 3
12 Time C-s1-mismatch 0.01
13 Hash=2d13cb3431b8cafa6f620b5e78c88150

Therefore, don't mix and match srcu_struct structures unless you really mean to do so!

Here is one way to successfully combine two different srcu_struct structures:

Litmus Test #3 
  1 C SRCU-42-A
  2
  3 {
  4 }
  5
  6 P0(int *x0, int *x1, struct srcu_struct *ssp1)
  7 {
  8   int r0;
  9   int r1;
 10
 11   r0 = srcu_read_lock(ssp1);
 12   r1 = READ_ONCE(*x0);
 13   WRITE_ONCE(*x1, 1);
 14   srcu_read_unlock(ssp1, r0);
 15 }
 16
 17 P1(int *x1, int *x2, struct srcu_struct *ssp1)
 18 {
 19   int r1;
 20
 21   r1 = READ_ONCE(*x1);
 22   synchronize_srcu(ssp1);
 23   WRITE_ONCE(*x2, 1);
 24 }
 25
 26 P2(int *x2, int *x3, struct srcu_struct *ssp2)
 27 {
 28   int r0;
 29   int r1;
 30
 31   r0 = srcu_read_lock(ssp2);
 32   WRITE_ONCE(*x3, 1);
 33   r1 = READ_ONCE(*x2);
 34   srcu_read_unlock(ssp2, r0);
 35 }
 36
 37 P3(int *x3, int *x0, struct srcu_struct *ssp2)
 38 {
 39   int r1;
 40
 41   r1 = READ_ONCE(*x3);
 42   synchronize_srcu(ssp2);
 43   WRITE_ONCE(*x0, 1);
 44 }
 45
 46 exists
 47 (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1)

In this litmus test, P0() has an SRCU read-side critical section for ssp1 and P1() has an SRCU grace period, also for ssp1. Similarly, P2() has an SRCU read-side critical section for ssp2 and P3() has an SRCU grace period, also for ssp2. This combination causes the exists clause to be forbidden:

Outcome for Litmus Test #3 (linux-kernel model) 
 1 Test SRCU-42-A Allowed
 2 States 15
 3 0:r1=0; 1:r1=0; 2:r1=0; 3:r1=0;
 4 0:r1=0; 1:r1=0; 2:r1=0; 3:r1=1;
 5 0:r1=0; 1:r1=0; 2:r1=1; 3:r1=0;
 6 0:r1=0; 1:r1=0; 2:r1=1; 3:r1=1;
 7 0:r1=0; 1:r1=1; 2:r1=0; 3:r1=0;
 8 0:r1=0; 1:r1=1; 2:r1=0; 3:r1=1;
 9 0:r1=0; 1:r1=1; 2:r1=1; 3:r1=0;
10 0:r1=0; 1:r1=1; 2:r1=1; 3:r1=1;
11 0:r1=1; 1:r1=0; 2:r1=0; 3:r1=0;
12 0:r1=1; 1:r1=0; 2:r1=0; 3:r1=1;
13 0:r1=1; 1:r1=0; 2:r1=1; 3:r1=0;
14 0:r1=1; 1:r1=0; 2:r1=1; 3:r1=1;
15 0:r1=1; 1:r1=1; 2:r1=0; 3:r1=0;
16 0:r1=1; 1:r1=1; 2:r1=0; 3:r1=1;
17 0:r1=1; 1:r1=1; 2:r1=1; 3:r1=0;
18 No
19 Witnesses
20 Positive: 0 Negative: 15
21 Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1)
22 Observation SRCU-42-A Never 0 15
23 Time SRCU-42-A 0.04
24 Hash=e4a3edb6d5fb0f8ec03bffd98ca3f784

Quick Quiz 2: Wouldn't different srcu_struct structures normally be used independently, instead of in the strange in-tandem manner shown in Litmus Test #3?
Answer

It is tempting to assume that you can mix and match srcu_struct structures as long as the cycle contains at least as many SRCU grace periods as SRCU read-side critical sections for each srcu_struct structure (taking the lesson from Litmus Test #2), but this is not the case, as illustrated by this litmus test:

Litmus Test #4 
  1 C SRCU-42
  2
  3 {
  4 }
  5
  6 P0(int *x0, int *x1, struct srcu_struct *ssp1)
  7 {
  8   int r0;
  9   int r1;
 10
 11   r0 = srcu_read_lock(ssp1);
 12   WRITE_ONCE(*x0, 1);
 13   r1 = READ_ONCE(*x1);
 14   srcu_read_unlock(ssp1, r0);
 15 }
 16
 17 P1(int *x1, int *x2, struct srcu_struct *ssp2)
 18 {
 19   int r0;
 20   int r1;
 21
 22   r0 = srcu_read_lock(ssp2);
 23   WRITE_ONCE(*x1, 1);
 24   r1 = READ_ONCE(*x2);
 25   srcu_read_unlock(ssp2, r0);
 26 }
 27
 28 P2(int *x2, int *x3, struct srcu_struct *ssp1)
 29 {
 30   int r1;
 31
 32   WRITE_ONCE(*x2, 1);
 33   synchronize_srcu(ssp1);
 34   r1 = READ_ONCE(*x3);
 35 }
 36
 37 P3(int *x3, int *x0, struct srcu_struct *ssp2)
 38 {
 39   int r1;
 40
 41   WRITE_ONCE(*x3, 1);
 42   synchronize_srcu(ssp2);
 43   r1 = READ_ONCE(*x0);
 44 }
 45
 46 exists
 47 (0:r1=0 /\ 1:r1=0 /\ 2:r1=0 /\ 3:r1=0)

Here the exists clause really can be satisfied:

Outcome for Litmus Test #4 (linux-kernel model) 
 1 Test SRCU-42 Allowed
 2 States 16
 3 0:r1=0; 1:r1=0; 2:r1=0; 3:r1=0;
 4 0:r1=0; 1:r1=0; 2:r1=0; 3:r1=1;
 5 0:r1=0; 1:r1=0; 2:r1=1; 3:r1=0;
 6 0:r1=0; 1:r1=0; 2:r1=1; 3:r1=1;
 7 0:r1=0; 1:r1=1; 2:r1=0; 3:r1=0;
 8 0:r1=0; 1:r1=1; 2:r1=0; 3:r1=1;
 9 0:r1=0; 1:r1=1; 2:r1=1; 3:r1=0;
10 0:r1=0; 1:r1=1; 2:r1=1; 3:r1=1;
11 0:r1=1; 1:r1=0; 2:r1=0; 3:r1=0;
12 0:r1=1; 1:r1=0; 2:r1=0; 3:r1=1;
13 0:r1=1; 1:r1=0; 2:r1=1; 3:r1=0;
14 0:r1=1; 1:r1=0; 2:r1=1; 3:r1=1;
15 0:r1=1; 1:r1=1; 2:r1=0; 3:r1=0;
16 0:r1=1; 1:r1=1; 2:r1=0; 3:r1=1;
17 0:r1=1; 1:r1=1; 2:r1=1; 3:r1=0;
18 0:r1=1; 1:r1=1; 2:r1=1; 3:r1=1;
19 Ok
20 Witnesses
21 Positive: 1 Negative: 15
22 Condition exists (0:r1=0 /\ 1:r1=0 /\ 2:r1=0 /\ 3:r1=0)
23 Observation SRCU-42 Sometimes 1 15
24 Time SRCU-42 0.03
25 Hash=b53320b2e58dbd41d4d24f7df3f1689f

Although the counting rule still applies, it applies in a more elaborate way. It is not enough for the total count of SRCU grace periods to exceed that of SRCU read-side critical sections for each srcu_struct structure. In addition, in the simplest cases it must be possible to divide the cycle into a series of contiguous segments, where each segment obeys the counting rule and each process in the segment uses the same srcu_struct structure. (There are additional more-complex arrangements that also preserve order; they are described by the cat code below.) This per-segment counting rule is obeyed by Litmus Test #3, but it is violated by both P0() and P1() of Litmus Test #4, each of which constitutes a single-process segment and each of which has a SRCU read-side critical section but no SRCU grace periods. Therefore, neither P0() nor P1() provide any ordering, and the cycle specified by the exists clause on lines 46-47 is allowed.

Quick Quiz 3: Given the complexity of the per-segment counting rule, isn't relying on the interactions of SRCU read-side critical sections and SRCU grace periods for multiple srcu_struct structures an accident waiting to happen?
Answer

Quick Quiz 4: What happens when you add RCU to the mix as well?
Answer

Approximating SRCU: Why and How?

Up to this point, all litmus tests have had at most one SRCU read-side critical section per process, rendering moot any questions about nesting. This section takes a look at the interactions of multiple SRCU read-side critical sections within the confines of a single process.

TL;DR: Don't misnest SRCU read-side critical sections for the same srcu_struct structure.

Because SRCU requires that the return value from srcu_read_lock() be passed to srcu_read_unlock(), it is possible to partially overlap or misnest SRCU read-side critical sections. An example is shown in the following litmus test:

Litmus Test #5 
  1 C C-SRCU-misnest
  2
  3 {
  4 }
  5
  6 P0(int *x0, int *x1, struct srcu_struct *ssp1)
  7 {
  8   int r0;
  9   int r1;
 10   int r2;
 11
 12   r0 = srcu_read_lock(ssp1);
 13   r1 = READ_ONCE(*x1);
 14   r2 = srcu_read_lock(ssp1);
 15   srcu_read_unlock(ssp1, r0);
 16   WRITE_ONCE(*x0, 1);
 17   srcu_read_unlock(ssp1, r2);
 18 }
 19
 20 P1(int *x0, int *x1, struct srcu_struct *ssp1)
 21 {
 22   int r0;
 23   int r1;
 24
 25   WRITE_ONCE(*x1, 1);
 26   synchronize_srcu(ssp1);
 27   r1 = READ_ONCE(*x0);
 28 }
 29
 30 exists
 31 (0:r1=0 /\ 1:r1=0)

The return value from the srcu_read_lock() on line 12 is passed to the srcu_read_unlock() on line 15, so that this SRCU read-side critical section overlaps that of the srcu_read_lock() on line 14 and the srcu_read_unlock() on line 17.

In theory, this is quite straightforward: Any SRCU grace period starting after P0() reaches line 12 cannot complete until some time after P0() reaches line 15, and any SRCU grace period starting after P0() reaches line 14 cannot complete until some time after P0() reaches line 17, because grace periods must wait for pre-existing critical sections. However, in practice, the only known use cases for overlapping SRCU read-side critical sections have been to hide subtle bugs. LKMM therefore discourages this practice, as shown on line 9 of the outcome:

Outcome for Litmus Test #5 (linux-kernel model) 
 1 Test C-SRCU-misnest Allowed
 2 States 3
 3 0:r1=0; 1:r1=1;
 4 0:r1=1; 1:r1=0;
 5 0:r1=1; 1:r1=1;
 6 No
 7 Witnesses
 8 Positive: 0 Negative: 3
 9 Flag srcu-bad-nesting
10 Condition exists (0:r1=0 /\ 1:r1=0)
11 Observation C-SRCU-misnest Never 0 3
12 Time C-SRCU-misnest 0.01
13 Hash=ade0dd8e2f787f74d8a7eecc26a4bbc4
The “Flag srcu-bad-nesting” is LKMM complaining about the bug-prone misnesting of SRCU read-side critical sections in this litmus test.

Quick Quiz 5: But how do you know that there are no valid use cases for overlapping SRCU read-side critical sections?
Answer

Because LKMM flags misnested SRCU read-side critical sections, it can legitimately approximate such critical sections by acting as if they were properly nested. This can of course cause misleading outcomes (as is the case for Litmus Test #5) but such cases will be flagged with “Flag srcu-bad-nesting” (as is also the case for Litmus Test #5), alerting the user to the problem.

Quick Quiz 6: How can Litmus Test #5 satisfy its exists clause when running in the Linux kernel?
Answer

Quick Quiz 7: Does LKMM catch all instances of misnested SRCU read-side critical sections?
Answer

In short, LKMM flags any litmus tests with misnested SRCU read-side critical sections and analyzes them as if those critical sections were properly nested.

Quick Quiz 8: Why doesn't LKMM simply accept misnested SRCU read-side critical sections and handle them the same way as the Linux kernel does?
Answer

Adding SRCU to LKMM

These approximations allow LKMM's SRCU model to be quite similar to that of RCU. The following lines are added to the linux-kernel.bell file: 

 1 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
 2 let srcu-rscs = let rec
 3       unmatched-locks = Srcu-lock \ domain(matched)
 4   and unmatched-unlocks = Srcu-unlock \ range(matched)
 5   and unmatched = unmatched-locks | unmatched-unlocks
 6   and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
 7   and unmatched-locks-to-unlocks =
 8     ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
 9   and matched = matched | (unmatched-locks-to-unlocks \
10     (unmatched-po ; unmatched-po))
11   in matched
12
13 (* Validate nesting *)
14 flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
15 flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
16
17 (* Check for use of synchronize_srcu() inside an RCU critical section *)
18 flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
19
20 (* Validate SRCU dynamic match *)
21 flag ~empty different-values(srcu-rscs) as srcu-bad-nesting

These lines are quite similar to their RCU counterparts. Differences include:

  1. Identifiers containing “rcu” substitute “srcu” and, similarly, identifiers containing “Rcu” substitute “Srcu”.
  2. Lines 6 and 8 add “& loc” to ensure that srcu_read_lock() and srcu_read_unlock() invocations are properly segregated by srcu_struct structure.
  3. Line 18 complains if synchronize_srcu() appears within an RCU read-side critical section, on the grounds that RCU read-side critical sections are not allowed to block.
  4. Line 21 complains if SRCU read-side critical sections for a given srcu_struct are misnested.

In the linux-kernel.cat file, the SRCU support is interleaved into that of RCU: 

 1 let rcu-gp = [Sync-rcu]
 2 let srcu-gp = [Sync-srcu]
 3 let rcu-rscsi = rcu-rscs^-1
 4 let srcu-rscsi = srcu-rscs^-1
 5
 6 let rcu-link = po? ; hb* ; pb* ; prop ; po
 7
 8 let rec rcu-fence = rcu-gp | srcu-gp |
 9   (rcu-gp ; rcu-link ; rcu-rscsi) |
10   ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |
11   (rcu-rscsi ; rcu-link ; rcu-gp) |
12   ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |
13   (rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
14   ((srcu-gp ; rcu-link ; rcu-fence ; rcu-link ; srcu-rscsi) & loc) |
15   (rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) |
16   ((srcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; srcu-gp) & loc) |
17   (rcu-fence ; rcu-link ; rcu-fence)
18
19 let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
20
21 irreflexive rb as rcu

Quick Quiz 9: That is some serious mutually assured recursion there! So did Alan write this?
Answer

Lines 2, 4, 8, 10, 12, 14, and 16 add the SRCU support. As with the .bell file, any expressions involving multiple SRCU primitives use “& loc” to segregate these primitives by srcu_struct instance. And we are now in a position to state SRCU's more-elaborate forbidden-cycle counting rule in its full glory. As you might expect, the definition is recursive:

  1. A linked sequence of threads is ordered if each entry in the sequence contains a call to smp_mb() or synchronize_rcu() or synchronize_srcu().
  2. Matching read-side critical sections and grace periods:
    1. A linked sequence of two threads is ordered if one thread contains an RCU read-side critical section and the other calls synchronize_rcu().
    2. A linked sequence of two threads is ordered if one thread contains an SRCU read-side critical section and the other calls synchronize_srcu() using the same srcu_struct structure.
  3. Extending with read-side critical sections and grace periods:
    1. An ordered sequence can be extended by linking a thread to its start and a thread to its end, where one of the new threads contains an RCU read-side critical section and the other calls synchronize_rcu().
    2. An ordered sequence can be extended by linking a thread to its start and a thread to its end, where one of the new threads contains an SRCU read-side critical section and the other calls synchronize_srcu() using the same srcu_struct structure.
  4. Lastly, the linked concatenation of two ordered sequences is also ordered.

LKMM says that a linked sequence of threads ordered in this way must not form a cycle. Since the definition always requires a synchronize_rcu() call to be added along with each RCU read-side critical section, and a synchronize_srcu() call to be added along with each SRCU read-side critical section, you can see how the counting rule falls out.

Conclusions

We have demonstrated LKMM's versatility by adding SRCU support. As before, we hope will be useful for education, concurrent design, and for inclusion in other tooling. As far as we know, this is the first realistic formal memory model that includes SRCU ordering properties.

As before, this model is not set in stone, but subject to change with the evolution of hardware and of Linux-kernel use cases. And in fact, in not quite one year about 40 patches have been applied to the memory model. However, many of these patches provided tests and documentation. Only 18, less than half, have modified the memory model itself, and most of these 18 have been non-substantive changes for code style and commenting.

The limitations called out in the 2017 article still apply and bear repeating:

  1. These memory models do not constitute official statements by the various CPU vendors on their respective architectures. For example, any of these vendors might report bugs at any time against any version of this memory model. This memory model is therefore not a substitute for a carefully designed and vigorously executed validation regime. In addition, this memory model is under active development and might change at any time.
  2. It is quite possible that this memory model will disagree with CPU architectures or with real hardware. For example, the model might well choose to allow behavior that all CPUs forbid if forbidding that behavior would render the model excessively complex. On the other hand, any situation where the model forbids behavior that some CPU allows constitutes a bug, either in the model or in the CPU.
  3. This tool is exponential in nature. Litmus tests that seem quite small compared to the entire Linux kernel might well take geologic time for the herd tool to analyze. That said, this tool can be extremely effective in exhaustively analyzing the code at the core of a synchronization primitive.
  4. The herd tool can only detect problems for which you have coded an assertion. This weakness is common to all formal methods, and is one reason that we expect testing to continue to be important. In the immortal words of Donald Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

On the other hand, one advantage of formal memory models is that tools based on them can detect any problem that might occur, even if the probability of occurrence is vanishingly small, in fact, even if current hardware is incapable of making that problem happen. Use of tools based on this memory model is therefore an excellent way to future-proof your code.

Acknowledgments

We owe thanks to the LWN editors for their review of this document. We are also grateful to Jessica Murillo, Mark Figley, and Kara Todd for their support of this effort.

This work represents the views of the authors and does not necessarily represent the views of University College London, ARM Ltd., INRIA Paris, Amarula Solutions, Harvard University, Intel, Red Hat, Nvidia, or IBM Corporation.

Linux is a registered trademark of Linus Torvalds.

Other company, product, and service names may be trademarks or service marks of others.

Answers to Quick Quizzes

Quick Quiz 1: What if a pair of SRCU read-side critical sections using the same srcu_struct structure partially overlap instead of being properly nested?

Answer: That story is told later.

Back to Quick Quiz 1.

Quick Quiz 2: Wouldn't different srcu_struct structures normally be used independently, instead of in the strange in-tandem manner shown in Litmus Test #3?

Answer: You are quite correct, different srcu_struct structures would in fact normally be used independently. We therefore cordially invite you to construct a litmus test demonstrating this use case.

Back to Quick Quiz 2.

Quick Quiz 3: Given the complexity of the per-segment counting rule, isn't relying on the interactions of SRCU read-side critical sections and SRCU grace periods for multiple srcu_struct structures an accident waiting to happen?

Answer: Quite possibly. So if you find yourself relying on such interactions, you should step back and take a harder look at the problem you are trying to solve. But if you do find a need for this sort of thing, please let us know! This of course raises the question “Why bother modeling such interactions?” The answer is that we do need a mathematically complete model.

Back to Quick Quiz 3.

Quick Quiz 4: What happens when you add RCU to the mix as well?

Answer: This is covered later in this article.

Back to Quick Quiz 4.

Quick Quiz 5: But how do you know that there are no valid use cases for overlapping SRCU read-side critical sections?

Answer: We don't. But the better question is “Can you come up with a real use case for overlapping SRCU read-side critical sections?” If good use cases are found, LKMM will be appropriately adjusted.

Back to Quick Quiz 5.

Quick Quiz 6: How can Litmus Test #5 satisfy its exists clause when running in the Linux kernel?

Answer: The entirety of P1() might execute between lines 13 and 16 of P0(), which would result in both P0()'s and P1()'s instances of r1 having final values of zero, as specified in the exists clause. Such an outcome is admittedly unlikely, given the relatively high overhead of synchronize_srcu(), but it could happen given interrupts or preemption at just the wrong place during P0()'s execution.

Back to Quick Quiz 6.

Quick Quiz 7: Does LKMM catch all instances of misnested SRCU read-side critical sections?

Answer: No, only those that are actually reached by an execution. For example, consider this litmus test:

Litmus Test #6 
  1 C C-SRCU-misnest-not
  2
  3 {
  4 }
  5
  6 P0(int *x0, int *x1, int *x2, struct srcu_struct *ssp1)
  7 {
  8   int r0;
  9   int r1;
 10   int r2;
 11   int r3;
 12
 13   r0 = READ_ONCE(*x2);
 14   r1 = srcu_read_lock(ssp1);
 15   r2 = READ_ONCE(*x1);
 16   if (r0)
 17     r3 = srcu_read_lock(ssp1);
 18   srcu_read_unlock(ssp1, r1);
 19   WRITE_ONCE(*x0, 1);
 20   if (r0)
 21     srcu_read_unlock(ssp1, r3);
 22 }
 23
 24 P1(int *x0, int *x1, struct srcu_struct *ssp1)
 25 {
 26   int r0;
 27   int r1;
 28
 29   WRITE_ONCE(*x1, 1);
 30   synchronize_srcu(ssp1);
 31   r1 = READ_ONCE(*x0);
 32 }
 33
 34 exists
 35 (0:r2=0 /\ 1:r1=0)

Here, the srcu_read_lock() on line 17 and the srcu_read_unlock() on line 21 are never executed, so LKMM doesn't flag the misnesting:

Outcome for Litmus Test #6 (linux-kernel model) 
 1 Test C-SRCU-misnest-not Allowed
 2 States 4
 3 0:r2=0; 1:r1=0;
 4 0:r2=0; 1:r1=1;
 5 0:r2=1; 1:r1=0;
 6 0:r2=1; 1:r1=1;
 7 Ok
 8 Witnesses
 9 Positive: 1 Negative: 3
10 Condition exists (0:r2=0 /\ 1:r1=0)
11 Observation C-SRCU-misnest-not Sometimes 1 3
12 Time C-SRCU-misnest-not 0.01
13 Hash=3152306568bd9d54fc1f62e0604124c8

On the other hand, one can reasonably ask whether something that is never executed is really a problem. In addition, it is usually best to avoid adding never-executed code to the Linux kernel, with carefully conceived debugging code being the exception that proves this rule. Besides, in this case LKMM does correctly analyze this litmus test, correctly noting that the exists clause can in fact be satisfied.

Back to Quick Quiz 7.

Quick Quiz 8: Why doesn't LKMM simply accept misnested SRCU read-side critical sections and handle them the same way as the Linux kernel does?

Answer: At the time SRCU support was first added to LKML, herd did not possess any capability of matching the return value from one function call with the argument to another, so there was no choice but to assume that the nesting was correct. Later on, when this capability was added along with the srcu-bad-nesting flag, nobody modified the cat code to interpret misnested calls correctly.

Back to Quick Quiz 8.

Quick Quiz 9: That is some serious mutually assured recursion there! So did Alan write this?

Answer: Indeed he did! Luc wrote an earlier version and also provided some herd features needed to support SRCU. The rest of us provided some interesting litmus tests, some documentation, but were otherwise smart enough to stay out of the way.

Back to Quick Quiz 9.