From mboxrd@z Thu Jan 1 00:00:00 1970 From: Akira Yokosawa Subject: Re: Some -serious- BPF-related litmus tests Date: Tue, 26 May 2020 07:01:35 +0900 Message-ID: <69ed3604-4275-d73e-a5d6-2b70dd877104@gmail.com> References: <20200522003850.GA32698@paulmck-ThinkPad-P72> <20200522094407.GK325280@hirez.programming.kicks-ass.net> <20200522143201.GB32434@rowland.harvard.edu> <20200522174352.GJ2869@paulmck-ThinkPad-P72> <006e2bc6-7516-1584-3d8c-e253211c157e@fb.com> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Return-path: Received: from lindbergh.monkeyblade.net ([23.128.96.19]:33678 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1726937AbgEYWBm (ORCPT ); Mon, 25 May 2020 18:01:42 -0400 In-Reply-To: Content-Language: en-US Sender: linux-arch-owner@vger.kernel.org List-ID: To: Andrii Nakryiko Cc: Andrii Nakryiko , "Paul E . McKenney" , Alan Stern , Peter Zijlstra , parri.andrea@gmail.com, will@kernel.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, dlustig@nvidia.com, Joel Fernandes , open list , linux-arch@vger.kernel.org, Akira Yokosawa On Mon, 25 May 2020 11:31:27 -0700, Andrii Nakryiko wrote: > On Sun, May 24, 2020 at 5:09 AM Akira Yokosawa 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.co= m/ >>>>>>> >>>>>>> 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 (depen= ding >>>>> 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 th= ought that it's necessary, this algorithm went through a bunch of iterati= ons, starting as completely lockless, also using READ_ONCE/WRITE_ONCE at = some point, and settling on smp_read_acquire/smp_store_release, eventuall= y. Maybe there was some reason, but might be that I was just over-cautiou= s. See reply on patch thread as well ([0]). >>> >>> [0] https://lore.kernel.org/bpf/CAEf4Bza26AbRMtWcoD5+TFhnmnU6p5YJ8z= O+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 (bou= nded 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-P= 72/ >>> >>> 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 erro= rs >> 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 n= ot match any write >> >> Converted code by klitmus7 fails to build with the following warning m= essages: >> >> $ make >> make -C /lib/modules/5.3.0-53-generic/build/ M=3D/home/akira/bpf-rb/kl= itmus 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 =E2=80=98code1=E2=80= =99: >> /home/akira/bpf-rb/klitmus/litmus000.c:426:14: error: passing argument= 1 of =E2=80=98atomic_inc=E2=80=99 >> from incompatible pointer type [-Werror=3Dincompatible-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 =E2=80= =98atomic_t * {aka struct *}=E2=80=99 but argument is of type= =E2=80=98int *=E2=80=99 >> 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 =E2=80=98thread0=E2= =80=99: >> ./include/linux/compiler.h:187:26: warning: =E2=80=98rLenPtr=E2=80=99 = may be used uninitialized in this function [-Wmaybe-uninitialized] >> case 4: *(__u32 *)res =3D *(volatile __u32 *)p; break; \ >> ^ >> /home/akira/bpf-rb/klitmus/litmus000.c:365:7: note: =E2=80=98rLenPtr=E2= =80=99 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 =E2=80=98thread1=E2= =80=99: >> ./include/linux/compiler.h:225:31: warning: =E2=80=98rLenPtr=E2=80=99 = may be used uninitialized in this function [-Wmaybe-uninitialized] >> case 4: *(volatile __u32 *)p =3D *(__u32 *)res; break; >> ~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~ >> /home/akira/bpf-rb/klitmus/litmus000.c:417:7: note: =E2=80=98rLenPtr=E2= =80=99 was declared here >> int *rLenPtr; >> ^~~~~~~ >> cc1: some warnings being treated as errors >> scripts/Makefile.build:288: recipe for target '/home/akira/bpf-rb/klit= mus/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 barr= ier.) >> >> The other variants need similar changes. >=20 > 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!) >=20 >> >> What I did here are: >> >> - Remove unnecessary initialization (shared variables are 0 by def= ault) >> - Declare "dropped" as atomic_t >=20 > These two look good. >=20 >> - Promote rLenPtr to a shared variable LenPtr >=20 > 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. Ah, I knew I had missed something... > But I think I can work around unitialized read warning by assigning it > to 0 in failure case. Yes, that should work. You can find a basic introduction of klitmus7 in tools/memory-model/READM= E. Thanks, Akira >=20 >> >> 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 =3D 1; >> - len1 =3D 0; >> - px =3D 0; >> - cx =3D 0; >> - dropped =3D 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 =3D smp_load_acquire(px); >> if (rCx < rPx) { >> if (rCx =3D=3D 0) >> - rLenPtr =3D len1; >> + LenPtr =3D len1; >> else >> rFail =3D 1; >> >> - rLen =3D smp_load_acquire(rLenPtr); >> + rLen =3D smp_load_acquire(LenPtr); >> if (rLen =3D=3D 0) { >> rFail =3D 1; >> } else if (rLen =3D=3D 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, in= t *max_len) >> +P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, atomic_t *droppe= d, int *max_len, int *LenPtr) >> { >> int rPx; >> int rCx; >> int rFail; >> - int *rLenPtr; >> >> rFail =3D 0; >> rCx =3D smp_load_acquire(cx); >> @@ -69,17 +64,17 @@ P1(int *len1, spinlock_t *rb_lock, int *px, int *c= x, int *dropped, int *max_len) >> spin_unlock(rb_lock); >> } else { >> if (rPx =3D=3D 0) >> - rLenPtr =3D len1; >> + LenPtr =3D len1; >> else >> rFail =3D 1; >> >> - *rLenPtr =3D -1; >> + *LenPtr =3D -1; >> smp_wmb(); >> smp_store_release(px, rPx + 1); >> >> spin_unlock(rb_lock); >> >> - smp_store_release(rLenPtr, 1); >> + smp_store_release(LenPtr, 1); >> } >> } >> >> ---------------- >>