Analysing the Kconfig Semantics and Its Analysis Tools

作者：El Sharkawy Sascha^*; Krafczyk Adam^*; Schmid Klaus^*

来源：ACM Sigplan Notices, 2016, 51(3): 45-54.

DOI：10.1145/2814204.2814222

• Software Product Lines
• Linux Kernel Analysis
• Kconfig
• Undertaker
• Kconfig Reader
• Linux Variability Analysis Tools
• LVAT
• Verification

The Linux kernel is often used as a real world case study to demonstrate novel Software Product Line Engineering research methods. An important point in this is often the analysis of the Kconfig semantics. However, we detected that the semantics of Kconfig is rather unclear and has many special cases, which are not documented in its short specification. We performed a systematic analysis to uncover the correct behaviour of Kconfig and present the results, which are necessary for applying semantically correct analyses. Further, we analyse existing analysis tools of the research community whether they are aware of the correct semantics of Kconfig. These analyses can be used for improving existing analysis tools as well as decision support for selecting an appropriate tool for a specific analysis. Our main goal is to contribute to a better understanding of Kconfig in the research community to improve the validity of evaluations based on Linux.

• 出版日期2016-3