Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po

[Jonas Oberhauser]

On 2/27/2023 5:16 PM, Alan Stern wrote:
> On Mon, Feb 27, 2023 at 03:03:16PM +0100, Jonas Oberhauser wrote:
>
> > > > Note there's also rw-xbstar (used with fr) which doesn't check for
> > > > r-pre-bounded, but it should be ok. That's because only reads would be
> > > > unordered, as a result the read (in the if (x != ..) x=..) should provide
> > > > the correct value. The store would be issued as necessary, and the issued
> > > > store would still be ordered correctly w.r.t the read.
> > > That isn't the reason I left r-pre-bounded out from rw-xbstar.  If the
> > > write gets changed to a read there's no need for rw-xbstar to check
> > > r-pre-bounded, because then rw-race would be comparing a read with
> > > another read (instead of with a write) and so there would be no
> > > possibility of a race in any case.
> > That is the first part of my explanation (only reads would be unordered) but
> It is?  I couldn't tell from what you wrote that this was supposed to
> imply we didn't have to worry about a data race.

Because it wasn't supposed to imply that, in the sense that by itself, 
the fact that the things that are left unordered are reads does not 
immediately imply that we don't have to worry about a data race. It's 
just a step in the sequence of reasoning. But of course I won't claim 
that I laid out that sequence in full enough detail to make sense.

> > I don't think it's sufficient in general.
> > Imagine a hypothetical memory model with a release fence that upgrades the
> > next memory operation only (and only stores) to release (e.g., to save some
> > opcode design space you do weird_release_fence;str x1 x2 instead of stlr x1
> > x2).
> > Then in the message passing pattern
> >
> > T1 {
> >     u = a;
> >     release(&x, 1);
> > }
> >
> > T2 {
> >    t = READ_ONCE(&x);
> >    weird_release_fence;
> >    a = 1;
> > }
> [That isn't the Message Passing pattern.  In the MP pattern, one thread
> does two writes and the other thread does two reads.  This is the Read
> Buffering (RB) pattern: Each thread does a read followed by a write.]

Ah, thanks. Somehow I misremembered MP to be any case of [do stuff on a] 
; x = ...  || read that update from x; [do stuff on a].

> > where T2 is changed by the compiler to
> >
> > T2 {
> >    t = READ_ONCE(&x);
> >    weird_release_fence();
> >    if (a!=1) a = 1;
> > }
> >
> > In the specific executions where t==1, there wouldn't be a data race when
> > just considering the equivalent of rw-xbstar, but u==1 and t==1 would be
> > possible (even though it might not seem so from the first example).
> If such a fence existed in the LKMM, we would handle this case by saying
> that weird_release_fence() does not give release semantics to an
> immediately following plain store; only to an immediately following
> marked store.  The reason being that the compiler is allowed to muck
> around with the code generated for plain accesses, so there's no
> guarantee that the first machine instruction generated for "a = 1;" will
> be a store.
>
> As a result, there would not be an rw-xbstar link from T1 to T2.

Sure, but IMHO a well-designed high-level model like LKMM shouldn't have 
such a fence at all :D This is something you might use in the 
implementation of a release store in inline-assembly, it doesn't belong 
in the source code. But it's just for the sake of argument anyways.


> > Of course in LKMM there's no such fence, but I think to make the argument
> > complete you still need to go through every case that provides the
> > w-pre-bounding and make sure it still provides the necessary order in the
> > compiler-generated version. (or you can try a more complicated argument of
> > the form "there would be another execution of the same program that would
> > have a data race", which works at least for this example, not sure in
> > general)
> 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'.

jonas