Linux kconfig SAT integration
The Linux kernel uses kconfig to help enable configuring the kernel and try to ensure expressed dependencies are met. Kconfig has its limitations though and integrating a SAT solver is expected to help not only address some of Kconfig's limitations but also give us quite a bit advanced bells and whistles within Kconfig. This project aims at doing integration of a SAT solver into Linux by addressing the most simple use case of a SAT solver, while leaving the rest of the optional bells and whistles up for future development. For more futuristic possible uses of SAT solvers on linux refer to the linux-sat page.
At this point in time this project is simply listed as work needed, it is not associated with GSoC, Outreachy, or anything else. We are simply grouping people interested together in document why we want this, and helping mentor it getting upstream.
How you get this upstream is up to you, the developer.
Contents
Problem description
Below we'll split definitions of kconfig, SAT solvers, provide references for prior known uses of SAT solvers with Kconfig, prior stated interest in this work, then also some references to other uses of SAT Solvers used in the Linux ecosystem and finally then go into detail on evaluating proposed work of integrating a SAT solver into the Linux kernel.
More more futuristic uses of SAT solver on Linux refer to linux-sate page which documents known possible uses of SAT solvers within the Linux kernel.
Defining kconfig
Kconfig is the variability modeling languages used in Linux, used to express kernel build dependency relationships. This is done through a series of symbols and expressed relationships between symbols. A user configures a kernel build through a menu interface, the job of kconfig is to entrust the defined relationships expressed by developers and then ensure that the only sensible symbols are displayed which will not create any build or run time conflicts.
Defining a SAT solver
A SAT solver specializes in evaluating if there exists an interpretation that satisfies a given boolean formula. In the simplest case this in turn will tell you if a series of variables and their relationships are satisfiable or not. This won't explain why things are unsatisfiable though, or what is the minimal set of satisfiable set of variables that are allowed. There are advanced aspects of SAT solving though that deal with later elements of the satisfiable question, for instance a A SAT solver with Minimally Unsatisfiable Subformulas (MUSes) support should be able to show the minimum set of variables which can be enabled that are satisfiable.
Previous SAT solver kconfig integration work
In May 2010, Vegard Nossum announced a GSoC project to use a SAT solver to generate full kernel configs based on a set of constraints given by the user. As of May 2016, the project is usable in practice but not yet merged. The patchset embeds PicoSAT and includes three new targets:
- 'make satconfig' (automatically generating a near-minimal .config satisfying .satconfig),
- 'make satrandconfig' (also satisfying .satconfig, but with other options enabled at random), and
- 'make satmenuconfig' (allows editing .satconfig interactively, immediately showing the solution found by the SAT solver).
The biggest missing feature is proper handling of string/int/hex options in the solver -- these values are currently derived from defaults or explicit settings.
To pull the code, do: git fetch git@github.com:vegard/linux-2.6.git v4.3+kconfig-sat (or see https://github.com/vegard/linux-2.6/tree/v4.3+kconfig-sat)
The project is aiming for upstream inclusion once the last bugs have been sorted out.
Non-upstream SAT solver use in Linux with Kconfig
Two research projects are known to have toyed with using SAT solvers for Linux and Kconfig:
Inferring semantics for kconfig: translated Kconfig logic into boolean formulas and ran a SAT solver on it
Undertaker: extracted variability models from Kconfig, and put them together with a propositional formula extracted from CPP #ifdefs and build-rules into a SAT solver in order to find dead code, dead files, and dead symbols.
SAT solver uses in the Linux ecosystem
SAT solvers have also been used in other areas of the Linux distribution ecosystem. One of the known areas was for package dependency resolution. The 3 year Mancoosi research project challenged researchers and developers with solutions for software package resolution dependencies requiring free software licenses for proposed solutions, some of the solutions proposed used SAT solvers, one of which was CryManSolver which used CryptoMiniSat (github) as backend (a SAT solver in itself).
SAT software candidates for Linux kconfig integration
The obvious candidates currently evaluated have been:
CryptoMiniSat - Great documentation, GPL-compatible code, maintainer is active, willing to help. Down side: C++, Python interfaces
PicoSAT - already used in a few Kconfig integration projects, and is written in C, maintainer is active and is willing to help
Integrating a SAT into Linux only makes sense if we know we can count on support from SAT solving experts to help with long term maintenance and issues, we have confirmation of interest to help Linux's integration and future issues by both SAT solver experts, the authors of both PicoSAT and CryptoMiniSat - Armin Biere and Máté Soós.
SAT solver integration on kconfig upstream
This section documents why and how its envisioned we can integrate a SAT solver into Linux for use by Kconfig.
A simple desirable feature to strive for to start off with Kconfig is to have the option to avoid displaying symbols from the configurator, or make a symbol unselectable (and optionally explain then why its not selectable if selected) if its known that selecting a symbol would break an existing configuration. Kconfig will currently avoid displaying a symbol only if its dependencies explicitly annotated with a with 'depends on' cannot be met, however conflicts and implicit dependencies with 'select' are ignored. This is actually a feature of how kconfig 'select' works to help with loading a preset known set of required symbols for an architecture. Select can however be used widely on drivers and its use then can cause unexpected issues when configuring the kernel. Even if 'select' is used within architecture Kconfig files, if a symbol is being selected by architecture but it leads to possibly broken configuration state we want to know about this and fix these issues.
This is one task, let's break this task down further:
- 1) Calling PicoSAT directly from Kconfig, which would imply that existing Kconfig code needs to be extended such that Kconfig data can be transformed into a model for PicoSAT.
- 2) Checks if a given symbol has issues
1) seems to be the crux of the work required, we have tools that do 2) but we don't want independent tools, but rather an integrated solution. One can stage work by first implementing 1) and then using an existing tool to test 2).
Optional advanced features one can strive for:
- a) Use the SAT solver to find symbols which are known to be dead code, that is code which we know cannot possibly be enabled through Kconfig
- b) Explain why a selectable symbols is in conflict. This can be accomplished by taking advantage of PicoSAT's Minimally Unsatisfiable Subformulas (MUS) support
- c) Avoid symbol circular dependency by displaying the dependency relationship issues at build time and providing a more useful description of the existing conflict (making use of PicoSAT's MUS)
kconfig heavy handed select
Kconfig currently enables a select to be enabled without first evaluating if the symbols that the selectable has would conflict or create an issue with any of the known currently set set of symbols. This is actually a feature of kconfig, given select was designed to be heavy handed for architecture to preload a set of symbols it needs. Kconfig then currently does not check the list of symbols listed on a symbol's "select" list, this is done on purpose to help load a set of known required symbols. Because of this use of select should be used with caution.
The option B and C are clearly contradicting with respect to A. However, when A is set, C can be set as well because Kconfig does not visit the dependencies of the select target (in this case B). And since Kconfig does not visit the dependencies, it breaks the dependencies of B (!A).
This is best shown with the following sample Kconfig file. Copy
Test with:
- make KBUILD_KCONFIG=Kconfig.select-break menuconfig
Copy and paste the following code into a file called Kconfig.select-break, note though you will need to fix tons spacing issues to use, alternatively you can just download this file which has the spacing issues addressed.
- mainmenu "Simple example to demo kconfig select broken dependency issue" config A
- bool "CONFIG A"
- bool "CONFIG B" depends on !A
- bool "CONFIG C" depends on A select B
Mentors and areas of expertise
Valentin Rothberg <valentinrothberg@gmail.com> - one of the authors behind Undertaker, willing to help with using PicoSAT, interfacing PicoSAT with with Kconfig
Andrzej Wąsowski <wasowski@itu.dk> - Experience in modeling configuration problems in SAT both in Kconfig and other universes
Armin Biere <biere@jku.at> - author of PicoSAT - SAT expert
Máté Soós <soos.mate@gmail.com> - author of CryptoMiniSat - SAT expert
Luis R. Rodriguez <mcgrof@suse.com> - Kernel developer - willing to help with general advice
Thorsten Berger <bergert@chalmers.se> - Willing to mentor, if a student is found interested in this as part of a thesis topic at University of Gothenburg
Interested developers
Folks considering hacking on this and getting this upstream:
Chi Pham <chidaph@gmail.com>
Mailing list
We'll eventually use the linux-kbuild@vger.kernel.org mailing list for upstream development discussions, but for now we'll want you to use this specialized list:
https://groups.google.com/d/forum/kconfig-sat
Anyone can subscribe. Count on the above folks as being subscribed.
Code
TBD!