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

[Jonas Oberhauser]

On 1/31/2023 4:06 PM, Alan Stern wrote:
> On Tue, Jan 31, 2023 at 02:56:00PM +0100, Jonas Oberhauser wrote:
> > I have some additional thoughts now. It seems that you could weaken the
> > operational model by stating that an A-cumulative fence orders propagation
> > of all *external* stores (in addition to all po-earlier stores) that
> > propagated to you before the fence is executed.
> How is that a weakening of the operational model?  It's what the
> operational model says right now.

No, as in the part that you have quoted, it is stated that an 
A-cumulative fence orderes propagation of *all* stores that propagated 
to you before the fence is executed.
I'm saying you could weaken this to only cover all *external* stores.

More precisely, I would change

> 	For each other CPU C', any store which propagates to C before
> 	a release fence is executed (including all po-earlier
> 	stores executed on C) is forced to propagate to C' before the
> 	store associated with the release fence does.

Into something like


     For each other CPU C', any *external* store which propagates to C 
before
     a release fence is executed as well as any po-earlier
     store executed on C is forced to propagate to C' before the
     store associated with the release fence does.

The difference is that po-later stores that happen to propagate to C 
before the release fence is executed would no longer be ordered.
That should be consistent with the axiomatic model.


> In theory, we could weaken the operational model by saying that pfences
> order propagation of stores from other CPUs only when those stores are
> read-from by instructions po-before the fence.  But I suspect that's not
> such a good idea.

That indeed looks too confusing.


> > It seems that on power, from an operational model perspective, there's
> > currently no difference between propagation fences ordering all stores vs
> > only external stores that propagated to the CPU before the fence is
> > executed, because they only have bidirectional (*->W) fences (sync, lwsync)
> > and not uni-directional (acquire, release), and so it is not possible for a
> > store that is po-later than the barrier to be executed before the barrier;
> > i.e., on power, every internal store that propagates to a CPU before the
> > fence executes is also po-earler than the fence.
> >
> > If power did introduce release stores, I think you could potentially create
> > implementations that allow the behavior in the example you have given, but I
> > don't think they are the most natural ones:
> Maybe so.  In any case, it's a moot point.  In fact, I don't know if any
> architecture supporting Linux allows a write that is po-after a release
> store to be reordered before the release store.

Arm and Risc5 do, but they are multi-copy-atomic anyways.

> > > P0(int *x, int *y, int *z)
> > > {
> > > 	int r1;
> > >
> > > 	r1 = READ_ONCE(*x);
> > > 	smp_store_release(y, 1);
> > > 	WRITE_ONCE(*z, 1);
> > > }
> > >
> > > P1(int *x, int *y, int *z)
> > > {
> > > 	int r2;
> > >
> > > 	r2 = READ_ONCE(*z);
> > > 	WRITE_ONCE(*x, r2);
> > > }
> > >
> > > P2(int *x, int *y, int *z)
> > > {
> > > 	int r3;
> > > 	int r4;
> > >
> > > 	r3 = READ_ONCE(*y);
> > > 	smp_rmb();
> > > 	r4 = READ_ONCE(*z);
> > > }
> > >
> > > exists (0:r1=1 /\ 2:r3=1 /\ 2:r4=0)
> > I could imagine that P0 posts both of its stores in a shared store buffer
> > before reading *x, but marks the release store as "not ready".
> > Then P1 forwards *z=1 from the store buffer and posts *x=1, which P0 reads,
> > and subsequently marks its release store as "ready".
> That isn't how release stores are meant to work.  The read of x is
> supposed to be complete before the release store becomes visible to any
> other CPU.

Note that the release store isn't observed until it becomes "ready", so 
it is really indistinguishable of whether it had become visible to any 
other CPU.
Indeed stores that aren't marked "ready" would be ignored during 
forwarding, and not allowed to be pushed to the cache.

The reason this kind of implementation seems less natural to me is that 
such an "not ready" store would need to be pushed back in the buffer (if 
it is the head of the buffer and the cache is ready to take a store), 
stall the later stores, or be aborted until it becomes ready.
That just seems to create a lot of hassle for no discernible benefit.
A "not ready" store probably shouldn't be put into a store queue, even 
if the only reason it is not ready is that there are some otherwise 
unrelated reads that haven't completed yet.



> This is true even in C11.

Arguable... The following pseudo-code litmus test should demonstrate this:

P0 {
   int r = read_relaxed(&x);
   store_release(&y,1);
}


P1 {
   int s = read_relaxed(&y);
   store_release(&x,1);
}

In C11, it should be possible to read r==s==1.


> > Then the release store is sent to the cache, where P2 reads *y=1 and then
> > *z=0.
> > Finally P0 sends its *z=1 store to the cache.
> >
> > However, a perhaps more natural implementation would not post the release
> > store to the store buffer until it is "ready", in which case the order in
> > the store buffer would be *z=1 before *y=1, and in this case the release
> > ordering would presumably work like your current operational model.
> >
> > Nevertheless, perhaps this slightly weaker operational model isn't as absurd
> > as it sounds. And I think many people wouldn't be shocked if the release
> > store didn't provide ordering with *z=1.
> This issue is one we should discuss with all the other people involved
> in maintaining the LKMM.
>
> Alan

Sure.

Btw, how to proceed for your SRCU patch and this one?
Are you planning to make any changes? I think the version you have is ok 
if you don't think the patch is improved by anything I brought up.

Any additional concerns/changes for this patch?

Best wishes, jonas