Date:   Tue, 2 Mar 2021 16:14:46 -0500
From:   Alan Stern <stern@...land.harvard.edu>
To:     Björn Töpel <bjorn.topel@...il.com>
Cc:     bpf <bpf@...r.kernel.org>, LKML <linux-kernel@...r.kernel.org>,
        parri.andrea@...il.com, Will Deacon <will@...nel.org>,
        Peter Zijlstra <peterz@...radead.org>, boqun.feng@...il.com,
        npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
        luc.maranget@...ia.fr, paulmck@...nel.org, akiyks@...il.com,
        dlustig@...dia.com, joel@...lfernandes.org,
        Toke Høiland-Jørgensen <toke@...hat.com>,
        "Karlsson, Magnus" <magnus.karlsson@...el.com>
Subject: Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote:
> 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.

> 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

Powered by blists - more mailing lists