Hi,
Thank you for your answers!
I've read the first source you've indicated. I think that I will not
try to run the tests myself for now, especially
if I can simply get the error traces from a database and that doing it
myself would be quite complicated.
Regarding the two warnings you've indicated to me, I've started to
have a look at the first and this is what
I could understand:
- The first path can be executed when there's a system call (I
guess) to get statistics for the wireless network.
"airo_get_wireless_stats" is a callback function called by this.
The information about the signal noise is reset
to zero "local->wstats.qual.noise = 0; " and is thus invalidated
("IW_QUAL_NOISE_INVALID" in "local->wstats.qual.updated =
IW_QUAL_QUAL_UPDATED | IW_QUAL_LEVEL_UPDATED | IW_QUAL_NOISE_INVALID |
IW_QUAL_DBM;")
- The second path can be executed when there's an interrupt from the
wireless card when it has received a packet.
At some point, it reads the signal level stored in the statistics
of the driver.
It looks like that these two paths can be indeed executed in two
different threads at the same time because we
can have a parallel handling of the interrupts while we read statistic
data from the driver. And as mentioned
in the comment. But except traces of a semaphore being manipulated in
the first path, I don't see any other
synchronization primitives being called. Does this mean that there can
indeed be a data race?
What about the "rtnl_lock()" at the beginning of the error trace? Is
this the synchronization primitive that should be
used here? I don't see it used anywhere in the source file of the module.
I'd like to know what can I do to develop from this point and
determine the status of this warning, please.
Regards,
Eisha Chen-yen-su
On Wed, Mar 13, 2019 at 7:00 AM Evgeny Novikov <[email protected]> wrote:
>
> Hi Eisha,
>
> I would like to improve the previous answer.
>
> First of all, I attached the more actual paper that describes both practical
> issues of using software verification (software model checking) and Klever.
>
> Latest versions of Klever are absolutely stable. I recommend you to use the
> most recent one, Klever 2.0 (tag v2.0 in the Git repository). Usually we
> maintain backward compatibility by allowing migrating data collected thus far
> automatically. But sometimes this has little sense since old data misses too
> many necessary things that can be added automatically. In particular, Klever
> 3.0 will break backward compatibility because we will change most of data
> formats very considerably. You will be able to either use Klever 2.0 further
> or switch to Klever 3.0 completely. I hope that we will release Klever 3.0
> until this summer.
>
> Thanks to our collaboration with guys from the SIL2LinuxMP project, we
> developed scripts and documentation simplifying deployment very considerably.
> If you will follow https://klever.readthedocs.io/en/v2.0/deploy.html you will
> be able to deploy Klever in several minutes if you have a dedicated machine
> with Debian or Ubuntu.
>
> This document describes things that are very welcome in Klever. Many of them
> will help to use Klever more easily and efficiently. Especially this is the
> case for new users. Unfortunately we have not enough resources to implement
> them quickly.
>
> In your particular case it may be better to provide you verification results
> that we will obtain using our servers since the latter is not the purpose of
> the given GSoC project. So, you will just analyze error traces representing
> warnings and report bugs. But if you would like to experience the whole
> verification workflow, I recommend you to deploy Klever as well as to obtain
> verification results yourself. There are very simple instructions how to do
> the latter. I can provide you them if you are interested. Regarding analysis
> of verification results there is no good documentation but often it is quite
> intuitive.
>
> --
> Evgeny Novikov
> Linux Verification Center, ISP RAS
> http://linuxtesting.org
>
>
>
> 12.03.2019, 19:35, "Vadim Mutilin" <[email protected]>:
>
> 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
_______________________________________________
lsb-discuss mailing list
[email protected]
https://lists.linuxfoundation.org/mailman/listinfo/lsb-discuss
