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

Jonas Oberhauser
2023-02-01T10:39:17Z

On 1/31/2023 5:55 PM, Alan Stern wrote:
> On Tue, Jan 31, 2023 at 04:33:25PM +0100, Jonas Oberhauser wrote:
>>
>> 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.
> I had to check that it wouldn't affect the (xbstar & int) part of vis,
> but it looks all right. This seems like a reasonable change.
>
> However, it only fixes part of the problem. Suppose an external write
> is read by an instruction po-after the release-store, but the read
> executes before the release-store. The operational model would still
> say the external write has to obey the propagation ordering, whereas the
> formal model doesn't require it.

Ouch. I had only thought about the [W];(xbstar & int);[Release] case,
but there's also the rfe;(xbstar & int);[Release] case....

>> Any additional concerns/changes for this patch?
> It should give the same data-race diagnostics as the current LKMM. This
> probably means the patch will need to punch up the definitions of
> *-pre-bounded and *-post-bounded, unless you can think of a better
> approach.
>
> Alan

Seems the 1 thing per patch mentally hasn't yet become ingrained in me.
Thanks!

jonas