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. This page could be extended to help keep track of that and also refers to even more futuristic possible uses of SAT solvers on Linux.
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.
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 [http://kernelnewbies.org/KernelProjects/linux-sat 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 [http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf 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
A GSoC student claimed to have been accepted to work on integrating a SAT solver into Linux and [https://lkml.org/lkml/2010/5/17/164? announced this on lkml on May 2010] but after that we never heard back from the student...
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:
[http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf Inferring semantics for kconfig]: translated Kconfig logic into boolean formulas and ran a SAT solver on it
[https://undertaker.cs.fau.de 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 [http://mancoosi.org/ 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 [http://www.msoos.org/cryptominisat4/ CryptoMiniSat] ([https://github.com/msoos/cryptominisat/ github]) as backend (a SAT solver in itself).
SAT software candidates for Linux kconfig integration
The obvious candidates currently evaluated have been:
[http://www.msoos.org/cryptominisat4/ CryptoMiniSat] - Great documentation, GPL-compatible code, maintainer is active, willing to help. Down side: C++, Python interfaces
[http://fmv.jku.at/picosat/ 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.
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 [http://drvbp1.linux-foundation.org/~mcgrof/kconfig/Kconfig.select-break 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!