Re: [PATCH tip/core/rcu 1/9] rcu: Provide GP ordering in face of migrations and delays

[Peter Zijlstra]

On Thu, Oct 05, 2017 at 11:22:04AM -0700, Paul E. McKenney wrote:
> Hmmm...  Here is what I was worried about:
> 
> 	C C-PaulEMcKenney-W+RWC4+2017-10-05
> 
> 	{
> 	}
> 
> 	P0(int *a, int *x)
> 	{
> 		WRITE_ONCE(*a, 1);
> 		smp_mb(); /* Lock acquisition for rcu_node ->lock. */
> 		WRITE_ONCE(*x, 1);
> 	}
> 
> 	P1(int *x, int *y, spinlock_t *l)
> 	{
> 		r3 = READ_ONCE(*x);
> 		smp_mb(); /* Lock acquisition for rcu_node ->lock. */
> 		spin_lock(l); /* Locking in complete(). */
> 		WRITE_ONCE(*y, 1);
> 		spin_unlock(l);
> 	}
> 
> 	P2(int *y, int *b, spinlock_t *l)
> 	{
> 		spin_lock(l); /* Locking in wait_for_completion. */
> 		r4 = READ_ONCE(*y);
> 		spin_unlock(l);
> 		r1 = READ_ONCE(*b);
> 	}
> 
> 	P3(int *b, int *a)
> 	{
> 		WRITE_ONCE(*b, 1);
> 		smp_mb();
> 		r2 = READ_ONCE(*a);
> 	}
> 
> 	exists (1:r3=1 /\ 2:r4=1 /\ 2:r1=0 /\ 3:r2=0)


/me goes and install this herd thing again.. I'm sure I had it running
_somewhere_.. A well.


	C C-PaulEMcKenney-W+RWC4+2017-10-05

	{
	}

	P0(int *a, int *x)
	{
		WRITE_ONCE(*a, 1);
		smp_mb(); /* Lock acquisition for rcu_node ->lock. */
		WRITE_ONCE(*x, 1);
	}

	P1(int *x, int *y)
	{
		r3 = READ_ONCE(*x);
		smp_mb(); /* Lock acquisition for rcu_node ->lock. */
		smp_store_release(y, 1);
	}

	P2(int *y, int *b)
	{
		r4 = smp_load_acquire(y);
		r1 = READ_ONCE(*b);
	}

	P3(int *b, int *a)
	{
		WRITE_ONCE(*b, 1);
		smp_mb();
		r2 = READ_ONCE(*a);
	}

	exists (1:r3=1 /\ 2:r4=1 /\ 2:r1=0 /\ 3:r2=0)


Is what I was thinking of, I think that is the minimal ordering
complete()/wait_for_completion() need to provide.

(also, that r# numbering confuses the hell out of me, its not related to
P nor to the variables)

Test C-PaulEMcKenney-W+RWC4+2017-10-05 Allowed
States 15
1:r3=0; 2:r1=0; 2:r4=0; 3:r2=0;
1:r3=0; 2:r1=0; 2:r4=0; 3:r2=1;
1:r3=0; 2:r1=0; 2:r4=1; 3:r2=0;
1:r3=0; 2:r1=0; 2:r4=1; 3:r2=1;
1:r3=0; 2:r1=1; 2:r4=0; 3:r2=0;
1:r3=0; 2:r1=1; 2:r4=0; 3:r2=1;
1:r3=0; 2:r1=1; 2:r4=1; 3:r2=0;
1:r3=0; 2:r1=1; 2:r4=1; 3:r2=1;
1:r3=1; 2:r1=0; 2:r4=0; 3:r2=0;
1:r3=1; 2:r1=0; 2:r4=0; 3:r2=1;
1:r3=1; 2:r1=0; 2:r4=1; 3:r2=1;
1:r3=1; 2:r1=1; 2:r4=0; 3:r2=0;
1:r3=1; 2:r1=1; 2:r4=0; 3:r2=1;
1:r3=1; 2:r1=1; 2:r4=1; 3:r2=0;
1:r3=1; 2:r1=1; 2:r4=1; 3:r2=1;
No
Witnesses
Positive: 0 Negative: 15
Condition exists (1:r3=1 /\ 2:r4=1 /\ 2:r1=0 /\ 3:r2=0)
Observation C-PaulEMcKenney-W+RWC4+2017-10-05 Never 0 15
Time C-PaulEMcKenney-W+RWC4+2017-10-05 0.04
Hash=f7f8ad6eab33e90718a394bcb021557d