lkml.org 
[lkml]   [2023]   [Feb]   [6]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
From
Date
SubjectRe: Current LKMM patch disposition
On Mon, Feb 6, 2023 at 1:39 PM Alan Stern <stern@rowland.harvard.edu> 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.

\
 
 \ /
  Last update: 2023-03-27 00:11    [W:0.356 / U:0.180 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site