gsoc:2024-gsoc-lsb-projects
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
gsoc:2024-gsoc-lsb-projects [2024/02/07 20:35] khoroshilov |
gsoc:2024-gsoc-lsb-projects [2024/02/07 20:54] (current) khoroshilov |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| =====Analysis and fixing of race condition warnings in the Linux kernel===== | =====Analysis and fixing of race condition warnings in the Linux kernel===== | ||
| - | 1 contributor full-size OR 2 contributors half-size | + | 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. | 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. | ||
| Line 33: | Line 33: | ||
| 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. | 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 500 warnings in a recent Linux kernel. | + | 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.\\ | **Desired knowledge:** Linux kernel development, synchronization primitives, debugging tools for Linux kernel.\\ | ||
| Line 40: | Line 40: | ||
| =====Development of environment model specifications for static verification of Linux Kernel===== | =====Development of environment model specifications for static verification of Linux Kernel===== | ||
| - | 1 contributor full-size | + | 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 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. | ||
gsoc/2024-gsoc-lsb-projects.1707338154.txt.gz · Last modified: 2024/02/07 20:35 by khoroshilov
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International
