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

[Alan Stern]

On Wed, Jan 25, 2023 at 02:06:01PM +0100, Jonas Oberhauser wrote:
> 
> 
> On 1/25/2023 3:57 AM, Alan Stern wrote:
> > 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.

My mistake; what I meant was something a little smaller than rb.  That 
is,

	(overwrite & ext) ; wprop* ; rfe? ; rcu-fence

In other words, a relation expressing that rcu-fence acts as a strong 
fence.  But also something expressing that rcu-fence acts as an efence? 
-- I guess this is covered if the (overwrite & ext) part above is made 
optional, although that feels a little artificial.

I don't think we will be able to include rcu-fence in sprop, because we 
will need to use sprop in the definition of rcu-fence.

Oh yes, one other piece of terminology I forgot to mention.  The things 
you referred to before as "ordering operations" could instead be called 
"extended fences".  What do you think?

> > 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.

An invasive, multi-faceted change like this has to be broken down into 
multiple patches, each doing only one thing and each easily verified as 
not changing the meaning of the code.  Feel free to go ahead and work 
out a proposal.

Alan