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-andr...@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+soajcdtp1jv...@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.
What I did here are:
- Remove unnecessary initialization (shared variables are 0 by default)
- Declare "dropped" as atomic_t
- Promote rLenPtr to a shared variable LenPtr
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);
}
}
----------------
