From: "Paul E. McKenney" <paulmck@linux.ibm.com>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: David Goldblatt <davidtgoldblatt@gmail.com>,
mathieu.desnoyers@efficios.com,
Florian Weimer <fweimer@redhat.com>,
triegel@redhat.com, libc-alpha@sourceware.org,
andrea.parri@amarulasolutions.com, will.deacon@arm.com,
peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
akiyks@gmail.com, dlustig@nvidia.com, linux-arch@vger.kernel.org,
linux-kernel@vger.kernel.org
Subject: Re: [PATCH] Linux: Implement membarrier function
Date: Thu, 13 Dec 2018 16:20:43 -0800 [thread overview]
Message-ID: <20181214002043.GP4170@linux.ibm.com> (raw)
In-Reply-To: <Pine.LNX.4.44L0.1812131026570.1586-100000@iolanthe.rowland.org>
On Thu, Dec 13, 2018 at 10:49:49AM -0500, Alan Stern wrote:
> On Wed, 12 Dec 2018, Paul E. McKenney wrote:
>
> > > Well, what are you trying to accomplish? Do you want to find an
> > > argument similar to the one I posted for the 6-CPU test to show that
> > > this test should be forbidden?
> >
> > I am trying to check odd corner cases. Your sys_membarrier() model
> > is quite nice and certainly fits nicely with the rest of the model,
> > but where I come from, that is actually reason for suspicion. ;-)
> >
> > All kidding aside, your argument for the 6-CPU test was extremely
> > valuable, as it showed me a way to think of that test from an
> > implementation viewpoint. Then the question is whether or not that
> > viewpoint actually matches the model, which seems to be the case thus far.
>
> It should, since I formulated the reasoning behind that viewpoint
> directly from the model. The basic idea is this:
>
> By induction, show that whenever we have A ->rcu-fence B then
> anything po-before A executes before anything po-after B, and
> furthermore, any write which propagates to A's CPU before A
> executes will propagate to every CPU before B finishes (i.e.,
> before anything po-after B executes).
>
> Using this, show that whenever X ->rb Y holds then X must
> execute before Y.
>
> That's what the 6-CPU argument did. In that litmus test we have
> mb2 ->rcu-fence mb23, Rc ->rb Re, mb1 ->rcu-fence mb14, Rb ->rb Rf,
> mb0 ->rcu-fence mb05, and lastly Ra ->rb Ra. The last one is what
> shows that the test is forbidden.
I really am not trying to be difficult. Well, no more difficult than
I normally am, anyway. Which admittedly isn't saying much. ;-)
> > A good next step would be to automatically generate random tests along
> > with an automatically generated prediction, like I did for RCU a few
> > years back. I should be able to generalize my time-based cheat for RCU to
> > also cover SRCU, though sys_membarrier() will require a bit more thought.
> > (The time-based cheat was to have fixed duration RCU grace periods and
> > RCU read-side critical sections, with the grace period duration being
> > slightly longer than that of the critical sections. The number of
> > processes is of course limited by the chosen durations, but that limit
> > can easily be made insanely large.)
>
> Imagine that each sys_membarrier call takes a fixed duration and each
> other instruction takes slightly less (the idea being that each
> instruction is a critical section). Instructions can be reordered
> (although not across a sys_membarrier call), but no matter how the
> reordering is done, the result is disallowed.
It gets a bit trickier with interleavings of different combinations
of RCU, SRCU, and sys_membarrier(). Yes, your cat code very elegantly
sorts this out, but my goal is to be able to explain a given example
to someone.
> > I guess that I still haven't gotten over being a bit surprised that the
> > RCU counting rule also applies to sys_membarrier(). ;-)
>
> Why not? They are both synchronization mechanisms with heavy-weight
> write sides and light-weight read sides, and most importantly, they
> provide the same Guarantee.
True, but I do feel the need to poke at it.
The zero-size sys_membarrier() read-side critical sections do make
things act a bit differently, for example, interchanging the accesses
in an RCU read-side critical section has no effect, while doing so in
a sys_membarrier() reader can cause the result to be allowed. One key
point is that everything before the end of a read-side critical section
of any type is ordered before any later grace period of that same type,
and vice versa.
This is why reordering accesses matters for sys_membarrier() readers but
not for RCU and SRCU readers -- in the case of RCU and SRCU readers,
the accesses are inside the read-side critical section, while for
sys_membarrier() readers, the read-side critical sections don't have
an inside. So yes, ordering also matters in the case of SRCU and
RCU readers for accesses outside of the read-side critical sections.
The reason sys_membarrier() seems surprising to me isn't because it is
any different in theoretical structure, but rather because the practice
is to put RCU and SRCU read-side accesses inside a read-side critical
sections, which is impossible for sys_membarrier().
The other thing that took some time to get used to is the possibility
of long delays during sys_membarrier() execution, allowing significant
execution and reordering between different CPUs' IPIs. This was key
to my understanding of the six-process example, and probably needs to
be clearly called out, including in an example or two.
The interleaving restrictions are straightforward for me, but the
fixed-time approach does have some interesting cross-talk potential
between sys_membarrier() and RCU read-side critical sections whose
accesses have been reversed. I don't believe that it is possible to
leverage this "order the other guy's read-side critical sections" effect
in the general case, but I could be missing something.
If you are claiming that I am worrying unnecessarily, you are probably
right. But if I didn't worry unnecessarily, RCU wouldn't work at all! ;-)
Thanx, Paul
next prev parent reply other threads:[~2018-12-14 0:20 UTC|newest]
Thread overview: 54+ messages / expand[flat|nested] mbox.gz Atom feed top
[not found] <8736rldyzm.fsf@oldenburg.str.redhat.com>
[not found] ` <1543444466.5493.220.camel@redhat.com>
[not found] ` <87y39c2dsg.fsf@oldenburg.str.redhat.com>
[not found] ` <1689938209.14804.1543502662882.JavaMail.zimbra@efficios.com>
[not found] ` <20181129150433.GH4170@linux.ibm.com>
[not found] ` <CAHD6eXcvx1bskbp-X+vuMYoMQiCLOt0PiCZ5FT1yFsda9Ud-yA@mail.gmail.com>
2018-12-06 21:54 ` [PATCH] Linux: Implement membarrier function Paul E. McKenney
2018-12-06 21:54 ` Paul E. McKenney
2018-12-10 16:22 ` Alan Stern
2018-12-10 16:22 ` Alan Stern
2018-12-10 18:25 ` Paul E. McKenney
2018-12-10 18:25 ` Paul E. McKenney
2018-12-11 16:21 ` Alan Stern
2018-12-11 16:21 ` Alan Stern
2018-12-11 19:08 ` Paul E. McKenney
2018-12-11 19:08 ` Paul E. McKenney
2018-12-11 20:09 ` Alan Stern
2018-12-11 20:09 ` Alan Stern
2018-12-11 21:22 ` Paul E. McKenney
2018-12-11 21:22 ` Paul E. McKenney
2018-12-12 17:07 ` Paul E. McKenney
2018-12-12 17:07 ` Paul E. McKenney
2018-12-12 18:04 ` Alan Stern
2018-12-12 18:04 ` Alan Stern
2018-12-12 19:42 ` Paul E. McKenney
2018-12-12 19:42 ` Paul E. McKenney
2018-12-12 21:32 ` Alan Stern
2018-12-12 21:32 ` Alan Stern
2018-12-12 21:52 ` Paul E. McKenney
2018-12-12 21:52 ` Paul E. McKenney
2018-12-12 22:12 ` Alan Stern
2018-12-12 22:12 ` Alan Stern
2018-12-12 22:49 ` Paul E. McKenney
2018-12-12 22:49 ` Paul E. McKenney
2018-12-13 15:49 ` Alan Stern
2018-12-13 15:49 ` Alan Stern
2018-12-14 0:20 ` Paul E. McKenney [this message]
2018-12-14 0:20 ` Paul E. McKenney
2018-12-14 2:26 ` Alan Stern
2018-12-14 2:26 ` Alan Stern
2018-12-14 5:20 ` Paul E. McKenney
2018-12-14 5:20 ` Paul E. McKenney
2018-12-14 15:31 ` Alan Stern
2018-12-14 15:31 ` Alan Stern
2018-12-14 18:43 ` Paul E. McKenney
2018-12-14 18:43 ` Paul E. McKenney
2018-12-14 21:39 ` Alan Stern
2018-12-14 21:39 ` Alan Stern
2018-12-16 18:51 ` Paul E. McKenney
2018-12-16 18:51 ` Paul E. McKenney
2018-12-17 16:02 ` Alan Stern
2018-12-17 16:02 ` Alan Stern
2018-12-17 18:32 ` Paul E. McKenney
2018-12-17 18:32 ` Paul E. McKenney
2018-12-12 22:19 ` Paul E. McKenney
2018-12-12 22:19 ` Paul E. McKenney
2018-12-11 6:42 ` David Goldblatt
2018-12-11 6:42 ` David Goldblatt
2018-12-11 14:49 ` Paul E. McKenney
2018-12-11 14:49 ` Paul E. McKenney
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=20181214002043.GP4170@linux.ibm.com \
--to=paulmck@linux.ibm.com \
--cc=akiyks@gmail.com \
--cc=andrea.parri@amarulasolutions.com \
--cc=boqun.feng@gmail.com \
--cc=davidtgoldblatt@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=fweimer@redhat.com \
--cc=j.alglave@ucl.ac.uk \
--cc=libc-alpha@sourceware.org \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mathieu.desnoyers@efficios.com \
--cc=npiggin@gmail.com \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=triegel@redhat.com \
--cc=will.deacon@arm.com \
/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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox