On Tue, 26 May 2020 13:15:49 -0700, Andrii Nakryiko wrote: > On Tue, May 26, 2020 at 3:50 AM Akira Yokosawa <akiyks@xxxxxxxxx> wrote: >> >> On Mon, 25 May 2020 16:31:05 -0700, Andrii Nakryiko wrote: >>> On Mon, May 25, 2020 at 3:01 PM Akira Yokosawa <akiyks@xxxxxxxxx> wrote: >>>> >> [...] >>>> Yes, that should work. >>> >>> Ok, assigning to zero didn't work (it still complained about >>> uninitialized read), but using a separate int *lenFail to assign to >>> rLenPtr worked. Curiously, if I used rLenPtr = len1; in error case, it >>> actually takes a bit more time to verify. >>> >>> So I've converted everything else as you suggested. I compiled latest >>> herd7 and it doesn't produce any warnings. But it's also extremely >>> slow, compared to the herd7 that I get by default. Validating simple >>> 1p1c cases takes about 2.5x times longer (0.03s vs 0.07), but trying >>> to validate 2p1c case, which normally validates in 42s (unbounded) and >>> 110s (bounded), it took more than 20 minutes and hasn't finished, >>> before I gave up. So I don't know what's going on there... >> >> herdtools7 has recently been heavily restructured. >> On the performance regression, I must defer to Luc. >> >> Luc, do you have any idea? >> >>> >>> As for klitmus7, I managed to generate everything without warnings, >>> but couldn't make it build completely due to: >>> >>> $ make >>> make -C /lib/modules/5.6.13-01802-g938d64da97c6/build/ >> >> So you are on Linux 5.6.x which requires cutting-edge klitmus7. >> > > Right, so I retried with the klitmus7 built from sources: > > $ klitmus7 -version > > 7.55+01(dev) > > Still can't compile, though task_struct problem went away, proc_ops > error is still present: > > $ make > grep: /lib/modules/5.7.0-rc5-02014-gb16540c748e9/build/include/linux/proc_fs.h: > No such file or directory Hmm, have you installed kernel-headers on your system? You are now on Linux 5.7-rc5 based system... Thanks, Akira > make -C /lib/modules/5.7.0-rc5-02014-gb16540c748e9/build/ > M=/home/andriin/local/linux-trees/tools/memory-model/mymodules modules > make[1]: Entering directory `/data/users/andriin/linux-build/fb-config' > make[2]: Entering directory `/data/users/andriin/linux-build/default-x86_64' > grep: /lib/modules/5.7.0-rc5-02014-gb16540c748e9/build/include/linux/proc_fs.h: > No such file or directory > CC [M] /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.o > /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c: > In function ‘litmus_init’: > /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c:621:67: > error: passing argument 4 of ‘proc_create’ from incompatible pointer > type [-Werror=incompatible-pointer-types] > struct proc_dir_entry *litmus_pde = > proc_create("litmus",0,NULL,&litmus_proc_ops); > > ^~~~~~~~~~~~~~~~ > In file included from > /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c:15: > /data/users/andriin/linux/include/linux/proc_fs.h:79:24: note: > expected ‘const struct proc_ops *’ but argument is of type ‘const > struct file_operations *’ > struct proc_dir_entry *proc_create(const char *name, umode_t mode, > struct proc_dir_entry *parent, const struct proc_ops *proc_ops); > ^~~~~~~~~~~ > cc1: some warnings being treated as errors > make[3]: *** [/home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.o] > Error 1 > make[2]: *** [/home/andriin/local/linux-trees/tools/memory-model/mymodules] > Error 2 > make[2]: Leaving directory `/data/users/andriin/linux-build/default-x86_64' > make[1]: *** [sub-make] Error 2 > make[1]: Leaving directory `/data/users/andriin/linux-build/fb-config' > make: *** [all] Error 2 > > Don't know if I'm missing some headers or whatever. > >>> M=/home/andriin/local/linux-trees/tools/memory-model/mymodules modules >>> make[1]: Entering directory `/data/users/andriin/linux-build/fb-config' >>> make[2]: Entering directory `/data/users/andriin/linux-build/default-x86_64' >>> CC [M] /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.o >>> /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c: >>> In function ‘zyva’: >>> /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c:507:12: >>> warning: ISO C90 forbids variable length array ‘th’ [-Wvla] >>> struct task_struct *th[nth]; >>> ^~~~~~~~~~~ >>> /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c: >>> In function ‘litmus_init’: >>> /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c:605:67: >>> error: passing argument 4 of ‘proc_create’ from incompatible pointer >>> type [-Werror=incompatible-pointer-types] >>> struct proc_dir_entry *litmus_pde = >>> proc_create("litmus",0,NULL,&litmus_proc_fops); >>> >>> ^~~~~~~~~~~~~~~~~ >>> In file included from >>> /home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.c:15: >>> /data/users/andriin/linux-fb/include/linux/proc_fs.h:64:24: note: >>> expected ‘const struct proc_ops *’ but argument is of type ‘const >>> struct file_operations *’ >>> struct proc_dir_entry *proc_create(const char *name, umode_t mode, >>> struct proc_dir_entry *parent, const struct proc_ops *proc_ops); >>> ^~~~~~~~~~~ >>> cc1: some warnings being treated as errors >>> make[3]: *** [/home/andriin/local/linux-trees/tools/memory-model/mymodules/litmus000.o] >>> Error 1 >>> make[2]: *** [/home/andriin/local/linux-trees/tools/memory-model/mymodules] >>> Error 2 >>> make[2]: Leaving directory `/data/users/andriin/linux-build/default-x86_64' >>> make[1]: *** [sub-make] Error 2 >>> make[1]: Leaving directory `/data/users/andriin/linux-build/fb-config' >>> make: *** [all] Error 2 >>> >> >> These errors suggest the klitmus7 you used is version 7.52 or some such. >> You said you have built herd7 from the source. Have you also built klitmus7? > > I did, but it wasn't in the PATH. I retried with latest klitmus7 and > still run into problems. > >> >> The up-to-date klitmus7 should generate code compatible with Linux 5.6.x. >> >> Could you try with the latest one? >> >> Thanks, Akira >> >>> >>> But at least it doesn't complain about atomic_t anymore. So anyways, >>> I'm going to post updated litmus tests separately from BPF ringbuf >>> patches, because Documentation/litmus-tests is not yet present in >>> bpf-next. >>> >>>> >>>> You can find a basic introduction of klitmus7 in tools/memory-model/README. >>>> >>>> Thanks, Akira >>>> >>>>> >>>>>> >>>>>> 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 >>>>>> >>> >>> [...] >>> >>