Messages in this thread | | | Date | Mon, 27 Feb 2023 13:41:25 -0500 | From | Alan Stern <> | Subject | Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po |
| |
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
| |