kernel/linux.git/tools/memory-model/lock.cat, branch v6.6.131

tools/memory-model: Fix bug in lock.cat

2024-08-03T06:54:21+00:00

commit 4c830eef806679dc243e191f962c488dd9d00708 upstream. Andrea reported that the following innocuous litmus test: C T {} P0(spinlock_t *x) { int r0; spin_lock(x); spin_unlock(x); r0 = spin_is_locked(x); } gives rise to a nonsensical empty result with no executions: $ herd7 -conf linux-kernel.cfg T.litmus Test T Required States 0 Ok Witnesses Positive: 0 Negative: 0 Condition forall (true) Observation T Never 0 0 Time T 0.00 Hash=6fa204e139ddddf2cb6fa963bad117c0 The problem is caused by a bug in the lock.cat part of the LKMM. Its computation of the rf relation for RU (read-unlocked) events is faulty; it implicitly assumes that every RU event must read from either a UL (unlock) event in another thread or from the lock's initial state. Neither is true in the litmus test above, so the computation yields no possible executions. The lock.cat code tries to make up for this deficiency by allowing RU events outside of critical sections to read from the last po-previous UL event. But it does this incorrectly, trying to keep these rfi links separate from the rfe links that might also be needed, and passing only the latter to herd7's cross() macro. The problem is fixed by merging the two sets of possible rf links for RU events and using them all in the call to cross(). Signed-off-by: Alan Stern Reported-by: Andrea Parri Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/ Tested-by: Andrea Parri Acked-by: Andrea Parri Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()") CC: Signed-off-by: Paul E. McKenney Signed-off-by: Greg Kroah-Hartman

tools/memory-model: Provide exact SRCU semantics

2023-03-22T19:02:21+00:00

LKMM has long provided only approximate handling of SRCU read-side critical sections. This has not been a pressing problem because LKMM's traditional handling is correct for the common cases of non-overlapping and properly nested critical sections. However, LKMM's traditional handling of partially overlapping critical sections incorrectly fuses them into one large critical section. For example, consider the following litmus test: ------------------------------------------------------------------------ C C-srcu-nest-5 (* * Result: Sometimes * * This demonstrates non-nested overlapping of SRCU read-side critical * sections. Unlike RCU, SRCU critical sections do not unconditionally * nest. *) {} P0(int *x, int *y, struct srcu_struct *s1) { int r1; int r2; int r3; int r4; r3 = srcu_read_lock(s1); r2 = READ_ONCE(*y); r4 = srcu_read_lock(s1); srcu_read_unlock(s1, r3); r1 = READ_ONCE(*x); srcu_read_unlock(s1, r4); } P1(int *x, int *y, struct srcu_struct *s1) { WRITE_ONCE(*y, 1); synchronize_srcu(s1); WRITE_ONCE(*x, 1); } locations [0:r1] exists (0:r1=1 /\ 0:r2=0) ------------------------------------------------------------------------ Current mainline incorrectly flattens the two critical sections into one larger critical section, giving "Never" instead of the correct "Sometimes": ------------------------------------------------------------------------ $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus Test C-srcu-nest-5 Allowed States 3 0:r1=0; 0:r2=0; 0:r1=0; 0:r2=1; 0:r1=1; 0:r2=1; No Witnesses Positive: 0 Negative: 3 Flag srcu-bad-nesting Condition exists (0:r1=1 /\ 0:r2=0) Observation C-srcu-nest-5 Never 0 3 Time C-srcu-nest-5 0.01 Hash=e692c106cf3e84e20f12991dc438ff1b ------------------------------------------------------------------------ To its credit, it does complain about bad nesting. But with this commit we get the following result, which has the virtue of being correct: ------------------------------------------------------------------------ $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus Test C-srcu-nest-5 Allowed States 4 0:r1=0; 0:r2=0; 0:r1=0; 0:r2=1; 0:r1=1; 0:r2=0; 0:r1=1; 0:r2=1; Ok Witnesses Positive: 1 Negative: 3 Condition exists (0:r1=1 /\ 0:r2=0) Observation C-srcu-nest-5 Sometimes 1 3 Time C-srcu-nest-5 0.05 Hash=e692c106cf3e84e20f12991dc438ff1b ------------------------------------------------------------------------ In addition, there are new srcu_down_read() and srcu_up_read() functions on their way to mainline. Roughly speaking, these are to srcu_read_lock() and srcu_read_unlock() as down() and up() are to mutex_lock() and mutex_unlock(). The key point is that srcu_down_read() can execute in one process and the matching srcu_up_read() in another, as shown in this litmus test: ------------------------------------------------------------------------ C C-srcu-nest-6 (* * Result: Never * * This would be valid for srcu_down_read() and srcu_up_read(). *) {} P0(int *x, int *y, struct srcu_struct *s1, int *idx, int *f) { int r2; int r3; r3 = srcu_down_read(s1); WRITE_ONCE(*idx, r3); r2 = READ_ONCE(*y); smp_store_release(f, 1); } P1(int *x, int *y, struct srcu_struct *s1, int *idx, int *f) { int r1; int r3; int r4; r4 = smp_load_acquire(f); r1 = READ_ONCE(*x); r3 = READ_ONCE(*idx); srcu_up_read(s1, r3); } P2(int *x, int *y, struct srcu_struct *s1) { WRITE_ONCE(*y, 1); synchronize_srcu(s1); WRITE_ONCE(*x, 1); } locations [0:r1] filter (1:r4=1) exists (1:r1=1 /\ 0:r2=0) ------------------------------------------------------------------------ When run on current mainline, this litmus test gets a complaint about an unknown macro srcu_down_read(). With this commit: ------------------------------------------------------------------------ herd7 -conf linux-kernel.cfg C-srcu-nest-6.litmus Test C-srcu-nest-6 Allowed States 3 0:r1=0; 0:r2=0; 1:r1=0; 0:r1=0; 0:r2=1; 1:r1=0; 0:r1=0; 0:r2=1; 1:r1=1; No Witnesses Positive: 0 Negative: 3 Condition exists (1:r1=1 /\ 0:r2=0) Observation C-srcu-nest-6 Never 0 3 Time C-srcu-nest-6 0.02 Hash=c1f20257d052ca5e899be508bedcb2a1 ------------------------------------------------------------------------ Note that the user must supply the flag "f" and the "filter" clause, similar to what must be done to emulate call_rcu(). The commit works by treating srcu_read_lock()/srcu_down_read() as loads and srcu_read_unlock()/srcu_up_read() as stores. This allows us to determine which unlock matches which lock by looking for a data dependency between them. In order for this to work properly, the data dependencies have to be tracked through stores to intermediate variables such as "idx" in the litmus test above; this is handled by the new carry-srcu-data relation. But it's important here (and in the existing carry-dep relation) to avoid tracking the dependencies through SRCU unlock stores. Otherwise, in situations resembling: A: r1 = srcu_read_lock(s); B: srcu_read_unlock(s, r1); C: r2 = srcu_read_lock(s); D: srcu_read_unlock(s, r2); it would look as if D was dependent on both A and C, because "s" would appear to be an intermediate variable written by B and read by C. This explains the complications in the definitions of carry-srcu-dep and carry-dep. As a debugging aid, the commit adds a check for errors in which the value returned by one call to srcu_read_lock()/srcu_down_read() is passed to more than one instance of srcu_read_unlock()/srcu_up_read(). Finally, since these SRCU-related primitives are now treated as ordinary reads and writes, we have to add them into the lists of marked accesses (i.e., not subject to data races) and lock-related accesses (i.e., one shouldn't try to access an srcu_struct with a non-lock-related primitive such as READ_ONCE() or a plain write). Portions of this approach were suggested by Boqun Feng and Jonas Oberhauser. [ paulmck: Fix space-before-tab whitespace nit. ] Reported-by: Paul E. McKenney Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney

