Fixing kconfig semantics

Session information has not yet been published for this event.

*
60 Minute Session
Scheduled: Thursday, November 3, 2016 from 2:00 – 3:00pm in Coronado

One Line Summary

Linux kconfig semantics are loose and this creates issues, lets review them and fix them

Abstract

Kconfig is one of the leading industrial variability modeling languages, it however has loose semantics. This has created a few issues. One the most well known issue is the ‘select’ issue which gives a recursive dependency issue.

The goal of this session is to review some of the issues with the semantics of kconfig, some proposals for helping with this, and actual valid uses for having these semantics fixed.

The use of Kconfig is broad, Linux is now only one of Kconfig’s users: one study has completed a broad analysis of Kconfig use in 12 projects 0. Despite its widespread use, and although this document does a reasonable job in documenting basic Kconfig syntax a more precise definition of Kconfig semantics is welcomed. One project deduced Kconfig semantics through the use of the xconfig configurator 1. Work should be done to confirm if the deduced semantics matches our intended Kconfig design goals.

Having well defined semantics can be useful for tools for practical evaluation of depenencies, for instance one such use known case was work to express in boolean abstraction of the inferred semantics of Kconfig to translate Kconfig logic into boolean formulas and run a SAT solver on this to find dead code / features (always inactive), 114 dead features were found in Linux using this methodology 1.

Confirming this could prove useful as Kconfig stands as one of the the leading industrial variability modeling languages 1 2. Its study would help evaluate practical uses of such languages, their use was only theoretical and real world requirements were not well understood. As it stands though only reverse engineering techniques have been used to deduce semantics from variability modeling languages such as Kconfig 3.

0 http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf
1 http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
2 http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf
3 http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf

Tags

linux, kconfig, semantics

Speaker