lkml.org 
[lkml]   [2019]   [Mar]   [28]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH] Convert struct pid count to refcount_t
On Thu, Mar 28, 2019 at 05:26:42PM +0100, Oleg Nesterov wrote:
> On 03/28, Jann Horn wrote:
> >
> > Since we're just talking about RCU stuff now, adding Paul McKenney to
> > the thread.
>
> Since you added Paul let me add more confusion to this thread ;)

Woo-hoo!!! More confusion! Bring it on!!! ;-)

> There were some concerns about the lack of barriers in put_pid(), but I can't
> find that old discussion and I forgot the result of that discussion...
>
> Paul, could you confirm that this code
>
> CPU_0 CPU_1
>
> X = 1; if (READ_ONCE(Y))
> mb(); X = 2;
> Y = 1; BUG_ON(X != 2);
>
>
> is correct? I think it is, control dependency pairs with mb(), right?

The BUG_ON() is supposed to happen at the end of time, correct?
As written, there is (in the strict sense) a data race between the load
of X in the BUG_ON() and CPU_0's store to X. In a less strict sense,
you could of course argue that this data race is harmless, especially
if X is a single byte. But the more I talk to compiler writers, the
less comfortable I become with data races in general. :-/

So I would also feel better if the "Y = 1" was WRITE_ONCE().

On the other hand, this is a great opportunity to try out Alan Stern's
prototype plain-accesses patch to the Linux Kernel Memory Model (LKMM)!

https://lkml.kernel.org/r/Pine.LNX.4.44L0.1903191459270.1593-200000@iolanthe.rowland.org

Also adding Alan on CC.

Here is what I believe is the litmus test that your are interested in:

------------------------------------------------------------------------
C OlegNesterov-put_pid

{}

P0(int *x, int *y)
{
*x = 1;
smp_mb();
*y = 1;
}

P1(int *x, int *y)
{
int r1;

r1 = READ_ONCE(*y);
if (r1)
*x = 2;
}

exists (1:r1=1 /\ ~x=2)
------------------------------------------------------------------------

Running this through herd with Alan's patch detects the data race
and says that the undesired outcome is allowed:

$ herd7 -conf linux-kernel.cfg /tmp/OlegNesterov-put_pid.litmus
Test OlegNesterov-put_pid Allowed
States 3
1:r1=0; x=1;
1:r1=1; x=1;
1:r1=1; x=2;
Ok
Witnesses
Positive: 1 Negative: 2
Flag data-race
Condition exists (1:r1=1 /\ not (x=2))
Observation OlegNesterov-put_pid Sometimes 1 2
Time OlegNesterov-put_pid 0.00
Hash=a3e0043ad753effa860fea37eeba0a76

Using WRITE_ONCE() for P0()'s store to y still allows this outcome,
although it does remove the "Flag data-race".

Using WRITE_ONCE() for both P0()'s store to y and P1()'s store to x
gets rid of both the "Flag data-race" and the undesired outcome:

$ herd7 -conf linux-kernel.cfg /tmp/OlegNesterov-put_pid-WO-WO.litmus
Test OlegNesterov-put_pid-WO-WO Allowed
States 2
1:r1=0; x=1;
1:r1=1; x=2;
No
Witnesses
Positive: 0 Negative: 2
Condition exists (1:r1=1 /\ not (x=2))
Observation OlegNesterov-put_pid-WO-WO Never 0 2
Time OlegNesterov-put_pid-WO-WO 0.01
Hash=6e1643e3c5e4739b590bde0a8e8a918e

Here is the corresponding litmus test, in case I messed something up:

------------------------------------------------------------------------
C OlegNesterov-put_pid-WO-WO

{}

P0(int *x, int *y)
{
*x = 1;
smp_mb();
WRITE_ONCE(*y, 1);
}

P1(int *x, int *y)
{
int r1;

r1 = READ_ONCE(*y);
if (r1)
WRITE_ONCE(*x, 2);
}

exists (1:r1=1 /\ ~x=2)
------------------------------------------------------------------------

> If not, then put_pid() needs atomic_read_acquire() as it was proposed in that
> discussion.

Good point, let's try with smp_load_acquire() in P1():

$ herd7 -conf linux-kernel.cfg /tmp/OlegNesterov-put_pid-WO-sla.litmus
Test OlegNesterov-put_pid-WO-sla Allowed
States 2
1:r1=0; x=1;
1:r1=1; x=2;
No
Witnesses
Positive: 0 Negative: 2
Condition exists (1:r1=1 /\ not (x=2))
Observation OlegNesterov-put_pid-WO-sla Never 0 2
Time OlegNesterov-put_pid-WO-sla 0.01
Hash=4fb0276eabf924793dec1970199db3a6

This also works. Here is the litmus test:

------------------------------------------------------------------------
C OlegNesterov-put_pid-WO-sla

{}

P0(int *x, int *y)
{
*x = 1;
smp_mb();
WRITE_ONCE(*y, 1);
}

P1(int *x, int *y)
{
int r1;

r1 = smp_load_acquire(y);
if (r1)
*x = 2;
}

exists (1:r1=1 /\ ~x=2)
------------------------------------------------------------------------

Demoting P0()'s WRITE_ONCE() to a plain write while leaving P1()'s
smp_load_acquire() gets us a data race and allows the undesired
outcome:

$ herd7 -conf linux-kernel.cfg /tmp/OlegNesterov-put_pid-sla.litmus
Test OlegNesterov-put_pid-sla Allowed
States 3
1:r1=0; x=1;
1:r1=1; x=1;
1:r1=1; x=2;
Ok
Witnesses
Positive: 1 Negative: 2
Flag data-race
Condition exists (1:r1=1 /\ not (x=2))
Observation OlegNesterov-put_pid-sla Sometimes 1 2
Time OlegNesterov-put_pid-sla 0.01
Hash=ec6f71f3d9f7cd6e45a874c872e3d946

But what if you are certain that the compiler cannot mess up your use
of plain C-language loads and stores? Then simply tell LKMM that they
are READ_ONCE() and WRITE_ONCE(), respectively. LKMM is admittedly
somewhat paranoid, but real C compilers really do tear stores of certain
constants on systems (like x86) that have store-immediate instructions,
so a bit of paranoia is not misplaced here. ;-)

Plus please note that this patch to LKMM is prototype and thus subject
to change.

Thanx, Paul

\
 
 \ /
  Last update: 2019-03-28 18:39    [W:0.096 / U:0.888 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site