lkml.org 
[lkml]   [2023]   [Jan]   [24]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH] tools/memory-model: Make ppo a subrelation of po
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. 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.

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?

Alan

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