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: <e4a2059d-8199-b74e-d776-116c99c73fe6@huaweicloud.com>
Date:   Sat, 8 Apr 2023 20:57:57 +0200
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.9.1
Subject: Re: Litmus test names
To:     Joel Fernandes <joel@joelfernandes.org>,
        "Paul E. McKenney" <paulmck@kernel.org>
Cc:     Alan Stern <stern@rowland.harvard.edu>,
        linux-kernel@vger.kernel.org, Boqun Feng <boqun.feng@gmail.com>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Luc Maranget <luc.maranget@inria.fr>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will.deacon@arm.com>,
        Akira Yokosawa <akiyks@gmail.com>,
        Andrea Parri <parri.andrea@gmail.com>,
        Daniel Lustig <dlustig@nvidia.com>,
        David Howells <dhowells@redhat.com>,
        Jonas Oberhauser <jonas.oberhauser@huawei.com>,
        linux-arch@vger.kernel.org, Nicholas Piggin <npiggin@gmail.com>,
        =?UTF-8?Q?Paul_Heidekr=c3=bcger?= <paul.heidekrueger@in.tum.de>,
        Will Deacon <will@kernel.org>
References: <ea9376b4-4b3d-48ee-9c27-ad8de8a7b5cb@paulmck-laptop>
 <3908932E-17D4-4B87-AB0C-D10564F10623@joelfernandes.org>
 <159545c3-0093-3cbd-e822-7298ae764966@huaweicloud.com>
 <d32901a8-3a07-440c-9089-36b37c3f04e5@paulmck-laptop>
 <20230408164956.GA680332@google.com>
From:   Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <20230408164956.GA680332@google.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Precedence: bulk


On 4/8/2023 6:49 PM, Joel Fernandes wrote:
> On Fri, Apr 07, 2023 at 05:49:02PM -0700, Paul E. McKenney wrote:
>> On Fri, Apr 07, 2023 at 03:05:01PM +0200, Jonas Oberhauser wrote:
>>>
>>> On 4/7/2023 2:12 AM, Joel Fernandes wrote:
>>>>
>>>>> On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
>>>>>
>>>>> ﻿On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
>>>>>> Paul:
>>>>>>
>>>>>> I just saw that two of the files in
>>>>>> tools/memory-model/litmus-tests have
>>>>>> almost identical names:
>>>>>>
>>>>>>   Z6.0+pooncelock+pooncelock+pombonce.litmus
>>>>>>   Z6.0+pooncelock+poonceLock+pombonce.litmus
>>>>>>
>>>>>> They differ only by a lower-case 'l' vs. a capital 'L'.  It's
>>>>>> not at all
>>>>>> easy to see, and won't play well in case-insensitive filesystems.
>>>>>>
>>>>>> Should one of them be renamed?
>>>>>
> FWIW, if I move that smp_mb_after..() a step lower, that also makes the test
> work (see below).
>
> If you may look over quickly my analysis of why this smp_mb_after..() is
> needed, it is because what I marked as a and d below don't have an hb
> relation right?

I think a and d have an hb relation due to the
a ->po-rel X ->rfe Y ->acq-po d
edges (where X and Y are the unlock/lock events I annotated in your 
example below).

Generally, an mb_unlock_lock isn't used to give you hb, but to turn some 
(coe/fre) ; hb* edges into pb edges

In this case, that would probably be
f ->fre a ->hb* f   (where a ->hb* f comes from a ->hb* d ->hb e ->hb f)
By adding the mb_unlock_lock_po in one of the right places, this becomes 
f ->pb f,
thus forbidden.


Have fun,
jonas


>
> (*
>    b ->rf c
>
>    d ->co e
>
>    e ->hb f
>
>    basically the issue is a ->po b ->rf c ->po d    does not imply a ->hb d
> *)
>
> P0(int *x, int *y, spinlock_t *mylock)
> {
> 	spin_lock(mylock);
> 	WRITE_ONCE(*x, 1); // a
> 	WRITE_ONCE(*y, 1); // b
> 	spin_unlock(mylock); // X
> }
>
> P1(int *y, int *z, spinlock_t *mylock)
> {
> 	int r0;
>
> 	spin_lock(mylock); // Y
> 	r0 = READ_ONCE(*y); // c
> 	smp_mb__after_spinlock(); // moving this a bit lower also works fwiw.
> 	WRITE_ONCE(*z, 1);  // d
> 	spin_unlock(mylock);
> }
>
> P2(int *x, int *z)
> {
> 	int r1;
>
> 	WRITE_ONCE(*z, 2);  // e
> 	smp_mb();
> 	r1 = READ_ONCE(*x); // f
> }
>
> exists (1:r0=1 /\ z=2 /\ 2:r1=0)
>
>
>> Would someone like to to a "git mv" send the resulting patch?
> Yes I can do that in return as I am thankful in advance for the above
> discussion. ;)
>
> thanks,
>
>   - Joel
>