Received-SPF: pass (google.com: domain of linux-kernel+bounces-106059-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:40f1:3f00::1 as permitted sender) client-ip=2604:1380:40f1:3f00::1;
Content-Type: text/plain;
	charset=utf-8
Precedence: bulk
Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3774.300.61.1.2\))
Subject: Re: Question about ISA2+pooncelock+pooncelock+pombonce litmus
From: Alan Huang <mmpgouride@gmail.com>
In-Reply-To: <17ddc858-a926-4f12-beda-3f54cb91bfbb@paulmck-laptop>
Date: Mon, 18 Mar 2024 19:19:56 +0800
Cc: linux-kernel@vger.kernel.org,
 linux-arch@vger.kernel.org,
 rcu@vger.kernel.org
Content-Transfer-Encoding: quoted-printable
Message-Id: <E73E4593-DFA7-4A46-924C-3867CC0B4807@gmail.com>
References: <12E5C279-ADB1-463E-83E2-0A4F5D193754@gmail.com>
 <17ddc858-a926-4f12-beda-3f54cb91bfbb@paulmck-laptop>
To: "Paul E . McKenney" <paulmck@kernel.org>


> 2024=E5=B9=B43=E6=9C=8818=E6=97=A5 07:02=EF=BC=8CPaul E. McKenney =
<paulmck@kernel.org> wrote=EF=BC=9A
>=20
> On Mon, Mar 18, 2024 at 01:47:43AM +0800, Alan Huang wrote:
>> Hi,
>>=20
>> I=E2=80=99m playing with the LKMM, then I saw the =
ISA2+pooncelock+pooncelock+pombonce.
>>=20
>> The original litmus is as follows:
>> ------------------------------------------------------
>> P0(int *x, int *y, spinlock_t *mylock)
>> {
>> spin_lock(mylock);
>> WRITE_ONCE(*x, 1);
>> WRITE_ONCE(*y, 1);
>> spin_unlock(mylock);
>> }
>>=20
>> P1(int *y, int *z, spinlock_t *mylock)
>> {
>> int r0;
>>=20
>> spin_lock(mylock);
>> r0 =3D READ_ONCE(*y);
>> WRITE_ONCE(*z, 1);
>> spin_unlock(mylock);
>> }
>>=20
>> P2(int *x, int *z)
>> {
>> int r1;
>> int r2;
>>=20
>> r2 =3D READ_ONCE(*z);
>> smp_mb();
>> r1 =3D READ_ONCE(*x);
>> }
>>=20
>> exists (1:r0=3D1 /\ 2:r2=3D1 /\ 2:r1=3D0)
>> ------------------------------------------------------
>> Of course, the result is Never.=20
>>=20
>> But when I delete P0=E2=80=99s spin_lock and P1=E2=80=99s =
spin_unlock:
>> -------------------------------------------------------
>> P0(int *x, int *y, spinlock_t *mylock)
>> {
>> WRITE_ONCE(*x, 1);
>> WRITE_ONCE(*y, 1);
>> spin_unlock(mylock);
>> }
>>=20
>> P1(int *y, int *z, spinlock_t *mylock)
>> {
>> int r0;
>>=20
>> spin_lock(mylock);
>> r0 =3D READ_ONCE(*y);
>> WRITE_ONCE(*z, 1);
>> }
>>=20
>> P2(int *x, int *z)
>> {
>> int r1;
>> int r2;
>>=20
>> r2 =3D READ_ONCE(*z);
>> smp_mb();
>> r1 =3D READ_ONCE(*x);
>> }
>>=20
>> exists (1:r0=3D1 /\ 2:r2=3D1 /\ 2:r1=3D0)
>> ------------------------------------------------------
>> Then herd told me the result is Sometimes.
>=20
> You mean like this?
>=20
> Test ISA2+pooncelock+pooncelock+pombonce Allowed
> States 8
> 1:r0=3D0; 2:r1=3D0; 2:r2=3D0;
> 1:r0=3D0; 2:r1=3D0; 2:r2=3D1;
> 1:r0=3D0; 2:r1=3D1; 2:r2=3D0;
> 1:r0=3D0; 2:r1=3D1; 2:r2=3D1;
> 1:r0=3D1; 2:r1=3D0; 2:r2=3D0;
> 1:r0=3D1; 2:r1=3D0; 2:r2=3D1;
> 1:r0=3D1; 2:r1=3D1; 2:r2=3D0;
> 1:r0=3D1; 2:r1=3D1; 2:r2=3D1;
> Ok
> Witnesses
> Positive: 1 Negative: 7
> Flag unmatched-unlock
> Condition exists (1:r0=3D1 /\ 2:r2=3D1 /\ 2:r1=3D0)
> Observation ISA2+pooncelock+pooncelock+pombonce Sometimes 1 7
> Time ISA2+pooncelock+pooncelock+pombonce 0.01
> Hash=3Df55b8515e48310f812aa676084f2cc88
>=20
>> Is this expected?=20
>=20
> There are no locks held initially, so why can't the following
> sequence of events unfold:
>=20
> o P1() acquires the lock.
>=20
> o P0() does WRITE_ONCE(*y, 1). (Yes, out of order)
>=20
> o P1() does READ_ONCE(*y), and gets 1.
>=20
> o P1() does WRITE_ONCE(*z, 1).
>=20
> o P2() does READ_ONCE(*z) and gets 1.
>=20
> o P2() does smp_mb(), but there is nothing to order with.
>=20
> o P2() does READ_ONCE(*x) and gets 0.
>=20
> o P0() does WRITE_ONCE(*x, 1), but too late to affect P2().
>=20
> o P0() releases the lock that is does not hold, which is why you see
> the "Flag unmatched-unlock" in the output.  LKMM is complaining
> that the litmus test is not legitimate, and rightly so!


Oh! I missed that line, Thank you for pointing this out! :)

>=20
> Or am I missing your point?
>=20
> Thanx, Paul