= 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
[[http://kernelnewbies.org/KernelProjects/linux-sat|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.
<<TableOfContents(4)>>
= 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 ==
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:
* [[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.
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 [[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"
config B
bool "CONFIG B"
depends on !A
config C
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:
kconfig-sat@googlegroups.com
https://groups.google.com/d/forum/kconfig-sat
Anyone can subscribe. Count on the above folks as being subscribed.
= Code =
TBD!