lkml.org 
[lkml]   [2020]   [May]   [25]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
From
Date
SubjectRe: Some -serious- BPF-related litmus tests
On Sun, May 24, 2020 at 5:09 AM Akira Yokosawa <akiyks@gmail.com> wrote:
>
> On Fri, 22 May 2020 12:38:21 -0700, Andrii Nakryiko wrote:
> > On 5/22/20 10:43 AM, Paul E. McKenney wrote:
> >> On Fri, May 22, 2020 at 10:32:01AM -0400, Alan Stern wrote:
> >>> On Fri, May 22, 2020 at 11:44:07AM +0200, Peter Zijlstra wrote:
> >>>> On Thu, May 21, 2020 at 05:38:50PM -0700, Paul E. McKenney wrote:
> >>>>> Hello!
> >>>>>
> >>>>> Just wanted to call your attention to some pretty cool and pretty serious
> >>>>> litmus tests that Andrii did as part of his BPF ring-buffer work:
> >>>>>
> >>>>> https://lore.kernel.org/bpf/20200517195727.279322-3-andriin@fb.com/
> >>>>>
> >>>>> Thoughts?
> >>>>
> >>>> I find:
> >>>>
> >>>> smp_wmb()
> >>>> smp_store_release()
> >>>>
> >>>> a _very_ weird construct. What is that supposed to even do?
> >>>
> >>> Indeed, it looks like one or the other of those is redundant (depending
> >>> on the context).
> >>
> >> Probably. Peter instead asked what it was supposed to even do. ;-)
> >
> > I agree, I think smp_wmb() is redundant here. Can't remember why I thought that it's necessary, this algorithm went through a bunch of iterations, starting as completely lockless, also using READ_ONCE/WRITE_ONCE at some point, and settling on smp_read_acquire/smp_store_release, eventually. Maybe there was some reason, but might be that I was just over-cautious. See reply on patch thread as well ([0]).
> >
> > [0] https://lore.kernel.org/bpf/CAEf4Bza26AbRMtWcoD5+TFhnmnU6p5YJ8zO+SoAJCDtp1jVhcQ@mail.gmail.com/
> >
> >
> >>
> >>> Also, what use is a spinlock that is accessed in only one thread?
> >>
> >> Multiple writers synchronize via the spinlock in this case. I am
> >> guessing that his larger 16-hour test contended this spinlock.
> >
> > Yes, spinlock is for coordinating multiple producers. 2p1c cases (bounded and unbounded) rely on this already. 1p1c cases are sort of subsets (but very fast to verify) checking only consumer/producer interaction.
> >
> >>
> >>> Finally, I doubt that these tests belong under tools/memory-model.
> >>> Shouldn't they go under the new Documentation/ directory for litmus
> >>> tests? And shouldn't the patch update a README file?
> >>
> >> Agreed, and I responded to that effect to his original patch:
> >>
> >> https://lore.kernel.org/bpf/20200522003433.GG2869@paulmck-ThinkPad-P72/
> >
> > Yep, makes sense, I'll will move.
>
> Hi Andrii,
>
> Andrea reported off-the-list that your litmus tests are incompatible
> with the to-be-released version 7.56 of herd7 and currently available
> versions of klitmus7.
>
> This is due to a couple of C-language level issues.
>
> herd7 used to be fairly generous in parsing C litmus tests.
> On the other hand, klitmus7 converts a litmus test into a
> kernel module. The converted code is built by an actual C compiler
> with kernel headers included, and can fail to build due to syntax errors
> or serious warnings.
> herd7 HEAD is getting slightly stricter on uninitialized variable and
> it emits an error to mpsc-rb+1p1c+bounded.litmus:
>
> Warning: File "mpsc-rb+1p1c+bounded.litmus": read on location 0 does not match any write
>
> Converted code by klitmus7 fails to build with the following warning messages:
>
> $ make
> make -C /lib/modules/5.3.0-53-generic/build/ M=/home/akira/bpf-rb/klitmus modules
> make[1]: Entering directory '/usr/src/linux-headers-5.3.0-53-generic'
> CC [M] /home/akira/bpf-rb/klitmus/litmus000.o
> /home/akira/bpf-rb/klitmus/litmus000.c: In function ‘code1’:
> /home/akira/bpf-rb/klitmus/litmus000.c:426:14: error: passing argument 1 of ‘atomic_inc’
> from incompatible pointer type [-Werror=incompatible-pointer-types]
> atomic_inc(dropped);
> ^~~~~~~
> In file included from ./arch/x86/include/asm/atomic.h:265:0,
> from ./arch/x86/include/asm/msr.h:67,
> from ./arch/x86/include/asm/processor.h:21,
> from ./arch/x86/include/asm/cpufeature.h:5,
> from ./arch/x86/include/asm/thread_info.h:53,
> from ./include/linux/thread_info.h:38,
> from ./arch/x86/include/asm/preempt.h:7,
> from ./include/linux/preempt.h:78,
> from ./include/linux/spinlock.h:51,
> from ./include/linux/seqlock.h:36,
> from ./include/linux/time.h:6,
> from ./include/linux/stat.h:19,
> from ./include/linux/module.h:10,
> from /home/akira/bpf-rb/klitmus/litmus000.c:11:
> ./include/asm-generic/atomic-instrumented.h:237:1: note: expected ‘atomic_t * {aka struct <anonymous> *}’ but argument is of type ‘int *’
> atomic_inc(atomic_t *v)
> ^~~~~~~~~~
> In file included from ./include/linux/export.h:45:0,
> from ./include/linux/linkage.h:7,
> from ./include/linux/kernel.h:8,
> from ./include/linux/list.h:9,
> from ./include/linux/module.h:9,
> from /home/akira/bpf-rb/klitmus/litmus000.c:11:
> /home/akira/bpf-rb/klitmus/litmus000.c: In function ‘thread0’:
> ./include/linux/compiler.h:187:26: warning: ‘rLenPtr’ may be used uninitialized in this function [-Wmaybe-uninitialized]
> case 4: *(__u32 *)res = *(volatile __u32 *)p; break; \
> ^
> /home/akira/bpf-rb/klitmus/litmus000.c:365:7: note: ‘rLenPtr’ was declared here
> int *rLenPtr;
> ^~~~~~~
> In file included from ./include/linux/export.h:45:0,
> from ./include/linux/linkage.h:7,
> from ./include/linux/kernel.h:8,
> from ./include/linux/list.h:9,
> from ./include/linux/module.h:9,
> from /home/akira/bpf-rb/klitmus/litmus000.c:11:
> /home/akira/bpf-rb/klitmus/litmus000.c: In function ‘thread1’:
> ./include/linux/compiler.h:225:31: warning: ‘rLenPtr’ may be used uninitialized in this function [-Wmaybe-uninitialized]
> case 4: *(volatile __u32 *)p = *(__u32 *)res; break;
> ~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~
> /home/akira/bpf-rb/klitmus/litmus000.c:417:7: note: ‘rLenPtr’ was declared here
> int *rLenPtr;
> ^~~~~~~
> cc1: some warnings being treated as errors
> scripts/Makefile.build:288: recipe for target '/home/akira/bpf-rb/klitmus/litmus000.o' failed
> make[2]: *** [/home/akira/bpf-rb/klitmus/litmus000.o] Error 1
> Makefile:1656: recipe for target '_module_/home/akira/bpf-rb/klitmus' failed
> make[1]: *** [_module_/home/akira/bpf-rb/klitmus] Error 2
> make[1]: Leaving directory '/usr/src/linux-headers-5.3.0-53-generic'
> Makefile:8: recipe for target 'all' failed
> make: *** [all] Error 2
>
> Appended below is a patch I applied to mpsc-rb+1p1c+bounded.litmus to make
> herd7 HEAD and klitmus7 happy. (Give or take the redundant memory barrier.)
>
> The other variants need similar changes.

