From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: "paulmck@kernel.org" <paulmck@kernel.org>,
Peter Zijlstra <peterz@infradead.org>,
"parri.andrea" <parri.andrea@gmail.com>, will <will@kernel.org>,
"boqun.feng" <boqun.feng@gmail.com>, npiggin <npiggin@gmail.com>,
dhowells <dhowells@redhat.com>, "j.alglave" <j.alglave@ucl.ac.uk>,
"luc.maranget" <luc.maranget@inria.fr>, akiyks <akiyks@gmail.com>,
dlustig <dlustig@nvidia.com>, joel <joel@joelfernandes.org>,
urezki <urezki@gmail.com>,
quic_neeraju <quic_neeraju@quicinc.com>,
frederic <frederic@kernel.org>,
Kernel development list <linux-kernel@vger.kernel.org>
Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
Date: Wed, 18 Jan 2023 21:28:28 -0500 [thread overview]
Message-ID: <Y8iqzJXVZX1lS7Kp@rowland.harvard.edu> (raw)
In-Reply-To: <839e1765-7d47-73df-02f0-8122306b5fb3@huaweicloud.com>
Jonas, each of your emails introduces too many new thoughts and ideas!
I can't keep up. So in this reply I'm going to skip over most of what
you wrote. If you think any of the items I have elided are worth
pursuing, you can bring them up in a new thread -- hopefully with just
one main thought per email! :-)
On Wed, Jan 18, 2023 at 12:25:05PM +0100, Jonas Oberhauser wrote:
>
>
> On 1/17/2023 10:19 PM, Alan Stern wrote:
> > On Tue, Jan 17, 2023 at 06:48:12PM +0100, Jonas Oberhauser wrote:
> > > On 1/14/2023 5:42 PM, Alan Stern wrote:
> > > Pretending for simplicity that rscs and grace periods aren't reads&writes
> > They aren't. You don't have to pretend.
>
> rscs are reads& writes in herd. That's how the data dependency works in your
> patch, right?
No, you're mixing up RCU and SRCU. The RCU operations rcu_read_lock()
and rcu_read_unlock() are not loads or stores; they're just fences. In
the current form of the LKMM the same is true for the SRCU operations
srcu_read_lock() and srcu_read_unlock(), but in the patch I submitted
they are indeed loads and stores.
> I consider that a hack though and don't like it.
It _is_ a bit of a hack, but not a huge one. srcu_read_lock() really
is a lot like a load, in that it returns a value obtained by reading
something from memory (along with some other operations, though, so it
isn't a simple straightforward read -- perhaps more like an
atomic_inc_return_relaxed).
srcu_read_unlock() is somewhat less like a store, but it does have one
notable similarity: It takes an input value and therefore can be the
target of a data dependency. The biggest difference is that an
srcu_read_unlock() can't really be read-from. It would be nice if herd
had an event type that behaved this way.
Also, herd doesn't have any way of saying that the value passed to a
store is an unmodified copy of the value obtained by a load. In our
case that doesn't matter much -- nobody should be writing litmus tests
in which the value returned by srcu_read_lock() is incremented and then
decremented again before being passed to srcu_write_lock()!
> > > > There was also something about what should happen when you have two
> > > > grace periods in a row.
> > > Note that two grace periods in a row are a subset of po;rcu-gp;po and thus
> > > gp, and so there's nothing to be done.
> > That is not stated carefully, but it probably is wrong. Consider this:
> >
> > P0 P1 P2
> > --------------- -------------- -----------------
> > rcu_read_lock Wy=1 rcu_read_lock
> > Wx=1 synchronize_rcu Wz=1
> > Ry=0 synchronize_rcu Rx=0
> > rcu_read_unlock Rz=0 rcu_read_unlock
> >
> > (W stands for Write and R for Read.) This execution is forbidden by the
> > counting rule: Its cycle has two grace periods and two critical
> > sections. But if we changed the definition of gp to be
> >
> > let gp = po ; [Sync-rcu | Sync-srcu] ; po
> >
> > then the memory model would allow the execution. So having the po? at
> > the end of gp is vital.
>
> I hadn't thought yet about the effect of modifying the definition of gp, but
> I don't think this example relies on gp at all.
> The model would forbid this even if rcu-fence and gp were both changed from
> po? to po.
> From Rz=0 we know
> second sync() ->rcu-gp;po Rz ->prop Wz ->po P2 unlock() ->rcu-rscsi P2
> lock()
> From Ry=0 we know
> P1 unlock() ->rcu-rsci P1 lock() ->po Ry ->prop Wy ->po;rcu-gp first
> sync()
>
> which are both rcu-order.
> Then from Rx=0 we have
> Rx ->prop Wx ->po P1 unlock() ->rcu-order first sync() ->po second sync()
> ->rcu-order P2 lock() ->po Rx
> of course since po is one case of rcu-link, we get
> Rx ->prop Wx ->po P1 unlock() ->rcu-order P2 lock() ->po Rx
> and hence
> Rx ->prop Wx ->rcu-fence Rx
> which is supposed to be irreflexive (even with rcu-fence=po;rcu-order;po).
By golly, you're right! I'm still thinking in terms of an older
version of the memory model, which used gp in place of rcu-gp. In
that version, P1's write and read would be linked by gp but not by
(gp ; rcu-link ; gp) if the po? at the end of the definition of gp
was replaced by po.
> Note that if your ordering relies on actually using gp twice in a row, then
> these must come from strong-fence, but you should be able to just take the
> shortcut by merging them into a single gp.
> po;rcu-gp;po;rcu-gp;po <= gp <= strong-fence <= hb & strong-order
I don't know what you mean by this. The example above does rely on
having two synchronize_rcu() calls; with only one it would be allowed.
> > > I don't think rcu-order is necessary at all to define LKMM, and one can
> > > probably just use rcu-extend instead of rcu-order (and in fact even a
> > > version of rcu-extend without any lone rcu-gps).
> > Sure, you could do that, but it wouldn't make sense. Why would anyone
> > want to define an RCU ordering relation that includes
> >
> > gp ... rscs ... gp ... rscs
> >
> > but not
> >
> > gp ... rscs ... rscs ... gp
> >
> > ?
>
> Because the the RCU Grace Period Guarantee doesn't say "if a gp happens
> before a gp, with some rscs in between, ...".
> So I think even the picture is not the best picture to draw for RCU
> ordering. I think the right picture to draw for RCU ordering is something
> like this:
> case (1): C ends before G does:
>
> rcsc ... ... ... ... ... gp
>
> case (2): G ends before C does:
>
> gp ... ... ... ... ... rscs
>
> where the dots are some relation that means "happens before".
Okay. So we could define rcu-order by:
let rec rcu-order = (rcu-gp ; rcu-link ; (rcu-order ; rcu-link)* ; rcu-rscsi) |
(rcu-rscsi ; rcu-link ; (rcu-order ; rcu-link)* ; rcu-gp)
(ignoring the SRCU cases). That is a little awkward; it might make
sense to factor out (rcu-link ; (rcu-order ; rcu-link)*) as a separate
relation and do a simultaneous recursion on both relations.
But either way, rcu-fence would have to be defined as (po ; rcu-order+ ; po?),
which looks a little odd.
Alan
next prev parent reply other threads:[~2023-01-19 2:28 UTC|newest]
Thread overview: 161+ messages / expand[flat|nested] mbox.gz Atom feed top
[not found] <20220921173109.GA1214281@paulmck-ThinkPad-P17-Gen-1>
[not found] ` <YytfFiMT2Xsdwowf@rowland.harvard.edu>
[not found] ` <YywXuzZ/922LHfjI@hirez.programming.kicks-ass.net>
[not found] ` <114ECED5-FED1-4361-94F7-8D9BC02449B7>
[not found] ` <YzSAnclenTz7KQyt@rowland.harvard.edu>
[not found] ` <f763bd5ff835458d8750b61da47fe316@huawei.com>
2023-01-03 18:56 ` Internal vs. external barriers (was: Re: Interesting LKMM litmus test) Alan Stern
2023-01-04 15:37 ` Andrea Parri
2023-01-04 20:58 ` Alan Stern
[not found] ` <ee186bc17a5e48298a5373f688496dce@huawei.com>
2023-01-05 17:32 ` Paul E. McKenney
[not found] ` <bea712c82e6346f8973399a5711ff78a@huawei.com>
2023-01-11 15:06 ` Alan Stern
[not found] ` <768ffe7edc7f4ddfacd5b0a8e844ed84@huawei.com>
2023-01-11 17:01 ` Alan Stern
[not found] ` <07579baee4b84532a76ea8b0b33052bb@huawei.com>
2023-01-12 21:57 ` Paul E. McKenney
2023-01-13 16:38 ` Alan Stern
2023-01-13 19:54 ` Paul E. McKenney
[not found] ` <06a8aef7eb8d46bca34521a80880dae3@huawei.com>
2023-01-14 17:42 ` Paul E. McKenney
[not found] ` <e51c82a113484b6bb62354a49376f248@huawei.com>
2023-01-14 16:42 ` Alan Stern
2023-01-17 17:48 ` Jonas Oberhauser
2023-01-17 21:19 ` Alan Stern
2023-01-18 11:25 ` Jonas Oberhauser
2023-01-19 2:28 ` Alan Stern [this message]
2023-01-19 11:22 ` Jonas Oberhauser
2023-01-19 16:41 ` Alan Stern
2023-01-19 18:43 ` Paul E. McKenney
2023-01-23 16:16 ` Jonas Oberhauser
2023-01-23 19:58 ` Alan Stern
2023-01-23 20:06 ` Jonas Oberhauser
2023-01-23 20:41 ` Alan Stern
2023-01-24 13:21 ` Jonas Oberhauser
2023-01-24 15:54 ` Jonas Oberhauser
2023-01-24 17:22 ` Alan Stern
[not found] ` <4c1abc7733794519ad7c5153ae8b58f9@huawei.com>
2023-01-13 16:28 ` Alan Stern
2023-01-13 20:07 ` Paul E. McKenney
2023-01-13 20:32 ` Paul E. McKenney
2023-01-14 17:40 ` Alan Stern
2023-01-14 17:48 ` Paul E. McKenney
[not found] ` <136d019d8c8049f6b737627df830e66f@huawei.com>
2023-01-14 17:53 ` Paul E. McKenney
2023-01-14 18:15 ` Paul E. McKenney
2023-01-14 19:58 ` Alan Stern
2023-01-15 5:19 ` Paul E. McKenney
2023-01-14 20:19 ` Alan Stern
2023-01-15 5:15 ` Paul E. McKenney
2023-01-15 16:23 ` Alan Stern
2023-01-15 18:10 ` Paul E. McKenney
2023-01-15 20:46 ` Alan Stern
2023-01-16 4:23 ` Paul E. McKenney
2023-01-16 18:11 ` Alan Stern
2023-01-16 19:06 ` Paul E. McKenney
2023-01-16 19:20 ` Alan Stern
2023-01-16 22:13 ` Paul E. McKenney
2023-01-17 11:46 ` Andrea Parri
2023-01-17 15:14 ` Paul E. McKenney
2023-01-17 15:56 ` Alan Stern
2023-01-17 17:43 ` Paul E. McKenney
2023-01-17 18:27 ` Jonas Oberhauser
2023-01-17 18:55 ` Paul E. McKenney
2023-01-17 20:20 ` Jonas Oberhauser
2023-01-17 20:15 ` Alan Stern
2023-01-18 3:50 ` Paul E. McKenney
2023-01-18 16:50 ` Alan Stern
2023-01-18 19:42 ` Jonas Oberhauser
2023-01-18 20:19 ` Paul E. McKenney
2023-01-18 20:30 ` Jonas Oberhauser
2023-01-18 21:12 ` Paul E. McKenney
2023-01-18 21:24 ` Jonas Oberhauser
2023-01-19 0:11 ` Paul E. McKenney
2023-01-19 13:39 ` Jonas Oberhauser
2023-01-19 18:41 ` Paul E. McKenney
2023-01-19 19:51 ` Alan Stern
2023-01-19 21:53 ` Paul E. McKenney
2023-01-19 22:04 ` Alan Stern
2023-01-19 23:03 ` Paul E. McKenney
2023-01-20 9:43 ` Jonas Oberhauser
2023-01-20 15:39 ` Paul E. McKenney
2023-01-20 20:46 ` Jonas Oberhauser
2023-01-20 21:37 ` Paul E. McKenney
2023-01-20 22:36 ` Jonas Oberhauser
2023-01-20 23:19 ` Paul E. McKenney
2023-01-21 0:03 ` Jonas Oberhauser
2023-01-21 0:34 ` Paul E. McKenney
2023-01-20 3:55 ` Paul E. McKenney
2023-01-20 9:20 ` Jonas Oberhauser
2023-01-20 12:34 ` Jonas Oberhauser
2023-01-20 12:51 ` Jonas Oberhauser
2023-01-20 15:32 ` Paul E. McKenney
2023-01-20 20:56 ` Jonas Oberhauser
2023-01-20 21:40 ` Paul E. McKenney
2023-01-20 16:14 ` Alan Stern
2023-01-20 17:30 ` Paul E. McKenney
2023-01-20 18:15 ` Alan Stern
2023-01-20 18:59 ` Paul E. McKenney
2023-01-20 10:13 ` Jonas Oberhauser
2023-01-20 15:47 ` Paul E. McKenney
2023-01-20 22:21 ` Jonas Oberhauser
2023-01-20 16:18 ` Alan Stern
2023-01-20 21:41 ` Jonas Oberhauser
2023-01-21 4:38 ` Paul E. McKenney
2023-01-21 17:36 ` Alan Stern
2023-01-21 18:40 ` Paul E. McKenney
2023-01-21 19:56 ` Alan Stern
2023-01-21 20:10 ` Paul E. McKenney
2023-01-21 21:03 ` Alan Stern
2023-01-21 23:49 ` Paul E. McKenney
2023-01-23 11:48 ` Jonas Oberhauser
2023-01-23 15:55 ` Alan Stern
2023-01-23 19:40 ` Jonas Oberhauser
2023-01-23 20:34 ` Alan Stern
2023-01-18 20:06 ` Paul E. McKenney
2023-01-18 20:54 ` Alan Stern
2023-01-18 21:05 ` Jonas Oberhauser
2023-01-19 0:02 ` Paul E. McKenney
2023-01-19 2:19 ` Alan Stern
2023-01-19 11:23 ` Paul E. McKenney
2023-01-20 16:01 ` Alan Stern
2023-01-20 17:58 ` Paul E. McKenney
2023-01-20 18:37 ` Alan Stern
2023-01-20 19:20 ` Paul E. McKenney
2023-01-20 20:36 ` Alan Stern
2023-01-20 21:20 ` Paul E. McKenney
2023-01-22 20:32 ` Alan Stern
2023-01-23 20:16 ` Paul E. McKenney
2023-01-24 2:18 ` Alan Stern
2023-01-24 4:06 ` Paul E. McKenney
2023-01-24 11:09 ` Andrea Parri
2023-01-24 14:54 ` Paul E. McKenney
2023-01-24 15:11 ` Jonas Oberhauser
2023-01-24 16:22 ` Paul E. McKenney
2023-01-24 16:39 ` Jonas Oberhauser
2023-01-24 17:26 ` Paul E. McKenney
2023-01-24 19:30 ` Jonas Oberhauser
2023-01-24 22:15 ` Paul E. McKenney
2023-01-24 22:35 ` Alan Stern
2023-01-24 22:54 ` Paul E. McKenney
2023-01-25 1:54 ` Alan Stern
2023-01-25 2:20 ` Paul E. McKenney
2023-01-25 13:10 ` Jonas Oberhauser
2023-01-25 15:05 ` Paul E. McKenney
2023-01-25 15:34 ` Alan Stern
2023-01-25 17:18 ` Paul E. McKenney
2023-01-25 17:42 ` Jonas Oberhauser
2023-01-25 19:08 ` Alan Stern
2023-01-25 19:46 ` Paul E. McKenney
2023-01-25 20:36 ` Andrea Parri
2023-01-25 21:10 ` Jonas Oberhauser
2023-01-25 21:23 ` Paul E. McKenney
2023-01-25 20:46 ` Alan Stern
2023-01-25 21:38 ` Paul E. McKenney
2023-01-25 23:33 ` Paul E. McKenney
2023-01-26 1:45 ` Alan Stern
2023-01-26 1:53 ` Paul E. McKenney
2023-01-26 12:17 ` Jonas Oberhauser
2023-01-26 18:48 ` Paul E. McKenney
2023-01-27 15:03 ` Jonas Oberhauser
2023-01-27 16:50 ` Paul E. McKenney
2023-01-27 16:54 ` Paul E. McKenney
2023-01-18 19:57 ` Jonas Oberhauser
2023-01-18 21:06 ` Paul E. McKenney
2023-01-18 2:15 ` Alan Stern
2023-01-18 5:17 ` Paul E. McKenney
2023-01-18 16:03 ` Alan Stern
2023-01-18 16:59 ` Boqun Feng
2023-01-18 17:08 ` Alan Stern
2023-01-18 17:41 ` Paul E. McKenney
2023-01-19 19:07 ` Paul E. McKenney
2023-01-14 16:55 ` Alan Stern
2023-01-14 17:35 ` Paul E. McKenney
[not found] ` <17078dd97cb6480f9c51e27058af3197@huawei.com>
2023-01-14 17:27 ` Alan Stern
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=Y8iqzJXVZX1lS7Kp@rowland.harvard.edu \
--to=stern@rowland.harvard.edu \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=jonas.oberhauser@huaweicloud.com \
--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=quic_neeraju@quicinc.com \
--cc=urezki@gmail.com \
--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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).