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

[Alan Stern]

On Mon, Feb 27, 2023 at 03:03:16PM +0100, Jonas Oberhauser wrote:
> Note that I don't want to remove the r-pre/post-bounded tests.
> What I agreed to is that the restriction to only addr for plain writes is an
> overly conservative "r-pre/post-bounded-style" test which is made redundant
> by the existence of the actual r-pre/post-bounded test.

Good, that agrees with what I've been thinking.

> > > 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.

> 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.]

> 
> 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.

> 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.

Alan