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-200...@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
