diff options
Diffstat (limited to 'tools/memory-model')
34 files changed, 1400 insertions, 298 deletions
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README index db90a26dbdf4..88870b0bceea 100644 --- a/tools/memory-model/Documentation/README +++ b/tools/memory-model/Documentation/README @@ -9,6 +9,8 @@ depending on what you know and what you would like to learn. Please note that the documents later in this list assume that the reader understands the material provided by documents earlier in this list. +If LKMM-specific terms lost you, glossary.txt might help you. + o You are new to Linux-kernel concurrency: simple.txt o You have some background in Linux-kernel concurrency, and would @@ -21,6 +23,12 @@ o You are familiar with the Linux-kernel concurrency primitives that you need, and just want to get started with LKMM litmus tests: litmus-tests.txt +o You need to locklessly access shared variables that are otherwise + protected by a lock: locking.txt + + This locking.txt file expands on the "Locking" section in + recipes.txt, but is self-contained. + o You are familiar with Linux-kernel concurrency, and would like a detailed intuitive understanding of LKMM, including situations involving more than two threads: recipes.txt @@ -28,12 +36,18 @@ o You are familiar with Linux-kernel concurrency, and would o You would like a detailed understanding of what your compiler can and cannot do to control dependencies: control-dependencies.txt +o You would like to mark concurrent normal accesses to shared + variables so that intentional "racy" accesses can be properly + documented, especially when you are responding to complaints + from KCSAN: access-marking.txt + o You are familiar with Linux-kernel concurrency and the use of LKMM, and would like a quick reference: cheatsheet.txt o You are familiar with Linux-kernel concurrency and the use of LKMM, and would like to learn about LKMM's requirements, - rationale, and implementation: explanation.txt + rationale, and implementation: explanation.txt and + herd-representation.txt o You are interested in the publications related to LKMM, including hardware manuals, academic literature, standards-committee @@ -47,6 +61,10 @@ DESCRIPTION OF FILES README This file. +access-marking.txt + Guidelines for marking intentionally concurrent accesses to + shared memory. + cheatsheet.txt Quick-reference guide to the Linux-kernel memory model. @@ -57,10 +75,21 @@ control-dependencies.txt explanation.txt Detailed description of the memory model. +glossary.txt + Brief definitions of LKMM-related terms. + +herd-representation.txt + The (abstract) representation of the Linux-kernel concurrency + primitives in terms of events. + litmus-tests.txt The format, features, capabilities, and limitations of the litmus tests that LKMM can evaluate. +locking.txt + Rules for accessing lock-protected shared variables outside of + their corresponding critical sections. + ordering.txt Overview of the Linux kernel's low-level memory-ordering primitives by category. diff --git a/tools/memory-model/Documentation/access-marking.txt b/tools/memory-model/Documentation/access-marking.txt index 65778222183e..3fbe77fd564a 100644 --- a/tools/memory-model/Documentation/access-marking.txt +++ b/tools/memory-model/Documentation/access-marking.txt @@ -6,7 +6,8 @@ normal accesses to shared memory, that is "normal" as in accesses that do not use read-modify-write atomic operations. It also describes how to document these accesses, both with comments and with special assertions processed by the Kernel Concurrency Sanitizer (KCSAN). This discussion -builds on an earlier LWN article [1]. +builds on an earlier LWN article [1] and Linux Foundation mentorship +session [2]. ACCESS-MARKING OPTIONS @@ -24,6 +25,11 @@ The Linux kernel provides the following access-marking options: 4. WRITE_ONCE(), for example, "WRITE_ONCE(a, b);" The various forms of atomic_set() also fit in here. +5. __data_racy, for example "int __data_racy a;" + +6. KCSAN's negative-marking assertions, ASSERT_EXCLUSIVE_ACCESS() + and ASSERT_EXCLUSIVE_WRITER(), are described in the + "ACCESS-DOCUMENTATION OPTIONS" section below. These may be used in combination, as shown in this admittedly improbable example: @@ -31,7 +37,7 @@ example: WRITE_ONCE(a, b + data_race(c + d) + READ_ONCE(e)); Neither plain C-language accesses nor data_race() (#1 and #2 above) place -any sort of constraint on the compiler's choice of optimizations [2]. +any sort of constraint on the compiler's choice of optimizations [3]. In contrast, READ_ONCE() and WRITE_ONCE() (#3 and #4 above) restrict the compiler's use of code-motion and common-subexpression optimizations. Therefore, if a given access is involved in an intentional data race, @@ -205,6 +211,23 @@ because doing otherwise prevents KCSAN from detecting violations of your code's synchronization rules. +Use of __data_racy +------------------ + +Adding the __data_racy type qualifier to the declaration of a variable +causes KCSAN to treat all accesses to that variable as if they were +enclosed by data_race(). However, __data_racy does not affect the +compiler, though one could imagine hardened kernel builds treating the +__data_racy type qualifier as if it was the volatile keyword. + +Note well that __data_racy is subject to the same pointer-declaration +rules as are other type qualifiers such as const and volatile. +For example: + + int __data_racy *p; // Pointer to data-racy data. + int *__data_racy p; // Data-racy pointer to non-data-racy data. + + ACCESS-DOCUMENTATION OPTIONS ============================ @@ -342,7 +365,7 @@ as follows: Because foo is read locklessly, all accesses are marked. The purpose of the ASSERT_EXCLUSIVE_WRITER() is to allow KCSAN to check for a buggy -concurrent lockless write. +concurrent write, whether marked or not. Lock-Protected Writes With Heuristic Lockless Reads @@ -594,5 +617,8 @@ REFERENCES [1] "Concurrency bugs should fear the big bad data-race detector (part 2)" https://lwn.net/Articles/816854/ -[2] "Who's afraid of a big bad optimizing compiler?" +[2] "The Kernel Concurrency Sanitizer" + https://www.linuxfoundation.org/webinars/the-kernel-concurrency-sanitizer + +[3] "Who's afraid of a big bad optimizing compiler?" https://lwn.net/Articles/793253/ diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index 11a1d2d4f681..34aa3172071b 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 @@ -1007,6 +1008,36 @@ order. Equivalently, where the rmw relation links the read and write events making up each atomic update. This is what the LKMM's "atomic" axiom says. +Atomic rmw updates play one more role in the LKMM: They can form "rmw +sequences". An rmw sequence is simply a bunch of atomic updates where +each update reads from the previous one. Written using events, it +looks like this: + + Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn ->rmw Zn, + +where Z0 is some store event and n can be any number (even 0, in the +degenerate case). We write this relation as: Z0 ->rmw-sequence Zn. +Note that this implies Z0 and Zn are stores to the same variable. + +Rmw sequences have a special property in the LKMM: They can extend the +cumul-fence relation. That is, if we have: + + U ->cumul-fence X -> rmw-sequence Y + +then also U ->cumul-fence Y. Thinking about this in terms of the +operational model, U ->cumul-fence X says that the store U propagates +to each CPU before the store X does. Then the fact that X and Y are +linked by an rmw sequence means that U also propagates to each CPU +before Y does. In an analogous way, rmw sequences can also extend +the w-post-bounded relation defined below in the PLAIN ACCESSES AND +DATA RACES section. + +(The notion of rmw sequences in the LKMM is similar to, but not quite +the same as, that of release sequences in the C11 memory model. They +were added to the LKMM to fix an obscure bug; without them, atomic +updates with full-barrier semantics did not always guarantee ordering +at least as strong as atomic updates with release-barrier semantics.) + THE PRESERVED PROGRAM ORDER RELATION: ppo ----------------------------------------- @@ -1818,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 within the same context. + (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 @@ -2545,7 +2731,7 @@ smp_store_release() -- which is basically how the Linux kernel treats them. Although we said that plain accesses are not linked by the ppo -relation, they do contribute to it indirectly. Namely, when there is +relation, they do contribute to it indirectly. Firstly, when there is an address dependency from a marked load R to a plain store W, followed by smp_wmb() and then a marked store W', the LKMM creates a ppo link from R to W'. The reasoning behind this is perhaps a little @@ -2554,6 +2740,13 @@ for this source code in which W' could execute before R. Just as with pre-bounding by address dependencies, it is possible for the compiler to undermine this relation if sufficient care is not taken. +Secondly, plain accesses can carry dependencies: If a data dependency +links a marked load R to a store W, and the store is read by a load R' +from the same thread, then the data loaded by R' depends on the data +loaded originally by R. Thus, if R' is linked to any access X by a +dependency, R is also linked to access X by the same dependency, even +if W' or R' (or both!) are plain. + There are a few oddball fences which need special treatment: smp_mb__before_atomic(), smp_mb__after_atomic(), and smp_mb__after_spinlock(). The LKMM uses fence events with special diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt index 6f3d16dbf467..7ead94bffa4e 100644 --- a/tools/memory-model/Documentation/glossary.txt +++ b/tools/memory-model/Documentation/glossary.txt @@ -15,14 +15,14 @@ Address Dependency: When the address of a later memory access is computed 3 do_something(p->a); 4 rcu_read_unlock(); - In this case, because the address of "p->a" on line 3 is computed - from the value returned by the rcu_dereference() on line 2, the - address dependency extends from that rcu_dereference() to that - "p->a". In rare cases, optimizing compilers can destroy address - dependencies. Please see Documentation/RCU/rcu_dereference.rst - for more information. + In this case, because the address of "p->a" on line 3 is computed + from the value returned by the rcu_dereference() on line 2, the + address dependency extends from that rcu_dereference() to that + "p->a". In rare cases, optimizing compilers can destroy address + dependencies. Please see Documentation/RCU/rcu_dereference.rst + for more information. - See also "Control Dependency" and "Data Dependency". + See also "Control Dependency" and "Data Dependency". Acquire: With respect to a lock, acquiring that lock, for example, using spin_lock(). With respect to a non-lock shared variable, @@ -59,12 +59,12 @@ Control Dependency: When a later store's execution depends on a test 1 if (READ_ONCE(x)) 2 WRITE_ONCE(y, 1); - Here, the control dependency extends from the READ_ONCE() on - line 1 to the WRITE_ONCE() on line 2. Control dependencies are - fragile, and can be easily destroyed by optimizing compilers. - Please see control-dependencies.txt for more information. + Here, the control dependency extends from the READ_ONCE() on + line 1 to the WRITE_ONCE() on line 2. Control dependencies are + fragile, and can be easily destroyed by optimizing compilers. + Please see control-dependencies.txt for more information. - See also "Address Dependency" and "Data Dependency". + See also "Address Dependency" and "Data Dependency". Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the name suggests. And in a great many cases, a pair of CPUs is all @@ -72,10 +72,10 @@ Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the extended to additional CPUs, and the result is called a "cycle". In a cycle, each CPU's ordering interacts with that of the next: - CPU 0 CPU 1 CPU 2 - WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1); - smp_mb(); smp_mb(); smp_mb(); - r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x); + CPU 0 CPU 1 CPU 2 + WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1); + smp_mb(); smp_mb(); smp_mb(); + r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x); CPU 0's smp_mb() interacts with that of CPU 1, which interacts with that of CPU 2, which in turn interacts with that of CPU 0 diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt new file mode 100644 index 000000000000..4e19b4f2a476 --- /dev/null +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -0,0 +1,113 @@ +# +# Legend: +# R, a Load event +# W, a Store event +# F, a Fence event +# LKR, a Lock-Read event +# LKW, a Lock-Write event +# UL, an Unlock event +# LF, a Lock-Fail event +# RL, a Read-Locked event +# RU, a Read-Unlocked event +# R*, a Load event included in RMW +# W*, a Store event included in RMW +# SRCU, a Sleepable-Read-Copy-Update event +# +# po, a Program-Order link +# rmw, a Read-Modify-Write link - every rmw link is a po link +# +# By convention, a blank line in a cell means "same as the preceding line". +# +# Note that the syntactic representation does not always match the sets and +# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and +# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw +# link, and W[ACQUIRE] are not included in the Acquire set. +# +# Disclaimer. The table includes representations of "add" and "and" operations; +# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor", +# "andnot" operations are omitted. +# + ------------------------------------------------------------------------------ + | C macro | Events | + ------------------------------------------------------------------------------ + | Non-RMW ops | | + ------------------------------------------------------------------------------ + | READ_ONCE | R[ONCE] | + | atomic_read | | + | WRITE_ONCE | W[ONCE] | + | atomic_set | | + | smp_load_acquire | R[ACQUIRE] | + | atomic_read_acquire | | + | smp_store_release | W[RELEASE] | + | atomic_set_release | | + | smp_store_mb | W[ONCE] ->po F[MB] | + | smp_mb | F[MB] | + | smp_rmb | F[rmb] | + | smp_wmb | F[wmb] | + | smp_mb__before_atomic | F[before-atomic] | + | smp_mb__after_atomic | F[after-atomic] | + | spin_unlock | UL | + | spin_is_locked | On success: RL | + | | On failure: RU | + | smp_mb__after_spinlock | F[after-spinlock] | + | smp_mb__after_unlock_lock | F[after-unlock-lock] | + | rcu_read_lock | F[rcu-lock] | + | rcu_read_unlock | F[rcu-unlock] | + | synchronize_rcu | F[sync-rcu] | + | rcu_dereference | R[ONCE] | + | rcu_assign_pointer | W[RELEASE] | + | srcu_read_lock | R[srcu-lock] | + | srcu_down_read | | + | srcu_read_unlock | W[srcu-unlock] | + | srcu_up_read | | + | synchronize_srcu | SRCU[sync-srcu] | + | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] | + ------------------------------------------------------------------------------ + | RMW ops w/o return value | | + ------------------------------------------------------------------------------ + | atomic_add | R*[NORETURN] ->rmw W*[NORETURN] | + | atomic_and | | + | spin_lock | LKR ->po LKW | + ------------------------------------------------------------------------------ + | RMW ops w/ return value | | + ------------------------------------------------------------------------------ + | atomic_add_return | R*[MB] ->rmw W*[MB] | + | atomic_fetch_add | | + | atomic_fetch_and | | + | atomic_xchg | | + | xchg | | + | atomic_add_negative | | + | atomic_add_return_relaxed | R*[ONCE] ->rmw W*[ONCE] | + | atomic_fetch_add_relaxed | | + | atomic_fetch_and_relaxed | | + | atomic_xchg_relaxed | | + | xchg_relaxed | | + | atomic_add_negative_relaxed | | + | atomic_add_return_acquire | R*[ACQUIRE] ->rmw W*[ACQUIRE] | + | atomic_fetch_add_acquire | | + | atomic_fetch_and_acquire | | + | atomic_xchg_acquire | | + | xchg_acquire | | + | atomic_add_negative_acquire | | + | atomic_add_return_release | R*[RELEASE] ->rmw W*[RELEASE] | + | atomic_fetch_add_release | | + | atomic_fetch_and_release | | + | atomic_xchg_release | | + | xchg_release | | + | atomic_add_negative_release | | + ------------------------------------------------------------------------------ + | Conditional RMW ops | | + ------------------------------------------------------------------------------ + | atomic_cmpxchg | On success: R*[MB] ->rmw W*[MB] | + | | On failure: R*[MB] | + | cmpxchg | | + | atomic_add_unless | | + | atomic_cmpxchg_relaxed | On success: R*[ONCE] ->rmw W*[ONCE] | + | | On failure: R*[ONCE] | + | atomic_cmpxchg_acquire | On success: R*[ACQUIRE] ->rmw W*[ACQUIRE] | + | | On failure: R*[ACQUIRE] | + | atomic_cmpxchg_release | On success: R*[RELEASE] ->rmw W*[RELEASE] | + | | On failure: R*[RELEASE] | + | spin_trylock | On success: LKR ->po LKW | + | | On failure: LF | + ------------------------------------------------------------------------------ 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..d6dc3cc34ab6 --- /dev/null +++ b/tools/memory-model/Documentation/locking.txt @@ -0,0 +1,303 @@ +[!] Note: + This file expands on the "Locking" section of recipes.txt, + focusing on locklessly accessing shared variables that are + otherwise protected by a lock. + +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. diff --git a/tools/memory-model/Documentation/ordering.txt b/tools/memory-model/Documentation/ordering.txt index 9b0949d3f5ec..7ab3744929d8 100644 --- a/tools/memory-model/Documentation/ordering.txt +++ b/tools/memory-model/Documentation/ordering.txt @@ -223,7 +223,7 @@ The Linux kernel's compiler barrier is barrier(). This primitive prohibits compiler code-motion optimizations that might move memory references across the point in the code containing the barrier(), but does not constrain hardware memory ordering. For example, this can be -used to prevent to compiler from moving code across an infinite loop: +used to prevent the compiler from moving code across an infinite loop: WRITE_ONCE(x, 1); while (dontstop) @@ -274,7 +274,7 @@ different pieces of the concurrent algorithm. The variable stored to by the smp_store_release(), in this case "y", will normally be used in an acquire operation in other parts of the concurrent algorithm. -To see the performance advantages, suppose that the above example read +To see the performance advantages, suppose that the above example reads from "x" instead of writing to it. Then an smp_wmb() could not guarantee ordering, and an smp_mb() would be needed instead: @@ -394,17 +394,17 @@ from the value returned by the rcu_dereference() or srcu_dereference() to that subsequent memory access. A call to rcu_dereference() for a given RCU-protected pointer is -usually paired with a call to a call to rcu_assign_pointer() for that -same pointer in much the same way that a call to smp_load_acquire() is -paired with a call to smp_store_release(). Calls to rcu_dereference() -and rcu_assign_pointer are often buried in other APIs, for example, +usually paired with a call to rcu_assign_pointer() for that same pointer +in much the same way that a call to smp_load_acquire() is paired with +a call to smp_store_release(). Calls to rcu_dereference() and +rcu_assign_pointer() are often buried in other APIs, for example, the RCU list API members defined in include/linux/rculist.h. For more information, please see the docbook headers in that file, the most -recent LWN article on the RCU API (https://lwn.net/Articles/777036/), +recent LWN article on the RCU API (https://lwn.net/Articles/988638/), and of course the material in Documentation/RCU. If the pointer value is manipulated between the rcu_dereference() -that returned it and a later dereference(), please read +that returned it and a later rcu_dereference(), please read Documentation/RCU/rcu_dereference.rst. It can also be quite helpful to review uses in the Linux kernel. @@ -457,7 +457,7 @@ described earlier in this document. These operations come in three categories: o Marked writes, such as WRITE_ONCE() and atomic_set(). These - primitives required the compiler to emit the corresponding store + primitives require the compiler to emit the corresponding store instructions in the expected execution order, thus suppressing a number of destructive optimizations. However, they provide no hardware ordering guarantees, and in fact many CPUs will happily @@ -465,7 +465,7 @@ o Marked writes, such as WRITE_ONCE() and atomic_set(). These operations, unless these operations are to the same variable. o Marked reads, such as READ_ONCE() and atomic_read(). These - primitives required the compiler to emit the corresponding load + primitives require the compiler to emit the corresponding load instructions in the expected execution order, thus suppressing a number of destructive optimizations. However, they provide no hardware ordering guarantees, and in fact many CPUs will happily @@ -506,7 +506,7 @@ of the old value and the new value. Unmarked C-language accesses are unordered, and are also subject to any number of compiler optimizations, many of which can break your -concurrent code. It is possible to used unmarked C-language accesses for +concurrent code. It is possible to use unmarked C-language accesses for shared variables that are subject to concurrent access, but great care is required on an ongoing basis. The compiler-constraining barrier() primitive can be helpful, as can the various ordering primitives discussed diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt index 03f58b11c252..52115ee5f393 100644 --- a/tools/memory-model/Documentation/recipes.txt +++ b/tools/memory-model/Documentation/recipes.txt @@ -61,6 +61,10 @@ usual) some things to be careful of: Locking ------- +[!] Note: + locking.txt expands on this section, providing more detail on + locklessly accessing lock-protected shared variables. + Locking is well-known and straightforward, at least if you don't think about it too hard. And the basic rule is indeed quite simple: Any CPU that has acquired a given lock sees any changes previously seen or made by any diff --git a/tools/memory-model/Documentation/references.txt b/tools/memory-model/Documentation/references.txt index c5fdfd19df24..d691390620b3 100644 --- a/tools/memory-model/Documentation/references.txt +++ b/tools/memory-model/Documentation/references.txt @@ -46,8 +46,7 @@ o ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8, o Imagination Technologies, LTD. 2015. "MIPS(R) Architecture For Programmers, Volume II-A: The MIPS64(R) Instruction, - Set Reference Manual". Imagination Technologies, - LTD. https://imgtec.com/?do-download=4302. + Set Reference Manual". Imagination Technologies, LTD. o Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter diff --git a/tools/memory-model/Documentation/simple.txt b/tools/memory-model/Documentation/simple.txt index 4c789ec8334f..2df148630cdc 100644 --- a/tools/memory-model/Documentation/simple.txt +++ b/tools/memory-model/Documentation/simple.txt @@ -134,7 +134,7 @@ Packaged primitives: Sequence locking Lockless programming is considered by many to be more difficult than lock-based programming, but there are a few lockless design patterns that have been built out into an API. One of these APIs is sequence locking. -Although this APIs can be used in extremely complex ways, there are simple +Although this API can be used in extremely complex ways, there are simple and effective ways of using it that avoid the need to pay attention to memory ordering. @@ -205,7 +205,7 @@ If you want to keep things simple, use the initialization and read-out operations from the previous section only when there are no racing accesses. Otherwise, use only fully ordered operations when accessing or modifying the variable. This approach guarantees that code prior -to a given access to that variable will be seen by all CPUs has having +to a given access to that variable will be seen by all CPUs as having happened before any code following any later access to that same variable. Please note that per-CPU functions are not atomic operations and @@ -266,5 +266,5 @@ More complex use cases ====================== If the alternatives above do not do what you need, please look at the -recipes-pairs.txt file to peel off the next layer of the memory-ordering +recipes.txt file to peel off the next layer of the memory-ordering onion. diff --git a/tools/memory-model/README b/tools/memory-model/README index dab38904206a..64c860863aa9 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS ============ -Version 7.52 or higher of the "herd7" and "klitmus7" tools must be +Version 7.58 or higher of the "herd7" and "klitmus7" tools must be downloaded separately: https://github.com/herd/herdtools7 @@ -79,7 +79,7 @@ Several thousand more example litmus tests are available here: https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus -Documentation describing litmus tests and now to use them may be found +Documentation describing litmus tests and how to use them may be found here: tools/memory-model/Documentation/litmus-tests.txt diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 5be86b1025e8..fe65998002b9 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -13,17 +13,18 @@ "Linux-kernel memory consistency model" -enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) || - 'release (*smp_store_release*) || - 'acquire (*smp_load_acquire*) || - 'noreturn (* R of non-return RMW *) -instructions R[{'once,'acquire,'noreturn}] -instructions W[{'once,'release}] -instructions RMW[{'once,'acquire,'release}] +enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) || + 'RELEASE (*smp_store_release*) || + 'ACQUIRE (*smp_load_acquire*) || + 'NORETURN (* R of non-return RMW *) || + 'MB (*xchg(),cmpxchg(),...*) +instructions R[Accesses] +instructions W[Accesses] +instructions RMW[Accesses] enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || - 'mb (*smp_mb*) || + 'MB (*smp_mb*) || 'barrier (*barrier*) || 'rcu-lock (*rcu_read_lock*) || 'rcu-unlock (*rcu_read_unlock*) || @@ -31,9 +32,21 @@ enum Barriers = 'wmb (*smp_wmb*) || 'before-atomic (*smp_mb__before_atomic*) || 'after-atomic (*smp_mb__after_atomic*) || 'after-spinlock (*smp_mb__after_spinlock*) || - 'after-unlock-lock (*smp_mb__after_unlock_lock*) + 'after-unlock-lock (*smp_mb__after_unlock_lock*) || + 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*) instructions F[Barriers] + +(* + * Filter out syntactic annotations that do not provide the corresponding + * semantic ordering, such as Acquire on a store or Mb on a failed RMW. + *) +let FailedRMW = RMW \ (domain(rmw) | range(rmw)) +let Acquire = ACQUIRE \ W \ FailedRMW +let Release = RELEASE \ R \ FailedRMW +let Mb = MB \ FailedRMW +let Noreturn = NORETURN \ W + (* SRCU *) enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu instructions SRCU[SRCU] @@ -53,32 +66,34 @@ let rcu-rscs = let rec in matched (* Validate nesting *) -flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking -flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking +flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rcu-lock +flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) -let srcu-rscs = let rec - unmatched-locks = Srcu-lock \ domain(matched) - and unmatched-unlocks = Srcu-unlock \ range(matched) - and unmatched = unmatched-locks | unmatched-unlocks - and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc - and unmatched-locks-to-unlocks = - ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc - and matched = matched | (unmatched-locks-to-unlocks \ - (unmatched-po ; unmatched-po)) - in matched +let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)* +let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc (* Validate nesting *) -flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking -flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking +flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock +flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock +flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches (* Check for use of synchronize_srcu() inside an RCU critical section *) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep (* Validate SRCU dynamic match *) -flag ~empty different-values(srcu-rscs) as srcu-bad-nesting +flag ~empty different-values(srcu-rscs) as srcu-bad-value-match (* Compute marked and plain memory accesses *) -let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | - LKR | LKW | UL | LF | RL | RU +let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW | + LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock let Plain = M \ Marked + +(* Redefine dependencies to include those carried through plain accesses *) +let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* +let addr = carry-dep ; addr +let ctrl = carry-dep ; ctrl +let data = carry-dep ; data + +flag ~empty (if "lkmmv2" then 0 else _) + as this-model-requires-variant-higher-than-lkmmv1 diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index d70315fddef6..d7e7bf13c831 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -34,11 +34,33 @@ let R4rmb = R \ Noreturn (* Reads for which rmb works *) let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] let wmb = [W] ; fencerel(Wmb) ; [W] let mb = ([M] ; fencerel(Mb) ; [M]) | + (* + * full-barrier RMWs (successful cmpxchg(), xchg(), etc.) act as + * though there were enclosed by smp_mb(). + * The effect of these virtual smp_mb() is formalized by adding + * Mb tags to the read and write of the operation, and providing + * the same ordering as though there were additional po edges + * between the Mb tag and the read resp. write. + *) + ([M] ; po ; [Mb & R]) | + ([Mb & W] ; po ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) +(* + * Note: The po-unlock-lock-po relation only passes the lock to the direct + * successor, perhaps giving the impression that the ordering of the + * smp_mb__after_unlock_lock() fence only affects a single lock handover. + * However, in a longer sequence of lock handovers, the implicit + * A-cumulative release fences of lock-release ensure that any stores that + * propagate to one of the involved CPUs before it hands over the lock to + * the next CPU will also propagate to the final CPU handing over the lock + * to the CPU that executes the fence. Therefore, all those stores are + * also affected by the fence. + *) + ([M] ; po-unlock-lock-po ; + [After-unlock-lock] ; po ; [M]) | + ([M] ; po? ; [Srcu-unlock] ; fencerel(After-srcu-read-unlock) ; [M]) let gp = po ; [Sync-rcu | Sync-srcu] ; po? let strong-fence = mb | gp @@ -69,13 +91,14 @@ let dep = addr | data let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) -let to-r = addr | (dep ; [Marked] ; rfi) -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) +let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi) +let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = (rfe ; [Marked])? ; r +let rmw-sequence = (rf ; rmw)* let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | - po-unlock-lock-po) ; [Marked] + po-unlock-lock-po) ; [Marked] ; rmw-sequence let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] @@ -174,7 +197,7 @@ let vis = cumul-fence* ; rfe? ; [Marked] ; let w-pre-bounded = [Marked] ; (addr | fence)? let r-pre-bounded = [Marked] ; (addr | nonrw-fence | ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded = fence? ; [Marked] +let w-post-bounded = fence? ; [Marked] ; rmw-sequence let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; [Marked] diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg index 3c8098e99f41..69b04f3aad73 100644 --- a/tools/memory-model/linux-kernel.cfg +++ b/tools/memory-model/linux-kernel.cfg @@ -1,6 +1,7 @@ macros linux-kernel.def bell linux-kernel.bell model linux-kernel.cat +variant lkmmv2 graph columns squished true showevents noregs diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index ef0f3c1850de..49e402782e49 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -6,35 +6,36 @@ // which appeared in ASPLOS 2018. // ONCE -READ_ONCE(X) __load{once}(X) -WRITE_ONCE(X,V) { __store{once}(X,V); } +READ_ONCE(X) __load{ONCE}(X) +WRITE_ONCE(X,V) { __store{ONCE}(X,V); } // Release Acquire and friends -smp_store_release(X,V) { __store{release}(*X,V); } -smp_load_acquire(X) __load{acquire}(*X) -rcu_assign_pointer(X,V) { __store{release}(X,V); } -rcu_dereference(X) __load{once}(X) -smp_store_mb(X,V) { __store{once}(X,V); __fence{mb}; } +smp_store_release(X,V) { __store{RELEASE}(*X,V); } +smp_load_acquire(X) __load{ACQUIRE}(*X) +rcu_assign_pointer(X,V) { __store{RELEASE}(X,V); } +rcu_dereference(X) __load{ONCE}(X) +smp_store_mb(X,V) { __store{ONCE}(X,V); __fence{MB}; } // Fences -smp_mb() { __fence{mb}; } +smp_mb() { __fence{MB}; } smp_rmb() { __fence{rmb}; } smp_wmb() { __fence{wmb}; } smp_mb__before_atomic() { __fence{before-atomic}; } smp_mb__after_atomic() { __fence{after-atomic}; } smp_mb__after_spinlock() { __fence{after-spinlock}; } smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; } +smp_mb__after_srcu_read_unlock() { __fence{after-srcu-read-unlock}; } barrier() { __fence{barrier}; } // Exchange -xchg(X,V) __xchg{mb}(X,V) -xchg_relaxed(X,V) __xchg{once}(X,V) -xchg_release(X,V) __xchg{release}(X,V) -xchg_acquire(X,V) __xchg{acquire}(X,V) -cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W) -cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W) -cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W) -cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) +xchg(X,V) __xchg{MB}(X,V) +xchg_relaxed(X,V) __xchg{ONCE}(X,V) +xchg_release(X,V) __xchg{RELEASE}(X,V) +xchg_acquire(X,V) __xchg{ACQUIRE}(X,V) +cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W) +cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W) +cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W) +cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W) // Spinlocks spin_lock(X) { __lock(X); } @@ -49,8 +50,10 @@ synchronize_rcu() { __fence{sync-rcu}; } synchronize_rcu_expedited() { __fence{sync-rcu}; } // SRCU -srcu_read_lock(X) __srcu{srcu-lock}(X) -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); } +srcu_read_lock(X) __load{srcu-lock}(*X) +srcu_read_unlock(X,Y) { __store{srcu-unlock}(*X,Y); } +srcu_down_read(X) __load{srcu-lock}(*X) +srcu_up_read(X,Y) { __store{srcu-unlock}(*X,Y); } synchronize_srcu(X) { __srcu{sync-srcu}(X); } synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); } @@ -60,57 +63,86 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); } atomic_read_acquire(X) smp_load_acquire(X) atomic_set_release(X,V) { smp_store_release(X,V); } -atomic_add(V,X) { __atomic_op(X,+,V); } -atomic_sub(V,X) { __atomic_op(X,-,V); } -atomic_inc(X) { __atomic_op(X,+,1); } -atomic_dec(X) { __atomic_op(X,-,1); } - -atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) -atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) -atomic_add_return_acquire(V,X) __atomic_op_return{acquire}(X,+,V) -atomic_add_return_release(V,X) __atomic_op_return{release}(X,+,V) -atomic_fetch_add(V,X) __atomic_fetch_op{mb}(X,+,V) -atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,+,V) -atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V) -atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V) - -atomic_inc_return(X) __atomic_op_return{mb}(X,+,1) -atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1) -atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1) -atomic_inc_return_release(X) __atomic_op_return{release}(X,+,1) -atomic_fetch_inc(X) __atomic_fetch_op{mb}(X,+,1) -atomic_fetch_inc_relaxed(X) __atomic_fetch_op{once}(X,+,1) -atomic_fetch_inc_acquire(X) __atomic_fetch_op{acquire}(X,+,1) -atomic_fetch_inc_release(X) __atomic_fetch_op{release}(X,+,1) - -atomic_sub_return(V,X) __atomic_op_return{mb}(X,-,V) -atomic_sub_return_relaxed(V,X) __atomic_op_return{once}(X,-,V) -atomic_sub_return_acquire(V,X) __atomic_op_return{acquire}(X,-,V) -atomic_sub_return_release(V,X) __atomic_op_return{release}(X,-,V) -atomic_fetch_sub(V,X) __atomic_fetch_op{mb}(X,-,V) -atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{once}(X,-,V) -atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{acquire}(X,-,V) -atomic_fetch_sub_release(V,X) __atomic_fetch_op{release}(X,-,V) - -atomic_dec_return(X) __atomic_op_return{mb}(X,-,1) -atomic_dec_return_relaxed(X) __atomic_op_return{once}(X,-,1) -atomic_dec_return_acquire(X) __atomic_op_return{acquire}(X,-,1) -atomic_dec_return_release(X) __atomic_op_return{release}(X,-,1) -atomic_fetch_dec(X) __atomic_fetch_op{mb}(X,-,1) -atomic_fetch_dec_relaxed(X) __atomic_fetch_op{once}(X,-,1) -atomic_fetch_dec_acquire(X) __atomic_fetch_op{acquire}(X,-,1) -atomic_fetch_dec_release(X) __atomic_fetch_op{release}(X,-,1) - -atomic_xchg(X,V) __xchg{mb}(X,V) -atomic_xchg_relaxed(X,V) __xchg{once}(X,V) -atomic_xchg_release(X,V) __xchg{release}(X,V) -atomic_xchg_acquire(X,V) __xchg{acquire}(X,V) -atomic_cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W) -atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W) -atomic_cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W) -atomic_cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) - -atomic_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) == 0 -atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) == 0 -atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) == 0 -atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 +atomic_add(V,X) { __atomic_op{NORETURN}(X,+,V); } +atomic_sub(V,X) { __atomic_op{NORETURN}(X,-,V); } +atomic_and(V,X) { __atomic_op{NORETURN}(X,&,V); } +atomic_or(V,X) { __atomic_op{NORETURN}(X,|,V); } +atomic_xor(V,X) { __atomic_op{NORETURN}(X,^,V); } +atomic_inc(X) { __atomic_op{NORETURN}(X,+,1); } +atomic_dec(X) { __atomic_op{NORETURN}(X,-,1); } +atomic_andnot(V,X) { __atomic_op{NORETURN}(X,&~,V); } + +atomic_add_return(V,X) __atomic_op_return{MB}(X,+,V) +atomic_add_return_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V) +atomic_add_return_acquire(V,X) __atomic_op_return{ACQUIRE}(X,+,V) +atomic_add_return_release(V,X) __atomic_op_return{RELEASE}(X,+,V) +atomic_fetch_add(V,X) __atomic_fetch_op{MB}(X,+,V) +atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{ONCE}(X,+,V) +atomic_fetch_add_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,+,V) +atomic_fetch_add_release(V,X) __atomic_fetch_op{RELEASE}(X,+,V) + +atomic_fetch_and(V,X) __atomic_fetch_op{MB}(X,&,V) +atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{ONCE}(X,&,V) +atomic_fetch_and_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,&,V) +atomic_fetch_and_release(V,X) __atomic_fetch_op{RELEASE}(X,&,V) + +atomic_fetch_or(V,X) __atomic_fetch_op{MB}(X,|,V) +atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{ONCE}(X,|,V) +atomic_fetch_or_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,|,V) +atomic_fetch_or_release(V,X) __atomic_fetch_op{RELEASE}(X,|,V) + +atomic_fetch_xor(V,X) __atomic_fetch_op{MB}(X,^,V) +atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{ONCE}(X,^,V) +atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,^,V) +atomic_fetch_xor_release(V,X) __atomic_fetch_op{RELEASE}(X,^,V) + +atomic_inc_return(X) __atomic_op_return{MB}(X,+,1) +atomic_inc_return_relaxed(X) __atomic_op_return{ONCE}(X,+,1) +atomic_inc_return_acquire(X) __atomic_op_return{ACQUIRE}(X,+,1) +atomic_inc_return_release(X) __atomic_op_return{RELEASE}(X,+,1) +atomic_fetch_inc(X) __atomic_fetch_op{MB}(X,+,1) +atomic_fetch_inc_relaxed(X) __atomic_fetch_op{ONCE}(X,+,1) +atomic_fetch_inc_acquire(X) __atomic_fetch_op{ACQUIRE}(X,+,1) +atomic_fetch_inc_release(X) __atomic_fetch_op{RELEASE}(X,+,1) + +atomic_sub_return(V,X) __atomic_op_return{MB}(X,-,V) +atomic_sub_return_relaxed(V,X) __atomic_op_return{ONCE}(X,-,V) +atomic_sub_return_acquire(V,X) __atomic_op_return{ACQUIRE}(X,-,V) +atomic_sub_return_release(V,X) __atomic_op_return{RELEASE}(X,-,V) +atomic_fetch_sub(V,X) __atomic_fetch_op{MB}(X,-,V) +atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{ONCE}(X,-,V) +atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,-,V) +atomic_fetch_sub_release(V,X) __atomic_fetch_op{RELEASE}(X,-,V) + +atomic_dec_return(X) __atomic_op_return{MB}(X,-,1) +atomic_dec_return_relaxed(X) __atomic_op_return{ONCE}(X,-,1) +atomic_dec_return_acquire(X) __atomic_op_return{ACQUIRE}(X,-,1) +atomic_dec_return_release(X) __atomic_op_return{RELEASE}(X,-,1) +atomic_fetch_dec(X) __atomic_fetch_op{MB}(X,-,1) +atomic_fetch_dec_relaxed(X) __atomic_fetch_op{ONCE}(X,-,1) +atomic_fetch_dec_acquire(X) __atomic_fetch_op{ACQUIRE}(X,-,1) +atomic_fetch_dec_release(X) __atomic_fetch_op{RELEASE}(X,-,1) + +atomic_xchg(X,V) __xchg{MB}(X,V) +atomic_xchg_relaxed(X,V) __xchg{ONCE}(X,V) +atomic_xchg_release(X,V) __xchg{RELEASE}(X,V) +atomic_xchg_acquire(X,V) __xchg{ACQUIRE}(X,V) +atomic_cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W) +atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W) +atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W) +atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W) + +atomic_sub_and_test(V,X) __atomic_op_return{MB}(X,-,V) == 0 +atomic_dec_and_test(X) __atomic_op_return{MB}(X,-,1) == 0 +atomic_inc_and_test(X) __atomic_op_return{MB}(X,+,1) == 0 +atomic_add_negative(V,X) __atomic_op_return{MB}(X,+,V) < 0 +atomic_add_negative_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V) < 0 +atomic_add_negative_acquire(V,X) __atomic_op_return{ACQUIRE}(X,+,V) < 0 +atomic_add_negative_release(V,X) __atomic_op_return{RELEASE}(X,+,V) < 0 + +atomic_fetch_andnot(V,X) __atomic_fetch_op{MB}(X,&~,V) +atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,&~,V) +atomic_fetch_andnot_release(V,X) __atomic_fetch_op{RELEASE}(X,&~,V) +atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{ONCE}(X,&~,V) + +atomic_add_unless(X,V,W) __atomic_add_unless{MB}(X,V,W) diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore index c492a1ddad91..19c379cf069d 100644 --- a/tools/memory-model/litmus-tests/.gitignore +++ b/tools/memory-model/litmus-tests/.gitignore @@ -1,2 +1,2 @@ # SPDX-License-Identifier: GPL-2.0-only -*.litmus.out +*.litmus.* diff --git a/tools/memory-model/litmus-tests/dep+plain.litmus b/tools/memory-model/litmus-tests/dep+plain.litmus new file mode 100644 index 000000000000..ebf84daa9a59 --- /dev/null +++ b/tools/memory-model/litmus-tests/dep+plain.litmus @@ -0,0 +1,31 @@ +C dep+plain + +(* + * Result: Never + * + * This litmus test demonstrates that in LKMM, plain accesses + * carry dependencies much like accesses to registers: + * The data stored to *z1 and *z2 by P0() originates from P0()'s + * READ_ONCE(), and therefore using that data to compute the + * conditional of P0()'s if-statement creates a control dependency + * from that READ_ONCE() to P0()'s WRITE_ONCE(). + *) + +{} + +P0(int *x, int *y, int *z1, int *z2) +{ + int a = READ_ONCE(*x); + *z1 = a; + *z2 = *z1; + if (*z2 == 1) + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r = smp_load_acquire(y); + smp_store_release(x, r); +} + +exists (x=1 /\ y=1) diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 6b52f365d73a..03c12efed66a 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -36,9 +36,9 @@ let RU = try RU with emptyset (* Treat RL as a kind of LF: a read with no ordering properties *) let LF = LF | RL -(* There should be no ordinary R or W accesses to spinlocks *) -let ALL-LOCKS = LKR | LKW | UL | LF | RU -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *) +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses (* Link Lock-Reads to their RMW-partner Lock-Writes *) let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) @@ -54,6 +54,12 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR *) empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest +(* + * In the same way, spin_is_locked() inside a critical section must always + * return True (no RU events can be in a critical section for the same lock). + *) +empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked + (* The final value of a spinlock should not be tested *) flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final @@ -79,42 +85,50 @@ empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks (* rfi for LF events: link each LKW to the LF events in its critical section *) let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc) -(* rfe for LF events *) +(* Utility macro to convert a single pair to a single-edge relation *) +let pair-to-relation p = p ++ 0 + +(* + * If a given LF event e is outside a critical section, it cannot read + * internally but it may read from an LKW event in another thread. + * Compute the relation containing these possible edges. + *) +let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext + +(* Compute set of sets of possible rfe edges for LF events *) let all-possible-rfe-lf = (* - * Given an LF event r, compute the possible rfe edges for that event - * (all those starting from LKW events in other threads), - * and then convert that relation to a set of single-edge relations. + * Convert the possible-rfe-noncrit-lf relation for e + * to a set of single edges *) - let possible-rfe-lf r = - let pair-to-relation p = p ++ 0 - in map pair-to-relation ((LKW * {r}) & loc & ext) - (* Do this for each LF event r that isn't in rfi-lf *) - in map possible-rfe-lf (LF \ range(rfi-lf)) + let set-of-singleton-rfe-lf e = + map pair-to-relation (possible-rfe-noncrit-lf e) + (* Do this for each LF event e that isn't in rfi-lf *) + in map set-of-singleton-rfe-lf (LF \ range(rfi-lf)) (* Generate all rf relations for LF events *) with rfe-lf from cross(all-possible-rfe-lf) let rf-lf = rfe-lf | rfi-lf (* - * RU, i.e., spin_is_locked() returning False, is slightly different. - * We rely on the memory model to rule out cases where spin_is_locked() - * within one of the lock's critical sections returns False. + * A given RU event e may read internally from the last po-previous UL, + * or it may read from a UL event in another thread or the initial write. + * Compute the relation containing these possible edges. *) - -(* rfi for RU events: an RU may read from the last po-previous UL *) -let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc) - -(* rfe for RU events: an RU may read from an external UL or the initial write *) -let all-possible-rfe-ru = - let possible-rfe-ru r = - let pair-to-relation p = p ++ 0 - in map pair-to-relation (((UL | IW) * {r}) & loc & ext) - in map possible-rfe-ru RU +let possible-rf-ru e = (((UL * {e}) & po-loc) \ + ([UL] ; po-loc ; [UL] ; po-loc)) | + (((UL | IW) * {e}) & loc & ext) + +(* Compute set of sets of possible rf edges for RU events *) +let all-possible-rf-ru = + (* Convert the possible-rf-ru relation for e to a set of single edges *) + let set-of-singleton-rf-ru e = + map pair-to-relation (possible-rf-ru e) + (* Do this for each RU event e *) + in map set-of-singleton-rf-ru RU (* Generate all rf relations for RU events *) -with rfe-ru from cross(all-possible-rfe-ru) -let rf-ru = rfe-ru | rfi-ru +with rf-ru from cross(all-possible-rf-ru) (* Final rf relation *) let rf = rf | rf-lf | rf-ru diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index 095c7eb36f9f..fb39bd0fd1b9 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -27,6 +27,14 @@ checklitmushist.sh checklitmus.sh Check a single litmus test against its "Result:" expected result. + Not intended to for manual use. + +checktheselitmus.sh + + Check the specified list of litmus tests against their "Result:" + expected results. This takes optional parseargs.sh arguments, + followed by "--" followed by pathnames starting from the current + directory. cmplitmushist.sh @@ -43,10 +51,10 @@ initlitmushist.sh judgelitmus.sh - Given a .litmus file and its .litmus.out herd7 output, check the - .litmus.out file against the .litmus file's "Result:" comment to - judge whether the test ran correctly. Not normally run manually, - provided instead for use by other scripts. + Given a .litmus file and its herd7 output, check the output file + against the .litmus file's "Result:" comment to judge whether + the test ran correctly. Not normally run manually, provided + instead for use by other scripts. newlitmushist.sh @@ -68,3 +76,35 @@ runlitmushist.sh README This file + +Testing a change to LKMM might go as follows: + + # Populate expected results without that change, and + # runs for about an hour on an 8-CPU x86 system: + scripts/initlitmushist.sh --timeout 10m --procs 10 + # Incorporate the change: + git am -s -3 /path/to/patch # Or whatever it takes. + + # Test the new version of LKMM as follows... + + # Runs in seconds, good smoke test: + scripts/checkalllitmus.sh + + # Compares results to those produced by initlitmushist.sh, + # and runs for about an hour on an 8-CPU x86 system: + scripts/checklitmushist.sh --timeout 10m --procs 10 + + # Checks results against Result tags, runs in minutes: + scripts/checkghlitmus.sh --timeout 10m --procs 10 + +The checkghlitmus.sh should not report errors in cases where the +checklitmushist.sh script did not also report a change. However, +this check is nevertheless valuable because it can find errors in the +original version of LKMM. Note however, that given the above procedure, +an error in the original LKMM version that is fixed by the patch will +be reported both as a mismatch by checklitmushist.sh and as an error +by checkghlitmus.sh. One exception to this rule of thumb is when the +test fails completely on the original version of LKMM and passes on the +new version. In this case, checklitmushist.sh will report a mismatch +and checkghlitmus.sh will report success. This happens when the change +to LKMM introduces a new primitive for which litmus tests already existed. diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh index 3c0c7fbbd223..2d3ee850a839 100755 --- a/tools/memory-model/scripts/checkalllitmus.sh +++ b/tools/memory-model/scripts/checkalllitmus.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash # SPDX-License-Identifier: GPL-2.0+ # # Run herd7 tests on all .litmus files in the litmus-tests directory @@ -8,6 +8,11 @@ # "^^^". It also outputs verification results to a file whose name is # that of the specified litmus test, but with ".out" appended. # +# If the --hw argument is specified, this script translates the .litmus +# C-language file to the specified type of assembly and verifies that. +# But in this case, litmus tests using complex synchronization (such as +# locking, RCU, and SRCU) are cheerfully ignored. +# # Usage: # checkalllitmus.sh # @@ -17,7 +22,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> . scripts/parseargs.sh @@ -30,29 +35,23 @@ else exit 255 fi -# Create any new directories that have appeared in the github litmus -# repo since the last run. +# Create any new directories that have appeared in the litmus-tests +# directory since the last run. if test "$LKMM_DESTDIR" != "." then find $litmusdir -type d -print | ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh ) fi -# Find the checklitmus script. If it is not where we expect it, then -# assume that the caller has the PATH environment variable set -# appropriately. -if test -x scripts/checklitmus.sh -then - clscript=scripts/checklitmus.sh -else - clscript=checklitmus.sh -fi - # Run the script on all the litmus tests in the specified directory ret=0 for i in $litmusdir/*.litmus do - if ! $clscript $i + if test -n "$LKMM_HW_MAP_FILE" && ! scripts/simpletest.sh $i + then + continue + fi + if ! scripts/checklitmus.sh $i then ret=1 fi diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh index 6589fbb6f653..d3dfb321259f 100755 --- a/tools/memory-model/scripts/checkghlitmus.sh +++ b/tools/memory-model/scripts/checkghlitmus.sh @@ -10,6 +10,7 @@ # parseargs.sh scripts for arguments. . scripts/parseargs.sh +. scripts/hwfnseg.sh T=/tmp/checkghlitmus.sh.$$ trap 'rm -rf $T' 0 @@ -32,19 +33,19 @@ then ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh ) fi -# Create a list of the C-language litmus tests previously run. -( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) | - sed -e 's/\.out$//' | - xargs -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' | +# Create a list of the specified litmus tests previously run. +( cd $LKMM_DESTDIR; find litmus -name "*.litmus${hwfnseg}.out" -print ) | + sed -e "s/${hwfnseg}"'\.out$//' | + xargs -r grep -E -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' | xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already # Create a list of C-language litmus tests with "Result:" commands and # no more than the specified number of processes. -find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C -xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result +find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C +xargs < $T/list-C -r grep -E -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short -# Form list of tests without corresponding .litmus.out files +# Form list of tests without corresponding .out files sort $T/list-C-already $T/list-C-result-short | uniq -u > $T/list-C-needed # Run any needed tests. diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh index 11461ed40b5e..4c1d0cf0ddad 100755 --- a/tools/memory-model/scripts/checklitmus.sh +++ b/tools/memory-model/scripts/checklitmus.sh @@ -1,10 +1,8 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# Run a herd7 test and invokes judgelitmus.sh to check the result against -# a "Result:" comment within the litmus test. It also outputs verification -# results to a file whose name is that of the specified litmus test, but -# with ".out" appended. +# Invokes runlitmus.sh and judgelitmus.sh on its arguments to run the +# specified litmus test and pass judgment on the results. # # Usage: # checklitmus.sh file.litmus @@ -15,20 +13,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> -litmus=$1 -herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} - -if test -f "$litmus" -a -r "$litmus" -then - : -else - echo ' --- ' error: \"$litmus\" is not a readable file - exit 255 -fi - -echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 - -scripts/judgelitmus.sh $litmus +scripts/runlitmus.sh $1 +scripts/judgelitmus.sh $1 diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh index 1d210ffb7c8a..406ecfc0aee4 100755 --- a/tools/memory-model/scripts/checklitmushist.sh +++ b/tools/memory-model/scripts/checklitmushist.sh @@ -12,7 +12,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> . scripts/parseargs.sh diff --git a/tools/memory-model/scripts/checktheselitmus.sh b/tools/memory-model/scripts/checktheselitmus.sh new file mode 100755 index 000000000000..10eeb5ecea6d --- /dev/null +++ b/tools/memory-model/scripts/checktheselitmus.sh @@ -0,0 +1,43 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Invokes checklitmus.sh on its arguments to run the specified litmus +# test and pass judgment on the results. +# +# Usage: +# checktheselitmus.sh -- [ file1.litmus [ file2.litmus ... ] ] +# +# Run this in the directory containing the memory model, specifying the +# pathname of the litmus test to check. The usual parseargs.sh arguments +# can be specified prior to the "--". +# +# This script is intended for use with pathnames that start from the +# tools/memory-model directory. If some of the pathnames instead start at +# the root directory, they all must do so and the "--destdir /" parseargs.sh +# argument must be specified prior to the "--". Alternatively, some other +# "--destdir" argument can be supplied as long as the needed subdirectories +# are populated. +# +# Copyright IBM Corporation, 2018 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +. scripts/parseargs.sh + +ret=0 +for i in "$@" +do + if scripts/checklitmus.sh $i + then + : + else + ret=1 + fi +done +if test "$ret" -ne 0 +then + echo " ^^^ VERIFICATION MISMATCHES" 1>&2 +else + echo All litmus tests verified as was expected. 1>&2 +fi +exit $ret diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh index 0f498aeeccf5..ca1ac8b64614 100755 --- a/tools/memory-model/scripts/cmplitmushist.sh +++ b/tools/memory-model/scripts/cmplitmushist.sh @@ -12,12 +12,49 @@ trap 'rm -rf $T' 0 mkdir $T # comparetest oldpath newpath +badmacnam=0 +timedout=0 perfect=0 obsline=0 noobsline=0 obsresult=0 badcompare=0 comparetest () { + if grep -q ': Unknown macro ' $1 || grep -q ': Unknown macro ' $2 + then + if grep -q ': Unknown macro ' $1 + then + badname=`grep ': Unknown macro ' $1 | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + echo 'Current LKMM version does not know "'$badname'"' $1 + fi + if grep -q ': Unknown macro ' $2 + then + badname=`grep ': Unknown macro ' $2 | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + echo 'Current LKMM version does not know "'$badname'"' $2 + fi + badmacnam=`expr "$badmacnam" + 1` + return 0 + elif grep -q '^Command exited with non-zero status 124' $1 || + grep -q '^Command exited with non-zero status 124' $2 + then + if grep -q '^Command exited with non-zero status 124' $1 && + grep -q '^Command exited with non-zero status 124' $2 + then + echo Both runs timed out: $2 + elif grep -q '^Command exited with non-zero status 124' $1 + then + echo Old run timed out: $2 + elif grep -q '^Command exited with non-zero status 124' $2 + then + echo New run timed out: $2 + fi + timedout=`expr "$timedout" + 1` + return 0 + fi grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1 @@ -38,7 +75,7 @@ comparetest () { return 0 fi else - echo Missing Observation line "(e.g., herd7 timeout)": $2 + echo Missing Observation line "(e.g., syntax error)": $2 noobsline=`expr "$noobsline" + 1` return 0 fi @@ -72,12 +109,20 @@ then fi if test "$noobsline" -ne 0 then - echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2 + echo Missing Observation line "(e.g., syntax error)": $noobsline 1>&2 fi if test "$obsresult" -ne 0 then echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2 fi +if test "$timedout" -ne 0 +then + echo "!!!" Timed out: $timedout 1>&2 +fi +if test "$badmacnam" -ne 0 +then + echo "!!!" Unknown primitive: $badmacnam 1>&2 +fi if test "$badcompare" -ne 0 then echo "!!!" Result changed: $badcompare 1>&2 diff --git a/tools/memory-model/scripts/hwfnseg.sh b/tools/memory-model/scripts/hwfnseg.sh new file mode 100755 index 000000000000..580c3281181c --- /dev/null +++ b/tools/memory-model/scripts/hwfnseg.sh @@ -0,0 +1,20 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Generate the hardware extension to the litmus-test filename, or the +# empty string if this is an LKMM run. The extension is placed in +# the shell variable hwfnseg. +# +# Usage: +# . hwfnseg.sh +# +# Copyright IBM Corporation, 2019 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +if test -z "$LKMM_HW_MAP_FILE" +then + hwfnseg= +else + hwfnseg=".$LKMM_HW_MAP_FILE" +fi diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh index 956b6957484d..31ea782955d3 100755 --- a/tools/memory-model/scripts/initlitmushist.sh +++ b/tools/memory-model/scripts/initlitmushist.sh @@ -60,7 +60,7 @@ fi # Create a list of the C-language litmus tests with no more than the # specified number of processes (per the --procs argument). -find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C +find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C xargs < $T/list-C -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short scripts/runlitmushist.sh < $T/list-C-short diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index 0cc63875e395..1ec5d89fcfbb 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -1,9 +1,22 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# Given a .litmus test and the corresponding .litmus.out file, check -# the .litmus.out file against the "Result:" comment to judge whether -# the test ran correctly. +# Given a .litmus test and the corresponding litmus output file, check +# the .litmus.out file against the "Result:" comment to judge whether the +# test ran correctly. If the --hw argument is omitted, check against the +# LKMM output, which is assumed to be in file.litmus.out. If either a +# "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker +# in the LKMM output is present, the other must also be as well, at least +# for litmus tests having a "Result:" comment. In this case, a failure of +# the Always/Sometimes/Never portion of the "Result:" prediction will be +# noted, but forgiven. +# +# If the --hw argument is provided, this is assumed to be a hardware +# test, and the output is assumed to be in file.litmus.HW.out, where +# "HW" is the --hw argument. In addition, non-Sometimes verification +# results will be noted, but forgiven. Furthermore, if there is no +# "Result:" comment but there is an LKMM .litmus.out file, the observation +# in that file will be used to judge the assembly-language verification. # # Usage: # judgelitmus.sh file.litmus @@ -13,7 +26,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> litmus=$1 @@ -24,55 +37,120 @@ else echo ' --- ' error: \"$litmus\" is not a readable file exit 255 fi -if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out +if test -z "$LKMM_HW_MAP_FILE" +then + litmusout=$litmus.out + lkmmout= +else + litmusout="`echo $litmus | + sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out" + lkmmout=$litmus.out +fi +if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" then : else - echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file + echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file exit 255 fi -if grep -q '^ \* Result: ' $litmus +if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" +then + datarace_modeled=1 +fi +if grep -q '^[( ]\* Result: ' $litmus +then + outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'` + if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus + then + datarace_predicted=1 + fi + if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE" + then + echo '!!! Predicted data race not modeled' $litmus + exit 252 + elif test -z "$datarace_predicted" -a -n "$datarace_modeled" + then + # Note that hardware models currently don't model data races + echo '!!! Unexpected data race modeled' $litmus + exit 253 + fi +elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 then - outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` + outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` else outcome=specified fi -grep '^Observation' $LKMM_DESTDIR/$litmus.out -if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out +grep '^Observation' $LKMM_DESTDIR/$litmusout +if grep -q '^Observation' $LKMM_DESTDIR/$litmusout then : +elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout +then + badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus" + echo $badmsg + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout + then + echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1 + fi + exit 254 +elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout +then + echo ' !!! Timeout' $litmus + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout + then + echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1 + fi + exit 124 else echo ' !!! Verification error' $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1 fi exit 255 fi if test "$outcome" = DEADLOCK then - if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$' + if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' then ret=0 else echo " !!! Unexpected non-$outcome verification" $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 fi ret=1 fi -elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe +elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' +then + echo " !!! Unexpected non-$outcome deadlock" $litmus + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout + then + echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1 + fi + ret=1 +elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe then ret=0 else - echo " !!! Unexpected non-$outcome verification" $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled" then - echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1 + flag="--- Forgiven" + ret=0 + else + flag="!!! Unexpected" + ret=1 + fi + echo " $flag non-$outcome verification" $litmus + if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout + then + echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 fi - ret=1 fi -tail -2 $LKMM_DESTDIR/$litmus.out | head -1 +tail -2 $LKMM_DESTDIR/$litmusout | head -1 exit $ret diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh index 991f8f814881..25235e2049cf 100755 --- a/tools/memory-model/scripts/newlitmushist.sh +++ b/tools/memory-model/scripts/newlitmushist.sh @@ -12,7 +12,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> . scripts/parseargs.sh @@ -43,7 +43,7 @@ fi # Form full list of litmus tests with no more than the specified # number of processes (per the --procs argument). -find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C-all +find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C-all xargs < $T/list-C-all -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short # Form list of new tests. Note: This does not handle litmus-test deletion! diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index 40f52080fdbd..08ded5909860 100755 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -1,7 +1,7 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# the corresponding .litmus.out file, and does not judge the result. +# Parse arguments common to the various scripts. # # . scripts/parseargs.sh # @@ -9,7 +9,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> T=/tmp/parseargs.sh.$$ mkdir $T @@ -27,6 +27,7 @@ initparam () { initparam LKMM_DESTDIR "." initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg" +initparam LKMM_HW_MAP_FILE "" initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN` initparam LKMM_PROCS "3" initparam LKMM_TIMEOUT "1m" @@ -37,10 +38,11 @@ usagehelp () { echo "Usage $scriptname [ arguments ]" echo " --destdir path (place for .litmus.out, default by .litmus)" echo " --herdopts -conf linux-kernel.cfg ..." + echo " --hw AArch64" echo " --jobs N (number of jobs, default one per CPU)" echo " --procs N (litmus tests with at most this many processes)" echo " --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')" - echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'" + echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --hw '$LKMM_HW_MAP_FILE' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'" exit 1 } @@ -81,7 +83,7 @@ do echo "Cannot create directory --destdir '$LKMM_DESTDIR'" usage fi - if test -d "$LKMM_DESTDIR" -a -w "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR" + if test -d "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR" then : else @@ -95,6 +97,11 @@ do LKMM_HERD_OPTIONS="$2" shift ;; + --hw) + checkarg --hw "(.map file architecture name)" "$#" "$2" '^[A-Za-z0-9_-]\+' '^--' + LKMM_HW_MAP_FILE="$2" + shift + ;; -j[1-9]*) njobs="`echo $1 | sed -e 's/^-j//'`" trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`" @@ -106,7 +113,7 @@ do LKMM_JOBS="`echo $njobs | sed -e 's/^\([0-9]\+\).*$/\1/'`" ;; --jobs|--job|-j) - checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]\+$' '^--' + checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]*$' '^--' LKMM_JOBS="$2" shift ;; @@ -120,6 +127,10 @@ do LKMM_TIMEOUT="$2" shift ;; + --) + shift + break + ;; *) echo Unknown argument $1 usage diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh new file mode 100755 index 000000000000..94608d4b6502 --- /dev/null +++ b/tools/memory-model/scripts/runlitmus.sh @@ -0,0 +1,80 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Without the -hw argument, runs a herd7 test and outputs verification +# results to a file whose name is that of the specified litmus test, +# but with ".out" appended. +# +# If the --hw argument is specified, this script translates the .litmus +# C-language file to the specified type of assembly and verifies that. +# But in this case, litmus tests using complex synchronization (such as +# locking, RCU, and SRCU) are cheerfully ignored. +# +# Either way, return the status of the herd7 command. +# +# Usage: +# runlitmus.sh file.litmus +# +# Run this in the directory containing the memory model, specifying the +# pathname of the litmus test to check. The caller is expected to have +# properly set up the LKMM environment variables. +# +# Copyright IBM Corporation, 2019 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +litmus=$1 +if test -f "$litmus" -a -r "$litmus" +then + : +else + echo ' !!! ' error: \"$litmus\" is not a readable file + exit 255 +fi + +if test -z "$LKMM_HW_MAP_FILE" -o ! -e $LKMM_DESTDIR/$litmus.out +then + # LKMM run + herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} + echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out + /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 + ret=$? + if test -z "$LKMM_HW_MAP_FILE" + then + exit $ret + fi + echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run +fi + +# Hardware run + +T=/tmp/checklitmushw.sh.$$ +trap 'rm -rf $T' 0 2 +mkdir $T + +# Generate filenames +mapfile="Linux2${LKMM_HW_MAP_FILE}.map" +themefile="$T/${LKMM_HW_MAP_FILE}.theme" +herdoptions="-model $LKMM_HW_CAT_FILE" +hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'` +hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` + +# Don't run on litmus tests with complex synchronization +if ! scripts/simpletest.sh $litmus +then + echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU + exit 254 +fi + +# Generate the assembly code and run herd7 on it. +gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile +jingle7 -v -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out +if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out +then + echo ' !!! ' jingle7 failed, errors in $hwlitmus.err + cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err + exit 253 +fi +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 + +exit $? diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh index 6ed376f495bb..c6c2bdc67a50 100755 --- a/tools/memory-model/scripts/runlitmushist.sh +++ b/tools/memory-model/scripts/runlitmushist.sh @@ -13,7 +13,9 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +. scripts/hwfnseg.sh T=/tmp/runlitmushist.sh.$$ trap 'rm -rf $T' 0 @@ -30,15 +32,12 @@ fi # Prefixes for per-CPU scripts for ((i=0;i<$LKMM_JOBS;i++)) do - echo dir="$LKMM_DESTDIR" > $T/$i.sh echo T=$T >> $T/$i.sh - echo herdoptions=\"$LKMM_HERD_OPTIONS\" >> $T/$i.sh cat << '___EOF___' >> $T/$i.sh runtest () { - echo ' ... ' /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 '>' $dir/$1.out '2>&1' - if /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 > $dir/$1.out 2>&1 + if scripts/runlitmus.sh $1 then - if ! grep -q '^Observation ' $dir/$1.out + if ! grep -q '^Observation ' $LKMM_DESTDIR/$1$2.out then echo ' !!! Herd failed, no Observation:' $1 fi @@ -47,10 +46,16 @@ do if test "$exitcode" -eq 124 then exitmsg="timed out" + elif test "$exitcode" -eq 253 + then + exitmsg= else exitmsg="failed, exit code $exitcode" fi - echo ' !!! Herd' ${exitmsg}: $1 + if test -n "$exitmsg" + then + echo ' !!! Herd' ${exitmsg}: $1 + fi fi } ___EOF___ @@ -59,11 +64,13 @@ done awk -v q="'" -v b='\\' ' { print "echo `grep " q "^P[0-9]" b "+(" q " " $0 " | tail -1 | sed -e " q "s/^P" b "([0-9]" b "+" b ")(.*$/" b "1/" q "` " $0 -}' | bash | -sort -k1n | -awk -v ncpu=$LKMM_JOBS -v t=$T ' +}' | sh | sort -k1n | +awk -v dq='"' -v hwfnseg="$hwfnseg" -v ncpu="$LKMM_JOBS" -v t="$T" ' { - print "runtest " $2 >> t "/" NR % ncpu ".sh"; + print "if test -z " dq hwfnseg dq " || scripts/simpletest.sh " dq $2 dq + print "then" + print "\techo runtest " dq $2 dq " " hwfnseg " >> " t "/" NR % ncpu ".sh"; + print "fi" } END { diff --git a/tools/memory-model/scripts/simpletest.sh b/tools/memory-model/scripts/simpletest.sh new file mode 100755 index 000000000000..7edc5d361665 --- /dev/null +++ b/tools/memory-model/scripts/simpletest.sh @@ -0,0 +1,35 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Give zero status if this is a simple test and non-zero otherwise. +# Simple tests do not contain locking, RCU, or SRCU. +# +# Usage: +# simpletest.sh file.litmus +# +# Copyright IBM Corporation, 2019 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + + +litmus=$1 + +if test -f "$litmus" -a -r "$litmus" +then + : +else + echo ' --- ' error: \"$litmus\" is not a readable file + exit 255 +fi +exclude="^[[:space:]]*\(" +exclude="${exclude}spin_lock(\|spin_unlock(\|spin_trylock(\|spin_is_locked(" +exclude="${exclude}\|rcu_read_lock(\|rcu_read_unlock(" +exclude="${exclude}\|synchronize_rcu(\|synchronize_rcu_expedited(" +exclude="${exclude}\|srcu_read_lock(\|srcu_read_unlock(" +exclude="${exclude}\|synchronize_srcu(\|synchronize_srcu_expedited(" +exclude="${exclude}\)" +if grep -q $exclude $litmus +then + exit 255 +fi +exit 0 |