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

[Jonas Oberhauser]

On 1/19/2023 4:13 AM, Alan Stern wrote:
> On Wed, Jan 18, 2023 at 10:38:11PM +0100, Jonas Oberhauser wrote:
> > On 1/18/2023 8:52 PM, Alan Stern wrote:
> > > On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote:
> > > > -	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> > > > -	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> > > > -		fencerel(After-unlock-lock) ; [M])
> > > > +	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
> > > Shouldn't the po case of (co | po) remain intact here?
> > You can leave it here, but it is already covered by two other parts: the
> > ordering given through ppo/hb is covered by the po-unlock-lock-po & int in
> > ppo, and the ordering given through pb is covered by its inclusion in
> > strong-order.
> What about the ordering given through
> A-cumul(strong-fence)/cumul-fence/prop/hb?  I suppose that might be
> superseded by pb as well,
Indeed, in fact all of A-cumul(strong-fence) is already covered through pb.
> but it seems odd not to have it in hb.
> In general, the idea in the memory model is that hb ordering relies on
> the non-strong properties of fences, whereas pb relies on the properties
> of strong fences, and rb relies on the properties of the RCU fences.

I agree in the sense that all strong-ordering operations are 
A-cumulative and not including them in A-cumul is weird.
On the other side  the model becomes a tiny bit smaller and simpler when 
all ordering of prop;strong-ordering goes through a single place (pb).

If you want, you could think of the A-cumulativity of strong ordering 
operations as being a consequence of their strong properties. 
Mathematically it already is the case, since
  overwrite&ext ; cumul-fence* ; rfe ; strong-fence ; cumul-fence* ; rfe?
is a subset of
  prop ; strong-fence ; hb*



> > > > @@ -91,8 +89,12 @@ acyclic hb as happens-before
> > > >    (* Write and fence propagation ordering *)
> > > >    (****************************************)
> > > > -(* Propagation: Each non-rf link needs a strong fence. *)
> > > > -let pb = prop ; strong-fence ; hb* ; [Marked]
> > > > +(* Strong ordering operations *)
> > > > +let strong-order = strong-fence | ([M] ; po-unlock-lock-po ;
> > > > +		[After-unlock-lock] ; po ; [M])
> > > This is not the same as the definition removed above.  In particular,
> > > po-unlock-lock-po only allows one step along the locking chain -- it has
> > > rf where the definition above has co.
> > Indeed it is not, but the subsequent lock-unlock sequences are in hb*. For
> > this reason it can be simplified to just consider the directly following
> > unlock().
> I'm not sure that argument is right.  The smp_mb__after_unlock_lock
> needs to go after the _last_ lock in the sequence, not after the first.
> So you don't have to worry about subsequent lock-unlock sequences; you
> have to worry about preceding lock-unlock sequences.

I formalized a proof of equivalence in Coq a few months ago, but I was 
recalling the argument incorrectly from memory.
I think the correct argument is that the previous po-unlock-lock-po form 
a cumul-fence*;rfe;po sequence that starts with a po-rel.
so any
    prop; .... ; co ; ... ; this fence ;...
can be rewritten to
    prop; cumul_fence* ; po-unlock-lock-po ; this fence ;...
and because the the first cumul-fence here needs to start with 
po-release, the prop ;cumul-fence* can be merged into a larger prop, leaving
    prop; po-unlock-lock-po ; this fence ;...

Best wishes,
jonas