lkml.org 
[lkml]   [2017]   [Oct]   [6]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH tip/core/rcu 1/9] rcu: Provide GP ordering in face of migrations and delays
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

\
 
 \ /
  Last update: 2017-10-06 11:08    [W:0.079 / U:2.856 seconds]
©2003-2017 Jasper Spaans. hosted at Digital OceanAdvertise on this site