On Mon, Feb 06, 2023 at 01:39:07PM -0500, Alan Stern 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. > > 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. > I am happy to make changes to explanation.txt (I am assuming that's the file you mentioned), but I was wondering what you thought of the following change. If the formulas are split up, that itself could be some documentation as well. I did add a small paragraph on the top of the formulas as well though. Some light testing shows it works with the cross-CPU litmus test (could still have bugs though and needs more testing). Let me know how you feel about it, and if I should submit something along these lines along with your suggestion to edit the explanation.txt. Thanks! diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index ce068700939c..1390d1b8ceee 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -57,9 +57,28 @@ 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 *) -let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)* -let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc +(* SRCU read-side section modeling + * Compute matching pairs of nested Srcu-lock and Srcu-unlock: + * Each SRCU read-side critical section is treated as independent, of other + * overlapping SRCU read-side critical sections even when on the same domain. + * For this, each Srcu-lock and Srcu-unlock pair is treated as loads and + * stores, with the data-dependency flow also treated as independent to prevent + * fusing. *) + +(* Data dependency between lock and idx store *) +let srcu-lock-to-store-idx = ([Srcu-lock]; data) + +(* Data dependency between idx load and unlock *) +let srcu-load-idx-to-unlock = (data; [Srcu-unlock]) + +(* Read-from dependency between idx store on one CPU and load on same/another. + * This is required to model the splitting of critical section across CPUs. *) +let srcu-store-to-load-idx = (rf ; srcu-load-idx-to-unlock) + +(* SRCU data dependency flow. Exclude the Srcu-unlock to not transcend back to back rscs *) +let carry-srcu-data = (srcu-lock-to-store-idx ; [~ Srcu-unlock] ; srcu-store-to-load-idx)* + +let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; [Srcu-unlock]) & loc (* Validate nesting *) flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock -- 2.39.1.581.gbfd45094c4-goog
