* [PATCH 0/2] SRCU changes for the Linux Kernel Memory Model @ 2023-01-25 20:19 Alan Stern 2023-01-25 20:20 ` [Patch 1/2] tools/memory-model: Update some warning labels Alan Stern 0 siblings, 1 reply; 15+ messages in thread From: Alan Stern @ 2023-01-25 20:19 UTC (permalink / raw) To: Paul E. McKenney Cc: Jonas Oberhauser, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list Paul et al.: Here are the promised patches for the LKMM. 1/2: tools/memory-model: Update some warning labels 2/2: tools/memory-model: Provide exact SRCU semantics Alan ^ permalink raw reply [flat|nested] 15+ messages in thread
* [Patch 1/2] tools/memory-model: Update some warning labels 2023-01-25 20:19 [PATCH 0/2] SRCU changes for the Linux Kernel Memory Model Alan Stern @ 2023-01-25 20:20 ` Alan Stern 2023-01-25 20:21 ` [Patch 2/2] tools/memory-model: Provide exact SRCU semantics Alan Stern 2023-01-25 20:35 ` [Patch 1/2] tools/memory-model: Update some warning labels Jonas Oberhauser 0 siblings, 2 replies; 15+ messages in thread From: Alan Stern @ 2023-01-25 20:20 UTC (permalink / raw) To: Paul E. McKenney Cc: Jonas Oberhauser, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list Some of the warning labels used in the LKMM are unfortunately ambiguous. In particular, the same warning is used for both an unmatched rcu_read_lock() call and for an unmatched rcu_read_unlock() call. Likewise for the srcu_* equivalents. Also, the warning about passing a wrong value to srcu_read_unlock() -- i.e., a value different from the one returned by the matching srcu_read_lock() -- talks about bad nesting rather than non-matching values. Let's update the warning labels to make their meanings more clear. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> --- tools/memory-model/linux-kernel.bell | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) Index: usb-devel/tools/memory-model/linux-kernel.bell =================================================================== --- usb-devel.orig/tools/memory-model/linux-kernel.bell +++ usb-devel/tools/memory-model/linux-kernel.bell @@ -53,8 +53,8 @@ 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 @@ -69,14 +69,14 @@ let srcu-rscs = let rec in matched (* 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 (* 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) | ^ permalink raw reply [flat|nested] 15+ messages in thread
* [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-25 20:20 ` [Patch 1/2] tools/memory-model: Update some warning labels Alan Stern @ 2023-01-25 20:21 ` Alan Stern 2023-01-25 21:04 ` Jonas Oberhauser 2023-02-01 10:31 ` Jonas Oberhauser 2023-01-25 20:35 ` [Patch 1/2] tools/memory-model: Update some warning labels Jonas Oberhauser 1 sibling, 2 replies; 15+ messages in thread From: Alan Stern @ 2023-01-25 20:21 UTC (permalink / raw) To: Paul E. McKenney Cc: Jonas Oberhauser, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list 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). [ paulmck: Fix space-before-tab whitespace nit. ] TBD-contributions-from: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> Signed-off-by: Alan Stern <stern@rowland.harvard.edu> --- tools/memory-model/linux-kernel.bell | 17 +++++------------ tools/memory-model/linux-kernel.def | 6 ++++-- tools/memory-model/lock.cat | 6 +++--- 3 files changed, 12 insertions(+), 17 deletions(-) Index: usb-devel/tools/memory-model/linux-kernel.bell =================================================================== --- usb-devel.orig/tools/memory-model/linux-kernel.bell +++ usb-devel/tools/memory-model/linux-kernel.bell @@ -57,20 +57,13 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) 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 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 @@ -80,11 +73,11 @@ flag ~empty different-values(srcu-rscs) (* Compute marked and plain memory accesses *) let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | - LKR | LKW | UL | LF | RL | RU + 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 ; rfi)* +let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* let addr = carry-dep ; addr let ctrl = carry-dep ; ctrl let data = carry-dep ; data Index: usb-devel/tools/memory-model/linux-kernel.def =================================================================== --- usb-devel.orig/tools/memory-model/linux-kernel.def +++ usb-devel/tools/memory-model/linux-kernel.def @@ -49,8 +49,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); } Index: usb-devel/tools/memory-model/lock.cat =================================================================== --- usb-devel.orig/tools/memory-model/lock.cat +++ usb-devel/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) ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-25 20:21 ` [Patch 2/2] tools/memory-model: Provide exact SRCU semantics Alan Stern @ 2023-01-25 21:04 ` Jonas Oberhauser 2023-01-25 21:58 ` Paul E. McKenney 2023-01-25 22:52 ` Alan Stern 2023-02-01 10:31 ` Jonas Oberhauser 1 sibling, 2 replies; 15+ messages in thread From: Jonas Oberhauser @ 2023-01-25 21:04 UTC (permalink / raw) To: Alan Stern, Paul E. McKenney Cc: Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On 1/25/2023 9:21 PM, Alan Stern wrote: > 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). > > [ paulmck: Fix space-before-tab whitespace nit. ] > > TBD-contributions-from: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu> In general this seems like a good solution for the time being. I do have a few minor questions. > --- > > tools/memory-model/linux-kernel.bell | 17 +++++------------ > tools/memory-model/linux-kernel.def | 6 ++++-- > tools/memory-model/lock.cat | 6 +++--- > 3 files changed, 12 insertions(+), 17 deletions(-) > > Index: usb-devel/tools/memory-model/linux-kernel.bell > =================================================================== > --- usb-devel.orig/tools/memory-model/linux-kernel.bell > +++ usb-devel/tools/memory-model/linux-kernel.bell > @@ -57,20 +57,13 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) > 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 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 Have you considered adding flag ~empty (srcu-rscs ; srcu-rscs^-1) \ id as mixed-srcu-cookie Although I think one has to be intentionally trying to trick herd to be violating this. If herd could produce different cookies, this would be easy to detect just by the different-values flag you already have. > > (* Check for use of synchronize_srcu() inside an RCU critical section *) > flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep > @@ -80,11 +73,11 @@ flag ~empty different-values(srcu-rscs) > > (* Compute marked and plain memory accesses *) > let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | > - LKR | LKW | UL | LF | RL | RU > + LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock Good catch! But why wasn't this necessary before? Is it only necessary now because the accesses became loads and stores (maybe to avoid data races?) > let Plain = M \ Marked > > (* Redefine dependencies to include those carried through plain accesses *) > -let carry-dep = (data ; rfi)* > +let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* > let addr = carry-dep ; addr > let ctrl = carry-dep ; ctrl > let data = carry-dep ; data > Index: usb-devel/tools/memory-model/linux-kernel.def > =================================================================== > --- usb-devel.orig/tools/memory-model/linux-kernel.def > +++ usb-devel/tools/memory-model/linux-kernel.def > @@ -49,8 +49,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); } How do you feel about introducing Srcu-up and Srcu-down with this patch? > synchronize_srcu(X) { __srcu{sync-srcu}(X); } > synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); } > > Index: usb-devel/tools/memory-model/lock.cat > =================================================================== > --- usb-devel.orig/tools/memory-model/lock.cat > +++ usb-devel/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 Since this was pointed out by Boqun, would it be appropriate to mention him in the patch somehow? > (* Link Lock-Reads to their RMW-partner Lock-Writes *) > let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) Thanks for your patience, jonas ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-25 21:04 ` Jonas Oberhauser @ 2023-01-25 21:58 ` Paul E. McKenney 2023-01-25 22:52 ` Alan Stern 1 sibling, 0 replies; 15+ messages in thread From: Paul E. McKenney @ 2023-01-25 21:58 UTC (permalink / raw) To: Jonas Oberhauser Cc: Alan Stern, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: > On 1/25/2023 9:21 PM, Alan Stern wrote: > > 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. [ . . . ] > > synchronize_srcu(X) { __srcu{sync-srcu}(X); } > > synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); } > > Index: usb-devel/tools/memory-model/lock.cat > > =================================================================== > > --- usb-devel.orig/tools/memory-model/lock.cat > > +++ usb-devel/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 > > Since this was pointed out by Boqun, would it be appropriate to mention him > in the patch somehow? Would you be willing to list who contributed what? Once you and Alan come to agreement on the list, I would be happy to wordsmith a version into the commit log. Thanx, Paul > > (* Link Lock-Reads to their RMW-partner Lock-Writes *) > > let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) > > Thanks for your patience, > jonas > ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-25 21:04 ` Jonas Oberhauser 2023-01-25 21:58 ` Paul E. McKenney @ 2023-01-25 22:52 ` Alan Stern 2023-01-26 11:30 ` Jonas Oberhauser 1 sibling, 1 reply; 15+ messages in thread From: Alan Stern @ 2023-01-25 22:52 UTC (permalink / raw) To: Jonas Oberhauser Cc: Paul E. McKenney, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: > > > On 1/25/2023 9:21 PM, Alan Stern wrote: > > (* Validate nesting *) > > 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 > > Have you considered adding > flag ~empty (srcu-rscs ; srcu-rscs^-1) \ id as mixed-srcu-cookie I had not considered it. You'd have to do something pretty bizarre if you wanted to trigger this warning, though. Like: r1 = srcu_read_lock(s); r2 = srcu_read_lock(s); srcu_read_unlock(s, r1 + r2); > Although I think one has to be intentionally trying to trick herd > to be violating this. If herd could produce different cookies, this would be > easy to detect just by the different-values flag you already have. Unless you did: srcu_read_unlock(s, r1 + r2 * 0). :-) > > (* Check for use of synchronize_srcu() inside an RCU critical section *) > > flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep > > @@ -80,11 +73,11 @@ flag ~empty different-values(srcu-rscs) > > (* Compute marked and plain memory accesses *) > > let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | > > - LKR | LKW | UL | LF | RL | RU > > + LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock > > Good catch! But why wasn't this necessary before? Is it only necessary now > because the accesses became loads and stores (maybe to avoid data races?) Exactly. Before this those events weren't memory accesses at all. > > // 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); } > > How do you feel about introducing Srcu-up and Srcu-down with this patch? Why invent new classes for them? They are literally the same operation as Srcu-lock and Srcu-unlock; the only difference is how the kernel's lockdep checker treats them. > > +(* 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 > > Since this was pointed out by Boqun, would it be appropriate to mention him > in the patch somehow? True. After we settle everything else, I'll add something to that effect. Alan ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-25 22:52 ` Alan Stern @ 2023-01-26 11:30 ` Jonas Oberhauser 2023-01-26 16:02 ` Alan Stern 2023-01-26 17:35 ` Paul E. McKenney 0 siblings, 2 replies; 15+ messages in thread From: Jonas Oberhauser @ 2023-01-26 11:30 UTC (permalink / raw) To: Alan Stern Cc: Paul E. McKenney, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On 1/25/2023 11:52 PM, Alan Stern wrote: > On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: >> >> On 1/25/2023 9:21 PM, Alan Stern wrote: >>> (* Validate nesting *) >>> 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 >> [...] >>> // 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); } >> How do you feel about introducing Srcu-up and Srcu-down with this patch? > Why invent new classes for them? They are literally the same operation > as Srcu-lock and Srcu-unlock; the only difference is how the kernel's > lockdep checker treats them. I don't think they're necessarily implemented in a compatible way, so r = srcu_lock(s); srcu_up(s,r); might not actually work, but would currently be ok'ed by LKMM. With different classes you could state flag ~empty [Srcu-lock];srcu-rscs;[Srcu-up] as srcu-mismatch-lock-to-up flag ~empty [Srcu-down];srcu-rscs;[Srcu-unlock] as srcu-mismatch-down-to-unlock I think with the current implementation this code might work, but I don't feel like this is inherently true. You could then also go ahead and define the "same CPU" requirement as a flag for lock and unlock specifically, like flag ~empty [Srcu-lock];srcu-rscs & ext as srcu-lock-unlock-mismatch-CPU or so. Best wishes, jonas ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-26 11:30 ` Jonas Oberhauser @ 2023-01-26 16:02 ` Alan Stern 2023-01-26 16:31 ` Jonas Oberhauser 2023-01-26 17:35 ` Paul E. McKenney 1 sibling, 1 reply; 15+ messages in thread From: Alan Stern @ 2023-01-26 16:02 UTC (permalink / raw) To: Jonas Oberhauser Cc: Paul E. McKenney, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Thu, Jan 26, 2023 at 12:30:14PM +0100, Jonas Oberhauser wrote: > > > On 1/25/2023 11:52 PM, Alan Stern wrote: > > On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: > > > > > > On 1/25/2023 9:21 PM, Alan Stern wrote: > > > > (* Validate nesting *) > > > > 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 > > > [...] > > > > // 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); } > > > How do you feel about introducing Srcu-up and Srcu-down with this patch? > > Why invent new classes for them? They are literally the same operation > > as Srcu-lock and Srcu-unlock; the only difference is how the kernel's > > lockdep checker treats them. > I don't think they're necessarily implemented in a compatible way, so > > r = srcu_lock(s); > srcu_up(s,r); > > might not actually work, but would currently be ok'ed by LKMM. I'll let Paul answer this. > With > different classes you could state > flag ~empty [Srcu-lock];srcu-rscs;[Srcu-up] as srcu-mismatch-lock-to-up > flag ~empty [Srcu-down];srcu-rscs;[Srcu-unlock] as > srcu-mismatch-down-to-unlock > > I think with the current implementation this code might work, but I don't > feel like this is inherently true. > > You could then also go ahead and define the "same CPU" requirement as a flag > for lock and unlock specifically, like > flag ~empty [Srcu-lock];srcu-rscs & ext as srcu-lock-unlock-mismatch-CPU > or so. Bear in mind that the herd7 model is not obliged to find and warn about all possible bugs in a litmus test. Especially if the same code would generate a warning or error when run in the kernel. Alan ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-26 16:02 ` Alan Stern @ 2023-01-26 16:31 ` Jonas Oberhauser 0 siblings, 0 replies; 15+ messages in thread From: Jonas Oberhauser @ 2023-01-26 16:31 UTC (permalink / raw) To: Alan Stern Cc: Paul E. McKenney, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On 1/26/2023 5:02 PM, Alan Stern wrote: > On Thu, Jan 26, 2023 at 12:30:14PM +0100, Jonas Oberhauser wrote: >> >> On 1/25/2023 11:52 PM, Alan Stern wrote: >>> On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: >>>> On 1/25/2023 9:21 PM, Alan Stern wrote: >>>>> (* Validate nesting *) >>>>> 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 >>>> [...] >>>>> // 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); } >>>> How do you feel about introducing Srcu-up and Srcu-down with this patch? >>> Why invent new classes for them? They are literally the same operation >>> as Srcu-lock and Srcu-unlock; the only difference is how the kernel's >>> lockdep checker treats them. >> I don't think they're necessarily implemented in a compatible way, so >> >> r = srcu_lock(s); >> srcu_up(s,r); >> >> might not actually work, but would currently be ok'ed by LKMM. > I'll let Paul answer this. > >> With >> different classes you could state >> flag ~empty [Srcu-lock];srcu-rscs;[Srcu-up] as srcu-mismatch-lock-to-up >> flag ~empty [Srcu-down];srcu-rscs;[Srcu-unlock] as >> srcu-mismatch-down-to-unlock >> >> I think with the current implementation this code might work, but I don't >> feel like this is inherently true. >> >> You could then also go ahead and define the "same CPU" requirement as a flag >> for lock and unlock specifically, like >> flag ~empty [Srcu-lock];srcu-rscs & ext as srcu-lock-unlock-mismatch-CPU >> or so. > Bear in mind that the herd7 model is not obliged to find and warn about > all possible bugs in a litmus test. Especially if the same code would > generate a warning or error when run in the kernel. I agree, and indeed it may not even possible to do so (even under a hypothetical formal proof that the list of bugs is complete, some might not be formalizable in a satisfactory way in herd). Mostly I'm just trying to see if you have considered the possibilities and decided against them intentionally, or if you just hadn't considered it. I don't have a strong opinion either way and would be ok with the patch as written. That said, I do like to think of the model as a kind of compact formal specification/documentation, including the assumptions the kernel makes about how these APIs are to be used. Best wishes, jonas ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-26 11:30 ` Jonas Oberhauser 2023-01-26 16:02 ` Alan Stern @ 2023-01-26 17:35 ` Paul E. McKenney 2023-01-26 19:10 ` Alan Stern 1 sibling, 1 reply; 15+ messages in thread From: Paul E. McKenney @ 2023-01-26 17:35 UTC (permalink / raw) To: Jonas Oberhauser Cc: Alan Stern, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Thu, Jan 26, 2023 at 12:30:14PM +0100, Jonas Oberhauser wrote: > > > On 1/25/2023 11:52 PM, Alan Stern wrote: > > On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: > > > > > > On 1/25/2023 9:21 PM, Alan Stern wrote: > > > > (* Validate nesting *) > > > > 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 > > > [...] > > > > // 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); } > > > How do you feel about introducing Srcu-up and Srcu-down with this patch? > > Why invent new classes for them? They are literally the same operation > > as Srcu-lock and Srcu-unlock; the only difference is how the kernel's > > lockdep checker treats them. > I don't think they're necessarily implemented in a compatible way, so > > r = srcu_lock(s); > srcu_up(s,r); > > might not actually work, but would currently be ok'ed by LKMM. In kernels built with CONFIG_PROVE_LOCKING=y (AKA built with lockdep enabled), lockdep would complain about having an srcu_read_lock() with no matching srcu_read_unlock(). Kernels built without lockdep (that is, kernels actually used in production) would be happy with this. So as Jonas suspects, this should be classified as not actually working. > With > different classes you could state > flag ~empty [Srcu-lock];srcu-rscs;[Srcu-up] as srcu-mismatch-lock-to-up > flag ~empty [Srcu-down];srcu-rscs;[Srcu-unlock] as > srcu-mismatch-down-to-unlock > > I think with the current implementation this code might work, but I don't > feel like this is inherently true. > > You could then also go ahead and define the "same CPU" requirement as a flag > for lock and unlock specifically, like > flag ~empty [Srcu-lock];srcu-rscs & ext as srcu-lock-unlock-mismatch-CPU > or so. > > Best wishes, jonas > ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-26 17:35 ` Paul E. McKenney @ 2023-01-26 19:10 ` Alan Stern 2023-01-26 19:31 ` Paul E. McKenney 0 siblings, 1 reply; 15+ messages in thread From: Alan Stern @ 2023-01-26 19:10 UTC (permalink / raw) To: Paul E. McKenney Cc: Jonas Oberhauser, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Thu, Jan 26, 2023 at 09:35:07AM -0800, Paul E. McKenney wrote: > On Thu, Jan 26, 2023 at 12:30:14PM +0100, Jonas Oberhauser wrote: > > I don't think they're necessarily implemented in a compatible way, so > > > > r = srcu_lock(s); > > srcu_up(s,r); > > > > might not actually work, but would currently be ok'ed by LKMM. > > In kernels built with CONFIG_PROVE_LOCKING=y (AKA built with lockdep > enabled), lockdep would complain about having an srcu_read_lock() with > no matching srcu_read_unlock(). Kernels built without lockdep (that is, > kernels actually used in production) would be happy with this. > > So as Jonas suspects, this should be classified as not actually working. Lockdep complaints don't actually stop things from working (unless you want them to). They're just warnings, right? Alan ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-26 19:10 ` Alan Stern @ 2023-01-26 19:31 ` Paul E. McKenney 0 siblings, 0 replies; 15+ messages in thread From: Paul E. McKenney @ 2023-01-26 19:31 UTC (permalink / raw) To: Alan Stern Cc: Jonas Oberhauser, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Thu, Jan 26, 2023 at 02:10:10PM -0500, Alan Stern wrote: > On Thu, Jan 26, 2023 at 09:35:07AM -0800, Paul E. McKenney wrote: > > On Thu, Jan 26, 2023 at 12:30:14PM +0100, Jonas Oberhauser wrote: > > > I don't think they're necessarily implemented in a compatible way, so > > > > > > r = srcu_lock(s); > > > srcu_up(s,r); > > > > > > might not actually work, but would currently be ok'ed by LKMM. > > > > In kernels built with CONFIG_PROVE_LOCKING=y (AKA built with lockdep > > enabled), lockdep would complain about having an srcu_read_lock() with > > no matching srcu_read_unlock(). Kernels built without lockdep (that is, > > kernels actually used in production) would be happy with this. > > > > So as Jonas suspects, this should be classified as not actually working. > > Lockdep complaints don't actually stop things from working (unless you > want them to). They're just warnings, right? True, but they are taken seriously due to lockdep disabling itself after the first warning. So a warning for this sort of thing could hide some other deadlock, which tend to strongly motivate fixing issues leading to lockdep warnings. Thanx, Paul ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics 2023-01-25 20:21 ` [Patch 2/2] tools/memory-model: Provide exact SRCU semantics Alan Stern 2023-01-25 21:04 ` Jonas Oberhauser @ 2023-02-01 10:31 ` Jonas Oberhauser 1 sibling, 0 replies; 15+ messages in thread From: Jonas Oberhauser @ 2023-02-01 10:31 UTC (permalink / raw) To: Alan Stern, Paul E. McKenney Cc: Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On 1/25/2023 9:21 PM, Alan Stern wrote: > 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). > > [ paulmck: Fix space-before-tab whitespace nit. ] > > TBD-contributions-from: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Reviewed-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > > --- > > tools/memory-model/linux-kernel.bell | 17 +++++------------ > tools/memory-model/linux-kernel.def | 6 ++++-- > tools/memory-model/lock.cat | 6 +++--- > 3 files changed, 12 insertions(+), 17 deletions(-) > > Index: usb-devel/tools/memory-model/linux-kernel.bell > =================================================================== > --- usb-devel.orig/tools/memory-model/linux-kernel.bell > +++ usb-devel/tools/memory-model/linux-kernel.bell > @@ -57,20 +57,13 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) > 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 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 > @@ -80,11 +73,11 @@ flag ~empty different-values(srcu-rscs) > > (* Compute marked and plain memory accesses *) > let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | > - LKR | LKW | UL | LF | RL | RU > + 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 ; rfi)* > +let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* > let addr = carry-dep ; addr > let ctrl = carry-dep ; ctrl > let data = carry-dep ; data > Index: usb-devel/tools/memory-model/linux-kernel.def > =================================================================== > --- usb-devel.orig/tools/memory-model/linux-kernel.def > +++ usb-devel/tools/memory-model/linux-kernel.def > @@ -49,8 +49,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); } > > Index: usb-devel/tools/memory-model/lock.cat > =================================================================== > --- usb-devel.orig/tools/memory-model/lock.cat > +++ usb-devel/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) ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 1/2] tools/memory-model: Update some warning labels 2023-01-25 20:20 ` [Patch 1/2] tools/memory-model: Update some warning labels Alan Stern 2023-01-25 20:21 ` [Patch 2/2] tools/memory-model: Provide exact SRCU semantics Alan Stern @ 2023-01-25 20:35 ` Jonas Oberhauser 2023-01-25 22:01 ` Paul E. McKenney 1 sibling, 1 reply; 15+ messages in thread From: Jonas Oberhauser @ 2023-01-25 20:35 UTC (permalink / raw) To: Alan Stern, Paul E. McKenney Cc: Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On 1/25/2023 9:20 PM, Alan Stern wrote: > Some of the warning labels used in the LKMM are unfortunately > ambiguous. In particular, the same warning is used for both an > unmatched rcu_read_lock() call and for an unmatched rcu_read_unlock() > call. Likewise for the srcu_* equivalents. Also, the warning about > passing a wrong value to srcu_read_unlock() -- i.e., a value different > from the one returned by the matching srcu_read_lock() -- talks about > bad nesting rather than non-matching values. > > Let's update the warning labels to make their meanings more clear. > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Reviewed-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > > --- > > tools/memory-model/linux-kernel.bell | 10 +++++----- > 1 file changed, 5 insertions(+), 5 deletions(-) > > Index: usb-devel/tools/memory-model/linux-kernel.bell > =================================================================== > --- usb-devel.orig/tools/memory-model/linux-kernel.bell > +++ usb-devel/tools/memory-model/linux-kernel.bell > @@ -53,8 +53,8 @@ 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 > @@ -69,14 +69,14 @@ let srcu-rscs = let rec > in matched > > (* 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 > > (* 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) | ^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: [Patch 1/2] tools/memory-model: Update some warning labels 2023-01-25 20:35 ` [Patch 1/2] tools/memory-model: Update some warning labels Jonas Oberhauser @ 2023-01-25 22:01 ` Paul E. McKenney 0 siblings, 0 replies; 15+ messages in thread From: Paul E. McKenney @ 2023-01-25 22:01 UTC (permalink / raw) To: Jonas Oberhauser Cc: Alan Stern, Andrea Parri, Jonas Oberhauser, Peter Zijlstra, will, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, Kernel development list On Wed, Jan 25, 2023 at 09:35:44PM +0100, Jonas Oberhauser wrote: > > > On 1/25/2023 9:20 PM, Alan Stern wrote: > > Some of the warning labels used in the LKMM are unfortunately > > ambiguous. In particular, the same warning is used for both an > > unmatched rcu_read_lock() call and for an unmatched rcu_read_unlock() > > call. Likewise for the srcu_* equivalents. Also, the warning about > > passing a wrong value to srcu_read_unlock() -- i.e., a value different > > from the one returned by the matching srcu_read_lock() -- talks about > > bad nesting rather than non-matching values. > > > > Let's update the warning labels to make their meanings more clear. > > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu> > > Reviewed-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> Applied for further review and testing. I am thinking in terms of v6.4, that is, the merge window after the upcoming one. Or does someone need it earlier? Thanx, Paul > > --- > > > > tools/memory-model/linux-kernel.bell | 10 +++++----- > > 1 file changed, 5 insertions(+), 5 deletions(-) > > > > Index: usb-devel/tools/memory-model/linux-kernel.bell > > =================================================================== > > --- usb-devel.orig/tools/memory-model/linux-kernel.bell > > +++ usb-devel/tools/memory-model/linux-kernel.bell > > @@ -53,8 +53,8 @@ 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 > > @@ -69,14 +69,14 @@ let srcu-rscs = let rec > > in matched > > (* 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 > > (* 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) | > ^ permalink raw reply [flat|nested] 15+ messages in thread
end of thread, other threads:[~2023-02-01 10:32 UTC | newest] Thread overview: 15+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2023-01-25 20:19 [PATCH 0/2] SRCU changes for the Linux Kernel Memory Model Alan Stern 2023-01-25 20:20 ` [Patch 1/2] tools/memory-model: Update some warning labels Alan Stern 2023-01-25 20:21 ` [Patch 2/2] tools/memory-model: Provide exact SRCU semantics Alan Stern 2023-01-25 21:04 ` Jonas Oberhauser 2023-01-25 21:58 ` Paul E. McKenney 2023-01-25 22:52 ` Alan Stern 2023-01-26 11:30 ` Jonas Oberhauser 2023-01-26 16:02 ` Alan Stern 2023-01-26 16:31 ` Jonas Oberhauser 2023-01-26 17:35 ` Paul E. McKenney 2023-01-26 19:10 ` Alan Stern 2023-01-26 19:31 ` Paul E. McKenney 2023-02-01 10:31 ` Jonas Oberhauser 2023-01-25 20:35 ` [Patch 1/2] tools/memory-model: Update some warning labels Jonas Oberhauser 2023-01-25 22:01 ` Paul E. McKenney
This is an external index of several public inboxes, see mirroring instructions on how to clone and mirror all data and code used by this external index.