Ok, cool, thanks for letting me know. I'll see if I can upgrade
everything and test on my side (if you have a pointer to instructions
how to use klitmus7, that would be greatly appreaciated!)

>
> What I did here are:
>
> - Remove unnecessary initialization (shared variables are 0 by default)
> - Declare "dropped" as atomic_t

These two look good.

> - Promote rLenPtr to a shared variable LenPtr

This one might work for single producer litmus tests, but it's wrong
for 2- and 3-producer cases, because it has to be local to producer.
But I think I can work around unitialized read warning by assigning it
to 0 in failure case.

>
> Please note that if you are on Linux 5.6 (or later), you need an up-to-date
> klitmus7 due to a change in kernel API.
>
> Any question is welcome!
>
> Thanks, Akira
>
> -----------------------
> diff --git a/mpsc-rb+1p1c+bounded.litmus b/mpsc-rb+1p1c+bounded.litmus
> index cafd17a..5af43c1 100644
> --- a/mpsc-rb+1p1c+bounded.litmus
> +++ b/mpsc-rb+1p1c+bounded.litmus
> @@ -17,15 +17,11 @@ C mpsc-rb+1p1c+bounded
>
> {
> max_len = 1;
> - len1 = 0;
> - px = 0;
> - cx = 0;
> - dropped = 0;
> + atomic_t dropped;
> }
>
> -P0(int *len1, int *cx, int *px)
> +P0(int *len1, int *cx, int *px, int *LenPtr)
> {
> - int *rLenPtr;
> int rLen;
> int rPx;
> int rCx;
> @@ -37,11 +33,11 @@ P0(int *len1, int *cx, int *px)
> rPx = smp_load_acquire(px);
> if (rCx < rPx) {
> if (rCx == 0)
> - rLenPtr = len1;
> + LenPtr = len1;
> else
> rFail = 1;
>
> - rLen = smp_load_acquire(rLenPtr);
> + rLen = smp_load_acquire(LenPtr);
> if (rLen == 0) {
> rFail = 1;
> } else if (rLen == 1) {
> @@ -51,12 +47,11 @@ P0(int *len1, int *cx, int *px)
> }
> }
>
> -P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len)
> +P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, atomic_t *dropped, int *max_len, int *LenPtr)
> {
> int rPx;
> int rCx;
> int rFail;
> - int *rLenPtr;
>
> rFail = 0;
> rCx = smp_load_acquire(cx);
> @@ -69,17 +64,17 @@ P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len)
> spin_unlock(rb_lock);
> } else {
> if (rPx == 0)
> - rLenPtr = len1;
> + LenPtr = len1;
> else
> rFail = 1;
>
> - *rLenPtr = -1;
> + *LenPtr = -1;
> smp_wmb();
> smp_store_release(px, rPx + 1);
>
> spin_unlock(rb_lock);
>
> - smp_store_release(rLenPtr, 1);
> + smp_store_release(LenPtr, 1);
> }
> }
>
> ----------------
>

\
 
 \ /
  Last update: 2020-05-25 20:32    [W:0.188 / U:1.804 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site