Messages in this thread Patch in this message | | | Date | Tue, 17 Jan 2023 21:15:15 -0500 | From | Alan Stern <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
On Tue, Jan 17, 2023 at 09:43:08AM -0800, Paul E. McKenney wrote: > On Tue, Jan 17, 2023 at 10:56:34AM -0500, Alan Stern wrote:
> > Isn't it true that the current code will flag srcu-bad-nesting if a > > litmus test has non-nested overlapping SRCU read-side critical sections? > > Now that you mention it, it does indeed, flagging srcu-bad-nesting. > > Just to see if I understand, different-values yields true if the set > contains multiple elements with the same value mapping to different > values. Or, to put it another way, if the relation does not correspond > to a function. > > Or am I still missing something? > > > And if it is true, is there any need to change the memory model at this > > point? > > > > (And if it's not true, that's most likely due to a bug in herd7.) > > Agreed, changes must wait for SRCU support in herd7.
Maybe we don't. Please test the patch below; I think it will do what you want -- and it doesn't rule out nesting.
Alan
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,12 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking (* 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 srcu-rscs = ([Srcu-lock] ; 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-unlock \ range(srcu-rscs) as unbalanced-srcu-unlocking +flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-unlocks (* Check for use of synchronize_srcu() inside an RCU critical section *) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep @@ -80,11 +72,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 ; rfi ; [~Srcu-lock])* 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,8 @@ 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); } synchronize_srcu(X) { __srcu{sync-srcu}(X); } synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); }
| |