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

[Jonas Oberhauser]

On 1/30/2023 3:39 AM, Alan Stern wrote:
> On Sun, Jan 29, 2023 at 11:19:32PM +0100, Jonas Oberhauser wrote:
> > You could do it, by turning the relation into one massive recursive
> > definition.
> Which would make pretty much the entire memory model one big recursion.
> I do not want to do that.

Neither do I :D

> > Thinking about what the options are:
> > 1) accept the difference and run with it by making it consistent inside the
> > axiomatic model
> > 2) fix it through the recursive definition, which seems to be quite ugly but
> > also consistent with the power operational model as far as I can tell
> > 3) weaken the operational model... somehow
> > 4) just ignore the anomaly
> > 5) ???
> >
> > Currently my least favorite option is 4) since it seems a bit off that the
> > reasoning applies in one specific case of LKMM, more specifically the data
> > race definition which should be equivalent to "the order of the two races
> > isn't fixed", but here the order isn't fixed but it's a data race.
> > I think the patch happens to almost do 1) because the xbstar&int at the end
> > should already imply ordering through the prop&int <= hb rule.
> > What would remain is to also exclude rcu-fence somehow.
> IMO 1) is the best choice.

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.

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:

> {}
>
> 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".
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.

Best wishes, jonas