Hi Eisha!
First of all, thank you for your interest in the project!
LDV infrastructure allows to prepare tasks for verifier tools. To get an
overview of our toolset I recommend the paper
http://www.ispras.ru/en/publications/configurable_toolset_for_static_verification_of_operating_systems_kernel_modules.pdf
As a verifier frontend we mostly use CPAchecker.
The new version of LDV, named Klever, is an open-souce project and
available at https://forge.ispras.ru/projects/klever.
However, the latest versions of the Klever tool are not stable and it is
difficult to install and launch the whole toolset.
The main contribution of GSoC project is fixed bugs, so a possible
option is to open you a public access to our server with results. Thus,
you may analyze them without actual run of LDV.
Here are examples of two warnings about potential race conditions:
http://linuxtesting.org/results/bug?id=111
and
http://linuxtesting.org/results/bug?id=113
Try to investigate them, are they real bugs or not. Memory accesses and
synchronization primitives are highlighted with dark blue color.
Best regards,
Vadim Mutilin
On 08.03.2019 11:03, Eisha Chen-yen-su wrote:
Hello everyone,
I'm Eisha Chen-yen-su, a CS student at Paris 6 University (aka UPMC).
I'm on my first year
of Master's degree, specialized in distributed applications and systems.
I would like to apply to the project "Analysis and fixing of race
condition warnings in
the Linux kernel".
I'm proficient in C. The last semester, I've got a course about
operating system kernels in
which I've studied general principles of process management and
scheduling, virtual memory
and file systems. I've also studied some portions of the source code
of the UNIXv7's kernel
during this course.
This semester, I'm fallowing a course about programming in the Linux
kernel and until now I've already studied how to compile the kernel,
and run it within a VM (using qemu and KVM),
as well as debugging techniques with KGDB over a serial line. I've
also learnt about
manipulating and writing kernel modules.
I have a good knowledge of concurrent programming: synchronization
primitives, being aware
of data races and deadlocks and the like. I've also been practicing it
with the POSIX threads
API in C, in Rust (a language which I use a lot) and lately I've been
learning implementation
of distributed algorithms with MPI. I also had a class about
concurrent programming during
the last semester.
Also, I've completed GSoC 2018 by contributing to Fractal (you can
find what was achieved here
https://summerofcode.withgoogle.com/archive/2018/projects/4724779168825344/).
I'm interested by this project mainly because I think it would be very
helpful to improve my
skills for debugging as I know that debugging a kernel as well as
tracking concurrent bugs can
be very tricky, so it will be useful for me later as I'm very keen on
parallel, concurrent and
distributed computing. This project would also be a way for me to
start contributing to the Linux
kernel.
I would like to know if there are particular resources that I should
start reading for making my
proposal? Any contributions to make? And maybe have more indications
about how to setup
and use tools from LDV, please.
I've already found this document
(http://linuxtesting.org/downloads/20140425-Dagstuhl-LDV.pdf), I
wonder whether it is
relevant for this project.
Regard,
Eisha Chen-yen-su
_______________________________________________
lsb-discuss mailing list
[email protected]
https://lists.linuxfoundation.org/mailman/listinfo/lsb-discuss
_______________________________________________
lsb-discuss mailing list
[email protected]
https://lists.linuxfoundation.org/mailman/listinfo/lsb-discuss