tools/memory-model: Do not use "herd" to refer to "herd7"

2019-06-19T16:32:10+00:00

Use "herd7" in each such reference. Signed-off-by: Andrea Parri Cc: Will Deacon Cc: Peter Zijlstra Cc: Boqun Feng Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: "Paul E. McKenney" Cc: Akira Yokosawa Cc: Daniel Lustig Acked-by: Alan Stern Signed-off-by: Paul E. McKenney

tools/memory-model: Avoid duplicating herdtools versions

2019-03-18T17:27:52+00:00

Currently, herdtools version information appears no fewer than three times in the LKMM source, which is difficult to maintain. This commit therefore places the required version in one place, namely the tools/memory-model/README file. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Alan Stern

tools/memory-model: Fix coding style in 'lock.cat'

2018-05-15T06:11:18+00:00

This commit uses tabs for indentation and adds spaces around binary operator. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Cc: Andrew Morton Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-16-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Remove out-of-date comments and code from lock.cat

2018-05-15T06:11:18+00:00

lock.cat contains old comments and code referring to the possibility of LKR events that are not part of an RMW pair. This is a holdover from when I though we might end up using LKR events to implement spin_is_locked(). Reword the comments to remove this assumption and replace domain(lk-rmw) in the code with LKR. Tested-by: Andrea Parri [ paulmck: Pulled as lock-nest into previous line as discussed. ] Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-15-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Improve mixed-access checking in lock.cat

2018-05-15T06:11:18+00:00

The code in lock.cat which checks for normal read/write accesses to spinlock variables doesn't take into account the newly added RL and RU events. Add them into the test, and move the resulting code up near the start of the file, since a violation would indicate a pretty severe conceptual error in a litmus test. Tested-by: Andrea Parri Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-14-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Improve comments in lock.cat

2018-05-15T06:11:18+00:00

This patch improves the comments in tools/memory-model/lock.cat. In addition to making the text more uniform and removing redundant comments, it adds a description of all the possible locking events that herd can generate. Tested-by: Andrea Parri Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-13-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Remove duplicated code from lock.cat

2018-05-15T06:11:17+00:00

This patch simplifies the implementation of spin_is_locked in the LKMM. It capitalizes on the fact that a failed spin_trylock() and a spin_is_locked() which returns True have exactly the same semantics (those of READ_ONCE) and ordering properties (none). Therefore the two kinds of events can be combined and handled by the same code, instead of treated separately as they are currently. Tested-by: Andrea Parri Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-12-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add model support for spin_is_locked()

2018-05-15T06:11:17+00:00

This commit first adds a trivial macro for spin_is_locked() to linux-kernel.def. It also adds cat code for enumerating all possible matches of lock write events (set LKW) with islocked events returning true (set RL, for Read from Lock), and unlock write events (set UL) with islocked events returning false (set RU, for Read from Unlock). Note that this intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally returns zero. It also adds a pair of litmus tests demonstrating the minimal ordering provided by spin_is_locked() in conjunction with spin_lock(). Will Deacon noted that this minimal ordering happens on ARMv8: https://lkml.kernel.org/r/20180226162426.GB17158@arm.com Notice that herd7 installations strictly older than version 7.49 do not handle the new constructs. Signed-off-by: Luc Maranget Signed-off-by: Paul E. McKenney Reviewed-by: Alan Stern Cc: Akira Yokosawa Cc: Andrea Parri Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Link: http://lkml.kernel.org/r/1526340837-12222-10-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar