Re: LKMM/RCU UNLOCK+LOCK pair Semantics Inquiry

[Andrea Parri]

(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