linux-kernel - Re: LKMM/RCU UNLOCK+LOCK pair Semantics Inquiry

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [day] [month] [year] [list]

Date: Tue, 20 Feb 2024 16:48:55 +0100
From: Andrea Parri <parri.andrea@...il.com>
To: "conrad.r.cole" <conrad.r.cole@...ton.me>
Cc: "paulmck@...ux.ibm.com" <paulmck@...ux.ibm.com>,
	"me@...coelver.com" <me@...coelver.com>,
	"boehm@....org" <boehm@....org>,
	"fpikus@...il.com" <fpikus@...il.com>,
	"mingo@...nel.org" <mingo@...nel.org>,
	"akiyks@...il.com" <akiyks@...il.com>,
	"stern@...land.harvard.edu" <stern@...land.harvard.edu>,
	linux-kernel@...r.kernel.org
Subject: Re: LKMM/RCU UNLOCK+LOCK pair Semantics Inquiry

(Dropping my long-dead @AS address and adding the Linux kernel mailing list)

> The example below seems a bit counterintuitive from my perspective. Why does the assert statement below not trigger when the memory barrier in thread 2 is included? How is it possible for Thread 2 to load a value of 0 for y, shouldn't the smp_mb__after_unlock_lock() act as a full memory barrier between the store to y by Thread 1 and the load by Thread 2?

[...]

>     Thread 1              Thread 2                        Thread 3
>     --------              --------                        --------
>     y = 1;                spin_lock(&l);                  x = 1;
>     spin_unlock(&l);      smp_mb__after_unlock_lock();    smp_mb();
>                           r1 = y;                         r3 = y;
>                           r2 = x;
>     
> 
>     assert(r1 == 0 || r2 != 0 || r3 != 0);

This test does not seem to be well-formed, due to the Unmatched lock operation;
you can check that by using the formal (upstream) LKMM:

$ cat conrad0.litmus
C conrad0

{}

P0(int *y, spinlock_t *l)
{
	WRITE_ONCE(*y, 1);
	spin_unlock(l);
}

P1(int *y, int *x, spinlock_t *l)
{
	int r1;
	int r2;

	spin_lock(l);
	smp_mb__after_unlock_lock();
	r1 = READ_ONCE(*y);
	r2 = READ_ONCE(*x);
}

P2(int *x, int *y)
{
	int r3;

	WRITE_ONCE(*x, 1);
	smp_mb();
	r3 = READ_ONCE(*y);
}

forall (1:r1=0 \/ ~1:r2=0 \/ ~2:r3=0)

$ herd7 -conf linux-kernel.cfg conrad0.litmus
Test conrad0 Required
States 8
1:r1=0; 1:r2=0; 2:r3=0;
1:r1=0; 1:r2=0; 2:r3=1;
1:r1=0; 1:r2=1; 2:r3=0;
1:r1=0; 1:r2=1; 2:r3=1;
1:r1=1; 1:r2=0; 2:r3=0;
1:r1=1; 1:r2=0; 2:r3=1;
1:r1=1; 1:r2=1; 2:r3=0;
1:r1=1; 1:r2=1; 2:r3=1;
No
Witnesses
Positive: 7 Negative: 1
Flag unmatched-unlock
Condition forall (1:r1=0 \/ not (1:r2=0) \/ not (2:r3=0))
Observation conrad0 Sometimes 7 1
Time conrad0 0.01
Hash=95ed1bbf05f8df26070ce4a3cc0968a3

(cf. the flag "unmatched-unlock" above).  Here is a well-formed variant of the
previous test together with the corresponding result:

$ cat conrad.litmus
C conrad

{}

P0(int *y, spinlock_t *l)
{
	spin_lock(l);
	WRITE_ONCE(*y, 1);
	spin_unlock(l);
}

P1(int *y, int *x, spinlock_t *l)
{
	int r1;
	int r2;

	spin_lock(l);
	smp_mb__after_unlock_lock();
	r1 = READ_ONCE(*y);
	r2 = READ_ONCE(*x);
	spin_unlock(l);
}

P2(int *x, int *y)
{
	int r3;

	WRITE_ONCE(*x, 1);
	smp_mb();
	r3 = READ_ONCE(*y);
}

forall (1:r1=0 \/ ~1:r2=0 \/ ~2:r3=0)

$ herd7 -conf linux-kernel.cfg conrad.litmus
Test conrad Required
States 7
1:r1=0; 1:r2=0; 2:r3=0;
1:r1=0; 1:r2=0; 2:r3=1;
1:r1=0; 1:r2=1; 2:r3=0;
1:r1=0; 1:r2=1; 2:r3=1;
1:r1=1; 1:r2=0; 2:r3=1;
1:r1=1; 1:r2=1; 2:r3=0;
1:r1=1; 1:r2=1; 2:r3=1;
Ok
Witnesses
Positive: 7 Negative: 0
Condition forall (1:r1=0 \/ not (1:r2=0) \/ not (2:r3=0))
Observation conrad Always 7 0
Time conrad 0.01
Hash=4611aa988bb39b8c0a27e0ed5f43044e

So the "assert" can indeed _not_ trigger (aka, fail) according to the model.  In
other words, the state "not (1:r1=0) /\ 1:r2=0 /\ 2:r3=0" is forbidden; such state
becomes allowed upon removal of the barrier (that "acts as a full barrier").

  Andrea