Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20;
Message-ID: <75c74fe1-a846-aed8-c00c-45deeb1cfdda@huaweicloud.com>
Date:   Thu, 19 Jan 2023 16:05:38 +0100
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.6.1
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po
To:     Alan Stern <stern@rowland.harvard.edu>
Cc:     paulmck@kernel.org, parri.andrea@gmail.com, will@kernel.org,
        peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
        dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
        akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
        urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
        linux-kernel@vger.kernel.org, viktor@mpi-sws.org
References: <20230117193159.22816-1-jonas.oberhauser@huaweicloud.com>
 <Y8hN7vs/w8LhMasT@rowland.harvard.edu>
 <c22ec058-b058-0b6e-718b-348ff5cb5004@huaweicloud.com>
 <Y8i1QNjnZwim5uMq@rowland.harvard.edu>
From:   Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <Y8i1QNjnZwim5uMq@rowland.harvard.edu>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Precedence: bulk


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