Received-SPF: pass (google.com: domain of linux-kernel+bounces-105485-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.199.223 as permitted sender) client-ip=147.75.199.223;
From: Alan Huang <mmpgouride@gmail.com>
Content-Type: text/plain;
	charset=utf-8
Content-Transfer-Encoding: quoted-printable
Precedence: bulk
Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3774.300.61.1.2\))
Subject: Question about ISA2+pooncelock+pooncelock+pombonce litmus
Message-Id: <12E5C279-ADB1-463E-83E2-0A4F5D193754@gmail.com>
Date: Mon, 18 Mar 2024 01:47:43 +0800
To: linux-kernel@vger.kernel.org,
 linux-arch@vger.kernel.org,
 rcu@vger.kernel.org

Hi,

I=E2=80=99m playing with the LKMM, then I saw the =
ISA2+pooncelock+pooncelock+pombonce.

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);
}

P1(int *y, int *z, spinlock_t *mylock)
{
	int r0;

	spin_lock(mylock);
	r0 =3D READ_ONCE(*y);
	WRITE_ONCE(*z, 1);
	spin_unlock(mylock);
}

P2(int *x, int *z)
{
	int r1;
	int r2;

	r2 =3D READ_ONCE(*z);
	smp_mb();
	r1 =3D READ_ONCE(*x);
}

exists (1:r0=3D1 /\ 2:r2=3D1 /\ 2:r1=3D0)
------------------------------------------------------
Of course, the result is Never.=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);
}

P1(int *y, int *z, spinlock_t *mylock)
{
	int r0;

	spin_lock(mylock);
	r0 =3D READ_ONCE(*y);
	WRITE_ONCE(*z, 1);
}

P2(int *x, int *z)
{
	int r1;
	int r2;

	r2 =3D READ_ONCE(*z);
	smp_mb();
	r1 =3D READ_ONCE(*x);
}

exists (1:r0=3D1 /\ 2:r2=3D1 /\ 2:r1=3D0)
------------------------------------------------------
Then herd told me the result is Sometimes.

Is this expected?=20