[lkml]   [2023]   [Jan]   [25]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
SubjectRe: [PATCH] tools/memory-model: Make ppo a subrelation of po

On 1/25/2023 3:57 AM, Alan Stern wrote:
> On Tue, Jan 24, 2023 at 09:23:02PM +0100, Jonas Oberhauser wrote:
>> On 1/24/2023 6:14 PM, Alan Stern wrote:
>>> On Tue, Jan 24, 2023 at 02:14:03PM +0100, Jonas Oberhauser wrote:
>>>> After mulling it over a bit in my big old head, I consider that even though
>>>> dropping the [W] may be shorter, it might make for the simpler model by
>>>> excluding lots of cases.
>>>> That makes me think you should do it for real in the definition of prop. And
>>>> not just at the very end, because in fact each cumul-fence link might come
>>>> from a non-A-cumulative fence. So the same argument you are giving should be
>>>> applied recursively.
>>>> Either
>>>> prop = (overwrite & ext)? ; (cumul-fence; [W])* ; rfe?
>>>> or integrate it directly into cumul-fence.
>>> I dislike this sort of argument. I understand the formal memory model
>>> by relating it to the informal operational model. Thus, cumul-fence
>>> links a write W to another event E when the fence guarantees that W will
>>> propagate to E's CPU before E executes.
>> I later wondered why it's not defined like this and realized that prop means
>> that it's before E executes.
>>> That's how the memory model
>>> expresses the propagation properties of these fences.
>> I don't think that's really a perfect match though.
>> For example, W ->wmb E (and thus cumul-fence) does guarantee that W
>> propagates to E's CPU before E executes.
>> But the propagation property of wmb is that W propagates to every CPU before
>> E propagates to that CPU.
>> It just so happens that the time E propagates to E's CPU is the time it
>> executes.
>> Indeed, looking at the non-strong properties of fences only, should give
>> rise to a relation that only says "W propagates to any CPU before E
>> propagates to that CPU" and that is a relation between stores. And quite
>> different from "W propagates to E's CPU before E executes".
>> I believe that relation is (cumul-fence;[W])+.
> Add an rfe? to the end and you get the "before E executes" version.

Yes, but with the minor caveat that this is only for the "because of the
weak propagation ordering of fences (pfence)" case.
Current prop also includes some other "before E executes" cases, e.g.,
when the last fence is po-unlock-lock-po or a strong-fence.

> Or more accurately (rfe? ; ppo*). Hmmm, the only reason for omitting that
> ppo* term in the model is that it would never be needed. So maybe we
> should after all do the same for the hb* term at the end of pb and the
> (hb* | pb*) part at the end of rb.
> Starting from first principles, it's apparent that each of these types
> of propagation fences is associated with two relations: one involving
> propagation order and a companion relation involving execution order.
> Here's what I mean. For the sake of discussion let's define several
> classes of fences:
> efences are those which constrain execution order;
> pfences are those which constrain propagation order;
> sfences are those which strongly constrain propagation order.
> Each class includes the following ones. (And if you like, you can
> insert afences between pfences and sfences -- they would be the
> A-cumulative fences.)
> Now, the memory model builds up successively more inclusive notions of
> execution order. This process starts with execution of instructions in
> the same CPU not involving fences. Thus we have the ppo relations:
> dependencies and a few oddball things like ((overwrite ; rfe) & int) or
> ([UL] ; po ; [LKR]).
> Next, the efences also restrict single-CPU execution order. These
> fences only need to have one associated relation since they don't
> specifically involve propagation. Adding rfe to the list gives us
> inter-CPU ordering.
> Then associated with pfences we have the relation you've been talking
> about:
> W propagates to each CPU before W' does.
> This is (cumul-fence ; [W]). Perhaps a better name for it would be
> wprop. Given this relation, we obtain a companion relation that
> restricts execution order:
> ((overwrite & ext) ; wprop+ ; rfe) & int.
> (Note that the overall form is the same for afences as for pfences.)
> Adding this companion relation into the mix gives us essentially hb.
> For sfences the associated relation expresses:
> W propagates to every CPU before Y executes.
> This is basically (wprop* ; rfe? ; sfence) (using the fact that all
> sfences are A-cumulative) -- or if you prefer, (wprop* ; cumul-sfence).
> We can call this sprop. Then the companion relation restricting
> execution order is:
> (overwrite & ext) ; sprop
> For RCU, the associated relation expressing t2(A) < t1(B) is rcu-order
> and the companion relation is rcu-fence.
Do we put rcu-order under sprop as well? Otherwise you need

(overwrite & ext)? ; rcu-fence

to express the full companion relation.

> Putting all those execution-order relations together gives us xb, the
> executes-before relation. Then the only axiom we need for all of this
> that xb is acyclic.
> Of course, I have left out a lot of details. Still, how does that sound
> as a scheme for rationalizing the memory model?

It seems like we're on the same page!
It would be an honor for me to fill in the details and propose a patch,
if you're interested.

Have fun, jonas

 \ /
  Last update: 2023-01-25 14:06    [W:0.249 / U:0.188 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site