On Mon, Feb 6, 2023 at 1:39 PM Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> wrote: > > On Sun, Feb 05, 2023 at 02:10:29PM +0000, Joel Fernandes wrote: > > On Sat, Feb 04, 2023 at 02:24:11PM -0800, Paul E. McKenney wrote: > > > On Sat, Feb 04, 2023 at 09:58:12AM -0500, Alan Stern wrote: > > > > On Fri, Feb 03, 2023 at 05:49:41PM -0800, Paul E. McKenney wrote: > > > > > On Fri, Feb 03, 2023 at 08:28:35PM -0500, Alan Stern wrote: > > > > > > The "Provide exact semantics for SRCU" patch should have: > > > > > > > > > > > > Portions suggested by Boqun Feng and Jonas Oberhauser. > > > > > > > > > > > > added at the end, together with your Reported-by: tag. With that, I > > > > > > think it can be queued for 6.4. > > > > > > > > > > Thank you! Does the patch shown below work for you? > > > > > > > > > > (I have tentatively queued this, but can easily adjust or replace it.) > > > > > > > > It looks fine. > > > > > > Very good, thank you for looking it over! I pushed it out on branch > > > stern.2023.02.04a. > > > > > > Would anyone like to ack/review/whatever this one? > > > > Would it be possible to add comments, something like the following? Apologies > > if it is missing some ideas. I will try to improve it later. > > > > thanks! > > > > - Joel > > > > ---8<----------------------- > > > > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell > > index ce068700939c..0a16177339bc 100644 > > --- a/tools/memory-model/linux-kernel.bell > > +++ b/tools/memory-model/linux-kernel.bell > > @@ -57,7 +57,23 @@ let rcu-rscs = let rec > > 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 *) > > +(***************************************************************) > > +(* > > + * carry-srcu-data: To handle the case of the SRCU critical section split > > + * across CPUs, where the idx is used to communicate the SRCU index across CPUs > > + * (say CPU0 and CPU1), data is between the R[srcu-lock] to W[once][idx] on > > + * CPU0, which is sequenced with the ->rf is between the W[once][idx] and the > > + * R[once][idx] on CPU1. The carry-srcu-data is made to exclude Srcu-unlock > > + * events to prevent capturing accesses across back-to-back SRCU read-side > > + * critical sections. > > + * > > + * srcu-rscs: Putting everything together, the carry-srcu-data is sequenced with > > + * a data relation, which is the data dependency between R[once][idx] on CPU1 > > + * and the srcu-unlock store, and loc ensures the relation is unique for a > > + * specific lock. > > + *) > > let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)* > > let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc > > My tendency has been to keep comments in the herd7 files to a minimum > and to put more extended descriptions in the explanation.txt file. > Right now that file contains almost nothing (a single paragraph!) about > SRCU, so it needs to be updated to talk about the new definition of > srcu-rscs. In my opinion, that's where this sort of comment belongs. That makes sense, I agree. > Joel, would you like to write an extra paragraph of two for that file, > explaining in more detail how SRCU lock-to-unlock matching is different > from regular RCU and how the definition of the srcu-rscs relation works? > I'd be happy to edit anything you come up with. Yes I would love to, I'll spend some more time studying this up a bit more so I don't write nonsense. But yes, I am quite interested in writing something up and I will do so! Thanks, - Joel > Alan > > PS: We also need to update the PLAIN ACCESSES AND DATA RACES section of > explanation.txt, to mention the carry-dep relation and why it is > important.
