Date:   Mon, 27 Feb 2023 13:41:25 -0500
From:   Alan Stern <stern@rowland.harvard.edu>
To:     Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc:     Jonas Oberhauser <jonas.oberhauser@huawei.com>,
        Boqun Feng <boqun.feng@gmail.com>,
        "Paul E. McKenney" <paulmck@kernel.org>, parri.andrea@gmail.com,
        will@kernel.org, peterz@infradead.org, 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
Subject: Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po
Message-ID: <Y/z5VXdhPFtbtd3V@rowland.harvard.edu>
References: <20230224183758.GQ2948950@paulmck-ThinkPad-P17-Gen-1>
 <20230226010110.GA1576556@paulmck-ThinkPad-P17-Gen-1>
 <Y/rEH2r9i0BtfxEW@rowland.harvard.edu>
 <Y/rNUfW509AQYCYn@boqun-archlinux>
 <Y/rSQ2FNTJyj2bqR@rowland.harvard.edu>
 <a862ee59-ca12-b609-48cc-0784c7ce24af@huaweicloud.com>
 <Y/uOA3umovz06/SV@rowland.harvard.edu>
 <dd87369d-825f-e932-dd86-8e46e92d1a7e@huaweicloud.com>
 <Y/zXYXM1lgk7Msig@rowland.harvard.edu>
 <b07b75cd-0627-da3c-54e8-cc22088c148e@huaweicloud.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <b07b75cd-0627-da3c-54e8-cc22088c148e@huaweicloud.com>
Precedence: bulk

On Mon, Feb 27, 2023 at 05:50:15PM +0100, Jonas Oberhauser wrote:
> > So I don't see this as a valid argument for not using rw-xbstar in
> > rw-race.  Even theoretically.
> 
> There's nothing wrong with using rw-xbstar in rw-race, especially in current
> LKMM, and I'm not arguing against that.
> 
> I'm saying that the argument
> "if rw-xbstar links a read R to a plain write W, and that plain write is
> replaced by a read R', and in case R' reads a value different from W,
> followed by a store W' (with some dependency from R' to W')? by the
> compiler, then the fact that R and R' can't have a data race means that it's
> safe to use rw-xbstar in rw-race"
> is incomplete. (Of course that doesn't mean the claim is wrong.)
> To make the argument complete, you also need that W' is generated if
> necessary, and more crucially that W' is still ordered behind R!
> Otherwise you would now have a data race between R and W', like in the
> hypothetical example I mentioned, even though R and R' don't race.
> 
> And if you do that second step in LKMM (even with the change of
> w-pre-bounded we are discussing) you quickly find that W' is indeed still
> ordered, so rw-xbstar is perfectly fine.
> 
> Perhaps that step is so trivial to you that you don't feel it needs
> mentioning : ) But speaking about LKMM-like models in general, some might
> have some subtle case where rw-xbstar links R and W but would not R and W'.

Ah, okay.  Yes, it is a subtle point.  And by the reasoning I just used, 
if such a case did exist then one could conclude it would be an example 
demonstrating that rw-xbstar should not have linked R and W in the first 
place.

And it looks like I should write up and submit a patch allowing more 
dependencies in the definition of w-pre-bounded.

Alan