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

[Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>]

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