User Tools

Site Tools


gsoc:2018-gsoc-lsb-projects

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
gsoc:2018-gsoc-lsb-projects [2018/01/29 21:13]
khoroshilov [Add support for C++11 to LSB]
gsoc:2018-gsoc-lsb-projects [2018/01/29 22:34] (current)
khoroshilov [Analysis and extermination of race condition warnings in the Linux kernel]
Line 33: Line 33:
  
 **Desired knowledge:​** C, Testing\\ Mentors: Alexey Khoroshilov,​ Roman Zybin **Desired knowledge:​** C, Testing\\ Mentors: Alexey Khoroshilov,​ Roman Zybin
 +
 +=====Analysis and fixing of race condition warnings in the Linux kernel=====
 +
 +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 student should determine whether it is a bug or false warning. For that purpose a student should analyze each path for the feasibility in the Linux kernel. Moreover, a student 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 student should analyze kernel source code and documentation to determine the possibility of parallel execution of threads. For more precise analysis a student 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://​forge.ispras.ru/​projects/​race-hound/​wiki|RaceHound]] for reproducing the conditions along the path of the warning. ​
 +
 +If a warning is classified as a bug then a student 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 student should prepare and send a bug report.
 +
 +The false warnings should be classified. A student 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 student is expected to analyze and to classify about 500 warnings in a recent Linux kernel.
 +
 +**Desired knowledge:​** Linux kernel development,​ synchronization primitives, debugging tools for Linux kernel.\\
 +**Mentors:​** Vadim Mutilin, Alexey Khoroshilov
  
 =====Development of environment model specifications for static verification of Linux Kernel===== =====Development of environment model specifications for static verification of Linux Kernel=====
Line 45: Line 68:
   * 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.   * 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.
  
-More than one application can be approved. 
  
 **Desired knowledge:​** C, understanding of Linux kernel including interrupt handling and deferred works execution.\\ **Desired knowledge:​** C, understanding of Linux kernel including interrupt handling and deferred works execution.\\
 +**Mentors:​** Ilja Zakharov, Alexey Khoroshilov
 +
 +=====Improve environment model for memory safety verification of the Linux Kernel=====
 +
 +The project is similar for the previous one, but the main goal of improvements is not to improve code coverage, but it is to make environment model more precise to avoid false positives in memory safety verification. For example, [[http://​linuxtesting.org/​27-08-2017|GSoC project of 2017]] reported that 340 warning are false alarms because of environment model inaccuracies. The root causes of these false alarms have to be fixed.
 +
 +A student is expected to write model and analyze changes in verification results for about 70 functions from recent Linux kernels. Models are C functions representing memory sensitive paths similar to the original code from static verification point of view but they are more simple. Those function models which help to improve verification will be included in LDV environment model. If a student detects a bug in the kernel then she should either prepare a patch fixing the bug and send it to the developers of the module or to send a bug report. ​
 +
 +**Desired knowledge:​** C, Linux kernel.\\
 **Mentors:​** Ilja Zakharov, Alexey Khoroshilov **Mentors:​** Ilja Zakharov, Alexey Khoroshilov
  
Line 96: Line 127:
 [[http://​ispras.linuxbase.org/​index.php/​LSB_DB_Tools|LSB_DB_Tools]]. [[http://​ispras.linuxbase.org/​index.php/​LSB_DB_Tools|LSB_DB_Tools]].
  
-Original ​idea was proposed in [[https://​www.mail-archive.com/​lsb-discuss@lists.linux-foundation.org/​msg00104.html|lsb-discuss]] mailing list.+The idea was proposed in [[https://​www.mail-archive.com/​lsb-discuss@lists.linux-foundation.org/​msg00104.html|lsb-discuss]] mailing list. So, it is preferred to discuss corresponding questions in that thread.
  
 **Desired knowledge:​** C++, C++ ABI, SQL databases, Perl\\ **Desired knowledge:​** C++, C++ ABI, SQL databases, Perl\\
 Mentors: Jeff Licquia, Denis Silakov, Alexey Khoroshilov Mentors: Jeff Licquia, Denis Silakov, Alexey Khoroshilov
  
gsoc/2018-gsoc-lsb-projects.1517260411.txt.gz ยท Last modified: 2018/01/29 21:13 by khoroshilov