From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huawei.com>
Cc: paulmck@kernel.org, parri.andrea@gmail.com, will@kernel.org,
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, joel@joelfernandes.org,
urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
linux-kernel@vger.kernel.org, viktor@mpi-sws.org
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po
Date: Thu, 19 Jan 2023 15:06:07 -0500 [thread overview]
Message-ID: <Y8mirwPeCBWY7tCH@rowland.harvard.edu> (raw)
In-Reply-To: <75c74fe1-a846-aed8-c00c-45deeb1cfdda@huaweicloud.com>
On Thu, Jan 19, 2023 at 04:05:38PM +0100, Jonas Oberhauser wrote:
>
>
> On 1/19/2023 4:13 AM, Alan Stern wrote:
> > On Wed, Jan 18, 2023 at 10:38:11PM +0100, Jonas Oberhauser wrote:
> > >
> > > On 1/18/2023 8:52 PM, Alan Stern wrote:
> > > > On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote:
> > > > > - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> > > > > - ([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> > > > > - fencerel(After-unlock-lock) ; [M])
> > > > > + ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
> > > > Shouldn't the po case of (co | po) remain intact here?
> > > You can leave it here, but it is already covered by two other parts: the
> > > ordering given through ppo/hb is covered by the po-unlock-lock-po & int in
> > > ppo, and the ordering given through pb is covered by its inclusion in
> > > strong-order.
> > What about the ordering given through
> > A-cumul(strong-fence)/cumul-fence/prop/hb? I suppose that might be
> > superseded by pb as well,
> Indeed, in fact all of A-cumul(strong-fence) is already covered through pb.
> > but it seems odd not to have it in hb.
> > In general, the idea in the memory model is that hb ordering relies on
> > the non-strong properties of fences, whereas pb relies on the properties
> > of strong fences, and rb relies on the properties of the RCU fences.
>
> I agree in the sense that all strong-ordering operations are A-cumulative
> and not including them in A-cumul is weird.
The reason for including A-cumul(strong-fence | po-rel) in the
definition of cumul-fence had nothing to do with the fact that the
fences needed to be strong. It was simply a convenient way to list
all the A-cumulative fences. It could just as well have been written
A-cumul(mb | gp | po-rel).
> On the other side the model becomes a tiny bit smaller and simpler when all
> ordering of prop;strong-ordering goes through a single place (pb).
>
> If you want, you could think of the A-cumulativity of strong ordering
> operations as being a consequence of their strong properties. Mathematically
That's backward logic. Being strong isn't the reason the fences are
A-cumulative. Indeed, the model could have been written not to assume
that strong fences are A-cumulative.
> it already is the case, since
> overwrite&ext ; cumul-fence* ; rfe ; strong-fence ; cumul-fence* ; rfe?
> is a subset of
> prop ; strong-fence ; hb*
Invalid reasoning. If strong fences had not been A-cumulative then this
inclusion wouldn't matter, because the pb relation would have been
defined differently.
> > > > > @@ -91,8 +89,12 @@ acyclic hb as happens-before
> > > > > (* Write and fence propagation ordering *)
> > > > > (****************************************)
> > > > > -(* Propagation: Each non-rf link needs a strong fence. *)
> > > > > -let pb = prop ; strong-fence ; hb* ; [Marked]
> > > > > +(* Strong ordering operations *)
> > > > > +let strong-order = strong-fence | ([M] ; po-unlock-lock-po ;
> > > > > + [After-unlock-lock] ; po ; [M])
> > > > This is not the same as the definition removed above. In particular,
> > > > po-unlock-lock-po only allows one step along the locking chain -- it has
> > > > rf where the definition above has co.
> > > Indeed it is not, but the subsequent lock-unlock sequences are in hb*. For
> > > this reason it can be simplified to just consider the directly following
> > > unlock().
> > I'm not sure that argument is right. The smp_mb__after_unlock_lock
> > needs to go after the _last_ lock in the sequence, not after the first.
> > So you don't have to worry about subsequent lock-unlock sequences; you
> > have to worry about preceding lock-unlock sequences.
>
> I formalized a proof of equivalence in Coq a few months ago, but I was
> recalling the argument incorrectly from memory.
> I think the correct argument is that the previous po-unlock-lock-po form a
> cumul-fence*;rfe;po sequence that starts with a po-rel.
> so any
> prop; .... ; co ; ... ; this fence ;...
> can be rewritten to
> prop; cumul_fence* ; po-unlock-lock-po ; this fence ;...
> and because the the first cumul-fence here needs to start with po-release,
> the prop ;cumul-fence* can be merged into a larger prop, leaving
> prop; po-unlock-lock-po ; this fence ;...
This may be so, but I would like to point out that the memory model was
not particularly designed to be as short or as simple as possible, but
more to reflect transparently the intuitions that kernel programmers
have about the ways ordering should work in the kernel. It may very
well include redundancies as a result. I don't think that's a bad
point.
For example, the prop relation is meant to cover all fences that order
store propagations in the usual way (basically all fences except rmb).
This includes both weak and strong fences; the fact that strong fences
also have other ordering properties doesn't mean they should be kept out
of prop.
Alan
next prev parent reply other threads:[~2023-01-19 20:06 UTC|newest]
Thread overview: 29+ messages / expand[flat|nested] mbox.gz Atom feed top
2023-01-17 19:31 [PATCH] tools/memory-model: Make ppo a subrelation of po Jonas Oberhauser
2023-01-17 23:45 ` Boqun Feng
2023-01-18 12:13 ` Jonas Oberhauser
2023-01-18 19:52 ` Alan Stern
2023-01-18 20:22 ` Andrea Parri
2023-01-18 21:38 ` Jonas Oberhauser
2023-01-19 3:13 ` Alan Stern
2023-01-19 15:05 ` Jonas Oberhauser
2023-01-19 20:06 ` Alan Stern [this message]
2023-01-20 11:12 ` Jonas Oberhauser
2023-01-20 16:32 ` Alan Stern
2023-01-21 0:41 ` Jonas Oberhauser
2023-01-21 20:56 ` Alan Stern
2023-01-23 13:59 ` Jonas Oberhauser
2023-01-23 17:28 ` Alan Stern
2023-01-23 19:33 ` Jonas Oberhauser
2023-01-23 21:10 ` Alan Stern
2023-01-24 13:14 ` Jonas Oberhauser
2023-01-24 17:14 ` Alan Stern
2023-01-24 20:23 ` Jonas Oberhauser
2023-01-25 2:57 ` Alan Stern
2023-01-25 13:06 ` Jonas Oberhauser
2023-01-25 15:56 ` Alan Stern
2023-01-23 18:25 ` Jonas Oberhauser
2023-01-23 20:25 ` Alan Stern
2023-01-24 12:54 ` Jonas Oberhauser
2023-01-24 16:03 ` Alan Stern
2023-01-18 21:30 ` Andrea Parri
2023-01-18 22:02 ` Jonas Oberhauser
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=Y8mirwPeCBWY7tCH@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@huawei.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=viktor@mpi-sws.org \
--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).