From: Joel Fernandes <joel@joelfernandes.org>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: linux-kernel@vger.kernel.org, Akira Yokosawa <akiyks@gmail.com>,
Andrea Parri <parri.andrea@gmail.com>,
Boqun Feng <boqun.feng@gmail.com>,
Daniel Lustig <dlustig@nvidia.com>,
David Howells <dhowells@redhat.com>,
Jade Alglave <j.alglave@ucl.ac.uk>,
linux-arch@vger.kernel.org, Luc Maranget <luc.maranget@inria.fr>,
Nicholas Piggin <npiggin@gmail.com>,
"Paul E. McKenney" <paulmck@kernel.org>,
Peter Zijlstra <peterz@infradead.org>,
Will Deacon <will@kernel.org>
Subject: Re: [PATCH 1/3] LKMM: Add litmus test for RCU GP guarantee where updater frees object
Date: Fri, 20 Mar 2020 16:15:16 -0400 [thread overview]
Message-ID: <20200320201516.GA129293@google.com> (raw)
In-Reply-To: <Pine.LNX.4.44L0.2003201049230.27303-100000@netrider.rowland.org>
On Fri, Mar 20, 2020 at 10:59:55AM -0400, Alan Stern wrote:
> On Fri, 20 Mar 2020, Joel Fernandes (Google) wrote:
>
> > This adds an example for the important RCU grace period guarantee, which
> > shows an RCU reader can never span a grace period.
> >
> > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > ---
> > .../litmus-tests/RCU+sync+free.litmus | 40 +++++++++++++++++++
> > 1 file changed, 40 insertions(+)
> > create mode 100644 tools/memory-model/litmus-tests/RCU+sync+free.litmus
> >
> > diff --git a/tools/memory-model/litmus-tests/RCU+sync+free.litmus b/tools/memory-model/litmus-tests/RCU+sync+free.litmus
> > new file mode 100644
> > index 0000000000000..c4682502dd296
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/RCU+sync+free.litmus
> > @@ -0,0 +1,40 @@
> > +C RCU+sync+free
> > +
> > +(*
> > + * Result: Never
> > + *
>
> The following comment needs some rewriting. The grammar is somewhat
> awkward and a very important "not" is missing.
>
> > + * This litmus test demonstrates that an RCU reader can never see a write after
> > + * the grace period, if it saw writes that happen before the grace period.
>
> An RCU reader can never see a write that follows a grace period if it
> did _not_ see writes that precede the grace period.
Yes, you are right. I will change your wording to 'did not see *all* writes
that precede'.
> > This
> > + * is a typical pattern of RCU usage, where the write before the grace period
> > + * assigns a pointer, and the writes after destroy the object that the pointer
> > + * points to.
>
> ... that the pointer used to point to.
Will fix.
> > + *
> > + * This guarantee also implies, an RCU reader can never span a grace period and
> > + * is an important RCU grace period memory ordering guarantee.
>
> Unnecessary comma, and it is not clear what "This" refers to. The
> whole sentence should be phrased differently:
>
> This is one implication of the RCU grace-period guarantee,
> which says (among other things) that an RCU reader cannot span
> a grace period.
Your wording is better, will use that.
thanks,
- Joel
prev parent reply other threads:[~2020-03-20 20:15 UTC|newest]
Thread overview: 19+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-03-20 6:55 [PATCH 1/3] LKMM: Add litmus test for RCU GP guarantee where updater frees object Joel Fernandes (Google)
2020-03-20 6:55 ` [PATCH 2/3] LKMM: Add litmus test for RCU GP guarantee where reader stores Joel Fernandes (Google)
2020-03-20 15:03 ` Alan Stern
2020-03-20 15:03 ` Alan Stern
2020-03-20 16:59 ` Joel Fernandes
2020-03-20 20:56 ` Alan Stern
2020-03-20 20:56 ` Alan Stern
2020-03-20 21:44 ` Joel Fernandes
2020-03-21 2:05 ` Boqun Feng
2020-03-23 1:31 ` Joel Fernandes
2020-03-20 6:55 ` [PATCH 3/3] LKMM: Rename MP+onceassign+derefonce for better clarity Joel Fernandes (Google)
2020-03-20 10:26 ` [PATCH 1/3] LKMM: Add litmus test for RCU GP guarantee where updater frees object Andrea Parri
2020-03-20 15:07 ` Alan Stern
2020-03-20 15:07 ` Alan Stern
2020-03-20 16:54 ` Joel Fernandes
2020-03-20 10:44 ` Andrea Parri
2020-03-20 14:59 ` Alan Stern
2020-03-20 14:59 ` Alan Stern
2020-03-20 20:15 ` Joel Fernandes [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20200320201516.GA129293@google.com \
--to=joel@joelfernandes.org \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=j.alglave@ucl.ac.uk \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=will@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.