[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <Y+FJSzUoGTgReLPB@rowland.harvard.edu>
Date: Mon, 6 Feb 2023 13:39:07 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Joel Fernandes <joel@...lfernandes.org>
Cc: "Paul E. McKenney" <paulmck@...nel.org>,
linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
kernel-team@...a.com, mingo@...nel.org, parri.andrea@...il.com,
will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
luc.maranget@...ia.fr, akiyks@...il.com
Subject: Re: Current LKMM patch disposition
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.
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.
Powered by blists - more mailing lists