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.
- Linux kconfig SAT integration
- Problem description
- Mentors and areas of expertise
- Interested developers
- Mailing list
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.
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:
To pull the code, do: git fetch firstname.lastname@example.org:vegard/linux-2.6.git v4.3+kconfig-sat (or see https://github.com/vegard/linux-2.6/tree/v4.3+kconfig-sat)
Non-upstream SAT solver use in Linux with 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
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
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.
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).
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).
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.
Mentors and areas of expertise
Valentin Rothberg <email@example.com> - one of the authors behind Undertaker, willing to help with using PicoSAT, interfacing PicoSAT with with Kconfig
Andrzej Wąsowski <firstname.lastname@example.org> - Experience in modeling configuration problems in SAT both in Kconfig and other universes
Armin Biere <email@example.com> - author of PicoSAT - SAT expert
Luis R. Rodriguez <firstname.lastname@example.org> - Kernel developer - willing to help with general advice
Thorsten Berger <email@example.com> - Willing to mentor, if a student is found interested in this as part of a thesis topic at University of Gothenburg
Chi Pham <firstname.lastname@example.org>
We'll eventually use the email@example.com mailing list for upstream development discussions, but for now we'll want you to use this specialized list: