Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote:

On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote:

quoted

Hi!

Firstly; The long Cc-list is to reach the LKMM-folks.

Some background; the XDP sockets use a ring-buffer to communicate
between the kernel and userland. It's a
single-consumer/single-producer ring, and described in
net/xdp/xsk_queue.h.

--8<---
/* The structure of the shared state of the rings are the same as the
 * ring buffer in kernel/events/ring_buffer.c. For the Rx and completion
 * ring, the kernel is the producer and user space is the consumer. For
 * the Tx and fill rings, the kernel is the consumer and user space is
 * the producer.
 *
 * producer                         consumer
 *
 * if (LOAD ->consumer) {           LOAD ->producer
 *                    (A)           smp_rmb()       (C)
 *    STORE $data                   LOAD $data
 *    smp_wmb()       (B)           smp_mb()        (D)
 *    STORE ->producer              STORE ->consumer
 * }
 *
 * (A) pairs with (D), and (B) pairs with (C).
...
-->8---

I'd like to replace the smp_{r,w,}mb() barriers with acquire-release
semantics [1], without breaking existing userspace applications.

So, I figured I'd use herd7 and the LKMM model to build a litmus test
for the barrier version, then for the acquire-release version, and
finally permutations of both.

The idea is to use a one element ring, with a state machine outlined
in the litmus test.

The basic test for the existing smp_{r,w,}mb() barriers looks like:

$ cat spsc-rb+1p1c.litmus
C spsc-rb+1p1c

// Stupid one entry ring:
// prod cons     allowed action       prod cons
//    0    0 =>       prod          =>   1    0
//    0    1 =>       cons          =>   0    0
//    1    0 =>       cons          =>   1    1
//    1    1 =>       prod          =>   0    1

{ prod = 1; }

// Here, we start at prod==1,cons==0, data==0, i.e. producer has
// written data=0, so from here only the consumer can start, and should
// consume data==0. Afterwards, producer can continue and write 1 to
// data. Can we enter state prod==0, cons==1, but consumer observerd
// the write of 1?

P0(int *prod, int *cons, int *data)
{
    int p;
    int c;
    int cond = 0;

    p = READ_ONCE(*prod);
    c = READ_ONCE(*cons);
    if (p == 0)
        if (c == 0)
            cond = 1;
    if (p == 1)
        if (c == 1)
            cond = 1;

    if (cond) {
        smp_mb();
        WRITE_ONCE(*data, 1);
        smp_wmb();
        WRITE_ONCE(*prod, p ^ 1);
    }
}

P1(int *prod, int *cons, int *data)
{
    int p;
    int c;
    int d = -1;
    int cond = 0;

    p = READ_ONCE(*prod);
    c = READ_ONCE(*cons);
    if (p == 1)
        if (c == 0)
            cond = 1;
    if (p == 0)
        if (c == 1)
            cond = 1;

    if (cond == 1) {
        smp_rmb();
        d = READ_ONCE(*data);
        smp_mb();
        WRITE_ONCE(*cons, c ^ 1);
    }
}

exists( 1:d=1 /\ prod=0 /\ cons=1 );

--

The weird state changing if-statements is because that I didn't get
'&&' and '||' to work with herd.

When this is run:

$ herd7 -conf linux-kernel.cfg litmus-tests/spsc-rb+1p1c.litmus
Test spsc-rb+1p1c Allowed
States 2
1:d=0; cons=1; prod=0;
1:d=0; cons=1; prod=1;
No
Witnesses
Positive: 0 Negative: 2
Condition exists (1:d=1 /\ prod=0 /\ cons=1)
Observation spsc-rb+1p1c Never 0 2
Time spsc-rb+1p1c 0.04
Hash=b399756d6a1301ca5bda042f32130791

Now to my question; In P0 there's an smp_mb(). Without that, the d==1
can be observed from P1 (consumer):

$ herd7 -conf linux-kernel.cfg litmus-tests/spsc-rb+1p1c.litmus
Test spsc-rb+1p1c Allowed
States 3
1:d=0; cons=1; prod=0;
1:d=0; cons=1; prod=1;
1:d=1; cons=1; prod=0;
Ok
Witnesses
Positive: 1 Negative: 2
Condition exists (1:d=1 /\ prod=0 /\ cons=1)
Observation spsc-rb+1p1c Sometimes 1 2
Time spsc-rb+1p1c 0.04
Hash=0047fc21fa77da9a9aee15e35ec367ef

This result is wrong, apparently because of a bug in herd7.  There 
should be control dependencies from each of the two loads in P0 to each 
of the two stores, but herd7 doesn't detect them.

Maybe Luc can find some time to check whether this really is a bug and 
if it is, fix it.

I agree that herd7's control dependency tracking could be improved.

But sadly, it is currently doing exactly what I asked Luc to make it do,
which is to confine the control dependency to its "if" statement.  But as
usual I wasn't thinking globally enough.  And I am not exactly sure what
to ask for.  Here a store to a local was control-dependency ordered after
a read, and so that should propagate to a read from that local variable.
Maybe treat local variables as if they were registers, so that from
herd7's viewpoint the READ_ONCE()s are able to head control-dependency
chains in multiple "if" statements?

Thoughts?

							Thanx, Paul

quoted

In commit c7f2e3cd6c1f ("perf: Optimize ring-buffer write by depending
on control dependencies") removes the corresponding smp_mb(), and also
the circular buffer in circular-buffers.txt (pre commit 6c43c091bdc5
("documentation: Update circular buffer for
load-acquire/store-release")) is missing the smp_mb() at the
producer-side.

I'm trying to wrap my head around why it's OK to remove the smp_mb()
in the cases above? I'm worried that the current XDP socket ring
implementation (which is missing smp_mb()) might be broken.

Because of the control dependencies, the smp_mb isn't needed.  The 
dependencies will order both of the stores after both of the loads.

Alan Stern