Contributor
Saubhik Mukherjee

LSB: Analysis & Fixing of Race Condition Warnings in the Linux Kernel


Mentors
Ilja Zakharov, Pavel Andrianov
Organization
The Linux Foundation

The task is to catch bugs due to race conditions in Linux Kernel 5.4 device drivers. A software verification framework called Klever automates the verification against a concurrency safety requirement specification. Using the Klever web interface, the generated error traces are analyzed and classified as false warnings or real bugs. In case of bugs, a bug fix patch is prepared and sent to the driver subsystem developers, or a bug report is sent. Causes of the false warnings are also determined to improve the tool's environment models.