From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.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: Tue, 24 Jan 2023 11:03:49 -0500 [thread overview]
Message-ID: <Y9ABZQ81oXTmggcY@rowland.harvard.edu> (raw)
In-Reply-To: <6f8575f3-f8b9-7738-24f0-5e390b50ac40@huaweicloud.com>
On Tue, Jan 24, 2023 at 01:54:14PM +0100, Jonas Oberhauser wrote:
>
>
> On 1/23/2023 9:25 PM, Alan Stern wrote:
> > On Mon, Jan 23, 2023 at 07:25:48PM +0100, Jonas Oberhauser wrote:
> > > Alright, after some synchronization in the other parts of this thread I am
> > > beginning to prepare the next iteration of the patch.
> > >
> > > 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, but it seems odd not to have it in hb.
> > > How should we resolve this?
> > > My current favorite (compromise :D) solution would be to
> > > 1. still eliminate both po and co cases from first definition of
> > > strong-fence which is used in ppo,
> > > 2. define a relation equal to the strong-order in this patch (with po|rf)
> > Wouldn't it need to have po|co? Consider:
> >
> > Wx=1 Rx=1 Ry=1 Rz=1
> > lock(s) lock(s) lock(s)
> > unlock(s) unlock(s) unlock(s)
> > Wy=1 Wz=1 smp_mb__after_unlock_lock
> > Rx=0
> >
> > With the co term this is forbidden. With only the rf term it is
> > allowed, because po-unlock-lock-po isn't A-cumulative.
> No, but unlock() is ( https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/tree/tools/memory-model/lock.cat?h=dev.2023.01.19a#n67
> ). So you get
So it is. I had forgotten about that. The model is getting too
complicated to fit entirely in my mind...
> Rx=0 ->overwrite Wx=1 ->rfe Rx1 ->po-rel T1:unlock(s) ->rfe T2:lock(s)
> ->po-unlock-lock-po;after ... fence;po Rx=0
> which is
> Rx=0 ->prop ; po-unlock-lock-po;after
> ... fence;po Rx=0
>
> Are you ok going forward like this then?
I guess so, provided we mention somewhere in the code or documentation
that this relation extends beyond a single rf.
Alan
next prev parent reply other threads:[~2023-01-24 16:03 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
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 [this message]
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=Y9ABZQ81oXTmggcY@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=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).