diff options
Diffstat (limited to 'tools/memory-model/Documentation')
| -rw-r--r-- | tools/memory-model/Documentation/explanation.txt | 178 | ||||
| -rw-r--r-- | tools/memory-model/Documentation/litmus-tests.txt | 27 | ||||
| -rw-r--r-- | tools/memory-model/Documentation/locking.txt | 298 |
3 files changed, 466 insertions, 37 deletions
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index 8e7085238470..6dc8b3642458 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -28,9 +28,10 @@ Explanation of the Linux-Kernel Memory Consistency Model 20. THE HAPPENS-BEFORE RELATION: hb 21. THE PROPAGATES-BEFORE RELATION: pb 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb - 23. LOCKING - 24. PLAIN ACCESSES AND DATA RACES - 25. ODDS AND ENDS + 23. SRCU READ-SIDE CRITICAL SECTIONS + 24. LOCKING + 25. PLAIN ACCESSES AND DATA RACES + 26. ODDS AND ENDS @@ -1848,14 +1849,169 @@ section in P0 both starts before P1's grace period does and ends before it does, and the critical section in P2 both starts after P1's grace period does and ends after it does. -Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in -addition to normal RCU. The ideas involved are much the same as -above, with new relations srcu-gp and srcu-rscsi added to represent -SRCU grace periods and read-side critical sections. There is a -restriction on the srcu-gp and srcu-rscsi links that can appear in an -rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp -links having the same SRCU domain with proper nesting); the details -are relatively unimportant. +The LKMM supports SRCU (Sleepable Read-Copy-Update) in addition to +normal RCU. The ideas involved are much the same as above, with new +relations srcu-gp and srcu-rscsi added to represent SRCU grace periods +and read-side critical sections. However, there are some significant +differences between RCU read-side critical sections and their SRCU +counterparts, as described in the next section. + + +SRCU READ-SIDE CRITICAL SECTIONS +-------------------------------- + +The LKMM uses the srcu-rscsi relation to model SRCU read-side critical +sections. They differ from RCU read-side critical sections in the +following respects: + +1. Unlike the analogous RCU primitives, synchronize_srcu(), + srcu_read_lock(), and srcu_read_unlock() take a pointer to a + struct srcu_struct as an argument. This structure is called + an SRCU domain, and calls linked by srcu-rscsi must have the + same domain. Read-side critical sections and grace periods + associated with different domains are independent of one + another; the SRCU version of the RCU Guarantee applies only + to pairs of critical sections and grace periods having the + same domain. + +2. srcu_read_lock() returns a value, called the index, which must + be passed to the matching srcu_read_unlock() call. Unlike + rcu_read_lock() and rcu_read_unlock(), an srcu_read_lock() + call does not always have to match the next unpaired + srcu_read_unlock(). In fact, it is possible for two SRCU + read-side critical sections to overlap partially, as in the + following example (where s is an srcu_struct and idx1 and idx2 + are integer variables): + + idx1 = srcu_read_lock(&s); // Start of first RSCS + idx2 = srcu_read_lock(&s); // Start of second RSCS + srcu_read_unlock(&s, idx1); // End of first RSCS + srcu_read_unlock(&s, idx2); // End of second RSCS + + The matching is determined entirely by the domain pointer and + index value. By contrast, if the calls had been + rcu_read_lock() and rcu_read_unlock() then they would have + created two nested (fully overlapping) read-side critical + sections: an inner one and an outer one. + +3. The srcu_down_read() and srcu_up_read() primitives work + exactly like srcu_read_lock() and srcu_read_unlock(), except + that matching calls don't have to execute on the same CPU. + (The names are meant to be suggestive of operations on + semaphores.) Since the matching is determined by the domain + pointer and index value, these primitives make it possible for + an SRCU read-side critical section to start on one CPU and end + on another, so to speak. + +In order to account for these properties of SRCU, the LKMM models +srcu_read_lock() as a special type of load event (which is +appropriate, since it takes a memory location as argument and returns +a value, just as a load does) and srcu_read_unlock() as a special type +of store event (again appropriate, since it takes as arguments a +memory location and a value). These loads and stores are annotated as +belonging to the "srcu-lock" and "srcu-unlock" event classes +respectively. + +This approach allows the LKMM to tell whether two events are +associated with the same SRCU domain, simply by checking whether they +access the same memory location (i.e., they are linked by the loc +relation). It also gives a way to tell which unlock matches a +particular lock, by checking for the presence of a data dependency +from the load (srcu-lock) to the store (srcu-unlock). For example, +given the situation outlined earlier (with statement labels added): + + A: idx1 = srcu_read_lock(&s); + B: idx2 = srcu_read_lock(&s); + C: srcu_read_unlock(&s, idx1); + D: srcu_read_unlock(&s, idx2); + +the LKMM will treat A and B as loads from s yielding values saved in +idx1 and idx2 respectively. Similarly, it will treat C and D as +though they stored the values from idx1 and idx2 in s. The end result +is much as if we had written: + + A: idx1 = READ_ONCE(s); + B: idx2 = READ_ONCE(s); + C: WRITE_ONCE(s, idx1); + D: WRITE_ONCE(s, idx2); + +except for the presence of the special srcu-lock and srcu-unlock +annotations. You can see at once that we have A ->data C and +B ->data D. These dependencies tell the LKMM that C is the +srcu-unlock event matching srcu-lock event A, and D is the +srcu-unlock event matching srcu-lock event B. + +This approach is admittedly a hack, and it has the potential to lead +to problems. For example, in: + + idx1 = srcu_read_lock(&s); + srcu_read_unlock(&s, idx1); + idx2 = srcu_read_lock(&s); + srcu_read_unlock(&s, idx2); + +the LKMM will believe that idx2 must have the same value as idx1, +since it reads from the immediately preceding store of idx1 in s. +Fortunately this won't matter, assuming that litmus tests never do +anything with SRCU index values other than pass them to +srcu_read_unlock() or srcu_up_read() calls. + +However, sometimes it is necessary to store an index value in a +shared variable temporarily. In fact, this is the only way for +srcu_down_read() to pass the index it gets to an srcu_up_read() call +on a different CPU. In more detail, we might have soething like: + + struct srcu_struct s; + int x; + + P0() + { + int r0; + + A: r0 = srcu_down_read(&s); + B: WRITE_ONCE(x, r0); + } + + P1() + { + int r1; + + C: r1 = READ_ONCE(x); + D: srcu_up_read(&s, r1); + } + +Assuming that P1 executes after P0 and does read the index value +stored in x, we can write this (using brackets to represent event +annotations) as: + + A[srcu-lock] ->data B[once] ->rf C[once] ->data D[srcu-unlock]. + +The LKMM defines a carry-srcu-data relation to express this pattern; +it permits an arbitrarily long sequence of + + data ; rf + +pairs (that is, a data link followed by an rf link) to occur between +an srcu-lock event and the final data dependency leading to the +matching srcu-unlock event. carry-srcu-data is complicated by the +need to ensure that none of the intermediate store events in this +sequence are instances of srcu-unlock. This is necessary because in a +pattern like the one above: + + A: idx1 = srcu_read_lock(&s); + B: srcu_read_unlock(&s, idx1); + C: idx2 = srcu_read_lock(&s); + D: srcu_read_unlock(&s, idx2); + +the LKMM treats B as a store to the variable s and C as a load from +that variable, creating an undesirable rf link from B to C: + + A ->data B ->rf C ->data D. + +This would cause carry-srcu-data to mistakenly extend a data +dependency from A to D, giving the impression that D was the +srcu-unlock event matching A's srcu-lock. To avoid such problems, +carry-srcu-data does not accept sequences in which the ends of any of +the intermediate ->data links (B above) is an srcu-unlock event. LOCKING diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt index 26554b1c5575..acac527328a1 100644 --- a/tools/memory-model/Documentation/litmus-tests.txt +++ b/tools/memory-model/Documentation/litmus-tests.txt @@ -1028,32 +1028,7 @@ Limitations of the Linux-kernel memory model (LKMM) include: additional call_rcu() process to the site of the emulated rcu-barrier(). - e. Although sleepable RCU (SRCU) is now modeled, there - are some subtle differences between its semantics and - those in the Linux kernel. For example, the kernel - might interpret the following sequence as two partially - overlapping SRCU read-side critical sections: - - 1 r1 = srcu_read_lock(&my_srcu); - 2 do_something_1(); - 3 r2 = srcu_read_lock(&my_srcu); - 4 do_something_2(); - 5 srcu_read_unlock(&my_srcu, r1); - 6 do_something_3(); - 7 srcu_read_unlock(&my_srcu, r2); - - In contrast, LKMM will interpret this as a nested pair of - SRCU read-side critical sections, with the outer critical - section spanning lines 1-7 and the inner critical section - spanning lines 3-5. - - This difference would be more of a concern had anyone - identified a reasonable use case for partially overlapping - SRCU read-side critical sections. For more information - on the trickiness of such overlapping, please see: - https://paulmck.livejournal.com/40593.html - - f. Reader-writer locking is not modeled. It can be + e. Reader-writer locking is not modeled. It can be emulated in litmus tests using atomic read-modify-write operations. diff --git a/tools/memory-model/Documentation/locking.txt b/tools/memory-model/Documentation/locking.txt new file mode 100644 index 000000000000..65c898c64a93 --- /dev/null +++ b/tools/memory-model/Documentation/locking.txt @@ -0,0 +1,298 @@ +Locking +======= + +Locking is well-known and the common use cases are straightforward: Any +CPU holding a given lock sees any changes previously seen or made by any +CPU before it previously released that same lock. This last sentence +is the only part of this document that most developers will need to read. + +However, developers who would like to also access lock-protected shared +variables outside of their corresponding locks should continue reading. + + +Locking and Prior Accesses +-------------------------- + +The basic rule of locking is worth repeating: + + Any CPU holding a given lock sees any changes previously seen + or made by any CPU before it previously released that same lock. + +Note that this statement is a bit stronger than "Any CPU holding a +given lock sees all changes made by any CPU during the time that CPU was +previously holding this same lock". For example, consider the following +pair of code fragments: + + /* See MP+polocks.litmus. */ + void CPU0(void) + { + WRITE_ONCE(x, 1); + spin_lock(&mylock); + WRITE_ONCE(y, 1); + spin_unlock(&mylock); + } + + void CPU1(void) + { + spin_lock(&mylock); + r0 = READ_ONCE(y); + spin_unlock(&mylock); + r1 = READ_ONCE(x); + } + +The basic rule guarantees that if CPU0() acquires mylock before CPU1(), +then both r0 and r1 must be set to the value 1. This also has the +consequence that if the final value of r0 is equal to 1, then the final +value of r1 must also be equal to 1. In contrast, the weaker rule would +say nothing about the final value of r1. + + +Locking and Subsequent Accesses +------------------------------- + +The converse to the basic rule also holds: Any CPU holding a given +lock will not see any changes that will be made by any CPU after it +subsequently acquires this same lock. This converse statement is +illustrated by the following litmus test: + + /* See MP+porevlocks.litmus. */ + void CPU0(void) + { + r0 = READ_ONCE(y); + spin_lock(&mylock); + r1 = READ_ONCE(x); + spin_unlock(&mylock); + } + + void CPU1(void) + { + spin_lock(&mylock); + WRITE_ONCE(x, 1); + spin_unlock(&mylock); + WRITE_ONCE(y, 1); + } + +This converse to the basic rule guarantees that if CPU0() acquires +mylock before CPU1(), then both r0 and r1 must be set to the value 0. +This also has the consequence that if the final value of r1 is equal +to 0, then the final value of r0 must also be equal to 0. In contrast, +the weaker rule would say nothing about the final value of r0. + +These examples show only a single pair of CPUs, but the effects of the +locking basic rule extend across multiple acquisitions of a given lock +across multiple CPUs. + + +Double-Checked Locking +---------------------- + +It is well known that more than just a lock is required to make +double-checked locking work correctly, This litmus test illustrates +one incorrect approach: + + /* See Documentation/litmus-tests/locking/DCL-broken.litmus. */ + void CPU0(void) + { + r0 = READ_ONCE(flag); + if (r0 == 0) { + spin_lock(&lck); + r1 = READ_ONCE(flag); + if (r1 == 0) { + WRITE_ONCE(data, 1); + WRITE_ONCE(flag, 1); + } + spin_unlock(&lck); + } + r2 = READ_ONCE(data); + } + /* CPU1() is the exactly the same as CPU0(). */ + +There are two problems. First, there is no ordering between the first +READ_ONCE() of "flag" and the READ_ONCE() of "data". Second, there is +no ordering between the two WRITE_ONCE() calls. It should therefore be +no surprise that "r2" can be zero, and a quick herd7 run confirms this. + +One way to fix this is to use smp_load_acquire() and smp_store_release() +as shown in this corrected version: + + /* See Documentation/litmus-tests/locking/DCL-fixed.litmus. */ + void CPU0(void) + { + r0 = smp_load_acquire(&flag); + if (r0 == 0) { + spin_lock(&lck); + r1 = READ_ONCE(flag); + if (r1 == 0) { + WRITE_ONCE(data, 1); + smp_store_release(&flag, 1); + } + spin_unlock(&lck); + } + r2 = READ_ONCE(data); + } + /* CPU1() is the exactly the same as CPU0(). */ + +The smp_load_acquire() guarantees that its load from "flags" will +be ordered before the READ_ONCE() from data, thus solving the first +problem. The smp_store_release() guarantees that its store will be +ordered after the WRITE_ONCE() to "data", solving the second problem. +The smp_store_release() pairs with the smp_load_acquire(), thus ensuring +that the ordering provided by each actually takes effect. Again, a +quick herd7 run confirms this. + +In short, if you access a lock-protected variable without holding the +corresponding lock, you will need to provide additional ordering, in +this case, via the smp_load_acquire() and the smp_store_release(). + + +Ordering Provided by a Lock to CPUs Not Holding That Lock +--------------------------------------------------------- + +It is not necessarily the case that accesses ordered by locking will be +seen as ordered by CPUs not holding that lock. Consider this example: + + /* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */ + void CPU0(void) + { + spin_lock(&mylock); + WRITE_ONCE(x, 1); + WRITE_ONCE(y, 1); + spin_unlock(&mylock); + } + + void CPU1(void) + { + spin_lock(&mylock); + r0 = READ_ONCE(y); + WRITE_ONCE(z, 1); + spin_unlock(&mylock); + } + + void CPU2(void) + { + WRITE_ONCE(z, 2); + smp_mb(); + r1 = READ_ONCE(x); + } + +Counter-intuitive though it might be, it is quite possible to have +the final value of r0 be 1, the final value of z be 2, and the final +value of r1 be 0. The reason for this surprising outcome is that CPU2() +never acquired the lock, and thus did not fully benefit from the lock's +ordering properties. + +Ordering can be extended to CPUs not holding the lock by careful use +of smp_mb__after_spinlock(): + + /* See Z6.0+pooncelock+poonceLock+pombonce.litmus. */ + void CPU0(void) + { + spin_lock(&mylock); + WRITE_ONCE(x, 1); + WRITE_ONCE(y, 1); + spin_unlock(&mylock); + } + + void CPU1(void) + { + spin_lock(&mylock); + smp_mb__after_spinlock(); + r0 = READ_ONCE(y); + WRITE_ONCE(z, 1); + spin_unlock(&mylock); + } + + void CPU2(void) + { + WRITE_ONCE(z, 2); + smp_mb(); + r1 = READ_ONCE(x); + } + +This addition of smp_mb__after_spinlock() strengthens the lock +acquisition sufficiently to rule out the counter-intuitive outcome. +In other words, the addition of the smp_mb__after_spinlock() prohibits +the counter-intuitive result where the final value of r0 is 1, the final +value of z is 2, and the final value of r1 is 0. + + +No Roach-Motel Locking! +----------------------- + +This example requires familiarity with the herd7 "filter" clause, so +please read up on that topic in litmus-tests.txt. + +It is tempting to allow memory-reference instructions to be pulled +into a critical section, but this cannot be allowed in the general case. +For example, consider a spin loop preceding a lock-based critical section. +Now, herd7 does not model spin loops, but we can emulate one with two +loads, with a "filter" clause to constrain the first to return the +initial value and the second to return the updated value, as shown below: + + /* See Documentation/litmus-tests/locking/RM-fixed.litmus. */ + void CPU0(void) + { + spin_lock(&lck); + r2 = atomic_inc_return(&y); + WRITE_ONCE(x, 1); + spin_unlock(&lck); + } + + void CPU1(void) + { + r0 = READ_ONCE(x); + r1 = READ_ONCE(x); + spin_lock(&lck); + r2 = atomic_inc_return(&y); + spin_unlock(&lck); + } + + filter (1:r0=0 /\ 1:r1=1) + exists (1:r2=1) + +The variable "x" is the control variable for the emulated spin loop. +CPU0() sets it to "1" while holding the lock, and CPU1() emulates the +spin loop by reading it twice, first into "1:r0" (which should get the +initial value "0") and then into "1:r1" (which should get the updated +value "1"). + +The "filter" clause takes this into account, constraining "1:r0" to +equal "0" and "1:r1" to equal 1. + +Then the "exists" clause checks to see if CPU1() acquired its lock first, +which should not happen given the filter clause because CPU0() updates +"x" while holding the lock. And herd7 confirms this. + +But suppose that the compiler was permitted to reorder the spin loop +into CPU1()'s critical section, like this: + + /* See Documentation/litmus-tests/locking/RM-broken.litmus. */ + void CPU0(void) + { + int r2; + + spin_lock(&lck); + r2 = atomic_inc_return(&y); + WRITE_ONCE(x, 1); + spin_unlock(&lck); + } + + void CPU1(void) + { + spin_lock(&lck); + r0 = READ_ONCE(x); + r1 = READ_ONCE(x); + r2 = atomic_inc_return(&y); + spin_unlock(&lck); + } + + filter (1:r0=0 /\ 1:r1=1) + exists (1:r2=1) + +If "1:r0" is equal to "0", "1:r1" can never equal "1" because CPU0() +cannot update "x" while CPU1() holds the lock. And herd7 confirms this, +showing zero executions matching the "filter" criteria. + +And this is why Linux-kernel lock and unlock primitives must prevent +code from entering critical sections. It is not sufficient to only +prevent code from leaving them. |