Message-ID: <6f8575f3-f8b9-7738-24f0-5e390b50ac40@huaweicloud.com>
Date:   Tue, 24 Jan 2023 13:54:14 +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>
 <1180fe22-5e1d-ec8b-8012-b6578b1ca7c0@huaweicloud.com>
 <Y87tHNcvb5E+t3da@rowland.harvard.edu>
From:   Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <Y87tHNcvb5E+t3da@rowland.harvard.edu>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Precedence: bulk


On 1/23/2023 9:25 PM, Alan Stern wrote:
> On Mon, Jan 23, 2023 at 07:25:48PM +0100, Jonas Oberhauser wrote:
>> Alright, after some synchronization in the other parts of this thread I am
>> beginning to prepare the next iteration of the patch.
>>
>> 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, but it seems odd not to have it in hb.
>> How should we resolve this?
>> My current favorite (compromise :D) solution would be to
>> 1. still eliminate both po and co cases from first definition of
>> strong-fence which is used in ppo,
>> 2. define a relation equal to the strong-order in this patch (with po|rf)
> Wouldn't it need to have po|co?  Consider:
>
> 	Wx=1	Rx=1		Ry=1		Rz=1
> 		lock(s)		lock(s)		lock(s)
> 		unlock(s)	unlock(s)	unlock(s)
> 		Wy=1		Wz=1		smp_mb__after_unlock_lock
> 						Rx=0
>
> With the co term this is forbidden.  With only the rf term it is
> allowed, because po-unlock-lock-po isn't A-cumulative.
No, but unlock() is ( 
https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/tree/tools/memory-model/lock.cat?h=dev.2023.01.19a#n67 
). So you get

   Rx=0 ->overwrite Wx=1  ->rfe Rx1 ->po-rel  T1:unlock(s) ->rfe 
T2:lock(s) ->po-unlock-lock-po;after ... fence;po Rx=0
which is
   Rx=0          ->prop ;                           
po-unlock-lock-po;after ... fence;po Rx=0

Are you ok going forward like this then?

If not, I might prefer to redefine po-unlock-lock-po into something that 
works for all its use cases if possible. I think
|

   po ; [UL] ; (po|co?;rf) ; [LKR] ; po

|might be such a definition but haven't fully thought about it.

best wishes, jonas