Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
======2024 GSoC LSB projects======

[[:gsoc:google-summer-code-2024|Go back to the main GSoC Linux Foundation page]]

Mailing list: [[http://lists.linux-foundation.org/mailman/listinfo/lsb-discuss|lsb-discuss at lists dot linux-foundation dot org]]

IRC: #lsb on irc.freenode.net

[[:lsb:start|Workgroup Resources]]

Code License: GPL/BSD, specs: GNU FDL

Mentors: Alexey Khoroshilov (alexey dot khoroshilov at gmail dot com), Jeff Licquia (licquia at linuxfoundation dot org), Vadim Mutilin, Denis Moskalev, Anton Vasilyev.

=====Analysis and fixing of race condition warnings in the Linux kernel=====

1 contributor full-size OR 2 contributors half-size (350 hours), Level of difficulty: Hard

One of the most difficult to catch causes of bugs are race conditions — they may manifest itself only on rare schedules, and they are hard to fix — they usually require rethinking and careful selection of synchronization mechanism. Various methods exist for detecting race conditions. One of them is a static analysis, which allows to find errors in the module parts hardly reachable with testing.

The [[http://linuxtesting.org/project/ldv|LDV Tools static verification framework]] performs the analysis of Linux kernel modules and detects both errors of incorrect usages of API between modules and kernel core and data race conditions – when two or more threads can access the same shared data simultaneously without proper synchronization. Race conditions are symptoms of bugs in the kernel, but not always bugs.

As the result LDV Tools reports a number of warnings for a kernel module. Not all warning are real bugs, because of inaccuracy of LDV Tools in both analysis of module itself and assumptions about an environment of the module. Depending on analyzed subsystem the true positives rate is from 15% to 40%.

For each data race warning the LDV Tools reports one or more error paths. An error path is a sequence of statements in the module source code including call to module callbacks and other functions, branches of if statements, the number of loop iterations. For a data race condition the tool reports two paths describing the execution sequences of statements for each thread participating in the race.  The accesses to shared data and the synchronization primitives are highlighted, e.g. the set of acquired mutex_locks are shown.

For each warning reported by LDV Tools a contributor should determine whether it is a bug or false warning. For that purpose a contributor should analyze each path for the feasibility in the Linux kernel. Moreover, a contributor should make sure the paths representing the threads may work in parallel in the Linux kernel and the assumptions about module environment are correct.

For accomplishing the task it is required to use the whole gamut of available means. A contributor should analyze kernel source code and documentation to determine the possibility of parallel execution of threads. For more precise analysis a contributor should use debugging tools and monitor thread creation inside the kernel subsystem for which the module is developed. It is required to use special tools modeling erroneous conditions, like [[https://www.kernel.org/doc/html/latest/dev-tools/kcsan.html|KCSan]] for reproducing the conditions along the path of the warning. 

If a warning is classified as a bug then a contributor should prepare a patch fixing the bug and send it to the developers of the module. At the worst case, if by some reason it is impossible to prepare a patch a contributor should prepare and send a bug report.

The false warnings should be classified. A contributor should determine if the warning is caused by inaccuracy of assumptions about the module environment, like the order of module callback invocations and the possibility to execute in parallel with each other, with interruptions, workqueue callbacks, etc. The warning may also be caused by inaccuracies in handling synchronization primitives, analysis of shared data, path conditions.

A contributor is expected to analyze and to classify about 200 warnings in a recent Linux kernel.

**Desired knowledge:** Linux kernel development, synchronization primitives, debugging tools for Linux kernel.\\
**Mentors:** Vadim Mutilin, Alexey Khoroshilov, Pavel Andrianov

=====Development of environment model specifications for static verification of Linux Kernel=====

1 contributor full-size (350 hours), Level of difficulty: Hard

The Linux Driver Verification (LDV) program aims to apply heavy-weight static verification tools to find bugs in Linux kernel modules. In contrast to widely used static analysis tools, the approach considers a module as a whole and performs thorough verification empowered by formal techniques.

The LDV framework generates an environment model as an additional C code for each provided kernel module on the base of its interface and runs a static verification tool which checks only that source code which is reachable with the generated environment model. Before the framework can create the environment model, an expert should prepare two kinds of specifications. The first one just describes declarations of an interface (types, references between them). The second specifies how environment model should triggers callbacks of a kernel module which implement the interface. Environment model specifications strongly influence verification results. Deficiencies in the model can lead to missed bugs as well as to false alarms.

The task assumes the following steps:
  * Study verification coverage reports generated by the framework. Choose several kernel interfaces which are not covered by the existing specification set.
  * Study existing environment model specifications and tests (simple kernel modules which implement the interface with stubs) examples. Develop own specifications for interfaces chosen during the previous step. Specifications of both referred kinds are quite short and easy to prepare. But before development, it is necessary to learn DSL languages and study kernel code to understand how the kernel invokes callbacks implemented by kernel modules, how it registers and deregisters them and how it initializes callback parameters. 
  * Obtain and analyze new verification results. Prove then now more code is covered. Analyze new verification results and prepare patches in case of found errors.


**Desired knowledge:** C, understanding of Linux kernel including interrupt handling and deferred works execution.\\
**Mentors:** Anton Vasilyev, Alexey Khoroshilov
Wiki

User Tools

Site Tools

Page Tools
